A single bounded linear elimination step. A chosen nonzero ideal equation of degree d becomes monic after a linear coordinate change with integer direction bounded by d+1. The quotient is integral over the remaining linear coordinates.

theorem CCDN.exists_bounded_full_degree_direction {σ : Type u_1} [Finite σ] (f : MvPolynomial (Option σ) ℚ) (hf : f ≠ 0) : ∃ (b : Option σ → ℤ), (∀ (i : Option σ), 0 ≤ b i ∧ b i ≤ ↑f.totalDegree + 1) ∧ b none ≠ 0 ∧ (MvPolynomial.eval fun (i : Option σ) => ↑(b i)) ((MvPolynomial.homogeneousComponent f.totalDegree) f) ≠ 0

A bounded integral direction simultaneously avoids the top form and the coordinate hyperplane needed for an invertible linear substitution.

noncomputable def CCDN.coordinateEliminationMap {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial (Option σ) K)) (e : MvPolynomial (Option σ) K ≃ₐ[K] MvPolynomial (Option σ) K) : MvPolynomial σ K →ₐ[K] MvPolynomial (Option σ) K ⧸ I

The retained variables, transported back through the coordinate automorphism, as elements of the original quotient.

Equations

• CCDN.coordinateEliminationMap I e = (Ideal.Quotient.mkₐ K I).comp ((↑e.symm).comp (MvPolynomial.rename some))

theorem CCDN.coordinateEliminationMap_direction_X {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial (Option σ) K)) (b : Option σ → K) (hb : b none ≠ 0) (i : σ) : (coordinateEliminationMap I (hypersurfaceAffineCoordinates 0 b hb)) (MvPolynomial.X i) = (Ideal.Quotient.mk I) (MvPolynomial.X (some i) - MvPolynomial.C (b (some i) / b none) * MvPolynomial.X none)

For the linear coordinate change attached to a direction b with b none ≠ 0, the elimination map sends the variable X i to the class of X (some i) - (b (some i) / b none) * X none.

theorem CCDN.coordinateEliminationMap_isIntegral {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial (Option σ) K)) (e : MvPolynomial (Option σ) K ≃ₐ[K] MvPolynomial (Option σ) K) (q : MvPolynomial (Option σ) K) (hq : q ∈ Ideal.map e I) (hm : ((MvPolynomial.optionEquivLeft K σ) q).Monic) : (coordinateEliminationMap I e).IsIntegral

A monic equation in the eliminated coordinate proves integrality over the retained coordinates, for any ideal containing the equation.