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 AddSubmonoid
s, AddSubgroup
s, or Submodule
s), this file
provides the Prop
typeclasses:
SetLike.GradedSmul A M
(which provides the obviousGradedMonoid.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 #
A graded version of Mul.toSMul
- 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
.
Instances
The graded version of Monoid.toMulAction
.
Shorthands for creating instance of the above typeclasses for collections of subobjects #
Internally graded version of Mul.toSMul
.