LeanPool.CCDN.Projection.FixedCoordinateElimination

Full-degree affine elimination also gives an integral projection of the projective closure, fixing its homogenizing coordinate.

One bounded integer-matrix elimination step on the standard Fin-indexed polynomial rings, ready for iteration.

The restriction of a bounded homogenization to the hyperplane at infinity is exactly its highest indicated homogeneous component.

source

theorem CCDN.scaledHomogenize_one_eval_at_infinity {K : Type u_1} [Field K] {n D : ℕ} (f : MvPolynomial (Fin n) K) (hf : f.totalDegree ≤ D) (b : Fin n → K) :

(MvPolynomial.eval (Fin.cons 0 b)) (scaledHomogenize D 1 f) = (MvPolynomial.eval b) ((MvPolynomial.homogeneousComponent D) f)

For f of total degree at most D, the degree-D homogenization of f, restricted to the hyperplane at infinity X₀ = 0, is the degree-D homogeneous component of f.

source

def CCDN.finEliminationMatrix {n : ℕ} (b : Option (Fin n) → ℤ) :

Fin n → Fin (n + 1) → ℤ

The integer matrix whose i-th row is the linear form b none * X (i + 1) - b (some i) * X 0, eliminating the coordinate X 0 along the direction b.

Equations

CCDN.finEliminationMatrix b i✝ i = Fin.cases (-b (some i✝)) (fun (j : Fin n) => if j = i✝ then b none else 0) i

Instances For

source

theorem CCDN.finEliminationMatrix_height {n d : ℕ} (b : Option (Fin n) → ℤ) (hb : ∀ (i : Option (Fin n)), 0 ≤ b i ∧ b i ≤ ↑d + 1) (i : Fin n) (j : Fin (n + 1)) :

|finEliminationMatrix b i j| ≤ ↑d + 1

If every entry of the direction b lies in [0, d + 1], then every entry of the elimination matrix has absolute value at most d + 1.

source

def CCDN.closurePivotEquiv (n : ℕ) :

Fin (n + 2) ≃ Option (Fin (n + 1))

The reindexing of Fin (n + 2) that sends coordinate 1 to none and the remaining coordinates, in order, to some 0, some 1, …; it makes the homogenizing coordinate 0 the first retained coordinate.

Equations