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 {ιA : Type u_1} {ιB : Type u_2} (A : ιAType u_3) (M : ιBType 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.

Instances
    theorem DirectSum.GdistribMulAction.smul_add {ιA : Type u_1} {ιB : Type u_2} {A : ιAType u_3} {M : ιBType 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) :
    theorem DirectSum.GdistribMulAction.smul_zero {ιA : Type u_1} {ιB : Type u_2} {A : ιAType u_3} {M : ιBType 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) :
    class DirectSum.Gmodule {ιA : Type u_1} {ιB : Type u_2} (A : ιAType u_3) (M : ιBType 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.

    Instances
      theorem DirectSum.Gmodule.add_smul {ιA : Type u_1} {ιB : Type u_2} {A : ιAType u_3} {M : ιBType 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) :
      theorem DirectSum.Gmodule.zero_smul {ιA : Type u_1} {ιB : Type u_2} {A : ιAType u_3} {M : ιBType 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) :
      instance DirectSum.GSemiring.toGmodule {ιA : Type u_1} (A : ιAType u_3) [AddMonoid ιA] [(i : ιA) → AddCommMonoid (A i)] [h : DirectSum.GSemiring A] :

      A graded version of Semiring.toModule.

      Equations
      @[simp]
      theorem DirectSum.gsmulHom_apply_apply {ιA : Type u_1} {ιB : Type u_2} (A : ιAType u_3) (M : ιBType 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) :
      def DirectSum.gsmulHom {ιA : Type u_1} {ιB : Type u_2} (A : ιAType u_3) (M : ιBType 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
      Instances For
        def DirectSum.Gmodule.smulAddMonoidHom {ιA : Type u_1} {ιB : Type u_2} (A : ιAType u_3) (M : ιBType 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.
        Instances For
          instance DirectSum.Gmodule.instSMulOfDecidableEq {ιA : Type u_1} {ιB : Type u_2} (A : ιAType u_3) (M : ιBType 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 : ιAType u_3) (M : ιBType 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) :
          @[simp]
          theorem DirectSum.Gmodule.smulAddMonoidHom_apply_of_of {ιA : Type u_1} {ιB : Type u_2} (A : ιAType u_3) (M : ιBType 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) :
          theorem DirectSum.Gmodule.of_smul_of {ιA : Type u_1} {ιB : Type u_2} (A : ιAType u_3) (M : ιBType 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) :
          instance DirectSum.Gmodule.module {ιA : Type u_1} {ιB : Type u_2} (A : ιAType u_3) (M : ιBType 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
          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
          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
          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
          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
          Instances For
            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
            Instances For