Homology of short complexes commutes with exact colimits

In an abelian category with exact colimits of shape J (HasExactColimitsOfShape J C, the axiom AB4 when J is discrete and AB5 when it is filtered), the homology functor ShortComplex C ⥤ C preserves colimits of shape J. A diagram of short complexes is a short complex S of diagrams; its colimit is S.map colim because colimits in ShortComplex C are computed after each projection, and the homology of S.map colim is colim of the homology of S by Mathlib's mapHomologyIso, since an exact colim preserves homology.

Main results

• ShortComplex.homologyFunctor_preservesColimitsOfShape: the instance.

Implementation notes

The colimit cocone of the diagram of short complexes is constructed by hand as colimCocone S, with legs S.mapNatTrans (colim.ι j), and shown to be a colimit through isColimitOfIsColimitπ, so that its image under homology can be compared with the colimit cocone of S.homology by homologyMap_mapNatTrans leg by leg.

noncomputable def CategoryTheory.ShortComplex.colimCocone {C : Type u} [Category.{v, u} C] [Abelian C] {J : Type w} [Category.{w', w} J] [Limits.HasColimitsOfShape J C] [HasExactColimitsOfShape J C] (S : ShortComplex (Functor J C)) : Limits.Cocone ((FunctorEquivalence.functor J C).obj S)

The cocone over the diagram of short complexes underlying S, with vertex S.map colim.

Equations

• S.colimCocone = { pt := S.map CategoryTheory.Limits.colim, ι := { app := fun (j : J) => S.mapNatTrans (CategoryTheory.Limits.colim.ι j), naturality := ⋯ } }

noncomputable def CategoryTheory.ShortComplex.isColimitColimCocone {C : Type u} [Category.{v, u} C] [Abelian C] {J : Type w} [Category.{w', w} J] [Limits.HasColimitsOfShape J C] [HasExactColimitsOfShape J C] (S : ShortComplex (Functor J C)) : Limits.IsColimit S.colimCocone

colimCocone S is a colimit cocone: it is one after each projection.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.homologyPointwiseIso {C : Type u} [Category.{v, u} C] [Abelian C] {J : Type w} [Category.{w', w} J] (S : ShortComplex (Functor J C)) : ((FunctorEquivalence.functor J C).obj S).comp (homologyFunctor C) ≅ S.homology

Homology in J ⥤ C is computed pointwise: the homology of the diagram of short complexes underlying S is the homology of S, evaluated (mapHomologyIso at each evaluation functor).

Equations

• S.homologyPointwiseIso = CategoryTheory.NatIso.ofComponents (fun (j : J) => S.mapHomologyIso ((CategoryTheory.evaluation J C).obj j)) ⋯

noncomputable def CategoryTheory.ShortComplex.isColimitMapCoconeColimCocone {C : Type u} [Category.{v, u} C] [Abelian C] {J : Type w} [Category.{w', w} J] [Limits.HasColimitsOfShape J C] [HasExactColimitsOfShape J C] (S : ShortComplex (Functor J C)) : Limits.IsColimit ((homologyFunctor C).mapCocone S.colimCocone)

Homology sends colimCocone S to a colimit cocone: its vertex is the homology of S.map colim, which mapHomologyIso identifies with colim of the homology of S, and its legs are the evaluated legs by homologyMap_mapNatTrans.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.ShortComplex.preservesColimit_homologyFunctor {C : Type u} [Category.{v, u} C] [Abelian C] {J : Type w} [Category.{w', w} J] [Limits.HasColimitsOfShape J C] [HasExactColimitsOfShape J C] (S : ShortComplex (Functor J C)) : Limits.PreservesColimit ((FunctorEquivalence.functor J C).obj S) (homologyFunctor C)

Homology preserves the colimit of the diagram of short complexes underlying S: the colimit cocone colimCocone S is sent to a colimit cocone. Only the OfShape instance below is meant to be found by instance search.

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

When colimits of shape J are exact, colim : (J ⥤ C) ⥤ C preserves homology (Functor.preservesHomologyOfExact), so mapHomologyIso identifies the homology of S.map colim with colim of the homology of S; every diagram of short complexes is such an S by functorEquivalence. Mathlib has the exactness of colim but not this consequence.