Coproducts in the homotopy category

The homotopy category has coproducts of every shape the underlying category has, computed on complexes, and the quotient functor preserves them. The description out of the quotient of a coproduct is the quotient of the description by lifted legs; uniqueness is Homotopy.sigma, which assembles the homotopies witnessing agreement on each summand into one homotopy.

Main definitions

• HomotopyCategory.cofanDesc: the morphism out of the quotient of ∐ X induced by a cofan.
• HomotopyCategory.isColimitCofan: the quotient of ∐ X is a coproduct of the quotients.

Main results

• HomotopyCategory.hasColimitsOfShape_discrete: the homotopy category has coproducts of shape κ when the underlying category does.
• HomotopyCategory.quotient_preservesColimitsOfShape_discrete: the quotient functor preserves them.
• HomotopyCategory.homologyFunctor_preservesCoproductsOfShape: homology on the homotopy category preserves coproducts when homology of complexes does, since it factors through the quotient.

Implementation notes

An object of the homotopy category is an object of a Quotient, but HomotopyCategory is a def over it and t.pt.as does not elaborate under the default backward.isDefEq.respectTransparency; the vertex of a cofan is therefore represented through Mathlib's Functor.objPreimage for the essentially surjective quotient C c, and legs are lifted with Functor.preimage. The description, its factorization, and its uniqueness are separate declarations with explicit types, because the vertex of Cofan.mk does not reduce syntactically inside Cofan.IsColimit.mk.

With Localization.isColimitCofan at the localization Qh : K(A) ⥤ D(A), these are two of the three inputs to coproducts in the derived category; the third, stability of quasi-isomorphisms under coproducts, is where exactness of coproducts in A enters.

noncomputable def HomotopyCategory.cofanDesc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] (X : κ → HomologicalComplex C c) (t : CategoryTheory.Limits.Cofan fun (k : κ) => (quotient C c).obj (X k)) : (quotient C c).obj (∐ X) ⟶ t.pt

The morphism out of the quotient of ∐ X induced by a cofan: the quotient of the description by Functor.preimages of the legs, then the identification of the vertex.

Equations

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

theorem HomotopyCategory.cofanDesc_fac {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] (X : κ → HomologicalComplex C c) (t : CategoryTheory.Limits.Cofan fun (k : κ) => (quotient C c).obj (X k)) (k : κ) : CategoryTheory.CategoryStruct.comp ((quotient C c).map (CategoryTheory.Limits.Sigma.ι X k)) (cofanDesc X t) = t.inj k

The fac field of Cofan.IsColimit.mk for isColimitCofan.

theorem HomotopyCategory.cofanDesc_uniq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] (X : κ → HomologicalComplex C c) (t : CategoryTheory.Limits.Cofan fun (k : κ) => (quotient C c).obj (X k)) (m : (quotient C c).obj (∐ X) ⟶ t.pt) (hm : ∀ (k : κ), CategoryTheory.CategoryStruct.comp ((quotient C c).map (CategoryTheory.Limits.Sigma.ι X k)) m = t.inj k) : m = cofanDesc X t

A morphism out of the quotient of ∐ X is determined by its restrictions to the summands: it lifts to a chain map, the two lifts are homotopic on each summand, and Homotopy.sigma assembles those homotopies.

noncomputable def HomotopyCategory.isColimitCofan {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] (X : κ → HomologicalComplex C c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk ((quotient C c).obj (∐ X)) fun (k : κ) => (quotient C c).map (CategoryTheory.Limits.Sigma.ι X k))

The quotient of a coproduct of complexes is a coproduct in the homotopy category.

Equations

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

instance HomotopyCategory.preservesColimit_discrete_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] (X : κ → HomologicalComplex C c) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor X) (quotient C c)

The quotient functor preserves the coproduct of a family of complexes.

instance HomotopyCategory.quotient_preservesColimitsOfShape_discrete {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete κ) (quotient C c)

The quotient functor preserves coproducts of shape κ.

instance HomotopyCategory.hasColimitsOfShape_discrete {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) (HomotopyCategory C c)

The homotopy category has coproducts of shape κ when the underlying category does: every family is isomorphic to the image of a family of complexes, whose coproduct isColimitCofan exhibits.

instance HomotopyCategory.homologyFunctor_preservesCoproductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] [CategoryTheory.CategoryWithHomology C] (n : ι) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete κ) (HomologicalComplex.homologyFunctor C c n)] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete κ) (homologyFunctor C c n)

Homology on the homotopy category preserves coproducts of shape κ when homology of complexes does: it factors through the essentially surjective quotient functor, which preserves them.