mathlib3 documentation

algebra.graded_mul_action

Additively-graded multiplicative action structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This module provides a set of heterogeneous typeclasses for defining a multiplicative structure over the sigma type graded_monoid 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 sigma_graded locale open, these respectively imbue:

For now, these typeclasses are primarily used in the construction of direct_sum.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 set_like subobjects (such as add_submonoids, add_subgroups, or submodules), this file provides the Prop typeclasses:

which provides the API lemma

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

tags #

graded action

Typeclasses #

@[class]
structure graded_monoid.ghas_smul {ι : Type u_1} (A : ι Type u_2) (M : ι Type u_3) [has_add ι] :
Type (max u_1 u_2 u_3)
  • smul : Π {i j : ι}, A i M j M (i + j)

A graded version of has_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 of this typeclass
Instances of other typeclasses for graded_monoid.ghas_smul
  • graded_monoid.ghas_smul.has_sizeof_inst
@[protected, instance]

A graded version of has_mul.to_has_smul

Equations
@[protected, instance]
Equations
theorem graded_monoid.mk_smul_mk {ι : Type u_1} (A : ι Type u_2) (M : ι Type u_3) [has_add ι] [graded_monoid.ghas_smul A M] {i j : ι} (a : A i) (b : M j) :
@[class]
structure graded_monoid.gmul_action {ι : Type u_1} (A : ι Type u_2) (M : ι Type u_3) [add_monoid ι] [graded_monoid.gmonoid A] :
Type (max u_1 u_2 u_3)

A graded version of mul_action.

Instances of this typeclass
Instances of other typeclasses for graded_monoid.gmul_action
  • graded_monoid.gmul_action.has_sizeof_inst
@[instance]

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

@[class]
structure set_like.has_graded_smul {ι : Type u_1} {S : Type u_3} {R : Type u_4} {N : Type u_5} {M : Type u_6} [set_like S R] [set_like N M] [has_smul R M] [has_add ι] (A : ι S) (B : ι N) :
Prop

A version of graded_monoid.ghas_smul for internally graded objects.

Instances of this typeclass
@[protected, instance]
def set_like.ghas_smul {ι : Type u_1} {S : Type u_2} {R : Type u_3} {N : Type u_4} {M : Type u_5} [set_like S R] [set_like N M] [has_smul R M] [has_add ι] (A : ι S) (B : ι N) [set_like.has_graded_smul A B] :
graded_monoid.ghas_smul (λ (i : ι), (A i)) (λ (i : ι), (B i))
Equations
@[simp]
theorem set_like.coe_ghas_smul {ι : Type u_1} {S : Type u_2} {R : Type u_3} {N : Type u_4} {M : Type u_5} [set_like S R] [set_like N M] [has_smul R M] [has_add ι] (A : ι S) (B : ι N) [set_like.has_graded_smul A B] {i j : ι} (x : (A i)) (y : (B j)) :
@[protected, instance]

Internally graded version of has_mul.to_has_smul.

theorem set_like.is_homogeneous.graded_smul {ι : Type u_1} {S : Type u_2} {R : Type u_3} {N : Type u_4} {M : Type u_5} [set_like S R] [set_like N M] [has_add ι] [has_smul R M] {A : ι S} {B : ι N} [set_like.has_graded_smul A B] {a : R} {b : M} :