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 {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [Add ι] :
Type (max (max u_1 u_2) u_3)
  • smul : {i j : ι} → A iM jM (i + j)

    The homogeneous multiplication map smul

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)

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

    A graded version of Mul.toSMul

    instance GradedMonoid.GSmul.toSMul {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [Add ι] [GradedMonoid.GSmul A M] :
    theorem GradedMonoid.mk_smul_mk {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [Add ι] [GradedMonoid.GSmul A M] {i : ι} {j : ι} (a : A i) (b : M j) :
    class GradedMonoid.GMulAction {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [AddMonoid ι] [GradedMonoid.GMonoid A] extends GradedMonoid.GSmul :
    Type (max (max u_1 u_2) u_3)

    A graded version of MulAction.

    Instances

      The graded version of Monoid.toMulAction.

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

      class SetLike.GradedSmul {ι : Type u_1} {S : Type u_3} {R : Type u_4} {N : Type u_5} {M : Type u_6} [SetLike S R] [SetLike N M] [SMul R M] [Add ι] (A : ιS) (B : ιN) :
      • smul_mem : ∀ ⦃i j : ι⦄ {ai : R} {bj : M}, ai A ibj B jai bj B (i + j)

        Multiplication is homogeneous

      A version of GradedMonoid.GSmul for internally graded objects.

      Instances
        instance SetLike.toGSmul {ι : Type u_1} {S : Type u_3} {R : Type u_4} {N : Type u_5} {M : Type u_6} [SetLike S R] [SetLike N M] [SMul R M] [Add ι] (A : ιS) (B : ιN) [SetLike.GradedSmul A B] :
        GradedMonoid.GSmul (fun i => { x // x A i }) fun i => { x // x B i }
        @[simp]
        theorem SetLike.coe_GSmul {ι : Type u_1} {S : Type u_3} {R : Type u_4} {N : Type u_5} {M : Type u_6} [SetLike S R] [SetLike N M] [SMul R M] [Add ι] (A : ιS) (B : ιN) [SetLike.GradedSmul A B] {i : ι} {j : ι} (x : { x // x A i }) (y : { x // x B j }) :
        ↑(GradedMonoid.GSmul.smul x y) = x y
        instance SetLike.GradedMul.toGradedSmul {ι : Type u_1} {R : Type u_2} [AddMonoid ι] [Monoid R] {S : Type u_3} [SetLike S R] (A : ιS) [SetLike.GradedMonoid A] :

        Internally graded version of Mul.toSMul.

        theorem SetLike.Homogeneous.graded_smul {ι : Type u_1} {S : Type u_2} {R : Type u_3} {N : Type u_4} {M : Type u_5} [SetLike S R] [SetLike N M] [Add ι] [SMul R M] {A : ιS} {B : ιN} [SetLike.GradedSmul A B] {a : R} {b : M} :