Constructive bounded linear Noether normalization. The coefficients of the integer linear forms are bounded by n! (d+1)^n, and the map of projective closures fixing the homogenizing coordinate is integral as well.

def CCDN.integerNormalizationHeight (n d : ℕ) : ℕ

The coefficient bound n! * (d + 1) ^ n for the bounded linear Noether normalization of a degree-d variety in n variables.

Equations

• CCDN.integerNormalizationHeight n d = n.factorial * (d + 1) ^ n

theorem CCDN.integerNormalizationHeight_pos (n d : ℕ) : 0 < integerNormalizationHeight n d

The normalization height is positive.

theorem CCDN.exists_bounded_integer_closure_normalization (m k : ℕ) (I : Ideal (MvPolynomial (Fin (m + 1 + k)) ℚ)) [I.IsPrime] (d : ℕ) (hdimdeg : HasProjectiveDimensionDegree I m d) : ∃ (a : Fin (m + 1) → Fin (m + 1 + k) → ℤ), (∀ (i : Fin (m + 1)) (j : Fin (m + 1 + k)), |a i j| ≤ ↑(integerNormalizationHeight (m + 1 + k) d)) ∧ (projectionCoordinateMap I fun (i : Fin (m + 1)) => integerLinearForm (a i)).IsIntegral ∧ Function.Injective ⇑(projectionCoordinateMap I fun (i : Fin (m + 1)) => integerLinearForm (a i)) ∧ (projectionCoordinateMap (projectiveClosureIdeal I) (closureProjectionCoordinates fun (i : Fin (m + 1)) => integerLinearForm (a i))).IsIntegral

Integer linear normalization of a prime quotient of positive Hilbert dimension. The resulting polynomial map is injective and integral, and so is the induced map of projective closures fixing the homogenizing coordinate.

theorem CCDN.exists_bounded_integer_normalization (m k : ℕ) (I : Ideal (MvPolynomial (Fin (m + 1 + k)) ℚ)) [I.IsPrime] (d : ℕ) (hdimdeg : HasProjectiveDimensionDegree I m d) : ∃ (a : Fin (m + 1) → Fin (m + 1 + k) → ℤ), (∀ (i : Fin (m + 1)) (j : Fin (m + 1 + k)), |a i j| ≤ ↑(integerNormalizationHeight (m + 1 + k) d)) ∧ (projectionCoordinateMap I fun (i : Fin (m + 1)) => integerLinearForm (a i)).IsIntegral ∧ Function.Injective ⇑(projectionCoordinateMap I fun (i : Fin (m + 1)) => integerLinearForm (a i))

Integer linear normalization of a prime quotient of positive Hilbert dimension. The resulting polynomial map is both injective and integral.