Documentation

Mathlib.Algebra.Module.GradedModule

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)

A graded version of DistribMulAction.

Instances
    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)

    A graded version of Module.

    Instances
      instance DirectSum.GSemiring.toGmodule {ι : Type u_1} (A : ι → Type u_2) [AddMonoid ι] [(i : ι) → AddCommMonoid (A i)] [h : DirectSum.GSemiring 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.

      Instances For
        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.

        Instances For
          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

          Instances For
            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.

            Instances For