Bicomplexes

Given a category C with zero morphisms and two complex shapes c₁ : ComplexShape I₁ and c₂ : ComplexShape I₂, we define the type of bicomplexes HomologicalComplex₂ C c₁ c₂ as an abbreviation for HomologicalComplex (HomologicalComplex C c₂) c₁. In particular, if K : HomologicalComplex₂ C c₁ c₂, then for each i₁ : I₁, K.X i₁ is a column of K.

In this file, we obtain the equivalence of categories HomologicalComplex₂.flipEquivalence : HomologicalComplex₂ C c₁ c₂ ≌ HomologicalComplex₂ C c₂ c₁ which is obtained by exchanging the horizontal and vertical directions.

@[reducible, inline]

abbrev HomologicalComplex₂ (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) : Type (max (max (max (max u_3 u_1) u_4) u_2) u_3 u_4)

Given a category C and two complex shapes c₁ and c₂ on types I₁ and I₂, the associated type of bicomplexes HomologicalComplex₂ C c₁ c₂ is K : HomologicalComplex (HomologicalComplex C c₂) c₁. Then, the object in position ⟨i₁, i₂⟩ can be obtained as (K.X i₁).X i₂.

def HomologicalComplex₂.toGradedObject {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) : CategoryTheory.GradedObject (I₁ × I₂) C

The graded object indexed by I₁ × I₂ induced by a bicomplex.

def HomologicalComplex₂.toGradedObjectMap {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) : K.toGradedObject ⟶ L.toGradedObject

The morphism of graded objects induced by a morphism of bicomplexes.

@[simp]

theorem HomologicalComplex₂.toGradedObjectMap_apply {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (i₁ : I₁) (i₂ : I₂) : toGradedObjectMap φ (i₁, i₂) = (φ.f i₁).f i₂

def HomologicalComplex₂.toGradedObjectFunctor (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) : CategoryTheory.Functor (HomologicalComplex₂ C c₁ c₂) (CategoryTheory.GradedObject (I₁ × I₂) C)

The functor which sends a bicomplex to its associated graded object.

@[simp]

theorem HomologicalComplex₂.toGradedObjectFunctor_obj (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (K : HomologicalComplex₂ C c₁ c₂) : (toGradedObjectFunctor C c₁ c₂).obj K = K.toGradedObject

@[simp]

theorem HomologicalComplex₂.toGradedObjectFunctor_map (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) {X✝ Y✝ : HomologicalComplex₂ C c₁ c₂} (φ : X✝ ⟶ Y✝) (i : I₁ × I₂) : (toGradedObjectFunctor C c₁ c₂).map φ i = toGradedObjectMap φ i

instance HomologicalComplex₂.instFaithfulGradedObjectProdToGradedObjectFunctor {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} : (toGradedObjectFunctor C c₁ c₂).Faithful

def HomologicalComplex₂.ofGradedObject {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : CategoryTheory.GradedObject (I₁ × I₂) C) (d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)) (d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')) (shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0) (shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0) (d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₁ i₁' i₁'' i₂) = 0) (d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₂ i₁ i₂' i₂'') = 0) (comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₂ i₁' i₂ i₂') = CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₁ i₁ i₁' i₂')) : HomologicalComplex₂ C c₁ c₂

Constructor for bicomplexes taking as inputs a graded object, horizontal differentials and vertical differentials satisfying suitable relations.

@[simp]

theorem HomologicalComplex₂.ofGradedObject_d_f {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : CategoryTheory.GradedObject (I₁ × I₂) C) (d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)) (d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')) (shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0) (shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0) (d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₁ i₁' i₁'' i₂) = 0) (d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₂ i₁ i₂' i₂'') = 0) (comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₂ i₁' i₂ i₂') = CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₁ i₁ i₁' i₂')) (i₁ i₁' : I₁) (i₂ : I₂) : ((ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).d i₁ i₁').f i₂ = d₁ i₁ i₁' i₂

@[simp]

theorem HomologicalComplex₂.ofGradedObject_X_d {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : CategoryTheory.GradedObject (I₁ × I₂) C) (d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)) (d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')) (shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0) (shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0) (d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₁ i₁' i₁'' i₂) = 0) (d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₂ i₁ i₂' i₂'') = 0) (comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₂ i₁' i₂ i₂') = CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₁ i₁ i₁' i₂')) (i₁ : I₁) (i₂ i₂' : I₂) : ((ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).X i₁).d i₂ i₂' = d₂ i₁ i₂ i₂'

@[simp]

