Extending a linear projection by one leading coordinate. Integrality and algebraic independence of the tail coordinates pass to the extended projection; for a homogeneous prime whose function field is generated by the extended coordinates, the image is a hypersurface cut out by a form of exactly the original degree.

theorem CCDN.projectionCoordinateMap_isIntegral_of_tail {K : Type u_1} {τ : Type u_2} [Field K] {m : ℕ} (I : Ideal (MvPolynomial τ K)) (l : Fin (m + 1) → MvPolynomial τ K) (h : (projectionCoordinateMap I fun (i : Fin m) => l i.succ).IsIntegral) : (projectionCoordinateMap I l).IsIntegral

A projection is integral as soon as the projection along its tail coordinates is.

theorem CCDN.exists_extended_projection_equation_degree_le {K : Type u_1} {τ : Type u_2} [Field K] [Fintype τ] [LinearOrder τ] {m : ℕ} (I : Ideal (MvPolynomial τ K)) [I.IsPrime] (l : Fin (m + 2) → MvPolynomial τ K) (hl : ∀ (i : Fin (m + 2)), (l i).totalDegree ≤ 1) (hinj : Function.Injective ⇑(projectionCoordinateMap I fun (i : Fin (m + 1)) => l i.succ)) (d : ℕ) (hdimdeg : HasProjectiveDimensionDegree I m d) : ∃ (f : MvPolynomial (Fin (m + 2)) K), Irreducible f ∧ 0 < f.totalDegree ∧ f.totalDegree ≤ d ∧ RingHom.ker (projectionCoordinateMap I l) = Ideal.span {f}

Extending a finite injective projection of a prime of projective dimension m and degree d by one linear coordinate gives a hypersurface equation: the kernel is generated by an irreducible polynomial of positive total degree at most d.

theorem CCDN.exists_homogeneous_extended_projection_equation {K : Type u_1} {F : Type u_2} {τ : Type u_3} [Field K] [Field F] [Algebra K F] [Fintype τ] [LinearOrder τ] {m : ℕ} (I : Ideal (MvPolynomial τ K)) [I.IsPrime] [Algebra (MvPolynomial τ K ⧸ I) F] [IsScalarTower K (MvPolynomial τ K ⧸ I) F] [IsFractionRing (MvPolynomial τ K ⧸ I) F] (hI : IsHomogeneousIdeal I) (l : Fin (m + 2) → MvPolynomial τ K) (hl : ∀ (i : Fin (m + 2)), (l i).IsHomogeneous 1) (hint : (projectionCoordinateMap I fun (i : Fin (m + 1)) => l i.succ).IsIntegral) (hinj : Function.Injective ⇑(projectionCoordinateMap I fun (i : Fin (m + 1)) => l i.succ)) (hfield : IntermediateField.adjoin K (Set.range fun (i : Fin (m + 2)) => (algebraMap (MvPolynomial τ K ⧸ I) F) ((Ideal.Quotient.mk I) (l i))) = ⊤) (d : ℕ) (hdimdeg : HasProjectiveDimensionDegree I m d) : ∃ (f : MvPolynomial (Fin (m + 2)) K), Irreducible f ∧ f.IsHomogeneous d ∧ f.totalDegree = d ∧ 0 < d ∧ RingHom.ker (projectionCoordinateMap I l) = Ideal.span {f}

A finite birational projection of a homogeneous prime of projective dimension m and degree d, obtained by extending a finite injective linear projection by one linear form and generating the function field, has image a hypersurface cut out by an irreducible form of degree exactly d.