Documentation

TauCeti.RingTheory.GradedAlgebra.Homogeneous.Quotient

The grading induced on a quotient by a homogeneous ideal #

A homogeneous two-sided ideal I in an R-algebra A graded by π’œ descends that grading to A β§Έ I. Its degree-i piece is TauCeti.GradedAlgebra.quotientPiece π’œ I i, the image of π’œ i under the quotient map. The scalar base R can be a commutative semiring.

The graded pieces are submodules of the quotient itself. Homogeneity lets the additive degree projections descend to the quotient, where they recover each coordinate of a finite sum. Thus the pieces form an internal direct sum, giving TauCeti.GradedAlgebra.gradedAlgebraQuotientPiece. This structure is a definition rather than a global instance: callers choose the grading locally with letI.

The construction follows Antoine Chambert-Loir's Mathlib PR #36501: the degree-i piece as the image of π’œ i under the quotient map, separation of the pieces via GradedRing.proj, and the induced GradedAlgebra assembled from DirectSum.IsInternal.

References #

Assem--Simson--SkowroΕ„ski, Elements of the Representation Theory of Associative Algebras I, Ch. II.

source
theorem TauCeti.GradedAlgebra.isInternal_quotientPiece {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ΞΉ] [AddMonoid ΞΉ] [CommSemiring R] [Ring A] [Algebra R A] (π’œ : ΞΉ β†’ Submodule R A) [GradedAlgebra π’œ] (I : Ideal A) [I.IsTwoSided] (hI : Ideal.IsHomogeneous π’œ I) :
DirectSum.IsInternal (quotientPiece π’œ I)

The quotient by a homogeneous ideal is the internal direct sum of its descended pieces.

source
theorem TauCeti.GradedAlgebra.iSupIndep_quotientPiece {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ΞΉ] [AddMonoid ΞΉ] [CommSemiring R] [Ring A] [Algebra R A] (π’œ : ΞΉ β†’ Submodule R A) [GradedAlgebra π’œ] (I : Ideal A) [I.IsTwoSided] (hI : Ideal.IsHomogeneous π’œ I) :
iSupIndep (quotientPiece π’œ I)

The images of the graded pieces are independent modulo a homogeneous ideal.

source
@[instance_reducible]
noncomputable def TauCeti.GradedAlgebra.gradedAlgebraQuotientPiece {ΞΉ : Type u_1} {R : Type u_2} {A : Type u_3} [DecidableEq ΞΉ] [AddMonoid ΞΉ] [CommSemiring R] [Ring A] [Algebra R A] (π’œ : ΞΉ β†’ Submodule R A) [GradedAlgebra π’œ] (I : Ideal A) [I.IsTwoSided] (hI : Ideal.IsHomogeneous π’œ I) :
GradedAlgebra (quotientPiece π’œ I)

The induced grading on the quotient by a homogeneous ideal. This is a definition rather than an instance so that callers choose when to introduce the grading.

Equations
Instances For