A bounded integer linear finite birational projection of a homogeneous prime quotient to a hypersurface of exactly the same degree.

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

The coefficient bound for the birational hypersurface projection in n variables and degree d: the maximum of the normalization height and (n * d ^ 2 + 1) ^ n, which bounds the moment row.

Equations

• CCDN.integerBirationalProjectionHeight n d = max (CCDN.integerNormalizationHeight n d) ((n * d ^ 2 + 1) ^ n)

theorem CCDN.integerBirationalProjectionHeight_one_le (n d : ℕ) : 1 ≤ integerBirationalProjectionHeight n d

The birational projection height is at least one.

theorem CCDN.integerLinearForm_moment_cons {m n : ℕ} (t : ℕ) (a : Fin (m + 1) → Fin n → ℤ) : (fun (i : Fin (m + 1 + 1)) => integerLinearForm ((fun (i : Fin (m + 1 + 1)) => Fin.cases (motive := fun (x : Fin (m + 1 + 1)) => Fin n → ℤ) (fun (j : Fin n) => ↑t ^ ↑j) a i) i)) = fun (i : Fin (m + 1 + 1)) => Fin.cases (momentCoordinate ℚ n t) (fun (i : Fin (m + 1)) => integerLinearForm (a i)) i

Prepending the integer moment row (t ^ j)_j to integer rows realizes the moment coordinate as the leading linear form.

theorem CCDN.moment_cons_abs_le_integerBirationalProjectionHeight {m n d t : ℕ} (ht : t ≤ n * d ^ 2) (a : Fin (m + 1) → Fin n → ℤ) (ha : ∀ (i : Fin (m + 1)) (j : Fin n), |a i j| ≤ ↑(integerNormalizationHeight n d)) (i : Fin (m + 2)) (j : Fin n) : |(fun (i : Fin (m + 1 + 1)) => Fin.cases (motive := fun (x : Fin (m + 1 + 1)) => Fin n → ℤ) (fun (j : Fin n) => ↑t ^ ↑j) a i) i j| ≤ ↑(integerBirationalProjectionHeight n d)

Prepending the moment row with parameter t ≤ n d² to rows bounded by the normalization height keeps every entry within the birational projection height.

theorem CCDN.exists_bounded_birational_hypersurface_projection_of_le (m n : ℕ) (hmn : m + 1 ≤ n) (I : Ideal (MvPolynomial (Fin n) ℚ)) [I.IsPrime] (hI : IsHomogeneousIdeal I) (d : ℕ) (hdimdeg : HasProjectiveDimensionDegree I m d) : ∃ (b : Fin (m + 2) → Fin n → ℤ) (f : MvPolynomial (Fin (m + 2)) ℚ), (∀ (i : Fin (m + 2)) (j : Fin n), |b i j| ≤ ↑(integerBirationalProjectionHeight n d)) ∧ (IsNoetherNormalization I fun (i : Fin (m + 1)) => integerLinearForm (b i.succ)) ∧ IsBirationalProjection I (fun (i : Fin (m + 2)) => integerLinearForm (b i)) f ∧ f.IsHomogeneous d ∧ f.totalDegree = d

A homogeneous prime ideal in n ≥ m + 1 variables, of projective dimension m and degree d, has a bounded integral linear projection to m + 2 coordinates: the integer coefficients are bounded by integerBirationalProjectionHeight n d, the projection is integral and birational, and its kernel is generated by an irreducible homogeneous form of degree d. The number of variables is arbitrary, not written as m + 1 + k.

The constructed projection has a coefficient bound polynomial in the degree, with exponent and constant depending only on ambient dimension.

def CCDN.birationalProjectionHeightConstant (n : ℕ) : ℕ

The constant n! * 2 ^ n + (n + 1) ^ n in the polynomial bound on the birational projection height in n variables.

Equations

• CCDN.birationalProjectionHeightConstant n = n.factorial * 2 ^ n + (n + 1) ^ n

theorem CCDN.birationalProjectionHeightConstant_pos (n : ℕ) : 0 < birationalProjectionHeightConstant n

The birational projection height constant is positive.

theorem CCDN.integerBirationalProjectionHeight_le (n d : ℕ) (hd : 1 ≤ d) : integerBirationalProjectionHeight n d ≤ birationalProjectionHeightConstant n * d ^ (2 * n)

For degree d ≥ 1, the birational projection height in n variables is at most birationalProjectionHeightConstant n * d ^ (2 * n).