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 {ιA : Type u_1} {ιM : Type u_3} (A : ιA → Type u_4) (M : ιM → Type 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 i → M j → M (i +ᵥ j)

  The homogeneous multiplication map smul

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

A graded version of Mul.toSMul

Equations

• GradedMonoid.GMul.toGSMul A = { smul := fun {i j : ιA} => GradedMonoid.GMul.mul }

instance GradedMonoid.GSMul.toSMul {ιA : Type u_1} {ιM : Type u_3} (A : ιA → Type u_4) (M : ιM → Type u_5) [VAdd ιA ιM] [GradedMonoid.GSMul A M] : SMul (GradedMonoid A) (GradedMonoid M)

Equations

• GradedMonoid.GSMul.toSMul A M = { smul := fun (x : GradedMonoid A) (y : GradedMonoid M) => ⟨x.fst +ᵥ y.fst, GradedMonoid.GSMul.smul x.snd y.snd⟩ }

theorem GradedMonoid.mk_smul_mk {ιA : Type u_1} {ιM : Type u_3} (A : ιA → Type u_4) (M : ιM → Type u_5) [VAdd ιA ιM] [GradedMonoid.GSMul A M] {i : ιA} {j : ιM} (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 {ιA : Type u_1} {ιM : Type u_3} (A : ιA → Type u_4) (M : ιM → Type 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.

• smul : {i : ιA} → {j : ιM} → 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 *

theorem GradedMonoid.GMulAction.one_smul {ιA : Type u_1} {ιM : Type u_3} {A : ιA → Type u_4} {M : ιM → Type u_5} : ∀ {inst : AddMonoid ιA} {inst_1 : VAdd ιA ιM} {inst_2 : 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 : ιA → Type u_4} {M : ιM → Type u_5} : ∀ {inst : AddMonoid ιA} {inst_1 : VAdd ιA ιM} {inst_2 : GradedMonoid.GMonoid A} [self : GradedMonoid.GMulAction A M] (a a' : GradedMonoid A) (b : GradedMonoid M), (a * a') • b = a • a' • b

Associativity of • and *

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

The graded version of Monoid.toMulAction.

Equations

• GradedMonoid.GMonoid.toGMulAction A = GradedMonoid.GMulAction.mk ⋯ ⋯

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

Equations

• GradedMonoid.GMulAction.toMulAction A M = MulAction.mk ⋯ ⋯

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 : ιA → S) (B : ιB → N) : Prop

A version of GradedMonoid.GSMul for internally graded objects.

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

  Multiplication is homogeneous

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} : ∀ {inst : SetLike S R} {inst_1 : SetLike N M} {inst_2 : SMul R M} {inst_3 : VAdd ιA ιB} {A : ιA → S} {B : ιB → N} [self : SetLike.GradedSMul A B] ⦃i : ιA⦄ ⦃j : ιB⦄ {ai : R} {bj : M}, ai ∈ A i → bj ∈ B j → ai • 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 : ιA → S) (B : ιB → N) [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 : ιA → S) (B : ιB → N) [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 : ιA → S) [SetLike.GradedMonoid A] : SetLike.GradedSMul A 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 : ιA → S} {B : ιB → N} [SetLike.GradedSMul A B] {a : R} {b : M} : SetLike.Homogeneous A a → SetLike.Homogeneous B b → SetLike.Homogeneous B (a • b)