Balanced coordinate-power reductions imply eventual generation by a linear parameter in arbitrary ambient dimension.
theorem
CCDN.filteredCoordinateSpace_mono
{K : Type u_1}
{σ : Type u_2}
[Field K]
(I : Ideal (MvPolynomial σ K))
{m n : ℕ}
(hmn : m ≤ n)
:
The degree filtration of the coordinate ring MvPolynomial σ K ⧸ I is increasing.
theorem
CCDN.filteredCoordinateSpace_mul_mem
{K : Type u_1}
{σ : Type u_2}
[Field K]
(I : Ideal (MvPolynomial σ K))
{m n : ℕ}
{x y : MvPolynomial σ K ⧸ I}
(hx : x ∈ filteredCoordinateSpace I m)
(hy : y ∈ filteredCoordinateSpace I n)
:
The degree filtration of the coordinate ring is multiplicative: a product of classes of
degree at most m and n has degree at most m + n.
theorem
CCDN.large_exponent_of_degree
{σ : Type u_1}
[Fintype σ]
(e : σ →₀ ℕ)
(N : ℕ)
(hpos : 0 < Finsupp.degree e)
(he : Fintype.card σ * N ≤ Finsupp.degree e)
:
∃ (j : σ), N ≤ e j
An exponent vector of positive degree at least Fintype.card σ * N has some coordinate
at least N.
theorem
CCDN.eventual_generation_of_power_reductions
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Fintype σ]
(I : Ideal (MvPolynomial σ K))
(l : MvPolynomial σ K)
(hl : l.totalDegree ≤ 1)
(N : ℕ)
(hN : 0 < N)
(hpow :
∀ (j : σ),
∃ (r : MvPolynomial σ K) (s : MvPolynomial σ K),
r.totalDegree ≤ N - 1 ∧ s.totalDegree ≤ N - 1 ∧ (Ideal.Quotient.mk I) (MvPolynomial.X j ^ N) = (Ideal.Quotient.mk I) r + (Ideal.Quotient.mk I) l * (Ideal.Quotient.mk I) s)
(n : ℕ)
:
n ≥ Fintype.card σ * N →
filteredCoordinateSpace I (n + 1) = filteredCoordinateSpace I n ⊔
Submodule.map (LinearMap.mulLeft K ((Ideal.Quotient.mk I) l)) (filteredCoordinateSpace I n)
Let l have total degree at most 1. If each coordinate power X j ^ N is congruent
modulo I to r + l * s with r and s of total degree at most N - 1, then for every
n ≥ Fintype.card σ * N the degree-(n + 1) piece of the filtered coordinate ring is the
degree-n piece plus l times the degree-n piece.