Integral projections of the projective closure that fix X₀ specialize to integral affine projections on the chart X₀ = 1.

noncomputable def CCDN.affineChartAlgHom (K : Type u_1) [Field K] (n : ℕ) : MvPolynomial (Fin (n + 1)) K →ₐ[K] MvPolynomial (Fin n) K

Dehomogenization at X 0 = 1, as a K-algebra homomorphism from polynomials in n + 1 variables to polynomials in n variables.

Equations

• CCDN.affineChartAlgHom K n = { toRingHom := CCDN.affineChart n, commutes' := ⋯ }

theorem CCDN.projectiveClosureIdeal_affineChart_mem {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (f : MvPolynomial (Fin (n + 1)) K) (hf : f ∈ projectiveClosureIdeal I) : (affineChart n) f ∈ I

Dehomogenizing at X 0 = 1 an element of the projective closure of I gives an element of I.

noncomputable def CCDN.projectiveClosureSpecialization {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) : MvPolynomial (Fin (n + 1)) K ⧸ projectiveClosureIdeal I →ₐ[K] MvPolynomial (Fin n) K ⧸ I

The specialization X 0 = 1 from the homogeneous coordinate ring of the projective closure of I to the affine coordinate ring of I.

Equations

• CCDN.projectiveClosureSpecialization I = Ideal.Quotient.liftₐ (CCDN.projectiveClosureIdeal I) ((Ideal.Quotient.mkₐ K I).comp (CCDN.affineChartAlgHom K n)) ⋯

@[simp]

theorem CCDN.projectiveClosureSpecialization_mk {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (f : MvPolynomial (Fin (n + 1)) K) : (projectiveClosureSpecialization I) ((Ideal.Quotient.mk (projectiveClosureIdeal I)) f) = (Ideal.Quotient.mk I) ((affineChart n) f)

The specialization X 0 = 1 sends the class of f to the class of its dehomogenization.

theorem CCDN.affine_projection_integral_of_closure_integral {K : Type u_1} [Field K] {m n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (a : Fin m → MvPolynomial (Fin n) K) (hint : (projectionCoordinateMap (projectiveClosureIdeal I) (closureProjectionCoordinates a)).IsIntegral) : (projectionCoordinateMap I a).IsIntegral

If the projection of the projective closure of I by the closure coordinates X 0, a 0, a 1, … is integral, then the affine projection of I by the forms a is integral.