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.

@[inline, reducible]

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_1 u_4) u_3) 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

• HomologicalComplex₂ C c₁ c₂ = HomologicalComplex (HomologicalComplex C c₂) c₁

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.

Equations

• HomologicalComplex₂.toGradedObject K x = match x with | (i₁, i₂) => (K.X i₁).X i₂

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) : HomologicalComplex₂.toGradedObject K ⟶ HomologicalComplex₂.toGradedObject L

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

Equations

• HomologicalComplex₂.toGradedObjectMap φ x = match x with | (i₁, i₂) => (φ.f i₁).f i₂

@[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]

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₂), (HomologicalComplex₂.toGradedObjectFunctor C c₁ c₂).map φ i = HomologicalComplex₂.toGradedObjectMap φ i

@[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₂) : (HomologicalComplex₂.toGradedObjectFunctor C c₁ c₂).obj K = HomologicalComplex₂.toGradedObject K

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.

Equations

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

instance HomologicalComplex₂.instFaithfulHomologicalComplex₂InstCategoryHomologicalComplexHomologicalComplexInstCategoryHomologicalComplexInstHasZeroMorphismsHomologicalComplexInstCategoryHomologicalComplexGradedObjectProdCategoryOfGradedObjectsToGradedObjectFunctor {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.Faithful (HomologicalComplex₂.toGradedObjectFunctor C c₁ c₂)

Equations

• ⋯ = ⋯

@[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_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₂)

@[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₂

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.

Equations

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

@[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₂.toGradedObject (HomologicalComplex₂.ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm) = 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 : HomologicalComplex₂.toGradedObject K ⟶ HomologicalComplex₂.toGradedObject L) (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 : HomologicalComplex₂.toGradedObject K ⟶ HomologicalComplex₂.toGradedObject L) (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' := ⋯ }

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) : CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (CategoryTheory.CategoryStruct.comp ((K.d i₁' i₁'').f i₂) h) = CategoryTheory.CategoryStruct.comp 0 h

@[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₁) : ((HomologicalComplex₂.flip K).X i).X j = (K.X j).X 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₁) : ((HomologicalComplex₂.flip K).d i i').f j = (K.X j).d i 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₁) : ((HomologicalComplex₂.flip K).X i).d j j' = (K.d j j').f i

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.

Equations

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

@[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₂) : HomologicalComplex₂.flip (HomologicalComplex₂.flip K) = K

@[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 = HomologicalComplex₂.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

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.

Equations

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

@[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)

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₂) ≅ CategoryTheory.Functor.comp (HomologicalComplex₂.flipFunctor C c₁ c₂) (HomologicalComplex₂.flipFunctor C c₂ c₁)

Auxiliary definition for HomologicalComplex₂.flipEquivalence.

Equations

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

@[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)

@[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)

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₂) : CategoryTheory.Functor.comp (HomologicalComplex₂.flipFunctor C c₂ c₁) (HomologicalComplex₂.flipFunctor C c₁ c₂) ≅ CategoryTheory.Functor.id (HomologicalComplex₂ C c₂ c₁)

Auxiliary definition for HomologicalComplex₂.flipEquivalence.

Equations

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

@[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₂) : (HomologicalComplex₂.flipEquivalence C c₁ c₂).counitIso = HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂

@[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₂) : (HomologicalComplex₂.flipEquivalence C c₁ c₂).inverse = HomologicalComplex₂.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₂) : (HomologicalComplex₂.flipEquivalence C c₁ c₂).functor = HomologicalComplex₂.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₂) : (HomologicalComplex₂.flipEquivalence C c₁ c₂).unitIso = HomologicalComplex₂.flipEquivalenceUnitIso C c₁ c₂

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.

Equations

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

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

• HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂ = CategoryTheory.eqToIso ⋯

@[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₂)