Homogenizing a linear affine projection while retaining its homogenizing coordinate gives the projective closure of its affine image ideal.

noncomputable def CCDN.closureProjectionCoordinates {K : Type u_1} [Field K] {m n : ℕ} (a : Fin m → MvPolynomial (Fin n) K) : Fin (m + 1) → MvPolynomial (Fin (n + 1)) K

The homogenization of a projection by forms a: the forms X 0, a 0, a 1, … on the projective coordinates, which keep the homogenizing coordinate X 0 and shift the variables of each a i.

Equations

• CCDN.closureProjectionCoordinates a = Fin.cons (MvPolynomial.X 0) fun (i : Fin m) => (MvPolynomial.rename Fin.succ) (a i)

theorem CCDN.closureProjectionCoordinates_homogeneous {K : Type u_1} [Field K] {m n : ℕ} (a : Fin m → MvPolynomial (Fin n) K) (ha : ∀ (i : Fin m), (a i).IsHomogeneous 1) (i : Fin (m + 1)) : (closureProjectionCoordinates a i).IsHomogeneous 1

If all the forms a i are homogeneous linear, then so are their closure projection coordinates.

theorem CCDN.affineChart_rename_succ {K : Type u_1} [Field K] {n : ℕ} (f : MvPolynomial (Fin n) K) : (affineChart n) ((MvPolynomial.rename Fin.succ) f) = f

Dehomogenizing at X 0 = 1 a polynomial not involving X 0 recovers the original polynomial.

theorem CCDN.affineChart_aeval_closureProjectionCoordinates {K : Type u_1} [Field K] {m n : ℕ} (a : Fin m → MvPolynomial (Fin n) K) (f : MvPolynomial (Fin (m + 1)) K) : (affineChart n) ((MvPolynomial.aeval (closureProjectionCoordinates a)) f) = (MvPolynomial.aeval a) ((affineChart m) f)

Dehomogenization at X 0 = 1 intertwines substitution of the closure projection coordinates with substitution of the original forms a.

theorem CCDN.projectiveClosureIdeal_projection_kernel {K : Type u_1} [Field K] {m n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (a : Fin m → MvPolynomial (Fin n) K) (ha : ∀ (i : Fin m), (a i).IsHomogeneous 1) : projectiveClosureIdeal (RingHom.ker (projectionCoordinateMap I a)) = RingHom.ker (projectionCoordinateMap (projectiveClosureIdeal I) (closureProjectionCoordinates a))

For homogeneous linear forms a, the projective closure of the kernel of the projection of I by a is the kernel of the projection of the projective closure of I by the closure coordinates X 0, a 0, a 1, …; this is an equality of ideals, not merely of zero sets.