Coproducts of homological complexes, degreewise; homology of colimits

A coproduct of homological complexes is computed degreewise: evaluation in each degree preserves it. This file names the degreewise identification (sigmaXIso), the two summand-inclusion lemmas, extensionality for maps out of a degree of the coproduct (sigmaX_ext_from), and the degreewise description of a family of maps out of the summands (sigmaXDesc), in the shape of Mathlib's biprodXIso for binary biproducts. The consumer is Homotopy.sigma, which assembles homotopies on the summands into one on the coproduct.

The second section is about colimits of any shape J the underlying category has: the short complex at a degree is a colimit-preserving functor of the complex, since its three components are evaluations, so homology in a degree commutes with colimits of shape J as soon as homology of short complexes does (which is the case when colimits of shape J are exact).

Main definitions

• HomologicalComplex.sigmaXIso: (∐ X).X i ≅ ∐ fun k => (X k).X i.
• HomologicalComplex.sigmaXDesc: the degreewise map out of (∐ X).X i assembled from maps out of the summands.

Main results

• HomologicalComplex.ι_f_sigmaXIso_hom, ι_sigmaXIso_inv: the summand inclusions on both sides of the identification.
• HomologicalComplex.sigmaX_ext_from: maps out of (∐ X).X i are determined by their restrictions to the summands.
• HomologicalComplex.homologyFunctor_preservesColimitsOfShape: homology in degree i preserves colimits of shape J when homology of short complexes does.
• HomologicalComplex.quasiIso_colimMap_of_preservesHomology: homology-preserving colimits preserve componentwise quasi-isomorphisms.
• HomologicalComplex.quasiIso_colimMap: the exact-colimit specialization.
• HomologicalComplex.quasiIso_app_colimit_of_preserves: a pointwise quasi-isomorphism between colimit-preserving functors is a quasi-isomorphism at a colimit.

Implementation notes

sigmaXIso is PreservesCoproduct.iso (eval C c i) X rather than asIso (sigmaComparison (eval C c i) X): inside a definition, the IsIso search for the comparison enters the coproduct instance on HomologicalComplex C c and does not terminate.

noncomputable def HomologicalComplex.sigmaXIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] (X : κ → HomologicalComplex C c) (i : ι) : (∐ X).X i ≅ ∐ fun (k : κ) => (X k).X i

Evaluation at i preserves the coproduct; see the implementation notes for the choice of spelling.

Equations

• HomologicalComplex.sigmaXIso X i = CategoryTheory.Limits.PreservesCoproduct.iso (HomologicalComplex.eval C c i) X

@[simp]

theorem HomologicalComplex.ι_sigmaXIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] (X : κ → HomologicalComplex C c) (k : κ) (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (k : κ) => (X k).X i) k) (sigmaXIso X i).inv = (CategoryTheory.Limits.Sigma.ι X k).f i

@[simp]

theorem HomologicalComplex.ι_sigmaXIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] (X : κ → HomologicalComplex C c) (k : κ) (i : ι) {Z : C} (h : (∐ X).X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (k : κ) => (X k).X i) k) (CategoryTheory.CategoryStruct.comp (sigmaXIso X i).inv h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Sigma.ι X k).f i) h

@[simp]

theorem HomologicalComplex.ι_f_sigmaXIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] (X : κ → HomologicalComplex C c) (k : κ) (i : ι) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Sigma.ι X k).f i) (sigmaXIso X i).hom = CategoryTheory.Limits.Sigma.ι (fun (k : κ) => (X k).X i) k

@[simp]

theorem HomologicalComplex.ι_f_sigmaXIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] (X : κ → HomologicalComplex C c) (k : κ) (i : ι) {Z : C} (h : (∐ fun (k : κ) => (X k).X i) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Sigma.ι X k).f i) (CategoryTheory.CategoryStruct.comp (sigmaXIso X i).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (k : κ) => (X k).X i) k) h

theorem HomologicalComplex.sigmaX_ext_from {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] {X : κ → HomologicalComplex C c} {i : ι} {A : C} {f g : (∐ X).X i ⟶ A} (h : ∀ (k : κ), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Sigma.ι X k).f i) f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Sigma.ι X k).f i) g) : f = g

Maps out of (∐ X).X i are determined by their restrictions to the summands, since evaluation preserves the coproduct.

noncomputable def HomologicalComplex.sigmaXDesc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] {X : κ → HomologicalComplex C c} {Y : HomologicalComplex C c} (φ : (k : κ) → (i j : ι) → (X k).X i ⟶ Y.X j) (i j : ι) : (∐ X).X i ⟶ Y.X j

