Bounded integral linear elimination with integer coefficients. Scaling the retained coordinates by the nonzero pivot preserves integrality.

A complete bounded elimination step: the contraction stays prime, retains dimension, and has no larger Hilbert multiplicity.

noncomputable def CCDN.eliminationLinearCoordinates {σ : Type u_1} (b : Option σ → ℚ) : σ → MvPolynomial (Option σ) ℚ

The linear forms X (some i) - (b (some i) / b none) * X none, projecting away the coordinate X none along the direction b.

Equations

• CCDN.eliminationLinearCoordinates b i = MvPolynomial.X (some i) - MvPolynomial.C (b (some i) / b none) * MvPolynomial.X none

theorem CCDN.coordinateEliminationMap_eq_projection {σ : Type u_1} (I : Ideal (MvPolynomial (Option σ) ℚ)) (b : Option σ → ℚ) (hb : b none ≠ 0) : coordinateEliminationMap I (hypersurfaceAffineCoordinates 0 b hb) = projectionCoordinateMap I (eliminationLinearCoordinates b)

For a direction b with b none ≠ 0, the elimination map of the associated linear coordinate change is the projection by the elimination linear forms of b.

noncomputable def CCDN.integerEliminationCoordinates {σ : Type u_1} (b : Option σ → ℤ) : σ → MvPolynomial (Option σ) ℚ

The linear forms b none * X (some i) - b (some i) * X none with integer coefficients, projecting away the coordinate X none along the integer direction b.

Equations

• CCDN.integerEliminationCoordinates b i = MvPolynomial.C ↑(b none) * MvPolynomial.X (some i) - MvPolynomial.C ↑(b (some i)) * MvPolynomial.X none

theorem CCDN.integerEliminationMap_isIntegral {σ : Type u_1} (I : Ideal (MvPolynomial (Option σ) ℚ)) (b : Option σ → ℤ) (hb : ↑(b none) ≠ 0) (hint : (projectionCoordinateMap I (eliminationLinearCoordinates fun (i : Option σ) => ↑(b i))).IsIntegral) : (projectionCoordinateMap I (integerEliminationCoordinates b)).IsIntegral

If the projection by the rational elimination forms of an integer direction b with b none ≠ 0 is integral, then so is the projection by the integer elimination forms, which differ by the scalar b none.