Linear coordinate substitutions preserve the total-degree filtration. Their image coordinate rings inject into the original filtered ring.
theorem
CCDN.aeval_totalDegree_le
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
[Finite σ]
(a : σ → MvPolynomial τ K)
{m : ℕ}
(ha : ∀ (i : σ), (a i).totalDegree ≤ m)
(f : MvPolynomial σ K)
:
Substituting polynomials of total degree at most m multiplies the total degree by at most m.
noncomputable def
CCDN.projectionCoordinateMap
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
(I : Ideal (MvPolynomial τ K))
(a : σ → MvPolynomial τ K)
:
The map from projection coordinates to the original coordinate ring.
Equations
- CCDN.projectionCoordinateMap I a = (Ideal.Quotient.mkₐ K I).comp (MvPolynomial.aeval a)
Instances For
theorem
CCDN.projectionCoordinateMap_filtered
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
[Finite σ]
(I : Ideal (MvPolynomial τ K))
(a : σ → MvPolynomial τ K)
(ha : ∀ (i : σ), (a i).totalDegree ≤ 1)
{M : ℕ}
(f : MvPolynomial σ K)
(hf : f.totalDegree ≤ M)
:
A linear coordinate substitution maps polynomials of total degree at most M into the filtered
piece of degree M of the coordinate ring.
theorem
CCDN.linear_projection_filtered_finrank_le
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
[Finite σ]
[Finite τ]
(I : Ideal (MvPolynomial τ K))
(a : σ → MvPolynomial τ K)
(ha : ∀ (i : σ), (a i).totalDegree ≤ 1)
(M : ℕ)
:
Module.finrank K ↥(filteredCoordinateSpace (RingHom.ker (projectionCoordinateMap I a)) M) ≤ Module.finrank K ↥(filteredCoordinateSpace I M)
Linear projection cannot increase any filtered coordinate-ring dimension.