Integral linear projections preserve Hilbert dimension and do not increase its multiplicity.
theorem
CCDN.integral_projection_hilbert_dimension_eq
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
[Fintype σ]
[Fintype τ]
[LinearOrder σ]
[LinearOrder τ]
(I : Ideal (MvPolynomial τ K))
[I.IsPrime]
(ψ : MvPolynomial σ K →ₐ[K] MvPolynomial τ K ⧸ I)
(hint : ψ.IsIntegral)
:
An integral map ψ from a polynomial ring to the quotient by a prime I preserves Hilbert
dimension: the filtered Hilbert polynomials of ker ψ and of I have the same degree.
theorem
CCDN.integral_linear_projection_dimension_degree
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
[Fintype σ]
[Fintype τ]
[LinearOrder σ]
[LinearOrder τ]
(I : Ideal (MvPolynomial τ K))
[I.IsPrime]
(a : σ → MvPolynomial τ K)
(ha : ∀ (i : σ), (a i).totalDegree ≤ 1)
(hint : (projectionCoordinateMap I a).IsIntegral)
{m d : ℕ}
(hdimdeg : HasAffineDimensionDegree I m d)
:
∃ (e : ℕ), 0 < e ∧ e ≤ d ∧ HasAffineDimensionDegree (RingHom.ker (projectionCoordinateMap I a)) m e
An integral linear projection of a prime of dimension m and degree d has dimension m
and a positive degree at most d.