The graded Nakayama lemma for generators

Let A be a commutative semiring graded by 𝒜 : ℕ → σ, and let A₊ = ⨁_{n > 0} 𝒜 n be its irrelevant ideal. If a set s of homogeneous elements of positive degree generates A₊ modulo A₊², that is, if the classes of the elements of s generate the indecomposables A₊ ⧸ A₊², then s generates A as an algebra over the degree-zero part 𝒜 0.

The proof is by strong induction on the degree. A homogeneous element x of degree n > 0 is a combination ∑ rᵢ tᵢ with each tᵢ either an element of s or a product a b of homogeneous elements of positive degree. Keeping only the degree-n components replaces each coefficient rᵢ by a homogeneous element of degree smaller than n, and each product a b that contributes has factors of degree smaller than n.

For a connected graded ring, such as the Lazard ring, this reduces generation by a family of homogeneous elements to a computation of the indecomposables.

Main results

• TauCeti.GradedAlgebra.adjoin_eq_top_of_irrelevant_le: homogeneous elements of positive degree generating the irrelevant ideal modulo its square generate the graded ring over its degree-zero part.
• TauCeti.GradedAlgebra.subalgebra_eq_top_of_irrelevant_le: for a graded R-algebra, a subalgebra containing the degree-zero part and such generators is everything.
• TauCeti.GradedAlgebra.adjoin_eq_top_of_irrelevant_le_of_mem_bot: when the degree-zero part consists of scalars, such generators generate the graded algebra as an R-algebra.
• TauCeti.GradedAlgebra.surjective_aeval_of_irrelevant_le: in that case, evaluation of polynomials at such a family of generators is surjective.

References

• J. F. Adams, Stable Homotopy and Generalised Homology, Part II, §7.

theorem TauCeti.GradedAlgebra.adjoin_eq_top_of_irrelevant_le {A : Type u_1} {σ : Type u_2} [CommSemiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {s : Set A} (hs : ∀ x ∈ s, ∃ (i : ℕ), 0 < i ∧ x ∈ 𝒜 i) (h : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span s ⊔ (HomogeneousIdeal.irrelevant 𝒜).toIdeal ^ 2) : Algebra.adjoin (↥(𝒜 0)) s = ⊤

The graded Nakayama lemma for generators. If a set s of homogeneous elements of positive degree generates the irrelevant ideal A₊ of an ℕ-graded commutative semiring modulo A₊², then s generates the semiring as an algebra over its degree-zero part.

theorem TauCeti.GradedAlgebra.subalgebra_eq_top_of_irrelevant_le {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (B : Subalgebra R A) (hB : ∀ x ∈ 𝒜 0, x ∈ B) {s : Set A} (hsB : s ⊆ ↑B) (hs : ∀ x ∈ s, ∃ (n : ℕ), 0 < n ∧ x ∈ 𝒜 n) (h : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span s ⊔ (HomogeneousIdeal.irrelevant 𝒜).toIdeal ^ 2) : B = ⊤

Graded Nakayama for algebras. Let s consist of homogeneous elements of positive degree which generate the irrelevant ideal A₊ modulo A₊ ^ 2. Then every subalgebra containing the degree-zero part and s is the whole algebra.

theorem TauCeti.GradedAlgebra.adjoin_eq_top_of_irrelevant_le_of_mem_bot {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (h𝒜 : ∀ x ∈ 𝒜 0, x ∈ ⊥) {s : Set A} (hs : ∀ x ∈ s, ∃ (n : ℕ), 0 < n ∧ x ∈ 𝒜 n) (h : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span s ⊔ (HomogeneousIdeal.irrelevant 𝒜).toIdeal ^ 2) : Algebra.adjoin R s = ⊤

Graded Nakayama for connected graded algebras. If the degree-zero part of A consists of scalars, homogeneous elements of positive degree which generate the irrelevant ideal A₊ modulo A₊ ^ 2 generate A as an R-algebra.

theorem TauCeti.GradedAlgebra.surjective_aeval_of_irrelevant_le {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (h𝒜 : ∀ x ∈ 𝒜 0, x ∈ ⊥) {ι : Type u_3} {f : ι → A} (hf : ∀ (i : ι), ∃ (n : ℕ), 0 < n ∧ f i ∈ 𝒜 n) (h : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f) ⊔ (HomogeneousIdeal.irrelevant 𝒜).toIdeal ^ 2) : Function.Surjective ⇑(MvPolynomial.aeval f)

If the degree-zero part of A consists of scalars, evaluation of polynomials at a family of homogeneous elements of positive degree which generate the irrelevant ideal modulo its square is surjective.