# Documentation

This module provides a set of heterogeneous typeclasses for defining a multiplicative structure over the sigma type GradedMonoid A such that (*) : A i → A j → A (i + j)→ A j → A (i + j)→ A (i + j); that is to say, A forms an additively-graded monoid. The typeclasses are:

• GradedMonoid.GOne A
• GradedMonoid.GMul A
• GradedMonoid.GMonoid A
• GradedMonoid.GCommMonoid A

With the SigmaGraded locale open, these respectively imbue:

• One (GradedMonoid A)
• Mul (GradedMonoid A)
• Monoid (GradedMonoid A)
• CommMonoid (GradedMonoid A)

the base type A 0 with:

• GradedMonoid.GradeZero.One
• GradedMonoid.GradeZero.Mul
• GradedMonoid.GradeZero.Monoid
• GradedMonoid.GradeZero.CommMonoid

and the ith grade A i with A 0-actions (•) defined as left-multiplication:

• (nothing)
• GradedMonoid.GradeZero.SMul (A 0)
• GradedMonoid.GradeZero.MulAction (A 0)
• (nothing)

For now, these typeclasses are primarily used in the construction of DirectSum.Ring and the rest of that file.

This also introduces List.dProd, which takes the (possibly non-commutative) product of a list of graded elements of type A i. This definition primarily exist to allow GradedMonoid.mk and DirectSum.of to be pulled outside a product, such as in GradedMonoid.mk_list_dProd and DirectSum.of_list_dProd.

In addition to the above typeclasses, in the most frequent case when A is an indexed collection of SetLike subobjects (such as AddSubmonoids, AddSubgroups, or Submodules), this file provides the Prop typeclasses:

• SetLike.GradedOne A (which provides the obvious GradedMonoid.GOne A instance)
• SetLike.GradedMul A (which provides the obvious GradedMonoid.GMul A instance)
• SetLike.GradedMonoid A (which provides the obvious GradedMonoid.GMonoid A and GradedMonoid.GCommMonoid A instances)

which respectively provide the API lemmas

• SetLike.one_mem_graded
• SetLike.mul_mem_graded
• SetLike.pow_mem_graded, SetLike.list_prod_map_mem_graded

Strictly this last class is unecessary as it has no fields not present in its parents, but it is included for convenience. Note that there is no need for SetLike.GradedRing or similar, as all the information it would contain is already supplied by GradedMonoid when A is a collection of objects satisfying AddSubmonoidClass such as Submodules. These constructions are explored in Algebra.DirectSum.Internal.

This file also defines:

• SetLike.isHomogeneous A (which says that a is homogeneous iff a ∈ A i∈ A i for some i : ι)
• SetLike.HomogeneouSubmonoid A, which is, as the name suggests, the submonoid consisting of all the homogeneous elements.

## tags #

def GradedMonoid {ι : Type u_1} (A : ιType u_2) :
Type (maxu_1u_2)

A type alias of sigma types for graded monoids.

Equations
instance GradedMonoid.instInhabitedGradedMonoid {ι : Type u_1} {A : ιType u_2} [inst : ] [inst : Inhabited (A default)] :
Equations
def GradedMonoid.mk {ι : Type u_1} {A : ιType u_2} (i : ι) :
A i

Construct an element of a graded monoid.

Equations

### Typeclasses #

class GradedMonoid.GOne {ι : Type u_1} (A : ιType u_2) [inst : Zero ι] :
Type u_2
• The term one of grade 0

one : A 0

A graded version of One, which must be of grade 0.

Instances
instance GradedMonoid.GOne.toOne {ι : Type u_1} (A : ιType u_2) [inst : Zero ι] [inst : ] :
One ()

GOne implies One (GradedMonoid A)

Equations
• = { one := { fst := 0, snd := GradedMonoid.GOne.one } }
class GradedMonoid.GMul {ι : Type u_1} (A : ιType u_2) [inst : Add ι] :
Type (maxu_1u_2)
• The homogeneous multiplication map mul

mul : {i j : ι} → A iA jA (i + j)

A graded version of Mul. Multiplication combines grades additively, like AddMonoidAlgebra.

Instances
instance GradedMonoid.GMul.toMul {ι : Type u_1} (A : ιType u_2) [inst : Add ι] [inst : ] :
Mul ()

GMul implies Mul (GradedMonoid A).

