Flip a complex of complexes

For now we don't have double complexes as a distinct thing, but we can model them as complexes of complexes.

Here we show how to flip a complex of complexes over the diagonal, exchanging the horizontal and vertical directions.

@[simp]

theorem HomologicalComplex.flipObj_d_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} {c : ComplexShape ι} {ι' : Type u_2} {c' : ComplexShape ι'} (C : HomologicalComplex (HomologicalComplex V c) c') (i : ι) (i' : ι) (j : ι') : HomologicalComplex.Hom.f (HomologicalComplex.d (HomologicalComplex.flipObj C) i i') j = HomologicalComplex.d (HomologicalComplex.X C j) i i'

@[simp]

theorem HomologicalComplex.flipObj_X_X {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} {c : ComplexShape ι} {ι' : Type u_2} {c' : ComplexShape ι'} (C : HomologicalComplex (HomologicalComplex V c) c') (i : ι) (j : ι') : HomologicalComplex.X (HomologicalComplex.X (HomologicalComplex.flipObj C) i) j = HomologicalComplex.X (HomologicalComplex.X C j) i

@[simp]

theorem HomologicalComplex.flipObj_X_d {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} {c : ComplexShape ι} {ι' : Type u_2} {c' : ComplexShape ι'} (C : HomologicalComplex (HomologicalComplex V c) c') (i : ι) (j : ι') (j' : ι') : HomologicalComplex.d (HomologicalComplex.X (HomologicalComplex.flipObj C) i) j j' = HomologicalComplex.Hom.f (HomologicalComplex.d C j j') i

def HomologicalComplex.flipObj {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} {c : ComplexShape ι} {ι' : Type u_2} {c' : ComplexShape ι'} (C : HomologicalComplex (HomologicalComplex V c) c') : HomologicalComplex (HomologicalComplex V c') c

Flip a complex of complexes over the diagonal, exchanging the horizontal and vertical directions.

@[simp]

theorem HomologicalComplex.flip_map_f_f (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') {C : HomologicalComplex (HomologicalComplex V c) c'} {D : HomologicalComplex (HomologicalComplex V c) c'} (f : C ⟶ D) (i : ι) (j : ι') : HomologicalComplex.Hom.f (HomologicalComplex.Hom.f ((HomologicalComplex.flip V c c').map f) i) j = HomologicalComplex.Hom.f (HomologicalComplex.Hom.f f j) i

@[simp]

theorem HomologicalComplex.flip_obj (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') (C : HomologicalComplex (HomologicalComplex V c) c') : (HomologicalComplex.flip V c c').obj C = HomologicalComplex.flipObj C

def HomologicalComplex.flip (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') : CategoryTheory.Functor (HomologicalComplex (HomologicalComplex V c) c') (HomologicalComplex (HomologicalComplex V c') c)

Flipping a complex of complexes over the diagonal, as a functor.

@[simp]

theorem HomologicalComplex.flipEquivalenceUnitIso_inv_app_f_f (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') (X : HomologicalComplex (HomologicalComplex V c) c') (i : ι') (j : ι) : HomologicalComplex.Hom.f (HomologicalComplex.Hom.f ((HomologicalComplex.flipEquivalenceUnitIso V c c').inv.app X) i) j = CategoryTheory.CategoryStruct.id (HomologicalComplex.X (HomologicalComplex.X X i) j)

@[simp]

theorem HomologicalComplex.flipEquivalenceUnitIso_hom_app_f_f (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') (X : HomologicalComplex (HomologicalComplex V c) c') (i : ι') (j : ι) : HomologicalComplex.Hom.f (HomologicalComplex.Hom.f ((HomologicalComplex.flipEquivalenceUnitIso V c c').hom.app X) i) j = CategoryTheory.CategoryStruct.id (HomologicalComplex.X (HomologicalComplex.X X i) j)

def HomologicalComplex.flipEquivalenceUnitIso (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') : CategoryTheory.Functor.id (HomologicalComplex (HomologicalComplex V c) c') ≅ CategoryTheory.Functor.comp (HomologicalComplex.flip V c c') (HomologicalComplex.flip V c' c)

Auxiliary definition for HomologicalComplex.flipEquivalence.

@[simp]

theorem HomologicalComplex.flipEquivalenceCounitIso_inv_app_f_f (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') (X : HomologicalComplex (HomologicalComplex V c') c) (i : ι) (j : ι') : HomologicalComplex.Hom.f (HomologicalComplex.Hom.f ((HomologicalComplex.flipEquivalenceCounitIso V c c').inv.app X) i) j = CategoryTheory.CategoryStruct.id (HomologicalComplex.X (HomologicalComplex.X X i) j)

@[simp]

theorem HomologicalComplex.flipEquivalenceCounitIso_hom_app_f_f (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') (X : HomologicalComplex (HomologicalComplex V c') c) (i : ι) (j : ι') : HomologicalComplex.Hom.f (HomologicalComplex.Hom.f ((HomologicalComplex.flipEquivalenceCounitIso V c c').hom.app X) i) j = CategoryTheory.CategoryStruct.id (HomologicalComplex.X (HomologicalComplex.X X i) j)

def HomologicalComplex.flipEquivalenceCounitIso (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') : CategoryTheory.Functor.comp (HomologicalComplex.flip V c' c) (HomologicalComplex.flip V c c') ≅ CategoryTheory.Functor.id (HomologicalComplex (HomologicalComplex V c') c)

Auxiliary definition for HomologicalComplex.flipEquivalence.

@[simp]

theorem HomologicalComplex.flipEquivalence_unitIso (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') : (HomologicalComplex.flipEquivalence V c c').unitIso = HomologicalComplex.flipEquivalenceUnitIso V c c'

@[simp]

theorem HomologicalComplex.flipEquivalence_functor (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') : (HomologicalComplex.flipEquivalence V c c').functor = HomologicalComplex.flip V c c'

@[simp]

theorem HomologicalComplex.flipEquivalence_counitIso (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') : (HomologicalComplex.flipEquivalence V c c').counitIso = HomologicalComplex.flipEquivalenceCounitIso V c c'

@[simp]

theorem HomologicalComplex.flipEquivalence_inverse (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') : (HomologicalComplex.flipEquivalence V c c').inverse = HomologicalComplex.flip V c' c

def HomologicalComplex.flipEquivalence (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} (c : ComplexShape ι) {ι' : Type u_2} (c' : ComplexShape ι') : HomologicalComplex (HomologicalComplex V c) c' ≌ HomologicalComplex (HomologicalComplex V c') c

Flipping a complex of complexes over the diagonal, as an equivalence of categories.