theorem HomologicalComplex₂.ofGradedObject_X_X {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : CategoryTheory.GradedObject (I₁ × I₂) C) (d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)) (d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')) (shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0) (shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0) (d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₁ i₁' i₁'' i₂) = 0) (d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₂ i₁ i₂' i₂'') = 0) (comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₂ i₁' i₂ i₂') = CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₁ i₁ i₁' i₂')) (i₁ : I₁) (i₂ : I₂) : ((ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).X i₁).X i₂ = X (i₁, i₂)

@[simp]

theorem HomologicalComplex₂.ofGradedObject_toGradedObject {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : CategoryTheory.GradedObject (I₁ × I₂) C) (d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)) (d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')) (shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0) (shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0) (d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₁ i₁' i₁'' i₂) = 0) (d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₂ i₁ i₂' i₂'') = 0) (comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₂ i₁' i₂ i₂') = CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₁ i₁ i₁' i₂')) : (ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).toGradedObject = X

def HomologicalComplex₂.homMk {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (f : K.toGradedObject ⟶ L.toGradedObject) (comm₁ : ∀ (i₁ i₁' : I₁) (i₂ : I₂), c₁.Rel i₁ i₁' → CategoryTheory.CategoryStruct.comp (f (i₁, i₂)) ((L.d i₁ i₁').f i₂) = CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (f (i₁', i₂))) (comm₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), c₂.Rel i₂ i₂' → CategoryTheory.CategoryStruct.comp (f (i₁, i₂)) ((L.X i₁).d i₂ i₂') = CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (f (i₁, i₂'))) : K ⟶ L

Constructor for a morphism K ⟶ L in the category HomologicalComplex₂ C c₁ c₂ which takes as inputs a morphism f : K.toGradedObject ⟶ L.toGradedObject and the compatibilites with both horizontal and vertical differentials.

@[simp]

theorem HomologicalComplex₂.homMk_f_f {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (f : K.toGradedObject ⟶ L.toGradedObject) (comm₁ : ∀ (i₁ i₁' : I₁) (i₂ : I₂), c₁.Rel i₁ i₁' → CategoryTheory.CategoryStruct.comp (f (i₁, i₂)) ((L.d i₁ i₁').f i₂) = CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (f (i₁', i₂))) (comm₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), c₂.Rel i₂ i₂' → CategoryTheory.CategoryStruct.comp (f (i₁, i₂)) ((L.X i₁).d i₂ i₂') = CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (f (i₁, i₂'))) (i₁ : I₁) (i₂ : I₂) : ((homMk f comm₁ comm₂).f i₁).f i₂ = f (i₁, i₂)

theorem HomologicalComplex₂.shape_f {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i₁ i₁' : I₁) (h : ¬c₁.Rel i₁ i₁') (i₂ : I₂) : (K.d i₁ i₁').f i₂ = 0

@[simp]

theorem HomologicalComplex₂.d_f_comp_d_f {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i₁ i₁' i₁'' : I₁) (i₂ : I₂) : CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) ((K.d i₁' i₁'').f i₂) = 0

@[simp]

theorem HomologicalComplex₂.d_f_comp_d_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i₁ i₁' i₁'' : I₁) (i₂ : I₂) {Z : C} (h : (K.X i₁'').X i₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (CategoryTheory.CategoryStruct.comp ((K.d i₁' i₁'').f i₂) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem HomologicalComplex₂.d_comm {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i₁ i₁' : I₁) (i₂ i₂' : I₂) : CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) ((K.X i₁').d i₂ i₂') = CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') ((K.d i₁ i₁').f i₂')

theorem HomologicalComplex₂.d_comm_assoc {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i₁ i₁' : I₁) (i₂ i₂' : I₂) {Z : C} (h : (K.X i₁').X i₂' ⟶ Z) : CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (CategoryTheory.CategoryStruct.comp ((K.X i₁').d i₂ i₂') h) = CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂') h)

@[simp]

theorem HomologicalComplex₂.comm_f {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (f : K ⟶ L) (i₁ i₁' : I₁) (i₂ : I₂) : CategoryTheory.CategoryStruct.comp ((f.f i₁).f i₂) ((L.d i₁ i₁').f i₂) = CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) ((f.f i₁').f i₂)

@[simp]

theorem HomologicalComplex₂.comm_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (f : K ⟶ L) (i₁ i₁' : I₁) (i₂ : I₂) {Z : C} (h : (L.X i₁').X i₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((f.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp ((L.d i₁ i₁').f i₂) h) = CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (CategoryTheory.CategoryStruct.comp ((f.f i₁').f i₂) h)

def HomologicalComplex₂.flip {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) : HomologicalComplex₂ C c₂ c₁

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

@[simp]

theorem HomologicalComplex₂.flip_X_d {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i : I₂) (j j' : I₁) : (K.flip.X i).d j j' = (K.d j j').f i

@[simp]

theorem HomologicalComplex₂.flip_d_f {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i i' : I₂) (j : I₁) : (K.flip.d i i').f j = (K.X j).d i i'

@[simp]

theorem HomologicalComplex₂.flip_X_X {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (i : I₂) (j : I₁) : (K.flip.X i).X j = (K.X j).X i

@[simp]

theorem HomologicalComplex₂.flip_flip {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) : K.flip.flip = K

def HomologicalComplex₂.flipFunctor (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) : CategoryTheory.Functor (HomologicalComplex₂ C c₁ c₂) (HomologicalComplex₂ C c₂ c₁)

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

@[simp]

theorem HomologicalComplex₂.flipFunctor_obj (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (K : HomologicalComplex₂ C c₁ c₂) : (flipFunctor C c₁ c₂).obj K = K.flip

@[simp]

theorem HomologicalComplex₂.flipFunctor_map_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) {K L : HomologicalComplex₂ C c₁ c₂} (f : K ⟶ L) (i : I₂) (j : I₁) : (((flipFunctor C c₁ c₂).map f).f i).f j = (f.f j).f i

def HomologicalComplex₂.flipEquivalenceUnitIso (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) : CategoryTheory.Functor.id (HomologicalComplex₂ C c₁ c₂) ≅ (flipFunctor C c₁ c₂).comp (flipFunctor C c₂ c₁)

Auxiliary definition for HomologicalComplex₂.flipEquivalence.

@[simp]

theorem HomologicalComplex₂.flipEquivalenceUnitIso_hom_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₁ c₂) (i : I₁) (i✝ : I₂) : (((flipEquivalenceUnitIso C c₁ c₂).hom.app X).f i).f i✝ = CategoryTheory.CategoryStruct.id ((X.X i).X i✝)

@[simp]

theorem HomologicalComplex₂.flipEquivalenceUnitIso_inv_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₁ c₂) (i : I₁) (i✝ : I₂) : (((flipEquivalenceUnitIso C c₁ c₂).inv.app X).f i).f i✝ = CategoryTheory.CategoryStruct.id ((X.X i).X i✝)

def HomologicalComplex₂.flipEquivalenceCounitIso (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) : (flipFunctor C c₂ c₁).comp (flipFunctor C c₁ c₂) ≅ CategoryTheory.Functor.id (HomologicalComplex₂ C c₂ c₁)

Auxiliary definition for HomologicalComplex₂.flipEquivalence.

@[simp]

theorem HomologicalComplex₂.flipEquivalenceCounitIso_inv_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₂ c₁) (i : I₂) (i✝ : I₁) : (((flipEquivalenceCounitIso C c₁ c₂).inv.app X).f i).f i✝ = CategoryTheory.CategoryStruct.id ((X.X i).X i✝)

@[simp]

theorem HomologicalComplex₂.flipEquivalenceCounitIso_hom_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₂ c₁) (i : I₂) (i✝ : I₁) : (((flipEquivalenceCounitIso C c₁ c₂).hom.app X).f i).f i✝ = CategoryTheory.CategoryStruct.id ((X.X i).X i✝)

def HomologicalComplex₂.flipEquivalence (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) : HomologicalComplex₂ C c₁ c₂ ≌ HomologicalComplex₂ C c₂ c₁

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

@[simp]

theorem HomologicalComplex₂.flipEquivalence_inverse (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) : (flipEquivalence C c₁ c₂).inverse = flipFunctor C c₂ c₁

@[simp]

theorem HomologicalComplex₂.flipEquivalence_functor (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) : (flipEquivalence C c₁ c₂).functor = flipFunctor C c₁ c₂

@[simp]

theorem HomologicalComplex₂.flipEquivalence_unitIso (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) : (flipEquivalence C c₁ c₂).unitIso = flipEquivalenceUnitIso C c₁ c₂

@[simp]

theorem HomologicalComplex₂.flipEquivalence_counitIso (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) : (flipEquivalence C c₁ c₂).counitIso = flipEquivalenceCounitIso C c₁ c₂

def HomologicalComplex₂.XXIsoOfEq (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (K : HomologicalComplex₂ C c₁ c₂) {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂) : (K.X x₁).X x₂ ≅ (K.X y₁).X y₂

The obvious isomorphism (K.X x₁).X x₂ ≅ (K.X y₁).X y₂ when x₁ = y₁ and x₂ = y₂.

@[simp]

theorem HomologicalComplex₂.XXIsoOfEq_rfl (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (K : HomologicalComplex₂ C c₁ c₂) (i₁ : I₁) (i₂ : I₂) : XXIsoOfEq C c₁ c₂ K ⋯ ⋯ = CategoryTheory.Iso.refl ((K.X i₁).X i₂)