Equations
theorem GradedMonoid.mk_mul_mk {ι : Type u_1} (A : ιType u_2) [inst : Add ι] [inst : ] {i : ι} {j : ι} (a : A i) (b : A j) :
* = GradedMonoid.mk (i + j) ()
def GradedMonoid.GMonoid.gnpowRec {ι : Type u_1} {A : ιType u_2} [inst : ] [inst : ] [inst : ] (n : ) {i : ι} :
A iA (n i)

A default implementation of power on a graded monoid, like npowRec. GMonoid.gnpow should be used instead.

Equations
@[simp]
theorem GradedMonoid.GMonoid.gnpowRec_zero {ι : Type u_1} {A : ιType u_2} [inst : ] [inst : ] [inst : ] (a : ) :
GradedMonoid.mk (0 a.fst) () = 1
@[simp]
theorem GradedMonoid.GMonoid.gnpowRec_succ {ι : Type u_1} {A : ιType u_2} [inst : ] [inst : ] [inst : ] (n : ) (a : ) :
GradedMonoid.mk ( a.fst) () = a * { fst := n a.fst, snd := }

A tactic to for use as an optional value for Gmonoid.gnpow_zero''

Equations
• One or more equations did not get rendered due to their size.

A tactic to for use as an optional value for Gmonoid.gnpow_succ''

Equations
• One or more equations did not get rendered due to their size.
class GradedMonoid.GMonoid {ι : Type u_1} (A : ιType u_2) [inst : ] extends , :
Type (maxu_1u_2)
• Muliplication by one on the left is the identity

one_mul : ∀ (a : ), 1 * a = a
• Muliplication by one on the right is the identity

mul_one : ∀ (a : ), a * 1 = a
• Multiplication is associative

mul_assoc : ∀ (a b c : ), a * b * c = a * (b * c)
• Optional field to allow definitional control of natural powers

gnpow : (n : ) → {i : ι} → A iA (n i)
• The zeroth power will yield 1

gnpow_zero' : autoParam (∀ (a : ), GradedMonoid.mk (0 a.fst) (gnpow 0 a.fst a.snd) = 1) _auto✝
• Successor powers behave as expected

gnpow_succ' : autoParam (∀ (n : ) (a : ), GradedMonoid.mk ( a.fst) (gnpow () a.fst a.snd) = a * { fst := n a.fst, snd := gnpow n a.fst a.snd }) _auto✝

A graded version of monoid

Like Monoid.npow, this has an optional GMonoid.gnpow field to allow definitional control of natural powers of a graded monoid.

Instances
instance GradedMonoid.GMonoid.toMonoid {ι : Type u_1} (A : ιType u_2) [inst : ] [inst : ] :

GMonoid implies a Monoid (GradedMonoid A).

Equations
• One or more equations did not get rendered due to their size.
theorem GradedMonoid.mk_pow {ι : Type u_1} (A : ιType u_2) [inst : ] [inst : ] {i : ι} (a : A i) (n : ) :
^ n = GradedMonoid.mk (n i) ()
class GradedMonoid.GCommMonoid {ι : Type u_1} (A : ιType u_2) [inst : ] extends :
Type (maxu_1u_2)
• Multiplication is commutative

mul_comm : ∀ (a b : ), a * b = b * a

A graded version of CommMonoid.

Instances
instance GradedMonoid.GCommMonoid.toCommMonoid {ι : Type u_1} (A : ιType u_2) [inst : ] [inst : ] :

GCommMonoid implies a CommMonoid (GradedMonoid A), although this is only used as an instance locally to define notation in gmonoid and similar typeclasses.

Equations

### Instances for A 0#

The various g* instances are enough to promote the AddCommMonoid (A 0) structure to various types of multiplicative structure.

instance GradedMonoid.GradeZero.one {ι : Type u_1} (A : ιType u_2) [inst : Zero ι] [inst : ] :
One (A 0)

1 : A 0 is the value provided in GOne.one.

Equations
• = { one := GradedMonoid.GOne.one }
instance GradedMonoid.GradeZero.smul {ι : Type u_1} (A : ιType u_2) [inst : ] [inst : ] (i : ι) :
SMul (A 0) (A i)

(•) : A 0 → A i → A i→ A i → A i→ A i is the value provided in GradedMonoid.GMul.mul, composed with an Eq.rec to turn A (0 + i) into A i.

