Theorems · Inductive type · ring theory

GradedRing

{ι : Type u_1} →
  {A : Type u_3} →
    {σ : Type u_4} →
      [DecidableEq ι] →
        [AddMonoid ι] →
          [inst : Semiring A] → [inst_1 : SetLike σ A] → [AddSubmonoidClass σ A] → (ι → σ) → Type (max u_1 u_3)

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

Cited by

424 results in Mathlib

Foundations

Depth 11 from the axioms, rests on 97 definitions · uses no axioms

Assumes

DecidableEqAddMonoidSemiringSetLikeAddSubmonoidClass