The constructed Hilbert dimension equals transcendence-basis cardinality. Consequently integral embeddings preserve Hilbert dimension.
Construct a finite linear parameter field from coordinate functions, in arbitrary Hilbert dimension.
theorem
CCDN.exists_hilbert_coordinate_transcendence_basis
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Fintype σ]
[LinearOrder σ]
(I : Ideal (MvPolynomial σ K))
[I.IsPrime]
:
∃ (U : Set σ),
Nat.card ↑U = (filteredHilbertPolynomial I).natDegree ∧ IsTranscendenceBasis K fun (i : ↑U) => (Ideal.Quotient.mk I) (MvPolynomial.X ↑i)
For a prime ideal I, some set of coordinate functions, of size the Hilbert dimension of I,
is a transcendence basis of K[X] ⧸ I over K.
theorem
CCDN.hilbert_dimension_eq_transcendence_basis_card
{K : Type u_1}
{σ : Type u_2}
{ι : Type u_3}
[Field K]
[Fintype σ]
[LinearOrder σ]
[Fintype ι]
(I : Ideal (MvPolynomial σ K))
[I.IsPrime]
(x : ι → MvPolynomial σ K ⧸ I)
(hx : IsTranscendenceBasis K x)
:
For a prime ideal I, the Hilbert dimension of I equals the cardinality of any transcendence
basis of K[X] ⧸ I over K.
theorem
CCDN.integral_embedding_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]
(J : Ideal (MvPolynomial τ K))
[J.IsPrime]
(ψ : MvPolynomial σ K ⧸ I →ₐ[K] MvPolynomial τ K ⧸ J)
(hψ : Function.Injective ⇑ψ)
(hint : ψ.IsIntegral)
:
Integral embeddings preserve the filtered Hilbert dimension, without assuming a normalization or a Hilbert polynomial.