Equations
• = { smul := fun x y => (_ : 0 + i = i) }
instance GradedMonoid.GradeZero.mul {ι : Type u_1} (A : ιType u_2) [inst : ] [inst : ] :
Mul (A 0)

(*) : A 0 → A 0 → A 0→ A 0 → A 0→ A 0 is the value provided in GradedMonoid.GMul.mul, composed with an Eq.rec to turn A (0 + 0) into A 0.

Equations
• = { mul := fun x x_1 => x x_1 }
@[simp]
theorem GradedMonoid.mk_zero_smul {ι : Type u_1} {A : ιType u_2} [inst : ] [inst : ] {i : ι} (a : A 0) (b : A i) :
@[simp]
theorem GradedMonoid.GradeZero.smul_eq_mul {ι : Type u_1} {A : ιType u_2} [inst : ] [inst : ] (a : A 0) (b : A 0) :
a b = a * b
instance GradedMonoid.instPowOfNatToOfNat0ToZeroNat {ι : Type u_1} (A : ιType u_2) [inst : ] [inst : ] :
Pow (A 0)
Equations
• = { pow := fun x n => (_ : n 0 = 0) }
@[simp]
theorem GradedMonoid.mk_zero_pow {ι : Type u_1} {A : ιType u_2} [inst : ] [inst : ] (a : A 0) (n : ) :
GradedMonoid.mk 0 (a ^ n) = ^ n
instance GradedMonoid.GradeZero.monoid {ι : Type u_1} (A : ιType u_2) [inst : ] [inst : ] :
Monoid (A 0)

The Monoid structure derived from GMonoid A.

Equations
• One or more equations did not get rendered due to their size.
instance GradedMonoid.GradeZero.commMonoid {ι : Type u_1} (A : ιType u_2) [inst : ] [inst : ] :

The CommMonoid structure derived from GCommMonoid A.

Equations
• One or more equations did not get rendered due to their size.
def GradedMonoid.mkZeroMonoidHom {ι : Type u_1} (A : ιType u_2) [inst : ] [inst : ] :
A 0 →*

GradedMonoid.mk 0 is a MonoidHom, using the GradedMonoid.GradeZero.monoid structure.

Equations
• One or more equations did not get rendered due to their size.
instance GradedMonoid.GradeZero.mulAction {ι : Type u_1} (A : ιType u_2) [inst : ] [inst : ] {i : ι} :
MulAction (A 0) (A i)

Each grade A i derives a A 0-action structure from GMonoid A.

Equations
• One or more equations did not get rendered due to their size.

### Dependent products of graded elements #

def List.dProdIndex {ι : Type u_1} {α : Type u_2} [inst : ] (l : List α) (fι : αι) :
ι

The index used by List.dProd. Propositionally this is equal to (l.map fι).Sum, but definitionally it needs to have a different form to avoid introducing Eq.recs in List.dProd.

Equations
@[simp]
theorem List.dProdIndex_nil {ι : Type u_1} {α : Type u_2} [inst : ] (fι : αι) :
@[simp]
theorem List.dProdIndex_cons {ι : Type u_2} {α : Type u_1} [inst : ] (a : α) (l : List α) (fι : αι) :
List.dProdIndex (a :: l) = a +
theorem List.dProdIndex_eq_map_sum {ι : Type u_2} {α : Type u_1} [inst : ] (l : List α) (fι : αι) :
def List.dProd {ι : Type u_1} {α : Type u_2} {A : ιType u_3} [inst : ] [inst : ] (l : List α) (fι : αι) (fA : (a : α) → A ( a)) :
A ()

A dependent product for graded monoids represented by the indexed family of types A i. This is a dependent version of (l.map fA).prod.

For a list l : list α, this computes the product of fA a over a, where each fA is of type A (fι a).

Equations
@[simp]
theorem List.dProd_nil {ι : Type u_2} {α : Type u_3} {A : ιType u_1} [inst : ] [inst : ] (fι : αι) (fA : (a : α) → A ( a)) :
@[simp]
theorem List.dProd_cons {ι : Type u_3} {α : Type u_1} {A : ιType u_2} [inst : ] [inst : ] (fι : αι) (fA : (a : α) → A ( a)) (a : α) (l : List α) :
List.dProd (a :: l) fA = GradedMonoid.GMul.mul (fA a) (List.dProd l fA)
theorem GradedMonoid.mk_list_dProd {ι : Type u_2} {α : Type u_1} {A : ιType u_3} [inst : ] [inst : ] (l : List α) (fι : αι) (fA : (a : α) → A ( a)) :
GradedMonoid.mk () (List.dProd l fA) = List.prod (List.map (fun a => GradedMonoid.mk ( a) (fA a)) l)
theorem GradedMonoid.list_prod_map_eq_dProd {ι : Type u_2} {α : Type u_1} {A : ιType u_3} [inst : ] [inst : ] (l : List α) (f : α) :
List.prod (List.map f l) = GradedMonoid.mk (List.dProdIndex l fun i => (f i).fst) (List.dProd l (fun i => (f i).fst) fun i => (f i).snd)

