Homology and exact colimits

This file proves that homology of short complexes in an abelian category, and hence homology of homological complexes, commutes with colimits of every shape whose colimits are exact. It also supplies the small-universe AB5 instance for module categories in which the ring and its modules live in unrelated universes.

Main results

• TauCeti.moduleCat_ab5OfSize: small filtered colimits of modules are exact.
• TauCeti.shortComplexHomologyFunctor_preservesColimitsOfShape: homology of short complexes preserves colimits of any exact shape.
• TauCeti.homologicalComplexShortComplexFunctor_preservesColimitsOfShape: the short complex associated to a homological complex preserves all existing colimits.
• TauCeti.homologicalComplexHomologyFunctor_preservesColimitsOfShape: homology of homological complexes preserves colimits of any exact shape.

Implementation notes

A diagram F : J ⥤ ShortComplex C corresponds under ShortComplex.functorEquivalence to a short complex S of diagrams, and the colimit cocone used here is the image of S under colim : (J ⥤ C) ⥤ C, with legs assembled from the counit of that equivalence. Working with the counit rather than with the definitional identification of the two presentations keeps every intermediate statement well typed for rw and simp: in a general category, unlike in a concrete one, neither the unit laws nor associativity hold definitionally, so the composites appearing here cannot be manipulated by rfl alone.

Exactness of J-shaped colimits makes colim preserve homology, which turns the homology of that cocone into the chosen colimit of the pointwise homology diagram.

Mathlib's AB5 instance for ModuleCat.{u} R asks for R : Type u. The instance here removes the corresponding restriction on the module universe for small filtered shapes by transporting exactness along the forgetful functor to abelian groups.

instance TauCeti.moduleCat_ab5OfSize {R : Type u} [Ring R] : CategoryTheory.AB5OfSize.{0, 0, v, max (v + 1) u} (ModuleCat R)

Small filtered colimits of R-modules are exact, with no relation imposed between the universe of the ring and the universe of the modules.

instance TauCeti.shortComplexHomologyFunctor_preservesColimitsOfShape {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Abelian C] {J : Type w} [CategoryTheory.Category.{w, w} J] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C] : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.ShortComplex.homologyFunctor C)

Homology of short complexes preserves colimits of any exact shape.

instance TauCeti.homologicalComplexShortComplexFunctor_preservesColimitsOfShape {J : Type w} [CategoryTheory.Category.{w, w} J] {I : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasColimitsOfShape J D] (c : ComplexShape I) (q : I) : CategoryTheory.Limits.PreservesColimitsOfShape J (HomologicalComplex.shortComplexFunctor D c q)

Sending a homological complex to its short complex at one degree preserves all existing colimits.

instance TauCeti.homologicalComplexHomologyFunctor_preservesColimitsOfShape {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Abelian C] {J : Type w} [CategoryTheory.Category.{w, w} J] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C] {I : Type u_1} (c : ComplexShape I) (q : I) : CategoryTheory.Limits.PreservesColimitsOfShape J (HomologicalComplex.homologyFunctor C c q)

Homology in any degree of a homological complex preserves colimits of any exact shape.