Naturality of the homology of an unopposite complex

For a homological complex K in an opposite category Vᵒᵖ, Mathlib identifies the homology of the complex K.unop in V with the unopposite of the homology of K (HomologicalComplex.homologyUnop), and proves that the analogous identification HomologicalComplex.homologyOp is natural (HomologicalComplex.homologyOp_hom_naturality). This file records the naturality of homologyUnop itself.

It is what lets a morphism of chain complexes of projectives, read through the contravariant functor Hom(-, Y), be compared with the induced map on the cohomology of the Hom-complexes: Mathlib's computation of Ext from a projective resolution passes through homologyUnop.

Main results

• TauCeti.HomologicalComplex.homologyUnop_inv_naturality: the inverse of homologyUnop is natural in the complex.

theorem TauCeti.HomologicalComplex.homologyUnop_inv_naturality {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i).unop (K.homologyUnop i).inv = CategoryTheory.CategoryStruct.comp (L.homologyUnop i).inv (HomologicalComplex.homologyMap ((HomologicalComplex.unopFunctor V c).map φ.op) i)

homologyUnop is natural. For a morphism φ : K ⟶ L of complexes in Vᵒᵖ, the square comparing the unopposite of homologyMap φ with the homology map of the unopposite morphism L.unop ⟶ K.unop commutes.