Homogeneous ideals: generators and componentwise absorption

The left ideal Ae generated by a homogeneous element e of a graded ring is homogeneous. This is the homogeneity witness for the left ideal Af generated by a degree-zero idempotent f, which TauCeti.GradedModuleCat.ofIdeal turns into a projective graded module.

This file also proves the absorption lemmas for componentwise membership: if every homogeneous component of x lies in an ideal, then so does every homogeneous component of a * x, and, when the ideal is two-sided, of x * a.

Finally, in a connected ℕ-graded algebra, whose degree-zero part consists of the scalars, every element is its constant term plus an element of the irrelevant ideal. So the scalars map onto A ⧸ A₊, and over a field the irrelevant ideal is maximal.

Main results

• Ideal.isHomogeneous_span_singleton: the left ideal generated by a homogeneous element is homogeneous.
• Ideal.proj_mul_mem_left and Ideal.proj_mul_mem_right: the absorption lemmas. The right one asks the ideal to be two-sided, through Ideal.IsTwoSided.
• CompleteOrthogonalIdempotents.mem_zero_of_isHomogeneous_span: a complete family of orthogonal idempotents with homogeneous left ideals consists of degree-zero elements.
• TauCeti.GradedAlgebra.exists_sub_algebraMap_mem_irrelevant: in a connected graded algebra every element is a scalar plus an element of the irrelevant ideal.
• TauCeti.GradedAlgebra.surjective_algebraMap_quotient_irrelevant: in a connected graded algebra the scalars map onto A ⧸ A₊.
• TauCeti.GradedAlgebra.isMaximal_toIdeal_irrelevant: the irrelevant ideal of a nontrivial connected graded algebra over a field is maximal.

Implementation notes

Mathlib's Ideal.mul_homogeneous_element_mem_of_mem supplies the homogeneous case of Ideal.proj_mul_mem_left, where the homogeneous factor is on the right. Its mirror image Ideal.homogeneous_element_mul_mem_of_mem, with the homogeneous factor on the left, is the one place two-sidedness is used.

References

The proof of Ideal.homogeneous_element_mul_mem_of_mem is adapted from Mathlib's proof of Ideal.mul_homogeneous_element_mem_of_mem, with the two factors swapped.

theorem Ideal.isHomogeneous_span_singleton {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {e : A} (he : SetLike.IsHomogeneousElem 𝒜 e) : IsHomogeneous 𝒜 (span {e})

The left ideal generated by a homogeneous element is homogeneous. This is the homogeneity witness for Af at a degree-zero idempotent f.

theorem Ideal.proj_mul_mem_left {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {I : Ideal A} {x : A} (hx : ∀ (i : ι), (GradedRing.proj 𝒜 i) x ∈ I) (a : A) (j : ι) : (GradedRing.proj 𝒜 j) (a * x) ∈ I

Left absorption of componentwise membership: if every homogeneous component of x lies in an ideal, so does every homogeneous component of a * x.

theorem Ideal.homogeneous_element_mul_mem_of_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {I : Ideal A} [I.IsTwoSided] {x : A} (hx : SetLike.IsHomogeneousElem 𝒜 x) (hxI : x ∈ I) (a : A) (j : ι) : (GradedRing.proj 𝒜 j) (x * a) ∈ I

The homogeneous components of x * a, for x a homogeneous element of a two-sided ideal, lie in that ideal. This is the mirror image of Ideal.mul_homogeneous_element_mem_of_mem.

theorem Ideal.proj_mul_mem_right {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {I : Ideal A} [I.IsTwoSided] {x : A} (hx : ∀ (i : ι), (GradedRing.proj 𝒜 i) x ∈ I) (a : A) (j : ι) : (GradedRing.proj 𝒜 j) (x * a) ∈ I

Right absorption of componentwise membership: if every homogeneous component of x lies in a two-sided ideal, so does every homogeneous component of x * a.

theorem CompleteOrthogonalIdempotents.mem_zero_of_isHomogeneous_span {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {I : Type u_4} [Fintype I] {e : I → A} (he : CompleteOrthogonalIdempotents e) (hI : ∀ (i : I), Ideal.IsHomogeneous 𝒜 (Ideal.span {e i})) (i : I) : e i ∈ 𝒜 0

A complete family of orthogonal idempotents with homogeneous left ideals is homogeneous of degree zero.

theorem TauCeti.GradedAlgebra.exists_sub_algebraMap_mem_irrelevant {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (h𝒜 : ∀ x ∈ 𝒜 0, x ∈ ⊥) (a : A) : ∃ (c : R), a - (algebraMap R A) c ∈ HomogeneousIdeal.irrelevant 𝒜

In a connected graded algebra, whose degree-zero part consists of the scalars, every element is a scalar plus an element of the irrelevant ideal.

theorem TauCeti.GradedAlgebra.surjective_algebraMap_quotient_irrelevant {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (h𝒜 : ∀ x ∈ 𝒜 0, x ∈ ⊥) : Function.Surjective ⇑(algebraMap R (A ⧸ (HomogeneousIdeal.irrelevant 𝒜).toIdeal))

In a connected graded algebra the scalars map onto A ⧸ A₊: every element is its constant term modulo A₊.

theorem TauCeti.GradedAlgebra.isMaximal_toIdeal_irrelevant {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Nontrivial A] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] (h𝒜 : ∀ x ∈ 𝒜 0, x ∈ ⊥) : (HomogeneousIdeal.irrelevant 𝒜).toIdeal.IsMaximal

The irrelevant ideal of a nontrivial connected graded algebra over a field is maximal, since the quotient A ⧸ A₊ is the field k.