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:

• GradedMonoid.GSmul A M
• GradedMonoid.GMulAction A M

With the SigmaGraded locale open, these respectively imbue:

• SMul (GradedMonoid A) (GradedMonoid M)
• MulAction (GradedMonoid A) (GradedMonoid M)

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:

• SetLike.GradedSmul A M (which provides the obvious GradedMonoid.GSmul A instance)

which provides the API lemma

• SetLike.graded_smul_mem_graded

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 i → M j → M (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)

instance GradedMonoid.GMul.toGSmul {ι : Type u_1} (A : ι → Type u_2) [Add ι] [GradedMonoid.GMul A] : GradedMonoid.GSmul A 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] : SMul (GradedMonoid A) (GradedMonoid 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) : GradedMonoid.mk i a • GradedMonoid.mk j b = GradedMonoid.mk (i + j) (GradedMonoid.GSmul.smul a b)

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)

• smul : {i j : ι} → A i → M j → M (i + j)
• one_smul : ∀ (b : GradedMonoid M), 1 • b = b

  One is the neutral element for •

• mul_smul : ∀ (a a' : GradedMonoid A) (b : GradedMonoid M), (a * a') • b = a • a' • b

  Associativity of • and *

A graded version of MulAction.

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

The graded version of Monoid.toMulAction.

instance GradedMonoid.GMulAction.toMulAction {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [AddMonoid ι] [GradedMonoid.GMonoid A] [GradedMonoid.GMulAction A M] : MulAction (GradedMonoid A) (GradedMonoid M)

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) : Prop

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

  Multiplication is homogeneous

A version of GradedMonoid.GSmul for internally graded objects.

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] : SetLike.GradedSmul A 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} : SetLike.Homogeneous A a → SetLike.Homogeneous B b → SetLike.Homogeneous B (a • b)