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 : 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

theorem DirectSum.GdistribMulAction.smul_add {ι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)] [self : DirectSum.GdistribMulAction A M] {i : ιA} {j : ιB} (a : A i) (b : M j) (c : M j) : GradedMonoid.GSMul.smul a (b + c) = GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a c

theorem DirectSum.GdistribMulAction.smul_zero {ι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)] [self : DirectSum.GdistribMulAction A M] {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 : 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

theorem DirectSum.Gmodule.add_smul {ι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] [self : DirectSum.Gmodule A M] {i : ιA} {j : ιB} (a : A i) (a' : A i) (b : M j) : GradedMonoid.GSMul.smul (a + a') b = GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a' b

theorem DirectSum.Gmodule.zero_smul {ι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] [self : DirectSum.Gmodule A M] {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 : DirectSum.GSemiring A] : DirectSum.Gmodule A A

A graded version of Semiring.toModule.

Equations

• DirectSum.GSemiring.toGmodule A = let __src := GradedMonoid.GMonoid.toGMulAction A; DirectSum.Gmodule.mk ⋯ ⋯

@[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] [DirectSum.Gmodule A M] {i : ιA} {j : ιB} (a : A i) (b : M j) : ((DirectSum.gsmulHom A M) a) b = GradedMonoid.GSMul.smul a b

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] [DirectSum.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.

Equations

• DirectSum.gsmulHom A M = { toFun := fun (a : A i) => { toFun := fun (b : M j) => GradedMonoid.GSMul.smul a b, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

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] [DirectSum.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.

Equations

• One or more equations did not get rendered due to their size.

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] [DirectSum.Gmodule A M] : SMul (DirectSum ιA fun (i : ιA) => A i) (DirectSum ιB fun (i : ιB) => M i)

Equations

• One or more equations did not get rendered due to their size.

@[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] [DirectSum.Gmodule A M] (x : DirectSum ιA fun (i : ιA) => A i) (y : DirectSum ιB fun (i : ιB) => M i) : x • y = ((DirectSum.Gmodule.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] [DirectSum.Gmodule A M] {i : ιA} {j : ιB} (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 {ι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] [DirectSum.Gmodule A M] {i : ιA} {j : ιB} (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 {ι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] [DirectSum.GSemiring A] [DirectSum.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.

Equations

• DirectSum.Gmodule.module A M = Module.mk ⋯ ⋯

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] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSMul 𝓐 𝓜] : GradedMonoid.GMulAction (fun (i : ιA) => ↥(𝓐 i)) fun (i : ιM) => ↥(𝓜 i)

Equations

• SetLike.gmulAction 𝓐 𝓜 = let __src := SetLike.toGSMul 𝓐 𝓜; GradedMonoid.GMulAction.mk ⋯ ⋯

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] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSMul 𝓐 𝓜] : DirectSum.GdistribMulAction (fun (i : ιA) => ↥(𝓐 i)) fun (i : ιM) => ↥(𝓜 i)

Equations

• SetLike.gdistribMulAction 𝓐 𝓜 = let __src := SetLike.gmulAction 𝓐 𝓜; DirectSum.GdistribMulAction.mk ⋯ ⋯

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] [SetLike.GradedMonoid 𝓐] [SetLike.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.

Equations

• SetLike.gmodule 𝓐 𝓜 = let __src := SetLike.gdistribMulAction 𝓐 𝓜; DirectSum.Gmodule.mk ⋯ ⋯

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

Equations

• GradedModule.isModule 𝓐 𝓜 = let __src := Module.compHom (DirectSum ιM fun (i : ιM) => ↥(𝓜 i)) (DirectSum.decomposeRingEquiv 𝓐).toRingHom; Module.mk ⋯ ⋯

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.

Equations

• GradedModule.linearEquiv 𝓐 𝓜 = { toAddHom := (DirectSum.decomposeAddEquiv 𝓜).toAddHom, map_smul' := ⋯, invFun := (DirectSum.decomposeAddEquiv 𝓜).symm.toFun, left_inv := ⋯, right_inv := ⋯ }