A variant of GradedMonoid.mk_list_dProd for rewriting in the other direction.

theorem GradedMonoid.list_prod_ofFn_eq_dProd {ι : Type u_1} {A : ιType u_2} [inst : ] [inst : ] {n : } (f : Fin n) :
= GradedMonoid.mk (List.dProdIndex () fun i => (f i).fst) (List.dProd () (fun i => (f i).fst) fun i => (f i).snd)

### Concrete instances #

@[simp]
theorem One.gOne_one (ι : Type u_1) {R : Type u_2} [inst : Zero ι] [inst : One R] :
instance One.gOne (ι : Type u_1) {R : Type u_2} [inst : Zero ι] [inst : One R] :
Equations
• = { one := 1 }
@[simp]
theorem Mul.gMul_mul (ι : Type u_1) {R : Type u_2} [inst : Add ι] [inst : Mul R] :
∀ {i j : ι} (x y : R), = x * y
instance Mul.gMul (ι : Type u_1) {R : Type u_2} [inst : Add ι] [inst : Mul R] :
Equations
• = { mul := fun {i j} x y => x * y }
@[simp]
theorem Monoid.gMonoid_gnpow (ι : Type u_1) {R : Type u_2} [inst : ] [inst : ] (n : ) :
∀ (x : ι) (a : R), = a ^ n
instance Monoid.gMonoid (ι : Type u_1) {R : Type u_2} [inst : ] [inst : ] :

If all grades are the same type and themselves form a monoid, then there is a trivial grading structure.

Equations
• One or more equations did not get rendered due to their size.
instance CommMonoid.gCommMonoid (ι : Type u_1) {R : Type u_2} [inst : ] [inst : ] :

If all grades are the same type and themselves form a commutative monoid, then there is a trivial grading structure.

Equations
@[simp]
theorem List.dProd_monoid (ι : Type u_2) {R : Type u_3} {α : Type u_1} [inst : ] [inst : ] (l : List α) (fι : αι) (fA : αR) :
List.dProd l fA = List.prod (List.map fA l)

When all the indexed types are the same, the dependent product is just the regular product.

### Shorthands for creating instance of the above typeclasses for collections of subobjects #

class SetLike.GradedOne {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : One R] [inst : Zero ι] (A : ιS) :

one_mem : 1 A 0

A version of GradedMonoid.GOne for internally graded objects.

Instances
theorem SetLike.one_mem_graded {ι : Type u_3} {R : Type u_2} {S : Type u_1} [inst : SetLike S R] [inst : One R] [inst : Zero ι] (A : ιS) [inst : ] :
1 A 0
instance SetLike.gOne {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : One R] [inst : Zero ι] (A : ιS) [inst : ] :
GradedMonoid.GOne fun i => { x // x A i }
Equations
• = { one := { val := 1, property := (_ : 1 A 0) } }
@[simp]
theorem SetLike.coe_gOne {ι : Type u_3} {R : Type u_2} {S : Type u_1} [inst : SetLike S R] [inst : One R] [inst : Zero ι] (A : ιS) [inst : ] :
class SetLike.GradedMul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : Mul R] [inst : Add ι] (A : ιS) :
• Multiplication is homogeneous

mul_mem : ∀ ⦃i j : ι⦄ {gi gj : R}, gi A igj A jgi * gj A (i + j)

A version of GradedMonoid.ghas_one for internally graded objects.

