Homology and exact limits

This file proves that homology of short complexes, and hence homology of homological complexes, commutes with limits of every shape whose limits are exact.

Main results

• TauCeti.shortComplexHomologyFunctor_preservesLimitsOfShape: homology of short complexes preserves limits of any exact shape.
• TauCeti.homologicalComplexShortComplexFunctor_preservesLimitsOfShape: the short complex associated to a homological complex preserves all existing limits.
• TauCeti.homologicalComplexHomologyFunctor_preservesLimitsOfShape: homology of homological complexes preserves limits of any exact shape.

Implementation notes

A diagram F : J ⥤ ShortComplex C corresponds under ShortComplex.functorEquivalence to a short complex S of diagrams. The limiting cone used here is the image of S under lim : (J ⥤ C) ⥤ C, with legs assembled from the counit of that equivalence. Working with the counit rather than with the definitional identification of this cone with ShortComplex.limitCone 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 limits makes lim preserve homology, identifying the homology of this cone with the chosen limit of the pointwise homology diagram.

Sources

This file is the exact-limit dual of TauCeti/Algebra/Homology/ShortComplex/Colimit, and follows that file's exact-colimit construction step for step. The formal inputs are Joël Riou's short complex API in Mathlib — ShortComplex.functorEquivalence in Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence, ShortComplex.isLimitOfIsLimitπ in Mathlib/Algebra/Homology/ShortComplex/Limits, ShortComplex.mapHomologyIso and NatTrans.app_homology in Mathlib/Algebra/Homology/ShortComplex/PreservesHomology and Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex — together with the exactness class HasExactLimitsOfShape of Dagur Asgeirsson, Isaac Hernando, Coleton Kotch and Adam Topaz in Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.

instance TauCeti.shortComplexHomologyFunctor_preservesLimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.HasExactLimitsOfShape J C] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.ShortComplex.homologyFunctor C)

Homology of short complexes preserves limits of any exact shape.

instance TauCeti.homologicalComplexShortComplexFunctor_preservesLimitsOfShape {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.HasLimitsOfShape J D] (c : ComplexShape I) (q : I) : CategoryTheory.Limits.PreservesLimitsOfShape J (HomologicalComplex.shortComplexFunctor D c q)

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

instance TauCeti.homologicalComplexHomologyFunctor_preservesLimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.HasExactLimitsOfShape J C] {I : Type u_1} (c : ComplexShape I) (q : I) : CategoryTheory.Limits.PreservesLimitsOfShape J (HomologicalComplex.homologyFunctor C c q)

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