Documentation

Mathlib.Algebra.GradedMonoid

Additively-graded multiplicative structures #

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:

With the SigmaGraded locale open, these respectively imbue:

the base type A 0 with:

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

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

Dependent graded products #

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.

Internally graded monoids #

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:

which respectively provide the API lemmas

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:

tags #

graded monoid

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 : Inhabited ι] [inst : Inhabited (A default)] :
Equations
  • GradedMonoid.instInhabitedGradedMonoid = { default := default }
def GradedMonoid.mk {ι : Type u_1} {A : ιType u_2} (i : ι) :
A iGradedMonoid A

Construct an element of a graded monoid.

Equations
  • GradedMonoid.mk = Sigma.mk

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 : GradedMonoid.GOne A] :

    GOne implies One (GradedMonoid A)

    Equations
    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 : GradedMonoid.GMul A] :

      GMul implies Mul (GradedMonoid A).

      Equations
      theorem GradedMonoid.mk_mul_mk {ι : Type u_1} (A : ιType u_2) [inst : Add ι] [inst : GradedMonoid.GMul A] {i : ι} {j : ι} (a : A i) (b : A j) :
      def GradedMonoid.GMonoid.gnpowRec {ι : Type u_1} {A : ιType u_2} [inst : AddMonoid ι] [inst : GradedMonoid.GMul A] [inst : GradedMonoid.GOne A] (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 : AddMonoid ι] [inst : GradedMonoid.GMul A] [inst : GradedMonoid.GOne A] (a : GradedMonoid A) :
      @[simp]
      theorem GradedMonoid.GMonoid.gnpowRec_succ {ι : Type u_1} {A : ιType u_2} [inst : AddMonoid ι] [inst : GradedMonoid.GMul A] [inst : GradedMonoid.GOne A] (n : ) (a : GradedMonoid A) :
      GradedMonoid.mk (Nat.succ n a.fst) (GradedMonoid.GMonoid.gnpowRec (Nat.succ n) a.snd) = a * { fst := n a.fst, snd := GradedMonoid.GMonoid.gnpowRec n a.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 : AddMonoid ι] extends GradedMonoid.GMul , GradedMonoid.GOne :
      Type (maxu_1u_2)

      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 : AddMonoid ι] [inst : GradedMonoid.GMonoid A] :

        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 : AddMonoid ι] [inst : GradedMonoid.GMonoid A] {i : ι} (a : A i) (n : ) :
        class GradedMonoid.GCommMonoid {ι : Type u_1} (A : ιType u_2) [inst : AddCommMonoid ι] extends GradedMonoid.GMonoid :
        Type (maxu_1u_2)
        • Multiplication is commutative

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

        A graded version of CommMonoid.

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

          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 : GradedMonoid.GOne A] :
          One (A 0)

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

          Equations
          instance GradedMonoid.GradeZero.smul {ι : Type u_1} (A : ιType u_2) [inst : AddZeroClass ι] [inst : GradedMonoid.GMul A] (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
          instance GradedMonoid.GradeZero.mul {ι : Type u_1} (A : ιType u_2) [inst : AddZeroClass ι] [inst : GradedMonoid.GMul A] :
          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
          @[simp]
          theorem GradedMonoid.mk_zero_smul {ι : Type u_1} {A : ιType u_2} [inst : AddZeroClass ι] [inst : GradedMonoid.GMul A] {i : ι} (a : A 0) (b : A i) :
          @[simp]
          theorem GradedMonoid.GradeZero.smul_eq_mul {ι : Type u_1} {A : ιType u_2} [inst : AddZeroClass ι] [inst : GradedMonoid.GMul A] (a : A 0) (b : A 0) :
          a b = a * b
          instance GradedMonoid.instPowOfNatToOfNat0ToZeroNat {ι : Type u_1} (A : ιType u_2) [inst : AddMonoid ι] [inst : GradedMonoid.GMonoid A] :
          Pow (A 0)
          Equations
          @[simp]
          theorem GradedMonoid.mk_zero_pow {ι : Type u_1} {A : ιType u_2} [inst : AddMonoid ι] [inst : GradedMonoid.GMonoid A] (a : A 0) (n : ) :
          instance GradedMonoid.GradeZero.monoid {ι : Type u_1} (A : ιType u_2) [inst : AddMonoid ι] [inst : GradedMonoid.GMonoid A] :
          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 : AddCommMonoid ι] [inst : GradedMonoid.GCommMonoid A] :

          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 : AddMonoid ι] [inst : GradedMonoid.GMonoid A] :

          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 : AddMonoid ι] [inst : GradedMonoid.GMonoid A] {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 : AddMonoid ι] (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 : AddMonoid ι] (fι : αι) :
          @[simp]
          theorem List.dProdIndex_cons {ι : Type u_2} {α : Type u_1} [inst : AddMonoid ι] (a : α) (l : List α) (fι : αι) :
          List.dProdIndex (a :: l) = a + List.dProdIndex l
          theorem List.dProdIndex_eq_map_sum {ι : Type u_2} {α : Type u_1} [inst : AddMonoid ι] (l : List α) (fι : αι) :
          def List.dProd {ι : Type u_1} {α : Type u_2} {A : ιType u_3} [inst : AddMonoid ι] [inst : GradedMonoid.GMonoid A] (l : List α) (fι : αι) (fA : (a : α) → A ( a)) :
          A (List.dProdIndex l )

          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 : AddMonoid ι] [inst : GradedMonoid.GMonoid A] (fι : αι) (fA : (a : α) → A ( a)) :
          List.dProd [] fA = GradedMonoid.GOne.one
          @[simp]
          theorem List.dProd_cons {ι : Type u_3} {α : Type u_1} {A : ιType u_2} [inst : AddMonoid ι] [inst : GradedMonoid.GMonoid A] (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 : AddMonoid ι] [inst : GradedMonoid.GMonoid A] (l : List α) (fι : αι) (fA : (a : α) → A ( a)) :
          GradedMonoid.mk (List.dProdIndex l ) (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 : AddMonoid ι] [inst : GradedMonoid.GMonoid A] (l : List α) (f : αGradedMonoid A) :
          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 : AddMonoid ι] [inst : GradedMonoid.GMonoid A] {n : } (f : Fin nGradedMonoid A) :
          List.prod (List.ofFn f) = GradedMonoid.mk (List.dProdIndex (List.finRange n) fun i => (f i).fst) (List.dProd (List.finRange n) (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] :
          GradedMonoid.GOne.one = 1
          instance One.gOne (ι : Type u_1) {R : Type u_2} [inst : Zero ι] [inst : One R] :
          Equations
          @[simp]
          theorem Mul.gMul_mul (ι : Type u_1) {R : Type u_2} [inst : Add ι] [inst : Mul R] :
          ∀ {i j : ι} (x y : R), GradedMonoid.GMul.mul x y = x * y
          instance Mul.gMul (ι : Type u_1) {R : Type u_2} [inst : Add ι] [inst : Mul R] :
          Equations
          @[simp]
          theorem Monoid.gMonoid_gnpow (ι : Type u_1) {R : Type u_2} [inst : AddMonoid ι] [inst : Monoid R] (n : ) :
          ∀ (x : ι) (a : R), GradedMonoid.GMonoid.gnpow n a = a ^ n
          instance Monoid.gMonoid (ι : Type u_1) {R : Type u_2} [inst : AddMonoid ι] [inst : Monoid R] :

          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 : AddCommMonoid ι] [inst : CommMonoid R] :

          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 : AddMonoid ι] [inst : Monoid R] (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 has grade zero

            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 : SetLike.GradedOne A] :
            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 : SetLike.GradedOne A] :
            GradedMonoid.GOne fun i => { x // x A i }
            Equations
            @[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 : SetLike.GradedOne A] :
            GradedMonoid.GOne.one = 1
            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 : SetLike.GradedMul A] ⦃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 : SetLike.GradedMul A] :
              GradedMonoid.GMul fun i => { x // x A i }
              Equations
              • SetLike.gMul A = { 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 : SetLike.GradedMul A] {i : ι} {j : ι} (x : { x // x A i }) (y : { x // x A j }) :
              ↑(GradedMonoid.GMul.mul x y) = x * y
              class SetLike.GradedMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : Monoid R] [inst : AddMonoid ι] (A : ιS) extends SetLike.GradedOne , SetLike.GradedMul :

                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 : Monoid R] [inst : AddMonoid ι] {A : ιS} [inst : SetLike.GradedMonoid A] (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 : Monoid R] [inst : AddMonoid ι] {A : ιS} [inst : SetLike.GradedMonoid A] {ι' : 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 : Monoid R] [inst : AddMonoid ι] {A : ιS} [inst : SetLike.GradedMonoid A] {n : } (i : Fin nι) (r : Fin nR) (h : ∀ (j : Fin n), r j A (i j)) :
                  instance SetLike.gMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : Monoid R] [inst : AddMonoid ι] (A : ιS) [inst : SetLike.GradedMonoid A] :
                  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 : Monoid R] [inst : AddMonoid ι] (A : ιS) [inst : SetLike.GradedMonoid A] {i : ι} (x : { x // x A i }) (n : ) :
                  instance SetLike.gCommMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : CommMonoid R] [inst : AddCommMonoid ι] (A : ιS) [inst : SetLike.GradedMonoid A] :
                  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 : Monoid R] [inst : AddMonoid ι] (A : ιS) [inst : SetLike.GradedMonoid A] (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 : Monoid R] [inst : AddMonoid ι] (A : ιS) [inst : SetLike.GradedMonoid A] (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 (List.dProdIndex l )) }

                  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 : SetLike.GradedOne A] :
                  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 : SetLike.GradedMul A] {a : R} {b : R} :
                  def SetLike.homogeneousSubmonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst : AddMonoid ι] [inst : Monoid R] (A : ιS) [inst : SetLike.GradedMonoid A] :

                  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.