Documentation

TauCeti.Algebra.Homology.DG.Module.Right.Category

The category of differential graded right modules #

DGRightModuleCat h bundles internally graded right modules over the DG algebra h. Its morphisms are the existing DGRightModuleHom: degree-preserving module maps commuting with differentials, equivalently the closed degree-zero elements of the Hom complex. The category is linear over the ground ring. Forgetting the grading, differential, and algebra action gives a faithful linear functor to modules over the ground ring.

This is the ordinary category of DG modules, before taking chain-homotopy classes or inverting quasi-isomorphisms.

The bundling constructor of and the forgetful functor expose their bodies so that their underlying carriers remain definitionally the supplied module types.

References #

source
structure TauCeti.DGRightModuleCat {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} (h : IsDGAlgebra ๐’œ d) :
Type (max (max uA (uM + 1)) uR)

A bundled differential graded right module over the DG algebra h.

Instances For
    source
    @[instance_reducible]
    instance TauCeti.DGRightModuleCat.instCoeSortType {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} :
    CoeSort (DGRightModuleCat h) (Type uM)
    Equations
    source
    @[reducible, inline]
    abbrev TauCeti.DGRightModuleCat.of {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M : Type uM} [AddCommGroup M] [Module R M] [Module Aแตแต’แต– M] [IsScalarTower R Aแตแต’แต– M] {โ„ณ : โ„ค โ†’ Submodule R M} [DirectSum.Decomposition โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณ] {dM : M โ†’โ‚—[R] M} (hM : IsDGRightModule h โ„ณ dM) :
    DGRightModuleCat h

    Bundle a differential graded right module with its existing structures.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance TauCeti.DGRightModuleCat.instCategory {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} :
      CategoryTheory.Category.{uM, max (max uA (uM + 1)) uR} (DGRightModuleCat h)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance TauCeti.DGRightModuleCat.instFunLikeHomCarrier {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} :
      FunLike (M โŸถ N) M.carrier N.carrier
      Equations
      source
      theorem TauCeti.DGRightModuleCat.hom_ext {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} {f g : M โŸถ N} (hfg : โˆ€ (x : M.carrier), f x = g x) :
      f = g

      Morphisms of bundled DG right modules are equal when their values agree.

      source
      theorem TauCeti.DGRightModuleCat.hom_ext_iff {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} {f g : M โŸถ N} :
      f = g โ†” โˆ€ (x : M.carrier), f x = g x
      source
      @[simp]
      theorem TauCeti.DGRightModuleCat.id_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} (M : DGRightModuleCat h) (x : M.carrier) :
      (CategoryTheory.CategoryStruct.id M) x = x
      source
      @[simp]
      theorem TauCeti.DGRightModuleCat.comp_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N P : DGRightModuleCat h} (f : M โŸถ N) (g : N โŸถ P) (x : M.carrier) :
      (CategoryTheory.CategoryStruct.comp f g) x = g (f x)
      source
      @[instance_reducible]
      instance TauCeti.DGRightModuleCat.instAddCommGroupHom {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} :
      AddCommGroup (M โŸถ N)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance TauCeti.DGRightModuleCat.instModuleHom {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} :
      Module R (M โŸถ N)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem TauCeti.DGRightModuleCat.zero_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} (x : M.carrier) :
      0 x = 0
      source
      @[simp]
      theorem TauCeti.DGRightModuleCat.neg_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} (f : M โŸถ N) (x : M.carrier) :
      (-f) x = -f x
      source
      @[simp]
      theorem TauCeti.DGRightModuleCat.sub_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} (f g : M โŸถ N) (x : M.carrier) :
      (f - g) x = f x - g x
      source
      @[simp]
      theorem TauCeti.DGRightModuleCat.add_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} (f g : M โŸถ N) (x : M.carrier) :
      (f + g) x = f x + g x
      source
      @[simp]
      theorem TauCeti.DGRightModuleCat.smul_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} (r : R) (f : M โŸถ N) (x : M.carrier) :
      (r โ€ข f) x = r โ€ข f x
      source
      instance TauCeti.DGRightModuleCat.instLinearMapClassHomMulOppositeCarrier {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} :
      LinearMapClass (M โŸถ N) Aแตแต’แต– M.carrier N.carrier
      source
      instance TauCeti.DGRightModuleCat.instGradedFunLikeHomCarrierSubmoduleIntGrading {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} :
      GradedFunLike (M โŸถ N) M.grading N.grading
      source
      @[simp]
      theorem TauCeti.DGRightModuleCat.map_d {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} (f : M โŸถ N) (x : M.carrier) :
      N.differential (f x) = f (M.differential x)

      A morphism of bundled DG modules commutes with the differentials.

      source
      @[instance_reducible]
      instance TauCeti.DGRightModuleCat.instPreadditive {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} :
      CategoryTheory.Preadditive (DGRightModuleCat h)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance TauCeti.DGRightModuleCat.instLinear {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} :
      CategoryTheory.Linear R (DGRightModuleCat h)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def TauCeti.DGRightModuleCat.forgetToModuleCat {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} :
      CategoryTheory.Functor (DGRightModuleCat h) (ModuleCat R)

      Forget the grading, differential, and algebra action of a DG right module.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.DGRightModuleCat.forgetToModuleCat_map_hom {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} {M N : DGRightModuleCat h} (f : M โŸถ N) :
        ModuleCat.Hom.hom (forgetToModuleCat.map f) = โ†‘R f.toLinearMap
        source
        instance TauCeti.DGRightModuleCat.instFaithfulModuleCatForgetToModuleCat {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} :
        forgetToModuleCat.Faithful
        source
        instance TauCeti.DGRightModuleCat.instAdditiveModuleCatForgetToModuleCat {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} :
        forgetToModuleCat.Additive
        source
        instance TauCeti.DGRightModuleCat.instLinearModuleCatForgetToModuleCat {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} :
        CategoryTheory.Functor.Linear R forgetToModuleCat