Graded Module

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

graded module

class DirectSum.GdistribMulAction {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [AddMonoid ι] [GradedMonoid.GMonoid A] [(i : ι) → AddMonoid (M i)] extends GradedMonoid.GMulAction : Type (max (max u_1 u_2) u_3)

• smul : {i j : ι} → A i → M j → M (i + j)
• one_smul : ∀ (b : GradedMonoid M), 1 • b = b
• mul_smul : ∀ (a a' : GradedMonoid A) (b : GradedMonoid M), (a * a') • b = a • a' • b
• smul_add : ∀ {i j : ι} (a : A i) (b c : M j), GradedMonoid.GSmul.smul a (b + c) = GradedMonoid.GSmul.smul a b + GradedMonoid.GSmul.smul a c
• smul_zero : ∀ {i j : ι} (a : A i), GradedMonoid.GSmul.smul a 0 = 0

A graded version of DistribMulAction.

class DirectSum.Gmodule {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [AddMonoid ι] [(i : ι) → AddMonoid (A i)] [(i : ι) → AddMonoid (M i)] [GradedMonoid.GMonoid A] extends DirectSum.GdistribMulAction : Type (max (max u_1 u_2) u_3)

• smul : {i j : ι} → A i → M j → M (i + j)
• one_smul : ∀ (b : GradedMonoid M), 1 • b = b
• mul_smul : ∀ (a a' : GradedMonoid A) (b : GradedMonoid M), (a * a') • b = a • a' • b
• smul_add : ∀ {i j : ι} (a : A i) (b c : M j), GradedMonoid.GSmul.smul a (b + c) = GradedMonoid.GSmul.smul a b + GradedMonoid.GSmul.smul a c
• smul_zero : ∀ {i j : ι} (a : A i), GradedMonoid.GSmul.smul a 0 = 0
• add_smul : ∀ {i j : ι} (a a' : A i) (b : M j), GradedMonoid.GSmul.smul (a + a') b = GradedMonoid.GSmul.smul a b + GradedMonoid.GSmul.smul a' b
• zero_smul : ∀ {i j : ι} (b : M j), GradedMonoid.GSmul.smul 0 b = 0

A graded version of Module.

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

A graded version of Semiring.toModule.

@[simp]

theorem DirectSum.gsmulHom_apply_apply {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [AddMonoid ι] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [GradedMonoid.GMonoid A] [DirectSum.Gmodule A M] {i : ι} {j : ι} (a : A i) (b : M j) : ↑(↑(DirectSum.gsmulHom A M) a) b = GradedMonoid.GSmul.smul a b

def DirectSum.gsmulHom {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [AddMonoid ι] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [GradedMonoid.GMonoid A] [DirectSum.Gmodule A M] {i : ι} {j : ι} : A i →+ M j →+ M (i + j)

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

def DirectSum.Gmodule.smulAddMonoidHom {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [AddMonoid ι] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [DecidableEq ι] [GradedMonoid.GMonoid A] [DirectSum.Gmodule A M] : (⨁ (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.

instance DirectSum.Gmodule.instSMulDirectSumDirectSum {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [AddMonoid ι] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [DecidableEq ι] [GradedMonoid.GMonoid A] [DirectSum.Gmodule A M] : SMul (⨁ (i : ι), A i) (⨁ (i : ι), M i)

@[simp]

theorem DirectSum.Gmodule.smul_def {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [AddMonoid ι] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [DecidableEq ι] [GradedMonoid.GMonoid A] [DirectSum.Gmodule A M] (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) [AddMonoid ι] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [DecidableEq ι] [GradedMonoid.GMonoid A] [DirectSum.Gmodule A M] {i : ι} {j : ι} (x : A i) (y : M j) : ↑(↑(DirectSum.Gmodule.smulAddMonoidHom A M) (↑(DirectSum.of A i) x)) (↑(DirectSum.of M j) y) = ↑(DirectSum.of M (i + j)) (GradedMonoid.GSmul.smul x y)

theorem DirectSum.Gmodule.of_smul_of {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [AddMonoid ι] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [DecidableEq ι] [GradedMonoid.GMonoid A] [DirectSum.Gmodule A M] {i : ι} {j : ι} (x : A i) (y : M j) : ↑(DirectSum.of A i) x • ↑(DirectSum.of M j) y = ↑(DirectSum.of M (i + j)) (GradedMonoid.GSmul.smul x y)

instance DirectSum.Gmodule.module {ι : Type u_1} (A : ι → Type u_2) (M : ι → Type u_3) [AddMonoid ι] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → AddCommMonoid (M i)] [DecidableEq ι] [DirectSum.GSemiring A] [DirectSum.Gmodule A M] : 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} [AddMonoid ι] [Semiring A] (𝓐 : ι → σ') [SetLike σ' A] (𝓜 : ι → σ) [AddMonoid M] [DistribMulAction A M] [SetLike σ M] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSmul 𝓐 𝓜] : 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} [AddMonoid ι] [Semiring A] (𝓐 : ι → σ') [SetLike σ' A] (𝓜 : ι → σ) [AddMonoid M] [DistribMulAction A M] [SetLike σ M] [AddSubmonoidClass σ M] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSmul 𝓐 𝓜] : 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} [AddMonoid ι] [Semiring A] (𝓐 : ι → σ') [SetLike σ' A] (𝓜 : ι → σ) [AddCommMonoid M] [Module A M] [SetLike σ M] [AddSubmonoidClass σ' A] [AddSubmonoidClass σ M] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSmul 𝓐 𝓜] : 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} [AddMonoid ι] [Semiring A] (𝓐 : ι → σ') [SetLike σ' A] (𝓜 : ι → σ) [AddCommMonoid M] [Module A M] [SetLike σ M] [AddSubmonoidClass σ' A] [AddSubmonoidClass σ M] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSmul 𝓐 𝓜] [DecidableEq ι] [GradedRing 𝓐] : 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

def GradedModule.linearEquiv {ι : Type u_1} {A : Type u_3} {M : Type u_4} {σ : Type u_5} {σ' : Type u_6} [AddMonoid ι] [Semiring A] (𝓐 : ι → σ') [SetLike σ' A] (𝓜 : ι → σ) [AddCommMonoid M] [Module A M] [SetLike σ M] [AddSubmonoidClass σ' A] [AddSubmonoidClass σ M] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSmul 𝓐 𝓜] [DecidableEq ι] [GradedRing 𝓐] [DirectSum.Decomposition 𝓜] : 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.