Naturality of the total-complex symmetry isomorphism

Mathlib constructs HomologicalComplex₂.totalFlipIso, identifying the total complex of a flipped bicomplex with the total complex of the original, but states no naturality lemma for it. Naturality is what a comparison argument needs when the bicomplex varies: a morphism of bicomplexes induces morphisms of both total complexes, and the two identifications must agree.

The proof is the universal property of the total complex: both sides are determined by their restrictions along the canonical inclusions ιTotal, on which the flip isomorphism is a signed inclusion and the induced total map is componentwise.

@[reducible, inline]

noncomputable abbrev HomologicalComplex₂.flipMap {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) : K.flip ⟶ L.flip

The flip of a morphism of bicomplexes, with its source and target named as flips rather than as values of flipFunctor.

Equations

• HomologicalComplex₂.flipMap φ = (HomologicalComplex₂.flipFunctor C c₁ c₂).map φ

instance HomologicalComplex₂.flipFunctor_hasTotal {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] (M : HomologicalComplex₂ C c₁ c₂) [M.HasTotal c] : ((flipFunctor C c₁ c₂).obj M).HasTotal c

Instance bridging the two spellings of the flip: flipFunctor is a def, so a total-complex instance stated for M.flip is not found for (flipFunctor _ _ _).obj M without this.

theorem HomologicalComplex₂.totalFlipIso_naturality {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [K.HasTotal c] [L.HasTotal c] [DecidableEq J] : CategoryTheory.CategoryStruct.comp (total.map (flipMap φ) c) (L.totalFlipIso c).hom = CategoryTheory.CategoryStruct.comp (K.totalFlipIso c).hom (total.map φ c)

The total-complex symmetry isomorphism commutes with morphisms of bicomplexes.

Both sides are determined by their restrictions along the canonical inclusions ιTotal, where the flip is a signed inclusion and the induced total map is componentwise.

theorem HomologicalComplex₂.totalFlipIso_naturality_assoc {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [K.HasTotal c] [L.HasTotal c] [DecidableEq J] {Z : HomologicalComplex C c} (h : L.total c ⟶ Z) : CategoryTheory.CategoryStruct.comp (total.map (flipMap φ) c) (CategoryTheory.CategoryStruct.comp (L.totalFlipIso c).hom h) = CategoryTheory.CategoryStruct.comp (K.totalFlipIso c).hom (CategoryTheory.CategoryStruct.comp (total.map φ c) h)

The total-complex symmetry isomorphism commutes with morphisms of bicomplexes.

Both sides are determined by their restrictions along the canonical inclusions ιTotal, where the flip is a signed inclusion and the induced total map is componentwise.

theorem HomologicalComplex₂.totalFlipIso_inv_naturality {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [K.HasTotal c] [L.HasTotal c] [DecidableEq J] : CategoryTheory.CategoryStruct.comp (total.map φ c) (L.totalFlipIso c).inv = CategoryTheory.CategoryStruct.comp (K.totalFlipIso c).inv (total.map (flipMap φ) c)

Inverse form of totalFlipIso_naturality.

theorem HomologicalComplex₂.totalFlipIso_inv_naturality_assoc {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [K.HasTotal c] [L.HasTotal c] [DecidableEq J] {Z : HomologicalComplex C c} (h : L.flip.total c ⟶ Z) : CategoryTheory.CategoryStruct.comp (total.map φ c) (CategoryTheory.CategoryStruct.comp (L.totalFlipIso c).inv h) = CategoryTheory.CategoryStruct.comp (K.totalFlipIso c).inv (CategoryTheory.CategoryStruct.comp (total.map (flipMap φ) c) h)

Inverse form of totalFlipIso_naturality.