mathlib documentation

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} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {ι : Type u_1} {c : complex_shape ι} {ι' : Type u_2} {c' : complex_shape ι'} (C : homological_complex (homological_complex V 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} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {ι : Type u_1} {c : complex_shape ι} {ι' : Type u_2} {c' : complex_shape ι'} (C : homological_complex (homological_complex V c) c') (i i' : ι) (j : ι') :
(C.flip_obj.d i i').f j = (C.X j).d i i'

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} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {ι : Type u_1} {c : complex_shape ι} {ι' : Type u_2} {c' : complex_shape ι'} (C : homological_complex (homological_complex V c) c') (i : ι) (j j' : ι') :
(C.flip_obj.X i).d j j' = (C.d j j').f i
@[simp]
@[simp]
theorem homological_complex.flip_map_f_f (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') (C D : homological_complex (homological_complex V c) c') (f : C D) (i : ι) (j : ι') :
(((homological_complex.flip V c c').map f).f i).f j = (f.f j).f i

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

Equations

Auxiliary definition for homological_complex.flip_equivalence .

Equations
@[simp]
theorem homological_complex.flip_equivalence_unit_iso_hom_app_f_f (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') (X : homological_complex (homological_complex V c) c') (i : ι') (j : ι) :
@[simp]
theorem homological_complex.flip_equivalence_unit_iso_inv_app_f_f (V : Type u) [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {ι : Type u_1} (c : complex_shape ι) {ι' : Type u_2} (c' : complex_shape ι') (X : homological_complex (homological_complex V c) c') (i : ι') (j : ι) :

Auxiliary definition for homological_complex.flip_equivalence .

Equations
@[simp]
@[simp]