The degreewise map out of (∐ X).X i assembled from maps out of the summands: the degreewise identification followed by Sigma.desc.

Equations

• HomologicalComplex.sigmaXDesc φ i j = CategoryTheory.CategoryStruct.comp (HomologicalComplex.sigmaXIso X i).hom (CategoryTheory.Limits.Sigma.desc fun (k : κ) => φ k i j)

@[simp]

theorem HomologicalComplex.ι_f_sigmaXDesc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] {X : κ → HomologicalComplex C c} {Y : HomologicalComplex C c} (φ : (k : κ) → (i j : ι) → (X k).X i ⟶ Y.X j) (k : κ) (i j : ι) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Sigma.ι X k).f i) (sigmaXDesc φ i j) = φ k i j

@[simp]

theorem HomologicalComplex.ι_f_sigmaXDesc_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] {X : κ → HomologicalComplex C c} {Y : HomologicalComplex C c} (φ : (k : κ) → (i j : ι) → (X k).X i ⟶ Y.X j) (k : κ) (i j : ι) {Z : C} (h : Y.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Sigma.ι X k).f i) (CategoryTheory.CategoryStruct.comp (sigmaXDesc φ i j) h) = CategoryTheory.CategoryStruct.comp (φ k i j) h

instance HomologicalComplex.shortComplexFunctor_preservesColimitsOfShape (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} (c : ComplexShape ι) {J : Type w'} [CategoryTheory.Category.{w'', w'} J] [CategoryTheory.Limits.HasColimitsOfShape J C] (i : ι) : CategoryTheory.Limits.PreservesColimitsOfShape J (shortComplexFunctor C c i)

shortComplexFunctor C c i preserves colimits of every shape C has: its three components are evaluations.

instance HomologicalComplex.homologyFunctor_preservesColimitsOfShape (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} (c : ComplexShape ι) {J : Type w'} [CategoryTheory.Category.{w'', w'} J] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.CategoryWithHomology C] (i : ι) [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.ShortComplex.homologyFunctor C)] : CategoryTheory.Limits.PreservesColimitsOfShape J (homologyFunctor C c i)

Homology in degree i commutes with colimits of shape J when homology of short complexes does, through the factorization homologyFunctorIso of homology of complexes.

theorem HomologicalComplex.quasiIso_colimMap_of_preservesHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] {J : Type w'} [CategoryTheory.Category.{w'', w'} J] [CategoryTheory.Limits.HasColimitsOfShape J C] {ι : Type u_1} {c : ComplexShape ι} [∀ (i : ι), CategoryTheory.Limits.PreservesColimitsOfShape J (homologyFunctor C c i)] {F G : CategoryTheory.Functor J (HomologicalComplex C c)} (α : F ⟶ G) (hα : ∀ (j : J), QuasiIso (α.app j)) : QuasiIso (CategoryTheory.Limits.colim.map α)

Commuting degreewise homology with this colimit identifies the homology map of colim.map α with the colimit of the pointwise homology maps, which are isomorphisms.

theorem HomologicalComplex.quasiIso_colimMap {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] {ι : Type u_1} {c : ComplexShape ι} {F G : CategoryTheory.Functor J (HomologicalComplex C c)} (α : F ⟶ G) (hα : ∀ (j : J), QuasiIso (α.app j)) : QuasiIso (CategoryTheory.Limits.colim.map α)

Exact colimits commute with homology through the short-complex comparison, so the homology-preserving criterion above applies. This includes filtered colimits in an AB5 category.

theorem HomologicalComplex.quasiIso_app_colimit_of_preserves {J : Type w₁} [CategoryTheory.Category.{w₂, w₁} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.Limits.HasColimitsOfShape J C] {ι : Type u_1} {c : ComplexShape ι} [∀ (i : ι), CategoryTheory.Limits.PreservesColimitsOfShape J (homologyFunctor C c i)] {H H' : CategoryTheory.Functor A (HomologicalComplex C c)} (F : CategoryTheory.Functor J A) (α : H ⟶ H') [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.PreservesColimit F H] [CategoryTheory.Limits.PreservesColimit F H'] (hα : ∀ (j : J), QuasiIso ((F.whiskerLeft α).app j)) : QuasiIso (α.app (CategoryTheory.Limits.colimit F))

A natural transformation between colimit-preserving functors to complexes is a quasi-isomorphism at a colimit when it is one on every object of the diagram. Preservation of the colimit by degreewise homology transfers the pointwise quasi-isomorphisms through colim.map; naturality of the preserved-colimit comparisons transfers the result back to the original transformation.