Graded Module #
Given an R
-algebra A
graded by š
, a graded A
-module M
is expressed as
direct_sum.decomposition š
and set_like.has_graded_smul š š
.
Then ⨠i, š i
is an A
-module and is isomorphic to M
.
Tags #
graded module
- to_gmul_action : graded_monoid.gmul_action A M
- smul_add : ā {i j : ι} (a : A i) (b c : M j), graded_monoid.gmul_action.smul a (b + c) = graded_monoid.gmul_action.smul a b + graded_monoid.gmul_action.smul a c
- smul_zero : ā {i j : ι} (a : A i), graded_monoid.gmul_action.smul a 0 = 0
A graded version of distrib_mul_action
.
Instances of this typeclass
Instances of other typeclasses for direct_sum.gdistrib_mul_action
- direct_sum.gdistrib_mul_action.has_sizeof_inst
- to_gdistrib_mul_action : direct_sum.gdistrib_mul_action A M
- add_smul : ā {i j : ι} (a a' : A i) (b : M j), graded_monoid.gmul_action.smul (a + a') b = graded_monoid.gmul_action.smul a b + graded_monoid.gmul_action.smul a' b
- zero_smul : ā {i j : ι} (b : M j), graded_monoid.gmul_action.smul 0 b = 0
A graded version of module
.
Instances of this typeclass
Instances of other typeclasses for direct_sum.gmodule
- direct_sum.gmodule.has_sizeof_inst
A graded version of semiring.to_module
.
Equations
- direct_sum.gsemiring.to_gmodule A = {to_gdistrib_mul_action := {to_gmul_action := {smul := graded_monoid.gmul_action.smul (graded_monoid.gmonoid.to_gmul_action A), one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
The piecewise multiplication from the has_mul
instance, as a bundled homomorphism.
For graded monoid A
and a graded module M
over A
. gmodule.smul_add_monoid_hom
is the
āØįµ¢ Aįµ¢
-scalar multiplication on āØįµ¢ Mįµ¢
induced by gsmul_hom
.
Equations
- direct_sum.gmodule.smul_add_monoid_hom A M = direct_sum.to_add_monoid (Ī» (i : ι), (direct_sum.to_add_monoid (Ī» (j : ι), ((āadd_monoid_hom.comp_hom (direct_sum.of M (i + j))).comp (direct_sum.gsmul_hom A M)).flip)).flip)
Equations
- direct_sum.gmodule.direct_sum.has_smul A M = {smul := Ī» (x : direct_sum ι (Ī» (i : ι), A i)) (y : direct_sum ι (Ī» (i : ι), M i)), ā(ā(direct_sum.gmodule.smul_add_monoid_hom A M) x) y}
The module
derived from gmodule A M
.
Equations
- direct_sum.gmodule.module A M = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul (direct_sum.gmodule.direct_sum.has_smul (λ (i : ι), A i) (λ (i : ι), M i))}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}
Equations
- set_like.gmul_action š š = {smul := graded_monoid.ghas_smul.smul (set_like.ghas_smul š š), one_smul := _, mul_smul := _}
Equations
- set_like.gdistrib_mul_action š š = {to_gmul_action := {smul := graded_monoid.gmul_action.smul (set_like.gmul_action š š), one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
[set_like.graded_monoid š] [set_like.has_graded_smul š š]
is the internal version of graded
module, the internal version can be translated into the external version gmodule
.
The smul multiplication of A
on ⨠i, š i
from (⨠i, š i) ā+ (⨠i, š i) ā+ ⨠i, š i
turns ⨠i, š i
into an A
-module
Equations
- graded_module.is_module š š = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := Ī» (a : A) (b : direct_sum ι (Ī» (i : ι), ā„(š i))), ā(direct_sum.decompose š) a ⢠b}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}
⨠i, š i
and M
are isomorphic as A
-modules.
"The internal version" and "the external version" are isomorphism as A
-modules.
Equations
- graded_module.linear_equiv š š = {to_fun := ā(direct_sum.decompose_add_equiv š), map_add' := _, map_smul' := _, inv_fun := (direct_sum.decompose_add_equiv š).inv_fun, left_inv := _, right_inv := _}