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
@[class]
structure
direct_sum.gdistrib_mul_action
{Ī¹ : Type u_1}
(A : Ī¹ ā Type u_2)
(M : Ī¹ ā Type u_3)
[add_monoid Ī¹]
[graded_monoid.gmonoid A]
[Ī (i : Ī¹), add_monoid (M i)] :
Type (max u_1 u_2 u_3)
- 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
@[class]
structure
direct_sum.gmodule
{Ī¹ : Type u_1}
(A : Ī¹ ā Type u_2)
(M : Ī¹ ā Type u_3)
[add_monoid Ī¹]
[Ī (i : Ī¹), add_monoid (A i)]
[Ī (i : Ī¹), add_monoid (M i)]
[graded_monoid.gmonoid A] :
Type (max u_1 u_2 u_3)
- 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
@[protected, instance]
def
direct_sum.gsemiring.to_gmodule
{Ī¹ : Type u_1}
(A : Ī¹ ā Type u_2)
[decidable_eq Ī¹]
[add_monoid Ī¹]
[Ī (i : Ī¹), add_comm_monoid (A i)]
[direct_sum.gsemiring A] :
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 := _}
@[simp]
theorem
direct_sum.gsmul_hom_apply_apply
{Ī¹ : Type u_1}
(A : Ī¹ ā Type u_2)
(M : Ī¹ ā Type u_3)
[add_monoid Ī¹]
[Ī (i : Ī¹), add_comm_monoid (A i)]
[Ī (i : Ī¹), add_comm_monoid (M i)]
[graded_monoid.gmonoid A]
[direct_sum.gmodule A M]
{i j : Ī¹}
(a : A i)
(b : M j) :
ā(ā(direct_sum.gsmul_hom A M) a) b = graded_monoid.ghas_smul.smul a b
def
direct_sum.gsmul_hom
{Ī¹ : Type u_1}
(A : Ī¹ ā Type u_2)
(M : Ī¹ ā Type u_3)
[add_monoid Ī¹]
[Ī (i : Ī¹), add_comm_monoid (A i)]
[Ī (i : Ī¹), add_comm_monoid (M i)]
[graded_monoid.gmonoid A]
[direct_sum.gmodule A M]
{i j : Ī¹} :
The piecewise multiplication from the has_mul instance, as a bundled homomorphism.
def
direct_sum.gmodule.smul_add_monoid_hom
{Ī¹ : Type u_1}
(A : Ī¹ ā Type u_2)
(M : Ī¹ ā Type u_3)
[add_monoid Ī¹]
[Ī (i : Ī¹), add_comm_monoid (A i)]
[Ī (i : Ī¹), add_comm_monoid (M i)]
[decidable_eq Ī¹]
[graded_monoid.gmonoid A]
[direct_sum.gmodule A M] :
direct_sum Ī¹ (Ī» (i : Ī¹), A i) ā+ direct_sum Ī¹ (Ī» (i : Ī¹), M i) ā+ direct_sum Ī¹ (Ī» (i : Ī¹), M i)
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)
@[protected, instance]
def
direct_sum.gmodule.direct_sum.has_smul
{Ī¹ : Type u_1}
(A : Ī¹ ā Type u_2)
(M : Ī¹ ā Type u_3)
[add_monoid Ī¹]
[Ī (i : Ī¹), add_comm_monoid (A i)]
[Ī (i : Ī¹), add_comm_monoid (M i)]
[decidable_eq Ī¹]
[graded_monoid.gmonoid A]
[direct_sum.gmodule A M] :
has_smul (direct_sum Ī¹ (Ī» (i : Ī¹), A i)) (direct_sum Ī¹ (Ī» (i : Ī¹), M i))
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}
@[simp]
theorem
direct_sum.gmodule.smul_def
{Ī¹ : Type u_1}
(A : Ī¹ ā Type u_2)
(M : Ī¹ ā Type u_3)
[add_monoid Ī¹]
[Ī (i : Ī¹), add_comm_monoid (A i)]
[Ī (i : Ī¹), add_comm_monoid (M i)]
[decidable_eq Ī¹]
[graded_monoid.gmonoid A]
[direct_sum.gmodule A M]
(x : direct_sum Ī¹ (Ī» (i : Ī¹), A i))
(y : direct_sum Ī¹ (Ī» (i : Ī¹), M i)) :
x ā¢ y = ā(ā(direct_sum.gmodule.smul_add_monoid_hom (Ī» (i : Ī¹), A i) (Ī» (i : Ī¹), M i)) x) y
@[simp]
theorem
direct_sum.gmodule.smul_add_monoid_hom_apply_of_of
{Ī¹ : Type u_1}
(A : Ī¹ ā Type u_2)
(M : Ī¹ ā Type u_3)
[add_monoid Ī¹]
[Ī (i : Ī¹), add_comm_monoid (A i)]
[Ī (i : Ī¹), add_comm_monoid (M i)]
[decidable_eq Ī¹]
[graded_monoid.gmonoid A]
[direct_sum.gmodule A M]
{i j : Ī¹}
(x : A i)
(y : M j) :
ā(ā(direct_sum.gmodule.smul_add_monoid_hom A M) (ā(direct_sum.of A i) x)) (ā(direct_sum.of M j) y) = ā(direct_sum.of M (i + j)) (graded_monoid.ghas_smul.smul x y)
@[simp]
theorem
direct_sum.gmodule.of_smul_of
{Ī¹ : Type u_1}
(A : Ī¹ ā Type u_2)
(M : Ī¹ ā Type u_3)
[add_monoid Ī¹]
[Ī (i : Ī¹), add_comm_monoid (A i)]
[Ī (i : Ī¹), add_comm_monoid (M i)]
[decidable_eq Ī¹]
[graded_monoid.gmonoid A]
[direct_sum.gmodule A M]
{i j : Ī¹}
(x : A i)
(y : M j) :
ā(direct_sum.of A i) x ā¢ ā(direct_sum.of M j) y = ā(direct_sum.of M (i + j)) (graded_monoid.ghas_smul.smul x y)
@[protected, instance]
def
direct_sum.gmodule.module
{Ī¹ : Type u_1}
(A : Ī¹ ā Type u_2)
(M : Ī¹ ā Type u_3)
[add_monoid Ī¹]
[Ī (i : Ī¹), add_comm_monoid (A i)]
[Ī (i : Ī¹), add_comm_monoid (M i)]
[decidable_eq Ī¹]
[direct_sum.gsemiring A]
[direct_sum.gmodule A M] :
module (direct_sum Ī¹ (Ī» (i : Ī¹), A i)) (direct_sum Ī¹ (Ī» (i : Ī¹), M i))
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 := _}
@[protected, instance]
def
set_like.gmul_action
{Ī¹ : Type u_1}
{A : Type u_3}
{M : Type u_4}
{Ļ : Type u_5}
{Ļ' : Type u_6}
[add_monoid Ī¹]
[semiring A]
(š : Ī¹ ā Ļ')
[set_like Ļ' A]
(š : Ī¹ ā Ļ)
[add_monoid M]
[distrib_mul_action A M]
[set_like Ļ M]
[set_like.graded_monoid š]
[set_like.has_graded_smul š š] :
graded_monoid.gmul_action (Ī» (i : Ī¹), ā„(š i)) (Ī» (i : Ī¹), ā„(š i))
Equations
- set_like.gmul_action š š = {smul := graded_monoid.ghas_smul.smul (set_like.ghas_smul š š), one_smul := _, mul_smul := _}
@[protected, instance]
def
set_like.gdistrib_mul_action
{Ī¹ : Type u_1}
{A : Type u_3}
{M : Type u_4}
{Ļ : Type u_5}
{Ļ' : Type u_6}
[add_monoid Ī¹]
[semiring A]
(š : Ī¹ ā Ļ')
[set_like Ļ' A]
(š : Ī¹ ā Ļ)
[add_monoid M]
[distrib_mul_action A M]
[set_like Ļ M]
[add_submonoid_class Ļ M]
[set_like.graded_monoid š]
[set_like.has_graded_smul š š] :
direct_sum.gdistrib_mul_action (Ī» (i : Ī¹), ā„(š i)) (Ī» (i : Ī¹), ā„(š i))
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 := _}
@[protected, instance]
def
set_like.gmodule
{Ī¹ : Type u_1}
{A : Type u_3}
{M : Type u_4}
{Ļ : Type u_5}
{Ļ' : Type u_6}
[add_monoid Ī¹]
[semiring A]
(š : Ī¹ ā Ļ')
[set_like Ļ' A]
(š : Ī¹ ā Ļ)
[add_comm_monoid M]
[module A M]
[set_like Ļ M]
[add_submonoid_class Ļ' A]
[add_submonoid_class Ļ M]
[set_like.graded_monoid š]
[set_like.has_graded_smul š š] :
direct_sum.gmodule (Ī» (i : Ī¹), ā„(š i)) (Ī» (i : Ī¹), ā„(š i))
[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.
def
graded_module.is_module
{Ī¹ : Type u_1}
{A : Type u_3}
{M : Type u_4}
{Ļ : Type u_5}
{Ļ' : Type u_6}
[add_monoid Ī¹]
[semiring A]
(š : Ī¹ ā Ļ')
[set_like Ļ' A]
(š : Ī¹ ā Ļ)
[add_comm_monoid M]
[module A M]
[set_like Ļ M]
[add_submonoid_class Ļ' A]
[add_submonoid_class Ļ M]
[set_like.graded_monoid š]
[set_like.has_graded_smul š š]
[decidable_eq Ī¹]
[graded_ring š] :
module A (direct_sum Ī¹ (Ī» (i : Ī¹), ā„(š i)))
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 := _}
def
graded_module.linear_equiv
{Ī¹ : Type u_1}
{A : Type u_3}
{M : Type u_4}
{Ļ : Type u_5}
{Ļ' : Type u_6}
[add_monoid Ī¹]
[semiring A]
(š : Ī¹ ā Ļ')
[set_like Ļ' A]
(š : Ī¹ ā Ļ)
[add_comm_monoid M]
[module A M]
[set_like Ļ M]
[add_submonoid_class Ļ' A]
[add_submonoid_class Ļ M]
[set_like.graded_monoid š]
[set_like.has_graded_smul š š]
[decidable_eq Ī¹]
[graded_ring š]
[direct_sum.decomposition š] :
M āā[A] direct_sum Ī¹ (Ī» (i : Ī¹), ā„(š i))
āØ 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 := _}