Documentation

TauCeti.Algebra.Homology.DG.Module.Right.Hom.Cohomology

Functorial cohomology of differential graded right modules #

A morphism of DG right modules over A induces a right H(A)-linear map on cohomology. The map is computed on cycle representatives and respects identities, composition, and addition. Consequently cohomology defines an additive functor from DG right modules to right modules over H(A). This is the cohomology invariant used when inverting quasi-isomorphisms of DG modules.

Homotopic DG module maps induce the same map on cohomology. Here a homotopy is an ordinary right-module linear map of degree minus one with f - g = d s + s d, in agreement with the existing right-module Hom complex. The equality criterion on cycles also applies without choosing such a homotopy.

The functor exposes its object construction so its values have the advertised cohomology carriers.

The construction uses Mathlib's Submodule.mapQ for descent to the quotient and the existing right H(A)-action on module cohomology.

References #

source
def TauCeti.DGRightModuleHom.cyclesMap {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} {N : Type uN} [AddCommGroup M] [Module R M] [Module Aแตแต’แต– M] [IsScalarTower R Aแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Aแตแต’แต– N] [IsScalarTower R Aแตแต’แต– N] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece ๐’ฉ] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {hM : IsDGRightModule h โ„ณ dM} {hN : IsDGRightModule h ๐’ฉ dN} (f : DGRightModuleHom hM hN) :
โ†ฅhM.cycles โ†’โ‚—[(โ†ฅh.cycles)แตแต’แต–] โ†ฅhN.cycles

