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); that is to say, A forms an additively-graded monoid. The typeclasses are:

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 unnecessary 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 (max u_1 u_2)

A type alias of sigma types for graded monoids.

Equations
Instances For
    instance GradedMonoid.instInhabitedOfDefault {ι : Type u_1} {A : ιType u_2} [Inhabited ι] [Inhabited (A default)] :
    Equations
    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
    Instances For

      Actions #

      instance GradedMonoid.instSMul {ι : Type u_1} {α : Type u_3} {A : ιType u_2} [(i : ι) → SMul α (A i)] :

      If R acts on each A i, then it acts on GradedMonoid A via the .2 projection.

      Equations
      @[simp]
      theorem GradedMonoid.fst_smul {ι : Type u_1} {α : Type u_3} {A : ιType u_2} [(i : ι) → SMul α (A i)] (a : α) (x : GradedMonoid A) :
      (a x).fst = x.fst
      @[simp]
      theorem GradedMonoid.snd_smul {ι : Type u_1} {α : Type u_3} {A : ιType u_2} [(i : ι) → SMul α (A i)] (a : α) (x : GradedMonoid A) :
      (a x).snd = a x.snd
      theorem GradedMonoid.smul_mk {ι : Type u_1} {α : Type u_3} {A : ιType u_2} [(i : ι) → SMul α (A i)] {i : ι} (c : α) (a : A i) :
      instance GradedMonoid.instSMulCommClass {ι : Type u_1} {α : Type u_3} {β : Type u_4} {A : ιType u_2} [(i : ι) → SMul α (A i)] [(i : ι) → SMul β (A i)] [∀ (i : ι), SMulCommClass α β (A i)] :
      Equations
      • =
      instance GradedMonoid.instIsScalarTower {ι : Type u_1} {α : Type u_3} {β : Type u_4} {A : ιType u_2} [SMul α β] [(i : ι) → SMul α (A i)] [(i : ι) → SMul β (A i)] [∀ (i : ι), IsScalarTower α β (A i)] :
      Equations
      • =
      instance GradedMonoid.instMulAction {ι : Type u_1} {α : Type u_3} {A : ιType u_2} [Monoid α] [(i : ι) → MulAction α (A i)] :
      Equations

      Typeclasses #

      class GradedMonoid.GOne {ι : Type u_1} (A : ιType u_2) [Zero ι] :
      Type u_2

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

      • one : A 0

        The term one of grade 0

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

        GOne implies One (GradedMonoid A)

        Equations
        @[simp]
        theorem GradedMonoid.fst_one {ι : Type u_1} (A : ιType u_2) [Zero ι] [GradedMonoid.GOne A] :
        @[simp]
        theorem GradedMonoid.snd_one {ι : Type u_1} (A : ιType u_2) [Zero ι] [GradedMonoid.GOne A] :
        Sigma.snd 1 = GradedMonoid.GOne.one
        class GradedMonoid.GMul {ι : Type u_1} (A : ιType u_2) [Add ι] :
        Type (max u_1 u_2)

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

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

          The homogeneous multiplication map mul

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

          GMul implies Mul (GradedMonoid A).

          Equations
          @[simp]
          theorem GradedMonoid.fst_mul {ι : Type u_1} (A : ιType u_2) [Add ι] [GradedMonoid.GMul A] (x : GradedMonoid A) (y : GradedMonoid A) :
          (x * y).fst = x.fst + y.fst
          @[simp]
          theorem GradedMonoid.snd_mul {ι : Type u_1} (A : ιType u_2) [Add ι] [GradedMonoid.GMul A] (x : GradedMonoid A) (y : GradedMonoid A) :
          (x * y).snd = GradedMonoid.GMul.mul x.snd y.snd
          theorem GradedMonoid.mk_mul_mk {ι : Type u_1} (A : ιType u_2) [Add ι] [GradedMonoid.GMul A] {i : ι} {j : ι} (a : A i) (b : A j) :
          def GradedMonoid.GMonoid.gnpowRec {ι : Type u_1} {A : ιType u_2} [AddMonoid ι] [GradedMonoid.GMul A] [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
          Instances For
            @[simp]
            theorem GradedMonoid.GMonoid.gnpowRec_succ {ι : Type u_1} {A : ιType u_2} [AddMonoid ι] [GradedMonoid.GMul A] [GradedMonoid.GOne A] (n : ) (a : GradedMonoid A) :
            GradedMonoid.mk (n.succ a.fst) (GradedMonoid.GMonoid.gnpowRec n.succ a.snd) = n a.fst, GradedMonoid.GMonoid.gnpowRec n a.snd * a

            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.
            Instances For

              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.
              Instances For
                class GradedMonoid.GMonoid {ι : Type u_1} (A : ιType u_2) [AddMonoid ι] extends GradedMonoid.GMul , GradedMonoid.GOne :
                Type (max u_1 u_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
                  theorem GradedMonoid.GMonoid.one_mul {ι : Type u_1} {A : ιType u_2} [AddMonoid ι] [self : GradedMonoid.GMonoid A] (a : GradedMonoid A) :
                  1 * a = a

                  Multiplication by one on the left is the identity

                  theorem GradedMonoid.GMonoid.mul_one {ι : Type u_1} {A : ιType u_2} [AddMonoid ι] [self : GradedMonoid.GMonoid A] (a : GradedMonoid A) :
                  a * 1 = a

                  Multiplication by one on the right is the identity

                  theorem GradedMonoid.GMonoid.mul_assoc {ι : Type u_1} {A : ιType u_2} [AddMonoid ι] [self : GradedMonoid.GMonoid A] (a : GradedMonoid A) (b : GradedMonoid A) (c : GradedMonoid A) :
                  a * b * c = a * (b * c)

                  Multiplication is associative

                  theorem GradedMonoid.GMonoid.gnpow_zero' {ι : Type u_1} {A : ιType u_2} [AddMonoid ι] [self : GradedMonoid.GMonoid A] (a : GradedMonoid A) :

                  The zeroth power will yield 1

                  theorem GradedMonoid.GMonoid.gnpow_succ' {ι : Type u_1} {A : ιType u_2} [AddMonoid ι] [self : GradedMonoid.GMonoid A] (n : ) (a : GradedMonoid A) :
                  GradedMonoid.mk (n.succ a.fst) (GradedMonoid.GMonoid.gnpow n.succ a.snd) = n a.fst, GradedMonoid.GMonoid.gnpow n a.snd * a

                  Successor powers behave as expected

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

                  GMonoid implies a Monoid (GradedMonoid A).

                  Equations
                  @[simp]
                  theorem GradedMonoid.fst_pow {ι : Type u_1} (A : ιType u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] (x : GradedMonoid A) (n : ) :
                  (x ^ n).fst = n x.fst
                  @[simp]
                  theorem GradedMonoid.snd_pow {ι : Type u_1} (A : ιType u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] (x : GradedMonoid A) (n : ) :
                  (x ^ n).snd = GradedMonoid.GMonoid.gnpow n x.snd
                  theorem GradedMonoid.mk_pow {ι : Type u_1} (A : ιType u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] {i : ι} (a : A i) (n : ) :
                  class GradedMonoid.GCommMonoid {ι : Type u_1} (A : ιType u_2) [AddCommMonoid ι] extends GradedMonoid.GMonoid :
                  Type (max u_1 u_2)

                  A graded version of CommMonoid.

                  Instances
                    theorem GradedMonoid.GCommMonoid.mul_comm {ι : Type u_1} {A : ιType u_2} [AddCommMonoid ι] [self : GradedMonoid.GCommMonoid A] (a : GradedMonoid A) (b : GradedMonoid A) :
                    a * b = b * a

                    Multiplication is commutative

                    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) [Zero ι] [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) [AddZeroClass ι] [GradedMonoid.GMul A] (i : ι) :
                    SMul (A 0) (A i)

                    (•) : A 0 → 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) [AddZeroClass ι] [GradedMonoid.GMul A] :
                    Mul (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} [AddZeroClass ι] [GradedMonoid.GMul A] {i : ι} (a : A 0) (b : A i) :
                    @[simp]
                    theorem GradedMonoid.GradeZero.smul_eq_mul {ι : Type u_1} {A : ιType u_2} [AddZeroClass ι] [GradedMonoid.GMul A] (a : A 0) (b : A 0) :
                    a b = a * b
                    instance GradedMonoid.instNatPowOfNat {ι : Type u_1} (A : ιType u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] :
                    NatPow (A 0)
                    Equations
                    @[simp]
                    theorem GradedMonoid.mk_zero_pow {ι : Type u_1} {A : ιType u_2} [AddMonoid ι] [GradedMonoid.GMonoid A] (a : A 0) (n : ) :
                    instance GradedMonoid.GradeZero.monoid {ι : Type u_1} (A : ιType u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] :
                    Monoid (A 0)

                    The Monoid structure derived from GMonoid A.

                    Equations
                    def GradedMonoid.mkZeroMonoidHom {ι : Type u_1} (A : ιType u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] :

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

                    Equations
                    Instances For
                      instance GradedMonoid.GradeZero.mulAction {ι : Type u_1} (A : ιType u_2) [AddMonoid ι] [GradedMonoid.GMonoid A] {i : ι} :
                      MulAction (A 0) (A i)

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

                      Equations

                      Dependent products of graded elements #

                      def List.dProdIndex {ι : Type u_1} {α : Type u_2} [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
                      • l.dProdIndex = List.foldr (fun (i : α) (b : ι) => i + b) 0 l
                      Instances For
                        @[simp]
                        theorem List.dProdIndex_nil {ι : Type u_1} {α : Type u_2} [AddMonoid ι] (fι : αι) :
                        [].dProdIndex = 0
                        @[simp]
                        theorem List.dProdIndex_cons {ι : Type u_1} {α : Type u_2} [AddMonoid ι] (a : α) (l : List α) (fι : αι) :
                        (a :: l).dProdIndex = a + l.dProdIndex
                        theorem List.dProdIndex_eq_map_sum {ι : Type u_1} {α : Type u_2} [AddMonoid ι] (l : List α) (fι : αι) :
                        l.dProdIndex = (List.map l).sum
                        def List.dProd {ι : Type u_1} {α : Type u_2} {A : ιType u_3} [AddMonoid ι] [GradedMonoid.GMonoid A] (l : List α) (fι : αι) (fA : (a : α) → A ( a)) :
                        A (l.dProdIndex )

                        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
                        • l.dProd fA = l.foldrRecOn (fun (i : α) (b : ι) => i + b) 0 GradedMonoid.GOne.one fun (x : ι) (x_1 : A x) (a : α) (x_2 : a l) => GradedMonoid.GMul.mul (fA a) x_1
                        Instances For
                          @[simp]
                          theorem List.dProd_nil {ι : Type u_1} {α : Type u_2} {A : ιType u_3} [AddMonoid ι] [GradedMonoid.GMonoid A] (fι : αι) (fA : (a : α) → A ( a)) :
                          [].dProd fA = GradedMonoid.GOne.one
                          @[simp]
                          theorem List.dProd_cons {ι : Type u_1} {α : Type u_2} {A : ιType u_3} [AddMonoid ι] [GradedMonoid.GMonoid A] (fι : αι) (fA : (a : α) → A ( a)) (a : α) (l : List α) :
                          (a :: l).dProd fA = GradedMonoid.GMul.mul (fA a) (l.dProd fA)
                          theorem GradedMonoid.mk_list_dProd {ι : Type u_1} {α : Type u_2} {A : ιType u_3} [AddMonoid ι] [GradedMonoid.GMonoid A] (l : List α) (fι : αι) (fA : (a : α) → A ( a)) :
                          GradedMonoid.mk (l.dProdIndex ) (l.dProd fA) = (List.map (fun (a : α) => GradedMonoid.mk ( a) (fA a)) l).prod
                          theorem GradedMonoid.list_prod_map_eq_dProd {ι : Type u_1} {α : Type u_2} {A : ιType u_3} [AddMonoid ι] [GradedMonoid.GMonoid A] (l : List α) (f : αGradedMonoid A) :
                          (List.map f l).prod = GradedMonoid.mk (l.dProdIndex fun (i : α) => (f i).fst) (l.dProd (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_3} [AddMonoid ι] [GradedMonoid.GMonoid A] {n : } (f : Fin nGradedMonoid A) :
                          (List.ofFn f).prod = GradedMonoid.mk ((List.finRange n).dProdIndex fun (i : Fin n) => (f i).fst) ((List.finRange n).dProd (fun (i : Fin n) => (f i).fst) fun (i : Fin n) => (f i).snd)

                          Concrete instances #

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

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

                          Equations
                          instance CommMonoid.gCommMonoid (ι : Type u_1) {R : Type u_2} [AddCommMonoid ι] [CommMonoid R] :
                          GradedMonoid.GCommMonoid fun (x : ι) => 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_1) {R : Type u_2} {α : Type u_3} [AddMonoid ι] [Monoid R] (l : List α) (fι : αι) (fA : αR) :
                          l.dProd fA = (List.map fA l).prod

                          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} [SetLike S R] [One R] [Zero ι] (A : ιS) :

                          A version of GradedMonoid.GOne for internally graded objects.

                          • one_mem : 1 A 0

                            One has grade zero

                          Instances
                            theorem SetLike.GradedOne.one_mem {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [One R] [Zero ι] {A : ιS} [self : SetLike.GradedOne A] :
                            1 A 0

                            One has grade zero

                            theorem SetLike.one_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [One R] [Zero ι] (A : ιS) [SetLike.GradedOne A] :
                            1 A 0
                            instance SetLike.gOne {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [One R] [Zero ι] (A : ιS) [SetLike.GradedOne A] :
                            GradedMonoid.GOne fun (i : ι) => (A i)
                            Equations
                            @[simp]
                            theorem SetLike.coe_gOne {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [One R] [Zero ι] (A : ιS) [SetLike.GradedOne A] :
                            GradedMonoid.GOne.one = 1
                            class SetLike.GradedMul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Mul R] [Add ι] (A : ιS) :

                            A version of GradedMonoid.ghas_one for internally graded objects.

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

                              Multiplication is homogeneous

                            Instances
                              theorem SetLike.GradedMul.mul_mem {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Mul R] [Add ι] {A : ιS} [self : SetLike.GradedMul A] ⦃i : ι ⦃j : ι {gi : R} {gj : R} :
                              gi A igj A jgi * gj A (i + j)

                              Multiplication is homogeneous

                              theorem SetLike.mul_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Mul R] [Add ι] {A : ιS} [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} [SetLike S R] [Mul R] [Add ι] (A : ιS) [SetLike.GradedMul A] :
                              GradedMonoid.GMul fun (i : ι) => (A i)
                              Equations
                              • SetLike.gMul A = { mul := fun {i j : ι} (a : (A i)) (b : (A j)) => a * b, }
                              @[simp]
                              theorem SetLike.coe_gMul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Mul R] [Add ι] (A : ιS) [SetLike.GradedMul A] {i : ι} {j : ι} (x : (A i)) (y : (A j)) :
                              (GradedMonoid.GMul.mul x y) = x * y
                              class SetLike.GradedMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [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_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] {A : ιS} [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_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] {A : ιS} [SetLike.GradedMonoid A] {ι' : Type u_4} (l : List ι') (i : ι'ι) (r : ι'R) (h : jl, r j A (i j)) :
                                  (List.map r l).prod A (List.map i l).sum
                                  theorem SetLike.list_prod_ofFn_mem_graded {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] {A : ιS} [SetLike.GradedMonoid A] {n : } (i : Fin nι) (r : Fin nR) (h : ∀ (j : Fin n), r j A (i j)) :
                                  (List.ofFn r).prod A (List.ofFn i).sum
                                  instance SetLike.gMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ιS) [SetLike.GradedMonoid A] :
                                  GradedMonoid.GMonoid fun (i : ι) => (A i)

                                  Build a GMonoid instance for a collection of subobjects.

                                  Equations
                                  @[simp]
                                  theorem SetLike.coe_gnpow {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ιS) [SetLike.GradedMonoid A] {i : ι} (x : (A i)) (n : ) :
                                  instance SetLike.gCommMonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [CommMonoid R] [AddCommMonoid ι] (A : ιS) [SetLike.GradedMonoid A] :
                                  GradedMonoid.GCommMonoid fun (i : ι) => (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_3} {S : Type u_4} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ιS) [SetLike.GradedMonoid A] (fι : αι) (fA : (a : α) → (A ( a))) (l : List α) :
                                  (l.dProd fA) = (List.map (fun (a : α) => (fA a)) l).prod

                                  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_3} {S : Type u_4} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ιS) [SetLike.GradedMonoid A] (fι : αι) (fA : (a : α) → (A ( a))) (l : List α) :
                                  l.dProd fA = (List.map (fun (a : α) => (fA a)) l).prod,

                                  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} [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.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem SetLike.homogeneous_coe {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] {A : ιS} {i : ι} (x : (A i)) :
                                    theorem SetLike.homogeneous_one {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Zero ι] [One R] (A : ιS) [SetLike.GradedOne A] :
                                    theorem SetLike.homogeneous_mul {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [Add ι] [Mul R] {A : ιS} [SetLike.GradedMul A] {a : R} {b : R} :
                                    def SetLike.homogeneousSubmonoid {ι : Type u_1} {R : Type u_2} {S : Type u_3} [SetLike S R] [AddMonoid ι] [Monoid R] (A : ιS) [SetLike.GradedMonoid A] :

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

                                    Equations
                                    Instances For