# Documentation

Given an R-algebra A graded by 𝓐, a graded A-module M is expressed as DirectSum.Decomposition 𝓜 and SetLike.GradedSmul 𝓐 𝓜. Then ⨁ i, 𝓜 i is an A-module and is isomorphic to M.

## Tags #

class DirectSum.GdistribMulAction {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [] [(i : ι) → AddMonoid (M i)] extends :
Type (max (max u_1 u_2) u_3)
• smul : {i j : ι} → A iM jM (i + j)
• one_smul : ∀ (b : ), 1 b = b
• mul_smul : ∀ (a a' : ) (b : ), (a * a') b = a a' b
• smul_add : ∀ {i j : ι} (a : A i) (b c : M j), GradedMonoid.GSmul.smul a (b + c) =
• smul_zero : ∀ {i j : ι} (a : A i),

A graded version of DistribMulAction.

Instances
class DirectSum.Gmodule {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [] [(i : ι) → AddMonoid (A i)] [(i : ι) → AddMonoid (M i)] extends :
Type (max (max u_1 u_2) u_3)
• smul : {i j : ι} → A iM jM (i + j)
• one_smul : ∀ (b : ), 1 b = b
• mul_smul : ∀ (a a' : ) (b : ), (a * a') b = a a' b
• smul_add : ∀ {i j : ι} (a : A i) (b c : M j), GradedMonoid.GSmul.smul a (b + c) =
• smul_zero : ∀ {i j : ι} (a : A i),
• add_smul : ∀ {i j : ι} (a a' : A i) (b : M j), GradedMonoid.GSmul.smul (a + a') b =
• zero_smul : ∀ {i j : ι} (b : M j),

A graded version of Module.

Instances
instance DirectSum.GSemiring.toGmodule {ι : Type u_1} (A : ιType u_2) [] [(i : ι) → AddCommMonoid (A i)] [h : ] :

A graded version of Semiring.toModule.

@[simp]
theorem DirectSum.gsmulHom_apply_apply {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [] {i : ι} {j : ι} (a : A i) (b : M j) :
↑(↑() a) b =
def DirectSum.gsmulHom {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [] {i : ι} {j : ι} :
A i →+ M j →+ M (i + j)

The piecewise multiplication from the Mul instance, as a bundled homomorphism.

Instances For
def DirectSum.Gmodule.smulAddMonoidHom {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [] [] :
(⨁ (i : ι), A i) →+ (⨁ (i : ι), M i) →+ ⨁ (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.

Instances For
instance DirectSum.Gmodule.instSMulDirectSumDirectSum {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [] [] :
SMul (⨁ (i : ι), A i) (⨁ (i : ι), M i)
@[simp]
theorem DirectSum.Gmodule.smul_def {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [] [] (x : ⨁ (i : ι), A i) (y : ⨁ (i : ι), M i) :
x y = ↑(↑(DirectSum.Gmodule.smulAddMonoidHom (fun i => A i) fun i => M i) x) y
@[simp]
theorem DirectSum.Gmodule.smulAddMonoidHom_apply_of_of {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [] [] {i : ι} {j : ι} (x : A i) (y : M j) :
↑(↑() (↑() x)) (↑() y) = ↑(DirectSum.of M (i + j)) ()
theorem DirectSum.Gmodule.of_smul_of {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [] [] {i : ι} {j : ι} (x : A i) (y : M j) :
↑() x ↑() y = ↑(DirectSum.of M (i + j)) ()
instance DirectSum.Gmodule.module {ι : Type u_1} (A : ιType u_2) (M : ιType u_3) [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [] [] :
Module (⨁ (i : ι), A i) (⨁ (i : ι), M i)

The Module derived from gmodule A M.

instance SetLike.gmulAction {ι : Type u_1} {A : Type u_3} {M : Type u_4} {σ : Type u_5} {σ' : Type u_6} [] [] (𝓐 : ισ') [SetLike σ' A] (𝓜 : ισ) [] [] [SetLike σ M] [] :
GradedMonoid.GMulAction (fun i => { x // x 𝓐 i }) fun i => { x // x 𝓜 i }
instance SetLike.gdistribMulAction {ι : Type u_1} {A : Type u_3} {M : Type u_4} {σ : Type u_5} {σ' : Type u_6} [] [] (𝓐 : ισ') [SetLike σ' A] (𝓜 : ισ) [] [] [SetLike σ M] [] [] :
DirectSum.GdistribMulAction (fun i => { x // x 𝓐 i }) fun i => { x // x 𝓜 i }
instance SetLike.gmodule {ι : Type u_1} {A : Type u_3} {M : Type u_4} {σ : Type u_5} {σ' : Type u_6} [] [] (𝓐 : ισ') [SetLike σ' A] (𝓜 : ισ) [] [Module A M] [SetLike σ M] [] [] [] :
DirectSum.Gmodule (fun i => { x // x 𝓐 i }) fun i => { x // x 𝓜 i }

[SetLike.GradedMonoid 𝓐] [SetLike.GradedSmul 𝓐 𝓜] is the internal version of graded module, the internal version can be translated into the external version gmodule.

def GradedModule.isModule {ι : Type u_1} {A : Type u_3} {M : Type u_4} {σ : Type u_5} {σ' : Type u_6} [] [] (𝓐 : ισ') [SetLike σ' A] (𝓜 : ισ) [] [Module A M] [SetLike σ M] [] [] [] [] [] :
Module A (⨁ (i : ι), { x // x 𝓜 i })

The smul multiplication of A on ⨁ i, 𝓜 i from (⨁ i, 𝓐 i) →+ (⨁ i, 𝓜 i) →+ ⨁ i, 𝓜 i turns ⨁ i, 𝓜 i into an A-module

Instances For
def GradedModule.linearEquiv {ι : Type u_1} {A : Type u_3} {M : Type u_4} {σ : Type u_5} {σ' : Type u_6} [] [] (𝓐 : ισ') [SetLike σ' A] (𝓜 : ισ) [] [Module A M] [SetLike σ M] [] [] [] [] [] :
M ≃ₗ[A] ⨁ (i : ι), { x // x 𝓜 i }

⨁ i, 𝓜 i and M are isomorphic as A-modules. "The internal version" and "the external version" are isomorphism as A-modules.

Instances For