Documentation

TauCeti.RingTheory.TwoSidedIdeal.Homogeneous

Two-sided ideals spanned by homogeneous elements #

A relation ideal of a noncommutative graded ring is presented as TwoSidedIdeal.span of a set of relators, and it is homogeneous as soon as those relators are. This file proves that, together with the two absorption lemmas the proof runs on: if every homogeneous component of x lies in an ideal, then so does every homogeneous component of a * x and of x * a.

Homogeneity itself is stated through Mathlib's Ideal.IsHomogeneous, applied to the underlying one-sided ideal TwoSidedIdeal.asIdeal, which is where the quotient by a two-sided ideal is formed.

Main results #

Implementation notes #

Mathlib's Ideal.mul_homogeneous_element_mem_of_mem supplies the one-sided half of TauCeti.Ideal.proj_mul_mem_left, where the homogeneous factor is on the right; multiplying on the right only asks the ideal to absorb on the left, so that lemma is stated for an Ideal and lives in the matching namespace. Its mirror image TauCeti.TwoSidedIdeal.homogeneous_element_mul_mem_of_mem is the one place two-sidedness is used, and it is therefore stated for a TwoSidedIdeal.

References #

Mathlib's Ideal.homogeneous_span is the one-sided statement that TauCeti.TwoSidedIdeal.homogeneous_span extends from Ideal.span to TwoSidedIdeal.span, and the proof of TauCeti.TwoSidedIdeal.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.

The open Mathlib PR #36501 builds the graded structure on the quotient of a graded ring by a homogeneous relation. That is the step after the one taken here, and it is independent of it: homogeneity of the relation is an input there, and it is what the statements below produce for a relation ideal presented by generators.

source
theorem TauCeti.Ideal.proj_mul_mem_left {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [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.

source
theorem TauCeti.TwoSidedIdeal.homogeneous_element_mul_mem_of_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Ring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I : TwoSidedIdeal A} {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, and it is where the two-sidedness is used.

source
theorem TauCeti.TwoSidedIdeal.proj_mul_mem_right {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Ring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I : TwoSidedIdeal A} {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.

source
theorem TauCeti.TwoSidedIdeal.homogeneous_span {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Ring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {s : Set A} (hs : ∀ x ∈ s, SetLike.IsHomogeneousElem 𝒜 x) :
Ideal.IsHomogeneous 𝒜 (TwoSidedIdeal.asIdeal (TwoSidedIdeal.span s))

A two-sided ideal spanned by homogeneous elements is homogeneous. This supplies the homogeneity condition needed to descend a grading to a relation quotient.