Graded Module #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 := _}