Instances
theorem SetLike.mul_mem_graded {ι : Type u_3} {R : Type u_2} {S : Type u_1} [inst : SetLike S R] [inst : Mul R] [inst : Add ι] {A : ιS} [inst : ] ⦃i : ι ⦃j : ι {gi : R} {gj : R} (hi : gi A i) (hj : gj A j) :
gi * gj A (i + j)
instance SetLike.gMul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : Mul R] [inst : Add ι] (A : ιS) [inst : ] :
GradedMonoid.GMul fun i => { x // x A i }
Equations
• = { mul := fun {i j} a b => { val := a * b, property := (_ : a * b A (i + j)) } }
@[simp]
theorem SetLike.coe_gMul {ι : Type u_3} {R : Type u_2} {S : Type u_1} [inst : SetLike S R] [inst : Mul R] [inst : Add ι] (A : ιS) [inst : ] {i : ι} {j : ι} (x : { x // x A i }) (y : { x // x A j }) :
↑() = x * y
class SetLike.GradedMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : ] [inst : ] (A : ιS) extends , :

A version of GradedMonoid.GMonoid for internally graded objects.

Instances
theorem SetLike.pow_mem_graded {ι : Type u_3} {R : Type u_1} {S : Type u_2} [inst : SetLike S R] [inst : ] [inst : ] {A : ιS} [inst : ] (n : ) {r : R} {i : ι} (h : r A i) :
r ^ n A (n i)
theorem SetLike.list_prod_map_mem_graded {ι : Type u_4} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : ] [inst : ] {A : ιS} [inst : ] {ι' : Type u_1} (l : List ι') (i : ι'ι) (r : ι'R) (h : ∀ (j : ι'), j lr j A (i j)) :
theorem SetLike.list_prod_ofFn_mem_graded {ι : Type u_3} {R : Type u_1} {S : Type u_2} [inst : SetLike S R] [inst : ] [inst : ] {A : ιS} [inst : ] {n : } (i : Fin nι) (r : Fin nR) (h : ∀ (j : Fin n), r j A (i j)) :
A ()
instance SetLike.gMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : ] [inst : ] (A : ιS) [inst : ] :
GradedMonoid.GMonoid fun i => { x // x A i }

Build a GMonoid instance for a collection of subobjects.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem SetLike.coe_gnpow {ι : Type u_3} {R : Type u_2} {S : Type u_1} [inst : SetLike S R] [inst : ] [inst : ] (A : ιS) [inst : ] {i : ι} (x : { x // x A i }) (n : ) :
↑() = x ^ n
instance SetLike.gCommMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : ] [inst : ] (A : ιS) [inst : ] :
GradedMonoid.GCommMonoid fun i => { x // x A i }

Build a GCommMonoid instance for a collection of subobjects.

Equations
@[simp]
theorem SetLike.coe_list_dProd {ι : Type u_1} {R : Type u_2} {α : Type u_4} {S : Type u_3} [inst : SetLike S R] [inst : ] [inst : ] (A : ιS) [inst : ] (fι : αι) (fA : (a : α) → { x // x A ( a) }) (l : List α) :
↑(List.dProd l fA) = List.prod (List.map (fun a => ↑(fA a)) l)

Coercing a dependent product of subtypes is the same as taking the regular product of the coercions.

theorem SetLike.list_dProd_eq {ι : Type u_1} {R : Type u_2} {α : Type u_4} {S : Type u_3} [inst : SetLike S R] [inst : ] [inst : ] (A : ιS) [inst : ] (fι : αι) (fA : (a : α) → { x // x A ( a) }) (l : List α) :
List.dProd l fA = { val := List.prod (List.map (fun a => ↑(fA a)) l), property := (_ : List.prod (List.map (fun a => ↑(fA a)) l) A ()) }

A version of List.coe_dProd_set_like with Subtype.mk.

def SetLike.Homogeneous {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] (A : ιS) (a : R) :

An element a : R is said to be homogeneous if there is some i : ι such that a ∈ A i∈ A i.

Equations
@[simp]
theorem SetLike.homogeneous_coe {ι : Type u_3} {R : Type u_1} {S : Type u_2} [inst : SetLike S R] {A : ιS} {i : ι} (x : { x // x A i }) :
theorem SetLike.homogeneous_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : Zero ι] [inst : One R] (A : ιS) [inst : ] :
theorem SetLike.homogeneous_mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : Add ι] [inst : Mul R] {A : ιS} [inst : ] {a : R} {b : R} :
SetLike.Homogeneous A (a * b)
def SetLike.homogeneousSubmonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : ] [inst : ] (A : ιS) [inst : ] :

When A is a SetLike.GradedMonoid A, then the homogeneous elements forms a submonoid.

Equations
• One or more equations did not get rendered due to their size.