Documentation

Mathlib.Algebra.Homology.HomologicalBicomplex

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₂.

Equations
Instances For

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

    Equations
    • K.toGradedObject x = match x with | (i₁, i₂) => (K.X i₁).X i₂
    Instances For
      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 : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (φ : K L) :
      K.toGradedObject L.toGradedObject

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

      Equations
      Instances For
        @[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 : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (φ : K L) (i₁ : I₁) (i₂ : I₂) :
        HomologicalComplex₂.toGradedObjectMap φ (i₁, i₂) = (φ.f i₁).f i₂
        @[simp]
        @[simp]

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[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₂' : I₂) :
          ((HomologicalComplex₂.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_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₂ : I₂) :
          ((HomologicalComplex₂.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_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₂) :
          ((HomologicalComplex₂.ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).X i₁).X i₂ = X (i₁, i₂)
          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₂')) :

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[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₂')) :
            (HomologicalComplex₂.ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).toGradedObject = X
            @[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 : HomologicalComplex₂ C c₁ c₂} {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₂) :
            ((HomologicalComplex₂.homMk f comm₁ comm₂).f i₁).f i₂ = f (i₁, i₂)
            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 : HomologicalComplex₂ C c₁ c₂} {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.

            Equations
            • HomologicalComplex₂.homMk f comm₁ comm₂ = { f := fun (i₁ : I₁) => { f := fun (i₂ : I₂) => f (i₁, i₂), comm' := }, comm' := }
            Instances For
              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₁' : I₁) (h : ¬c₁.Rel i₁ i₁') (i₂ : 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₁) (i₂ : I₂) {Z : C} (h : (K.X i₁'').X i₂ Z) :
              @[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₁) (i₂ : I₂) :
              CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) ((K.d i₁' i₁'').f i₂) = 0
              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₂) (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)
              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₂) (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₂')
              @[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 : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (f : K L) (i₁ : 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)
              @[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 : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (f : K L) (i₁ : 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₂.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_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 : I₁) (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' : I₂) (j : I₁) :
              (K.flip.d i i').f j = (K.X j).d i i'

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[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
                @[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 : HomologicalComplex₂ C c₁ c₂} {L : HomologicalComplex₂ C c₁ c₂} (f : K L) (i : I₂) (j : I₁) :
                (((HomologicalComplex₂.flipFunctor C c₁ c₂).map f).f i).f j = (f.f j).f i
                @[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₂) :
                (HomologicalComplex₂.flipFunctor C c₁ c₂).obj K = K.flip

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[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₂) :
                  (((HomologicalComplex₂.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₂) :
                  (((HomologicalComplex₂.flipEquivalenceUnitIso C c₁ c₂).inv.app X).f i✝).f i = CategoryTheory.CategoryStruct.id ((X.X i✝).X i)

                  Auxiliary definition for HomologicalComplex₂.flipEquivalence.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[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₁) :
                    (((HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂).hom.app X).f i✝).f i = CategoryTheory.CategoryStruct.id ((X.X i✝).X i)
                    @[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₁) :
                    (((HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂).inv.app X).f i✝).f i = CategoryTheory.CategoryStruct.id ((X.X i✝).X i)

                    Auxiliary definition for HomologicalComplex₂.flipEquivalence.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        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₁ : I₁} {y₁ : I₁} (h₁ : x₁ = y₁) {x₂ : I₂} {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₂.

                        Equations
                        Instances For
                          @[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₂) :
                          HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K = CategoryTheory.Iso.refl ((K.X i₁).X i₂)