mathlib3 documentation

algebra.module.graded_module

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)

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)

A graded version of module.

Instances of this typeclass
Instances of other typeclasses for direct_sum.gmodule
  • direct_sum.gmodule.has_sizeof_inst
@[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) :
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 : ι} :
A i →+ M j →+ M (i + j)

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

Equations
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
@[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
@[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) :
@[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) :
@[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
@[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
@[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
@[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.

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