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 {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [AddMonoid ιA] [VAdd ιA ιB] [GradedMonoid.GMonoid A] [(i : ιB) → AddMonoid (M i)] extends GradedMonoid.GMulAction A M : Type (max (max (max u_1 u_2) u_3) u_4)

A graded version of DistribMulAction.

• smul {i : ιA} {j : ιB} : 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 : ιA} {j : ιB} (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 : ιA} {j : ιB} (a : A i) : GradedMonoid.GSMul.smul a 0 = 0

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

A graded version of Module.

• smul {i : ιA} {j : ιB} : 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 : ιA} {j : ιB} (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 : ιA} {j : ιB} (a : A i) : GradedMonoid.GSMul.smul a 0 = 0
• add_smul {i : ιA} {j : ιB} (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 : ιA} {j : ιB} (b : M j) : GradedMonoid.GSMul.smul 0 b = 0

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

A graded version of Semiring.toModule.

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

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

@[simp]

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

def DirectSum.Gmodule.smulAddMonoidHom {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [AddMonoid ιA] [VAdd ιA ιB] [(i : ιA) → AddCommMonoid (A i)] [(i : ιB) → AddCommMonoid (M i)] [DecidableEq ιA] [DecidableEq ιB] [GradedMonoid.GMonoid A] [Gmodule A M] : (DirectSum ιA fun (i : ιA) => A i) →+ (DirectSum ιB fun (i : ιB) => M i) →+ DirectSum ιB fun (i : ιB) => M i

For graded monoid A and a graded module M over A. Gmodule.smulAddMonoidHom is the ⨁ᵢ Aᵢ-scalar multiplication on ⨁ᵢ Mᵢ induced by gsmul_hom.

instance DirectSum.Gmodule.instSMulOfDecidableEq {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [AddMonoid ιA] [VAdd ιA ιB] [(i : ιA) → AddCommMonoid (A i)] [(i : ιB) → AddCommMonoid (M i)] [DecidableEq ιA] [DecidableEq ιB] [GradedMonoid.GMonoid A] [Gmodule A M] : SMul (DirectSum ιA fun (i : ιA) => A i) (DirectSum ιB fun (i : ιB) => M i)

@[simp]

theorem DirectSum.Gmodule.smul_def {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [AddMonoid ιA] [VAdd ιA ιB] [(i : ιA) → AddCommMonoid (A i)] [(i : ιB) → AddCommMonoid (M i)] [DecidableEq ιA] [DecidableEq ιB] [GradedMonoid.GMonoid A] [Gmodule A M] (x : DirectSum ιA fun (i : ιA) => A i) (y : DirectSum ιB fun (i : ιB) => M i) : x • y = ((smulAddMonoidHom A M) x) y

@[simp]

theorem DirectSum.Gmodule.smulAddMonoidHom_apply_of_of {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [AddMonoid ιA] [VAdd ιA ιB] [(i : ιA) → AddCommMonoid (A i)] [(i : ιB) → AddCommMonoid (M i)] [DecidableEq ιA] [DecidableEq ιB] [GradedMonoid.GMonoid A] [Gmodule A M] {i : ιA} {j : ιB} (x : A i) (y : M j) : ((smulAddMonoidHom A M) ((of A i) x)) ((of M j) y) = (of M (i +ᵥ j)) (GradedMonoid.GSMul.smul x y)

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

instance DirectSum.Gmodule.module {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [AddMonoid ιA] [VAdd ιA ιB] [(i : ιA) → AddCommMonoid (A i)] [(i : ιB) → AddCommMonoid (M i)] [DecidableEq ιA] [DecidableEq ιB] [GSemiring A] [Gmodule A M] : Module (DirectSum ιA fun (i : ιA) => A i) (DirectSum ιB fun (i : ιB) => M i)

The Module derived from gmodule A M.

instance SetLike.gmulAction {ιA : Type u_1} {ιM : Type u_2} {A : Type u_4} {M : Type u_5} {σ : Type u_6} {σ' : Type u_7} [AddMonoid ιA] [AddAction ιA ιM] [Semiring A] (𝓐 : ιA → σ') [SetLike σ' A] (𝓜 : ιM → σ) [AddMonoid M] [DistribMulAction A M] [SetLike σ M] [GradedMonoid 𝓐] [GradedSMul 𝓐 𝓜] : GradedMonoid.GMulAction (fun (i : ιA) => ↥(𝓐 i)) fun (i : ιM) => ↥(𝓜 i)

instance SetLike.gdistribMulAction {ιA : Type u_1} {ιM : Type u_2} {A : Type u_4} {M : Type u_5} {σ : Type u_6} {σ' : Type u_7} [AddMonoid ιA] [AddAction ιA ιM] [Semiring A] (𝓐 : ιA → σ') [SetLike σ' A] (𝓜 : ιM → σ) [AddMonoid M] [DistribMulAction A M] [SetLike σ M] [AddSubmonoidClass σ M] [GradedMonoid 𝓐] [GradedSMul 𝓐 𝓜] : DirectSum.GdistribMulAction (fun (i : ιA) => ↥(𝓐 i)) fun (i : ιM) => ↥(𝓜 i)

instance SetLike.gmodule {ιA : Type u_1} {ιM : Type u_2} {A : Type u_4} {M : Type u_5} {σ : Type u_6} {σ' : Type u_7} [AddMonoid ιA] [AddAction ιA ιM] [Semiring A] (𝓐 : ιA → σ') [SetLike σ' A] (𝓜 : ιM → σ) [AddCommMonoid M] [Module A M] [SetLike σ M] [AddSubmonoidClass σ' A] [AddSubmonoidClass σ M] [GradedMonoid 𝓐] [GradedSMul 𝓐 𝓜] : DirectSum.Gmodule (fun (i : ιA) => ↥(𝓐 i)) fun (i : ιM) => ↥(𝓜 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 {ιA : Type u_1} {ιM : Type u_2} {A : Type u_4} {M : Type u_5} {σ : Type u_6} {σ' : Type u_7} [AddMonoid ιA] [AddAction ιA ιM] [Semiring A] (𝓐 : ιA → σ') [SetLike σ' A] (𝓜 : ιM → σ) [AddCommMonoid M] [Module A M] [SetLike σ M] [AddSubmonoidClass σ' A] [AddSubmonoidClass σ M] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSMul 𝓐 𝓜] [DecidableEq ιA] [DecidableEq ιM] [GradedRing 𝓐] : Module A (DirectSum ιM fun (i : ιM) => ↥(𝓜 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 {ιA : Type u_1} {ιM : Type u_2} {A : Type u_4} {M : Type u_5} {σ : Type u_6} {σ' : Type u_7} [AddMonoid ιA] [AddAction ιA ιM] [Semiring A] (𝓐 : ιA → σ') [SetLike σ' A] (𝓜 : ιM → σ) [AddCommMonoid M] [Module A M] [SetLike σ M] [AddSubmonoidClass σ' A] [AddSubmonoidClass σ M] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSMul 𝓐 𝓜] [DecidableEq ιA] [DecidableEq ιM] [GradedRing 𝓐] [DirectSum.Decomposition 𝓜] : M ≃ₗ[A] DirectSum ιM fun (i : ιM) => ↥(𝓜 i)

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