A DG module map restricts to a right-linear map over the algebra of cycles.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.DGRightModuleHom.cyclesMap_apply_coe {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} {N : Type uN} [AddCommGroup M] [Module R M] [Module Aแตแต’แต– M] [IsScalarTower R Aแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Aแตแต’แต– N] [IsScalarTower R Aแตแต’แต– N] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece ๐’ฉ] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {hM : IsDGRightModule h โ„ณ dM} {hN : IsDGRightModule h ๐’ฉ dN} (f : DGRightModuleHom hM hN) (z : โ†ฅhM.cycles) :
    โ†‘(f.cyclesMap z) = f โ†‘z
    source
    @[simp]
    theorem TauCeti.DGRightModuleHom.cyclesMap_id {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} :
    (DGRightModuleHom.id hM).cyclesMap = LinearMap.id

    Restriction to cycles preserves identity morphisms.

    source
    @[simp]
    theorem TauCeti.DGRightModuleHom.cyclesMap_comp {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} {N : Type uN} {P : Type uP} [AddCommGroup M] [Module R M] [Module Aแตแต’แต– M] [IsScalarTower R Aแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Aแตแต’แต– N] [IsScalarTower R Aแตแต’แต– N] [AddCommGroup P] [Module R P] [Module Aแตแต’แต– P] [IsScalarTower R Aแตแต’แต– P] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} {โ„ณP : โ„ค โ†’ Submodule R P} [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] [DirectSum.Decomposition โ„ณP] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece ๐’ฉ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณP] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {dP : P โ†’โ‚—[R] P} {hM : IsDGRightModule h โ„ณ dM} {hN : IsDGRightModule h ๐’ฉ dN} {hP : IsDGRightModule h โ„ณP dP} (g : DGRightModuleHom hN hP) (f : DGRightModuleHom hM hN) :
    (g.comp f).cyclesMap = g.cyclesMap โˆ˜โ‚— f.cyclesMap

    Restriction to cycles preserves composition.

    source
    @[simp]
    theorem TauCeti.DGRightModuleHom.cyclesMap_add {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} {N : Type uN} [AddCommGroup M] [Module R M] [Module Aแตแต’แต– M] [IsScalarTower R Aแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Aแตแต’แต– N] [IsScalarTower R Aแตแต’แต– N] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece ๐’ฉ] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {hM : IsDGRightModule h โ„ณ dM} {hN : IsDGRightModule h ๐’ฉ dN} (f g : DGRightModuleHom hM hN) :
    (f + g).cyclesMap = f.cyclesMap + g.cyclesMap

    Restriction to cycles preserves addition.

    source
    theorem TauCeti.DGRightModuleHom.cyclesMap_mem_boundaries {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} {N : Type uN} [AddCommGroup M] [Module R M] [Module Aแตแต’แต– M] [IsScalarTower R Aแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Aแตแต’แต– N] [IsScalarTower R Aแตแต’แต– N] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece ๐’ฉ] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {hM : IsDGRightModule h โ„ณ dM} {hN : IsDGRightModule h ๐’ฉ dN} (f : DGRightModuleHom hM hN) {z : โ†ฅhM.cycles} (hz : z โˆˆ hM.boundaries) :
    f.cyclesMap z โˆˆ hN.boundaries

    A DG module map sends boundaries to boundaries.

    source
    noncomputable def TauCeti.DGRightModuleHom.cohomologyMap {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} {N : Type uN} [AddCommGroup M] [Module R M] [Module Aแตแต’แต– M] [IsScalarTower R Aแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Aแตแต’แต– N] [IsScalarTower R Aแตแต’แต– N] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece ๐’ฉ] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {hM : IsDGRightModule h โ„ณ dM} {hN : IsDGRightModule h ๐’ฉ dN} (f : DGRightModuleHom hM hN) :
    hM.Cohomology โ†’โ‚—[h.Cohomologyแตแต’แต–] hN.Cohomology

    A DG module morphism induces a right-linear map over the cohomology algebra.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.DGRightModuleHom.cohomologyMap_mk {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} {N : Type uN} [AddCommGroup M] [Module R M] [Module Aแตแต’แต– M] [IsScalarTower R Aแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Aแตแต’แต– N] [IsScalarTower R Aแตแต’แต– N] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece ๐’ฉ] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {hM : IsDGRightModule h โ„ณ dM} {hN : IsDGRightModule h ๐’ฉ dN} (f : DGRightModuleHom hM hN) (z : โ†ฅhM.cycles) :
      f.cohomologyMap (Submodule.Quotient.mk z) = Submodule.Quotient.mk (f.cyclesMap z)

      Cohomology maps send the class of a cycle to the class of its image.

      source
      @[simp]
      theorem TauCeti.DGRightModuleHom.cohomologyMap_id {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} :
      (DGRightModuleHom.id hM).cohomologyMap = LinearMap.id

      Taking cohomology preserves the identity module map.

      source
      @[simp]
      theorem TauCeti.DGRightModuleHom.cohomologyMap_comp {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} {N : Type uN} {P : Type uP} [AddCommGroup M] [Module R M] [Module Aแตแต’แต– M] [IsScalarTower R Aแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Aแตแต’แต– N] [IsScalarTower R Aแตแต’แต– N] [AddCommGroup P] [Module R P] [Module Aแตแต’แต– P] [IsScalarTower R Aแตแต’แต– P] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} {โ„ณP : โ„ค โ†’ Submodule R P} [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] [DirectSum.Decomposition โ„ณP] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece ๐’ฉ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณP] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {dP : P โ†’โ‚—[R] P} {hM : IsDGRightModule h โ„ณ dM} {hN : IsDGRightModule h ๐’ฉ dN} {hP : IsDGRightModule h โ„ณP dP} (g : DGRightModuleHom hN hP) (f : DGRightModuleHom hM hN) :
      (g.comp f).cohomologyMap = g.cohomologyMap โˆ˜โ‚— f.cohomologyMap

      Taking cohomology preserves composition of module maps.

      source
      @[simp]
      theorem TauCeti.DGRightModuleHom.cohomologyMap_add {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} {N : Type uN} [AddCommGroup M] [Module R M] [Module Aแตแต’แต– M] [IsScalarTower R Aแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Aแตแต’แต– N] [IsScalarTower R Aแตแต’แต– N] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece ๐’ฉ] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {hM : IsDGRightModule h โ„ณ dM} {hN : IsDGRightModule h ๐’ฉ dN} (f g : DGRightModuleHom hM hN) :
      (f + g).cohomologyMap = f.cohomologyMap + g.cohomologyMap

      Taking cohomology preserves addition of module maps.

      source
      @[simp]
      theorem TauCeti.DGRightModuleHom.cohomologyMap_eq_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 : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [Module Aแตแต’แต– M] [IsScalarTower R Aแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Aแตแต’แต– N] [IsScalarTower R Aแตแต’แต– N] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece ๐’ฉ] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {hM : IsDGRightModule h โ„ณ dM} {hN : IsDGRightModule h ๐’ฉ dN} (f g : DGRightModuleHom hM hN) :
      f.cohomologyMap = g.cohomologyMap โ†” โˆ€ (z : โ†ฅhM.cycles), f โ†‘z - g โ†‘z โˆˆ dN.range

      Two DG module maps induce the same cohomology map exactly when their difference sends all cycles to boundaries.

      source
      theorem TauCeti.DGRightModuleHom.cohomologyMap_eq_of_homotopy {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} {N : Type uN} [AddCommGroup M] [Module R M] [Module Aแตแต’แต– M] [IsScalarTower R Aแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Aแตแต’แต– N] [IsScalarTower R Aแตแต’แต– N] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece ๐’ฉ] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {hM : IsDGRightModule h โ„ณ dM} {hN : IsDGRightModule h ๐’ฉ dN} (f g : DGRightModuleHom hM hN) (s : โ†ฅ(dgRightModuleCochains (-1))) (hs : โˆ€ (x : M), f x - g x = dN (โ†‘s x) + โ†‘s (dM x)) :
      f.cohomologyMap = g.cohomologyMap

      Homotopic DG module maps induce equal right H(A)-linear maps on cohomology.

      source
      noncomputable def TauCeti.DGRightModuleCat.cohomologyFunctor {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 h.Cohomologyแตแต’แต–)

      Cohomology as a functor to right modules over the cohomology algebra.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.DGRightModuleCat.cohomologyFunctor_obj {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) :
        cohomologyFunctor.obj M = โ†งโ‹ฏ.Cohomology

        The cohomology functor takes a DG module to its cohomology right module.

        source
        @[simp]
        theorem TauCeti.DGRightModuleCat.cohomologyFunctor_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 (cohomologyFunctor.map f) = DGRightModuleHom.cohomologyMap f
        source
        instance TauCeti.DGRightModuleCat.instAdditiveModuleCatMulOppositeCohomologyCohomologyFunctor {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {h : IsDGAlgebra ๐’œ d} :
        cohomologyFunctor.Additive

        Cohomology of DG right modules preserves addition of morphisms.