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:

graded_monoid.ghas_smul A M
graded_monoid.gmul_action A M

With the sigma_graded locale open, these respectively imbue:

has_smul (graded_monoid A) (graded_monoid M)
mul_action (graded_monoid A) (graded_monoid M)

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:

set_like.has_graded_smul A M (which provides the obvious graded_monoid.ghas_smul A instance)

which provides the API lemma

set_like.graded_smul_mem_graded

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 #

source

@[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

source

@[protected, instance]

def graded_monoid.ghas_mul.to_ghas_smul {ι : Type u_1} (A : ι → Type u_2) [has_add ι] [graded_monoid.ghas_mul A] :

graded_monoid.ghas_smul A A

A graded version of has_mul.to_has_smul

Equations

graded_monoid.ghas_mul.to_ghas_smul A = {smul := λ (_x _x_1 : ι), graded_monoid.ghas_mul.mul}

source

@[protected, instance]

def graded_monoid.ghas_smul.to_has_smul {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [has_add ι] [graded_monoid.ghas_smul A M] :

has_smul (graded_monoid A) (graded_monoid M)

Equations

graded_monoid.ghas_smul.to_has_smul A M = {smul := λ (x : graded_monoid A) (y : graded_monoid M), ⟨x.fst + y.fst, graded_monoid.ghas_smul.smul x.snd y.snd⟩}

source

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

graded_monoid.mk i a • graded_monoid.mk j b = graded_monoid.mk (i + j) (graded_monoid.ghas_smul.smul a b)

source

@[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)

smul : Π {i j : ι}, A i → M j → M (i + j)
one_smul : ∀ (b : graded_monoid M), 1 • b = b
mul_smul : ∀ (a a' : graded_monoid A) (b : graded_monoid M), (a * a') • b = a • a' • b

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

source

@[instance]

def graded_monoid.gmul_action.to_ghas_smul {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [add_monoid ι] [graded_monoid.gmonoid A] [self : graded_monoid.gmul_action A M] :

graded_monoid.ghas_smul A M

source

@[protected, instance]

def graded_monoid.gmonoid.to_gmul_action {ι : Type u_1} (A : ι → Type u_2) [add_monoid ι] [graded_monoid.gmonoid A] :

graded_monoid.gmul_action A A

The graded version of monoid.to_mul_action.

Equations

graded_monoid.gmonoid.to_gmul_action A = {smul := graded_monoid.ghas_smul.smul (graded_monoid.ghas_mul.to_ghas_smul (λ (i : ι), A i)), one_smul := _, mul_smul := _}

source

@[protected, instance]

def graded_monoid.gmul_action.to_mul_action {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [add_monoid ι] [graded_monoid.gmonoid A] [graded_monoid.gmul_action A M] :

mul_action (graded_monoid A) (graded_monoid M)

Equations

graded_monoid.gmul_action.to_mul_action A M = {to_has_smul := graded_monoid.ghas_smul.to_has_smul A M {smul := graded_monoid.gmul_action.smul _inst_3}, one_smul := _, mul_smul := _}

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

source

@[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

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

A version of graded_monoid.ghas_smul for internally graded objects.

Instances of this typeclass

set_like.has_graded_mul.to_has_graded_smul

source

@[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

set_like.ghas_smul A B = {smul := λ (i j : ι) (a : ↥(A i)) (b : ↥(B j)), ⟨↑a • ↑b, _⟩}

source

@[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)) :

↑(graded_monoid.ghas_smul.smul x y) = ↑x • ↑y

source

@[protected, instance]

def set_like.has_graded_mul.to_has_graded_smul {ι : Type u_1} {R : Type u_2} [add_monoid ι] [monoid R] {S : Type u_3} [set_like S R] (A : ι → S) [set_like.graded_monoid A] :

set_like.has_graded_smul A A

Internally graded version of has_mul.to_has_smul.

source

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} :

set_like.is_homogeneous A a → set_like.is_homogeneous B b → set_like.is_homogeneous B (a • b)