Algebraically independent linear coordinates have cardinality at most the degree of the filtered Hilbert polynomial.
theorem
CCDN.projectionCoordinateMap_eq_aeval
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
(I : Ideal (MvPolynomial τ K))
(a : σ → MvPolynomial τ K)
:
projectionCoordinateMap I a is evaluation at the classes of the coordinate polynomials a i
in K[X] ⧸ I.
theorem
CCDN.injective_projectionCoordinateMap_iff
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
{I : Ideal (MvPolynomial τ K)}
{a : σ → MvPolynomial τ K}
:
Function.Injective ⇑(projectionCoordinateMap I a) ↔ AlgebraicIndependent K fun (i : σ) => (Ideal.Quotient.mk I) (a i)
The projection map is injective exactly when the images of the coordinates in the quotient are algebraically independent.
theorem
CCDN.independent_linear_card_le_hilbert_dimension
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
[Fintype σ]
[Fintype τ]
[LinearOrder τ]
(I : Ideal (MvPolynomial τ K))
(a : σ → MvPolynomial τ K)
(ha : ∀ (i : σ), (a i).totalDegree ≤ 1)
(hi : AlgebraicIndependent K fun (i : σ) => (Ideal.Quotient.mk I) (a i))
:
If polynomials a i of degree at most one have algebraically independent classes in K[X] ⧸ I,
their number is at most the degree of the filtered Hilbert polynomial of I.
theorem
CCDN.linear_projection_not_injective_of_hilbert_dimension_lt
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
[Fintype σ]
[Fintype τ]
[LinearOrder τ]
(I : Ideal (MvPolynomial τ K))
(a : σ → MvPolynomial τ K)
(ha : ∀ (i : σ), (a i).totalDegree ≤ 1)
(hd : (filteredHilbertPolynomial I).natDegree < Fintype.card σ)
:
If more polynomials a i of degree at most one are given than the degree of the filtered
Hilbert polynomial of I, then projectionCoordinateMap I a is not injective.