# mathlibdocumentation

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 homological_complex.flip_obj_X_X {V : Type u} {ι : Type u_1} {c : complex_shape ι} {ι' : Type u_2} {c' : complex_shape ι'} (C : c') (i : ι) (j : ι') :
(C.flip_obj.X i).X j = (C.X j).X i
@[simp]
theorem homological_complex.flip_obj_d_f {V : Type u} {ι : Type u_1} {c : complex_shape ι} {ι' : Type u_2} {c' : complex_shape ι'} (C : c') (i i' : ι) (j : ι') :
(C.flip_obj.d i i').f j = (C.X j).d i i'
def homological_complex.flip_obj {V : Type u} {ι : Type u_1} {c : complex_shape ι} {ι' : Type u_2} {c' : complex_shape ι'} (C : c') :

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

Equations
@[simp]
theorem homological_complex.flip_obj_X_d {V : Type u} {ι : Type u_1} {c : complex_shape ι} {ι' : Type u_2} {c' : complex_shape ι'} (C : c') (i : ι) (j j' : ι') :
(C.flip_obj.X i).d j j' = (C.d j j').f i
@[simp]
theorem homological_complex.flip_obj_2 (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') (C : c') :
c').obj C = C.flip_obj
@[simp]
theorem homological_complex.flip_map_f_f (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') (C D : c') (f : C D) (i : ι) (j : ι') :
c c').map f).f i).f j = (f.f j).f i
def homological_complex.flip (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') :

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

Equations
def homological_complex.flip_equivalence_unit_iso (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') :
𝟭 c') c' c

Auxiliary definition for homological_complex.flip_equivalence .

Equations
@[simp]
theorem homological_complex.flip_equivalence_unit_iso_hom_app_f_f (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') (X : c') (i : ι') (j : ι) :
.hom.app X).f i).f j = 𝟙 ((X.X i).X j)
@[simp]
theorem homological_complex.flip_equivalence_unit_iso_inv_app_f_f (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') (X : c') (i : ι') (j : ι) :
.inv.app X).f i).f j = 𝟙 ((X.X i).X j)
def homological_complex.flip_equivalence_counit_iso (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') :
c c' 𝟭 c)

Auxiliary definition for homological_complex.flip_equivalence .

Equations
@[simp]
theorem homological_complex.flip_equivalence_counit_iso_inv_app_f_f (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') (X : c) (i : ι) (j : ι') :
X).f i).f j = 𝟙 ((X.X i).X j)
@[simp]
theorem homological_complex.flip_equivalence_counit_iso_hom_app_f_f (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') (X : c) (i : ι) (j : ι') :
X).f i).f j = 𝟙 ((X.X i).X j)
@[simp]
theorem homological_complex.flip_equivalence_inverse (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') :
= c
@[simp]
theorem homological_complex.flip_equivalence_functor (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') :
= c'
def homological_complex.flip_equivalence (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') :

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

Equations
@[simp]
theorem homological_complex.flip_equivalence_unit_iso_2 (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') :
@[simp]
theorem homological_complex.flip_equivalence_counit_iso_2 (V : Type u) {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') :