# Documentation

Mathlib.Algebra.Homology.Flip

# 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} {ι : Type u_1} {c : } {ι' : Type u_2} {c' : } (C : ) (i : ι) (i' : ι) (j : ι') :
@[simp]
theorem HomologicalComplex.flipObj_X_X {V : Type u} {ι : Type u_1} {c : } {ι' : Type u_2} {c' : } (C : ) (i : ι) (j : ι') :
@[simp]
theorem HomologicalComplex.flipObj_X_d {V : Type u} {ι : Type u_1} {c : } {ι' : Type u_2} {c' : } (C : ) (i : ι) (j : ι') (j' : ι') :
def HomologicalComplex.flipObj {V : Type u} {ι : Type u_1} {c : } {ι' : Type u_2} {c' : } (C : ) :

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

Instances For
@[simp]
theorem HomologicalComplex.flip_map_f_f (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) {C : } {D : } (f : C D) (i : ι) (j : ι') :
@[simp]
theorem HomologicalComplex.flip_obj (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) (C : ) :
().obj C =
def HomologicalComplex.flip (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) :

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

Instances For
@[simp]
theorem HomologicalComplex.flipEquivalenceUnitIso_inv_app_f_f (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) (X : ) (i : ι') (j : ι) :
@[simp]
theorem HomologicalComplex.flipEquivalenceUnitIso_hom_app_f_f (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) (X : ) (i : ι') (j : ι) :
def HomologicalComplex.flipEquivalenceUnitIso (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) :

Auxiliary definition for HomologicalComplex.flipEquivalence.

Instances For
@[simp]
theorem HomologicalComplex.flipEquivalenceCounitIso_inv_app_f_f (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) (X : ) (i : ι) (j : ι') :
@[simp]
theorem HomologicalComplex.flipEquivalenceCounitIso_hom_app_f_f (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) (X : ) (i : ι) (j : ι') :
def HomologicalComplex.flipEquivalenceCounitIso (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) :

Auxiliary definition for HomologicalComplex.flipEquivalence.

Instances For
@[simp]
theorem HomologicalComplex.flipEquivalence_unitIso (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) :
().unitIso =
@[simp]
theorem HomologicalComplex.flipEquivalence_functor (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) :
().functor =
@[simp]
theorem HomologicalComplex.flipEquivalence_counitIso (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) :
().counitIso =
@[simp]
theorem HomologicalComplex.flipEquivalence_inverse (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) :
().inverse =
def HomologicalComplex.flipEquivalence (V : Type u) {ι : Type u_1} (c : ) {ι' : Type u_2} (c' : ) :

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

Instances For