Flip a complex of complexes #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 : ι') :
@[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 : ι') :
def
homological_complex.flip_obj
{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') :
homological_complex (homological_complex V c') c
Flip a complex of complexes over the diagonal, exchanging the horizontal and vertical directions.
@[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' : ι') :
@[simp]
theorem
homological_complex.flip_obj_2
(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') :
(homological_complex.flip V c c').obj C = C.flip_obj
@[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 : ι') :
def
homological_complex.flip
(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 ι') :
homological_complex (homological_complex V c) c' ⥤ homological_complex (homological_complex V c') c
Flipping a complex of complexes over the diagonal, as a functor.
Equations
- homological_complex.flip V c c' = {obj := λ (C : homological_complex (homological_complex V c) c'), C.flip_obj, map := λ (C D : homological_complex (homological_complex V c) c') (f : C ⟶ D), {f := λ (i : ι), {f := λ (j : ι'), (f.f j).f i, comm' := _}, comm' := _}, map_id' := _, map_comp' := _}
def
homological_complex.flip_equivalence_unit_iso
(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 ι') :
𝟭 (homological_complex (homological_complex V c) c') ≅ homological_complex.flip V c c' ⋙ homological_complex.flip V c' c
Auxiliary definition for homological_complex.flip_equivalence .
Equations
- homological_complex.flip_equivalence_unit_iso V c c' = category_theory.nat_iso.of_components (λ (C : homological_complex (homological_complex V c) c'), {hom := {f := λ (i : ι'), {f := λ (j : ι), 𝟙 ((C.X i).X j), comm' := _}, comm' := _}, inv := {f := λ (i : ι'), {f := λ (j : ι), 𝟙 ((C.X i).X j), comm' := _}, comm' := _}, hom_inv_id' := _, inv_hom_id' := _}) _
@[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 : ι) :
def
homological_complex.flip_equivalence_counit_iso
(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 ι') :
homological_complex.flip V c' c ⋙ homological_complex.flip V c c' ≅ 𝟭 (homological_complex (homological_complex V c') c)
Auxiliary definition for homological_complex.flip_equivalence .
Equations
- homological_complex.flip_equivalence_counit_iso V c c' = category_theory.nat_iso.of_components (λ (C : homological_complex (homological_complex V c') c), {hom := {f := λ (i : ι), {f := λ (j : ι'), 𝟙 ((C.X i).X j), comm' := _}, comm' := _}, inv := {f := λ (i : ι), {f := λ (j : ι'), 𝟙 ((C.X i).X j), comm' := _}, comm' := _}, hom_inv_id' := _, inv_hom_id' := _}) _
@[simp]
theorem
homological_complex.flip_equivalence_counit_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 : ι') :
@[simp]
theorem
homological_complex.flip_equivalence_counit_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_inverse
(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 ι') :
(homological_complex.flip_equivalence V c c').inverse = homological_complex.flip V c' c
@[simp]
theorem
homological_complex.flip_equivalence_functor
(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 ι') :
(homological_complex.flip_equivalence V c c').functor = homological_complex.flip V c c'
def
homological_complex.flip_equivalence
(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 ι') :
homological_complex (homological_complex V c) c' ≌ homological_complex (homological_complex V c') c
Flipping a complex of complexes over the diagonal, as an equivalence of categories.
Equations
- homological_complex.flip_equivalence V c c' = {functor := homological_complex.flip V c c', inverse := homological_complex.flip V c' c, unit_iso := homological_complex.flip_equivalence_unit_iso V c c', counit_iso := homological_complex.flip_equivalence_counit_iso V c c', functor_unit_iso_comp' := _}
@[simp]
theorem
homological_complex.flip_equivalence_unit_iso_2
(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 ι') :
@[simp]
theorem
homological_complex.flip_equivalence_counit_iso_2
(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 ι') :