Linear-growth monomial sets

A downward-closed exponent set with a linear counting bound cannot contain a large square. Consequently its unbounded portions lie in coordinate rays.

instance CCDN.finite_boundedStandardExponents {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (I : Ideal (MvPolynomial σ K)) (m : MonomialOrder σ) (N : ℕ) : Finite ↑(I.boundedStandardExponents m N)

Bounded exponent sets are finite.

theorem CCDN.standard_at_most_one_large {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) (C : ℕ) (hbound : ∀ N ≥ 14, Module.finrank K ↥(filteredCoordinateSpace I N) ≤ C * (N + 2)) {a : σ →₀ ℕ} (ha : a ∈ I.standardExponents MonomialOrder.degLex) {i j : σ} (hi : 2 * C + 14 ≤ a i) (hj : 2 * C + 14 ≤ a j) : i = j

Under a linear Hilbert bound, at most one exponent can exceed a fixed threshold. This excludes every two-dimensional monomial quadrant.

noncomputable def CCDN.exponentRay {σ : Type u_1} [Fintype σ] (B : ℕ) (j : σ) (b : σ → Fin B) (n : ℕ) : σ →₀ ℕ

A coordinate ray whose other coordinates lie in a finite box.

Equations

• CCDN.exponentRay B j b n = (Finsupp.equivFunOnFinite.symm fun (k : σ) => ↑(b k)).update j n

@[simp]

theorem CCDN.exponentRay_apply {σ : Type u_1} [Fintype σ] [DecidableEq σ] (B : ℕ) (j : σ) (b : σ → Fin B) (n : ℕ) (k : σ) : (exponentRay B j b n) k = if k = j then n else ↑(b k)

The ray exponent exponentRay B j b n has coordinate n at j and coordinate b k at every other k.

theorem CCDN.lowerSet_rays_eventually_full {σ : Type u_1} [Fintype σ] (S : Set (σ →₀ ℕ)) (hS : IsLowerSet S) (B : ℕ) : ∃ M ≥ B, ∀ (j : σ) (b : σ → Fin B) (n : ℕ), M ≤ n → (exponentRay B j b n ∈ S ↔ ∀ (k : ℕ), exponentRay B j b k ∈ S)

Uniformly over all rays based in a finite box, membership in a lower set stabilizes to either the whole ray or the empty tail.