Documentation

Mathlib.Algebra.GradedMulAction

Additively-graded multiplicative action structures #

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

With the SigmaGraded locale open, these respectively imbue:

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

Internally graded multiplicative actions #

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 provides the API lemma

Note that there is no need for SetLike.graded_mul_action or similar, as all the information it would contain is already supplied by GradedSMul when the objects within A and M have a MulAction instance.

Tags #

graded action

Typeclasses #

class GradedMonoid.GSMul {ιA : Type u_1} {ιM : Type u_3} (A : ιAType u_4) (M : ιMType u_5) [VAdd ιA ιM] :
Type (max (max (max u_1 u_3) u_4) u_5)

A graded version of SMul. Scalar multiplication combines grades additively, i.e. if a ∈ A i and m ∈ M j, then a • b must be in M (i + j)

  • smul : {i : ιA} → {j : ιM} → A iM jM (i +ᵥ j)

    The homogeneous multiplication map smul

Instances
    instance GradedMonoid.GMul.toGSMul {ιA : Type u_1} (A : ιAType u_4) [Add ιA] [GradedMonoid.GMul A] :

    A graded version of Mul.toSMul

    Equations
    instance GradedMonoid.GSMul.toSMul {ιA : Type u_1} {ιM : Type u_3} (A : ιAType u_4) (M : ιMType u_5) [VAdd ιA ιM] [GradedMonoid.GSMul A M] :
    Equations
    theorem GradedMonoid.mk_smul_mk {ιA : Type u_1} {ιM : Type u_3} (A : ιAType u_4) (M : ιMType u_5) [VAdd ιA ιM] [GradedMonoid.GSMul A M] {i : ιA} {j : ιM} (a : A i) (b : M j) :
    class GradedMonoid.GMulAction {ιA : Type u_1} {ιM : Type u_3} (A : ιAType u_4) (M : ιMType u_5) [AddMonoid ιA] [VAdd ιA ιM] [GradedMonoid.GMonoid A] extends GradedMonoid.GSMul :
    Type (max (max (max u_1 u_3) u_4) u_5)

    A graded version of MulAction.

    Instances
      theorem GradedMonoid.GMulAction.one_smul {ιA : Type u_1} {ιM : Type u_3} {A : ιAType u_4} {M : ιMType u_5} [AddMonoid ιA] [VAdd ιA ιM] [GradedMonoid.GMonoid A] [self : GradedMonoid.GMulAction A M] (b : GradedMonoid M) :
      1 b = b

      One is the neutral element for

      theorem GradedMonoid.GMulAction.mul_smul {ιA : Type u_1} {ιM : Type u_3} {A : ιAType u_4} {M : ιMType u_5} [AddMonoid ιA] [VAdd ιA ιM] [GradedMonoid.GMonoid A] [self : GradedMonoid.GMulAction A M] (a : GradedMonoid A) (a' : GradedMonoid A) (b : GradedMonoid M) :
      (a * a') b = a a' b

      Associativity of and *

      instance GradedMonoid.GMulAction.toMulAction {ιA : Type u_1} {ιM : Type u_3} (A : ιAType u_4) (M : ιMType u_5) [AddMonoid ιA] [GradedMonoid.GMonoid A] [VAdd ιA ιM] [GradedMonoid.GMulAction A M] :
      Equations

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

      class SetLike.GradedSMul {ιA : Type u_1} {ιB : Type u_2} {S : Type u_5} {R : Type u_6} {N : Type u_7} {M : Type u_8} [SetLike S R] [SetLike N M] [SMul R M] [VAdd ιA ιB] (A : ιAS) (B : ιBN) :

      A version of GradedMonoid.GSMul for internally graded objects.

      • smul_mem : ∀ ⦃i : ιA⦄ ⦃j : ιB⦄ {ai : R} {bj : M}, ai A ibj B jai bj B (i +ᵥ j)

        Multiplication is homogeneous

      Instances
        theorem SetLike.GradedSMul.smul_mem {ιA : Type u_1} {ιB : Type u_2} {S : Type u_5} {R : Type u_6} {N : Type u_7} {M : Type u_8} [SetLike S R] [SetLike N M] [SMul R M] [VAdd ιA ιB] {A : ιAS} {B : ιBN} [self : SetLike.GradedSMul A B] ⦃i : ιA ⦃j : ιB {ai : R} {bj : M} :
        ai A ibj B jai bj B (i +ᵥ j)

        Multiplication is homogeneous

        instance SetLike.toGSMul {ιA : Type u_1} {ιB : Type u_2} {S : Type u_5} {R : Type u_6} {N : Type u_7} {M : Type u_8} [SetLike S R] [SetLike N M] [SMul R M] [VAdd ιA ιB] (A : ιAS) (B : ιBN) [SetLike.GradedSMul A B] :
        GradedMonoid.GSMul (fun (i : ιA) => (A i)) fun (i : ιB) => (B i)
        Equations
        • SetLike.toGSMul A B = { smul := fun {i : ιA} {j : ιB} (a : (A i)) (b : (B j)) => a b, }
        @[simp]
        theorem SetLike.coe_GSMul {ιA : Type u_1} {ιB : Type u_2} {S : Type u_5} {R : Type u_6} {N : Type u_7} {M : Type u_8} [SetLike S R] [SetLike N M] [SMul R M] [VAdd ιA ιB] (A : ιAS) (B : ιBN) [SetLike.GradedSMul A B] {i : ιA} {j : ιB} (x : (A i)) (y : (B j)) :
        (GradedMonoid.GSMul.smul x y) = x y
        instance SetLike.GradedMul.toGradedSMul {ιA : Type u_1} {R : Type u_4} [AddMonoid ιA] [Monoid R] {S : Type u_5} [SetLike S R] (A : ιAS) [SetLike.GradedMonoid A] :

        Internally graded version of Mul.toSMul.

        Equations
        • =
        theorem SetLike.Homogeneous.graded_smul {ιA : Type u_1} {ιB : Type u_2} {S : Type u_4} {R : Type u_5} {N : Type u_6} {M : Type u_7} [SetLike S R] [SetLike N M] [VAdd ιA ιB] [SMul R M] {A : ιAS} {B : ιBN} [SetLike.GradedSMul A B] {a : R} {b : M} :