Structures · Algebra

GradedRing

An internally-graded R-algebra A is one that can be decomposed into a collection of Submodule R As indexed by ι such that the canonical map A → ⨁ i, 𝒜 i is bijective and respects multiplication, i.e. the product of an element of degree i and an element of degree j is an element of degree i + j. Note that the fact that A is internally-graded, GradedAlgebra 𝒜, implies an externally-graded algebra structure DirectSum.GAlgebra R (fun i ↦ ↥(𝒜 i)), which in turn makes available an Algebra R (⨁ i, 𝒜 i) instance.

Defined in

Mathlib.RingTheory.GradedAlgebra.Basic

Shape

One type argument