Homogeneous generators of an ordinal-graded algebra

Let A (Lean R) be a commutative algebra over a field E graded by NatOrdinal (the ordinals under the natural sum ⊕), so that A_i A_j ⊆ A_{i ⊕ j}. Let A_+ := ⨁_{β ≠ 0} A_β be the ideal of elements of positive degree; its square meets A_β in (A_+)² ∩ A_β = ∑_{i ⊕ j = β, i, j ≠ 0} A_i A_j (the decomposable elements of degree β; Lean decomposableAt 𝒜 β). A minimal system of homogeneous generators is a family of homogeneous elements x i ∈ A_{wt i} of positive degree whose members of each degree β are linearly independent modulo (A_+)² ∩ A_β and span A_β modulo it — a basis of a complement of (A_+)² ∩ A_β in A_β for every β ≠ 0. Evaluation E[X_i] → A, X_i ↦ x i, is then graded for the degrees deg X_i = wt i (Mathlib's IsWeightedHomogeneous wt) and surjective, by well-founded induction on the degree. Whether it is injective is the question whether A is a polynomial algebra on the generators; this file only names the homogeneous pieces of that question, InjectiveAt β (evaluation is injective in degree β), and shows that they assemble into the injectivity of evaluation. The finite-degree theory of ConwayRefinement.Algebra.LoweringDerivation is the case of degrees in ℕ.

The square of the ideal of positive degree

def OrdinalGraded.decomposableAt {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] (𝒜 : NatOrdinal → Submodule E R) (β : NatOrdinal) : Submodule E R

(A_+)² ∩ A_β = ∑_{i ⊕ j = β, i, j ≠ 0} A_i A_j, the square of the ideal of positive degree in degree β.

Equations

• OrdinalGraded.decomposableAt 𝒜 β = ⨆ (i : NatOrdinal), ⨆ (j : NatOrdinal), ⨆ (_ : i ≠ 0), ⨆ (_ : j ≠ 0), ⨆ (_ : i + j = β), 𝒜 i * 𝒜 j

theorem OrdinalGraded.decomposableAt_le {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] (𝒜 : NatOrdinal → Submodule E R) {β : NatOrdinal} {N : Submodule E R} (h : ∀ (i j : NatOrdinal), i ≠ 0 → j ≠ 0 → i + j = β → 𝒜 i * 𝒜 j ≤ N) : decomposableAt 𝒜 β ≤ N

theorem OrdinalGraded.mul_mem_decomposableAt {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] (𝒜 : NatOrdinal → Submodule E R) {i j : NatOrdinal} (hi : i ≠ 0) (hj : j ≠ 0) {a b : R} (ha : a ∈ 𝒜 i) (hb : b ∈ 𝒜 j) : a * b ∈ decomposableAt 𝒜 (i + j)

theorem OrdinalGraded.decomposableAt_le_degree {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] (𝒜 : NatOrdinal → Submodule E R) [GradedAlgebra 𝒜] (β : NatOrdinal) : decomposableAt 𝒜 β ≤ 𝒜 β

(A_+)² ∩ A_β lies in A_β.

Minimal systems of homogeneous generators

structure OrdinalGraded.IsMinimalSystem {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] (𝒜 : NatOrdinal → Submodule E R) {ι : Type w} (wt : ι → NatOrdinal) (x : ι → R) : Prop

A minimal system of homogeneous generators of an ordinal-graded algebra: homogeneous elements x i ∈ A_{wt i} of positive degree whose members of degree β are linearly independent modulo (A_+)² ∩ A_β = ∑_{i ⊕ j = β, i, j ≠ 0} A_i A_j and span A_β modulo it, for every β ≠ 0.

• ne_zero (i : ι) : wt i ≠ 0

  Every generator has positive degree.

• mem (i : ι) : x i ∈ 𝒜 (wt i)

  x i is homogeneous of degree wt i.

• independent (β : NatOrdinal) (c : ι →₀ E) : (∀ i ∈ c.support, wt i = β) → (Finsupp.linearCombination E x) c ∈ decomposableAt 𝒜 β → c = 0

  The generators of degree β are linearly independent modulo (A_+)² ∩ A_β.

• spans (β : NatOrdinal) : β ≠ 0 → ∀ y ∈ 𝒜 β, ∃ (c : ι →₀ E), (∀ i ∈ c.support, wt i = β) ∧ y - (Finsupp.linearCombination E x) c ∈ decomposableAt 𝒜 β

  The generators of degree β span A_β modulo (A_+)² ∩ A_β, for β ≠ 0.

Graded evaluation

theorem OrdinalGraded.aeval_mem_of_forall_mem {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {𝒜 : NatOrdinal → Submodule E R} [GradedAlgebra 𝒜] {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (hmem : ∀ (i : ι), x i ∈ 𝒜 (wt i)) {F : MvPolynomial ι E} {β : NatOrdinal} (hF : MvPolynomial.IsWeightedHomogeneous wt F β) : (MvPolynomial.aeval x) F ∈ 𝒜 β

Evaluation of a polynomial homogeneous of degree β (for deg X_i = wt i) at homogeneous elements x i ∈ A_{wt i} lands in A_β.

theorem OrdinalGraded.decompose_aeval {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {𝒜 : NatOrdinal → Submodule E R} [GradedAlgebra 𝒜] {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (hmem : ∀ (i : ι), x i ∈ 𝒜 (wt i)) (F : MvPolynomial ι E) (β : NatOrdinal) : ↑(((DirectSum.decompose 𝒜) ((MvPolynomial.aeval x) F)) β) = (MvPolynomial.aeval x) ((MvPolynomial.weightedHomogeneousComponent wt β) F)

Evaluation at homogeneous x i ∈ A_{wt i} is graded: the degree-β component of F(x) is the evaluation of the degree-β component of F.

theorem OrdinalGraded.aeval_linearCombination_X {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {ι : Type w} {x : ι → R} (c : ι →₀ E) : (MvPolynomial.aeval x) ((Finsupp.linearCombination E MvPolynomial.X) c) = (Finsupp.linearCombination E x) c

A linear combination of the generators is the evaluation of the same combination of the variables.

theorem OrdinalGraded.isWeightedHomogeneous_linearCombination_X {E : Type u} [Field E] {ι : Type w} {wt : ι → NatOrdinal} {β : NatOrdinal} (c : ι →₀ E) (hc : ∀ i ∈ c.support, wt i = β) : MvPolynomial.IsWeightedHomogeneous wt ((Finsupp.linearCombination E MvPolynomial.X) c) β

A linear combination of variables of degree β is homogeneous of degree β.

Generation

theorem OrdinalGraded.IsMinimalSystem.map_algEquiv {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {𝒜 : NatOrdinal → Submodule E R} {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (hx : IsMinimalSystem 𝒜 wt x) {S : Type u_1} [CommRing S] [Algebra E S] {ℬ : NatOrdinal → Submodule E S} (e : R ≃ₐ[E] S) (hgrade : ∀ (n : NatOrdinal) (r : R), r ∈ 𝒜 n ↔ e r ∈ ℬ n) : IsMinimalSystem ℬ wt fun (i : ι) => e (x i)

An algebra equivalence preserving every homogeneous component carries minimal systems to minimal systems.

theorem OrdinalGraded.IsMinimalSystem.apply_ne_zero {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {𝒜 : NatOrdinal → Submodule E R} {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (hx : IsMinimalSystem 𝒜 wt x) (i : ι) : x i ≠ 0

No generator of a minimal system is zero: zero lies in (A_+)² ∩ A_β.

theorem OrdinalGraded.IsMinimalSystem.aeval_mem {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {𝒜 : NatOrdinal → Submodule E R} [GradedAlgebra 𝒜] {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (hx : IsMinimalSystem 𝒜 wt x) {F : MvPolynomial ι E} {β : NatOrdinal} (hF : MvPolynomial.IsWeightedHomogeneous wt F β) : (MvPolynomial.aeval x) F ∈ 𝒜 β

Evaluation of a polynomial homogeneous of degree β lands in A_β.

theorem OrdinalGraded.IsMinimalSystem.exists_aeval_eq {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {𝒜 : NatOrdinal → Submodule E R} {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (hx : IsMinimalSystem 𝒜 wt x) (h0 : LoweringDerivation.GradeZeroScalars 𝒜) (β : NatOrdinal) (y : R) : y ∈ 𝒜 β → ∃ (F : MvPolynomial ι E), MvPolynomial.IsWeightedHomogeneous wt F β ∧ (MvPolynomial.aeval x) F = y

Every element of A_β is the evaluation of a weighted-homogeneous polynomial of weight β at a minimal system relative to the family 𝒜.

theorem OrdinalGraded.IsMinimalSystem.aeval_surjective {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {𝒜 : NatOrdinal → Submodule E R} [GradedAlgebra 𝒜] {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (hx : IsMinimalSystem 𝒜 wt x) (h0 : LoweringDerivation.GradeZeroScalars 𝒜) : Function.Surjective ⇑(MvPolynomial.aeval x)

Evaluation is surjective.

Homogeneous polynomials of degree zero

theorem OrdinalGraded.eq_C_of_isWeightedHomogeneous_zero {E : Type u} [Field E] {ι : Type w} {wt : ι → NatOrdinal} (hwt : ∀ (i : ι), wt i ≠ 0) {p : MvPolynomial ι E} (hp : MvPolynomial.IsWeightedHomogeneous wt p 0) : p = MvPolynomial.C (p.coeff 0)

For degrees wt i ≠ 0, a polynomial homogeneous of degree zero is a constant.

Injectivity degree by degree

def OrdinalGraded.InjectiveAt (E : Type u) {R : Type v} [Field E] [CommRing R] [Algebra E R] {ι : Type w} (wt : ι → NatOrdinal) (x : ι → R) (β : NatOrdinal) : Prop

Evaluation is injective in degree β: F = 0 is the only polynomial homogeneous of degree β with F(x) = 0.

Equations

• OrdinalGraded.InjectiveAt E wt x β = ∀ (F : MvPolynomial ι E), MvPolynomial.IsWeightedHomogeneous wt F β → (MvPolynomial.aeval x) F = 0 → F = 0

theorem OrdinalGraded.injectiveAt_iff {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (β : NatOrdinal) : InjectiveAt E wt x β ↔ ∀ (F : MvPolynomial ι E), MvPolynomial.IsWeightedHomogeneous wt F β → (MvPolynomial.aeval x) F = 0 → F = 0

theorem OrdinalGraded.injectiveAt_zero {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} [Nontrivial R] (hwt : ∀ (i : ι), wt i ≠ 0) : InjectiveAt E wt x 0

In degree zero evaluation is injective: a homogeneous polynomial of degree zero is a scalar.

theorem OrdinalGraded.injectiveAt_of_zero_successor_limit {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (hzero : InjectiveAt E wt x 0) (hsuccessor : ∀ (α : NatOrdinal), α.constantCoeff ≠ 0 → (∀ β < α, InjectiveAt E wt x β) → InjectiveAt E wt x α) (hlimit : ∀ (α : NatOrdinal), α ≠ 0 → α.constantCoeff = 0 → (∀ β < α, InjectiveAt E wt x β) → InjectiveAt E wt x α) (α : NatOrdinal) : InjectiveAt E wt x α

Injectivity in every ordinal degree follows from the zero, successor, and limit cases.

theorem OrdinalGraded.aeval_injective_of_forall_injectiveAt {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {𝒜 : NatOrdinal → Submodule E R} [GradedAlgebra 𝒜] {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (hmem : ∀ (i : ι), x i ∈ 𝒜 (wt i)) (h : ∀ (β : NatOrdinal), InjectiveAt E wt x β) : Function.Injective ⇑(MvPolynomial.aeval x)

Injectivity in every degree gives injectivity of evaluation.

The linear part of a homogeneous polynomial

theorem OrdinalGraded.exists_linear_part {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {𝒜 : NatOrdinal → Submodule E R} [GradedAlgebra 𝒜] {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (hwt : ∀ (i : ι), wt i ≠ 0) (hmem : ∀ (i : ι), x i ∈ 𝒜 (wt i)) {F : MvPolynomial ι E} {β : NatOrdinal} (hβ : β ≠ 0) (hF : MvPolynomial.IsWeightedHomogeneous wt F β) : ∃ (c : ι →₀ E), (∀ i ∈ c.support, wt i = β) ∧ (MvPolynomial.aeval x) F - (Finsupp.linearCombination E x) c ∈ decomposableAt 𝒜 β ∧ ∀ (i : ι), c i = F.coeff (Finsupp.single i 1)

A polynomial homogeneous of degree β ≠ 0 evaluates at homogeneous generators of positive degree to its linear part in the degree-β variables plus an element of (A_+)² ∩ A_β; the linear coefficients are read off the polynomial.

Monomials of degree zero

theorem OrdinalGraded.eq_zero_of_weight_eq_zero {ι : Type w} {wt : ι → NatOrdinal} (hwt : ∀ (i : ι), wt i ≠ 0) {d : ι →₀ ℕ} (hd : (Finsupp.weight wt) d = 0) : d = 0

For degrees wt i ≠ 0, only the constant monomial has degree zero.

Relations have no linear part and only variables of smaller degree

theorem OrdinalGraded.IsMinimalSystem.coeff_single_eq_zero_of_aeval_eq_zero {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {𝒜 : NatOrdinal → Submodule E R} [GradedAlgebra 𝒜] {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (hx : IsMinimalSystem 𝒜 wt x) {F : MvPolynomial ι E} {β : NatOrdinal} (hβ : β ≠ 0) (hF : MvPolynomial.IsWeightedHomogeneous wt F β) (h0 : (MvPolynomial.aeval x) F = 0) (i : ι) : F.coeff (Finsupp.single i 1) = 0

A homogeneous relation F(x) = 0 of degree β ≠ 0 has no linear monomial: its linear part is a combination of the generators of degree β lying in (A_+)² ∩ A_β.

theorem OrdinalGraded.IsMinimalSystem.wt_lt_of_mem_vars_of_aeval_eq_zero {E : Type u} {R : Type v} [Field E] [CommRing R] [Algebra E R] {𝒜 : NatOrdinal → Submodule E R} [GradedAlgebra 𝒜] {ι : Type w} {wt : ι → NatOrdinal} {x : ι → R} (hx : IsMinimalSystem 𝒜 wt x) {F : MvPolynomial ι E} {β : NatOrdinal} (hβ : β ≠ 0) (hF : MvPolynomial.IsWeightedHomogeneous wt F β) (h0 : (MvPolynomial.aeval x) F = 0) {i : ι} (hi : i ∈ F.vars) : wt i < β

Every variable of a homogeneous relation F(x) = 0 of degree β ≠ 0 has degree below β.