The homotopy cofiber of a morphism of homological complexes

In this file, we construct the homotopy cofiber of a morphism φ : F ⟶ G between homological complexes in HomologicalComplex C c. In degree i, it is isomorphic to (F.X j) ⊞ (G.X i) if there is a j such that c.Rel i j, and G.X i otherwise. (This is also known as the mapping cone of φ. Under the name CochainComplex.mappingCone, a specific API shall be developed for the case of cochain complexes indexed by ℤ.)

When we assume hc : ∀ j, ∃ i, c.Rel i j (which holds in the case of chain complexes, or cochain complexes indexed by ℤ), then for any homological complex K, there is a bijection HomologicalComplex.homotopyCofiber.descEquiv φ K hc between homotopyCofiber φ ⟶ K and the tuples (α, hα) with α : G ⟶ K and hα : Homotopy (φ ≫ α) 0.

We shall also study the cylinder of a homological complex K: this is the homotopy cofiber of the morphism biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K. Then, a morphism K.cylinder ⟶ M is determined by the data of two morphisms φ₀ φ₁ : K ⟶ M and a homotopy h : Homotopy φ₀ φ₁, see cylinder.desc. There is also a homotopy equivalence cylinder.homotopyEquiv K : HomotopyEquiv K.cylinder K. From the construction of the cylinder, we deduce the lemma Homotopy.map_eq_of_inverts_homotopyEquivalences which assert that if a functor inverts homotopy equivalences, then the image of two homotopic maps are equal.

class HomologicalComplex.HasHomotopyCofiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) : Prop

A morphism of homological complexes φ : F ⟶ G has a homotopy cofiber if for all indices i and j such that c.Rel i j, the binary biproduct F.X j ⊞ G.X i exists.

• hasBinaryBiproduct : ∀ (i j : ι), c.Rel i j → CategoryTheory.Limits.HasBinaryBiproduct (F.X j) (G.X i)

instance HomologicalComplex.instHasHomotopyCofiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [CategoryTheory.Limits.HasBinaryBiproducts C] : HomologicalComplex.HasHomotopyCofiber φ

Equations

• (_ : HomologicalComplex.HasHomotopyCofiber φ) = (_ : HomologicalComplex.HasHomotopyCofiber φ)

noncomputable def HomologicalComplex.homotopyCofiber.X {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) : C

The X field of the homological complex homotopyCofiber φ.

Equations

• HomologicalComplex.homotopyCofiber.X φ i = if hi : c.Rel i (ComplexShape.next c i) then F.X (ComplexShape.next c i) ⊞ G.X i else G.X i

noncomputable def HomologicalComplex.homotopyCofiber.XIsoBiprod {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel i j) [CategoryTheory.Limits.HasBinaryBiproduct (F.X j) (G.X i)] : HomologicalComplex.homotopyCofiber.X φ i ≅ F.X j ⊞ G.X i

The canonical isomorphism (homotopyCofiber φ).X i ≅ F.X j ⊞ G.X i when c.Rel i j.

Equations

• HomologicalComplex.homotopyCofiber.XIsoBiprod φ i j hij = CategoryTheory.eqToIso (_ : HomologicalComplex.homotopyCofiber.X φ i = (F.X j ⊞ G.X i))

noncomputable def HomologicalComplex.homotopyCofiber.XIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (hi : ¬c.Rel i (ComplexShape.next c i)) : HomologicalComplex.homotopyCofiber.X φ i ≅ G.X i

The canonical isomorphism (homotopyCofiber φ).X i ≅ G.X i when ¬ c.Rel i (c.next i).

Equations

• HomologicalComplex.homotopyCofiber.XIso φ i hi = CategoryTheory.eqToIso (_ : (if hi : c.Rel i (ComplexShape.next c i) then F.X (ComplexShape.next c i) ⊞ G.X i else G.X i) = G.X i)

noncomputable def HomologicalComplex.homotopyCofiber.sndX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) : HomologicalComplex.homotopyCofiber.X φ i ⟶ G.X i

The second projection (homotopyCofiber φ).X i ⟶ G.X i.

Equations

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

noncomputable def HomologicalComplex.homotopyCofiber.inrX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) : G.X i ⟶ HomologicalComplex.homotopyCofiber.X φ i

The right inclusion G.X i ⟶ (homotopyCofiber φ).X i.

Equations

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

@[simp]

theorem HomologicalComplex.homotopyCofiber.inrX_sndX_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) {Z : C} (h : G.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ i) h) = h

@[simp]

theorem HomologicalComplex.homotopyCofiber.inrX_sndX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) (HomologicalComplex.homotopyCofiber.sndX φ i) = CategoryTheory.CategoryStruct.id (G.X i)

theorem HomologicalComplex.homotopyCofiber.sndX_inrX_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (hi : ¬c.Rel i (ComplexShape.next c i)) {Z : C} (h : HomologicalComplex.homotopyCofiber.X φ i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) h) = h

theorem HomologicalComplex.homotopyCofiber.sndX_inrX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (hi : ¬c.Rel i (ComplexShape.next c i)) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ i) (HomologicalComplex.homotopyCofiber.inrX φ i) = CategoryTheory.CategoryStruct.id (HomologicalComplex.homotopyCofiber.X φ i)

noncomputable def HomologicalComplex.homotopyCofiber.fstX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel i j) : HomologicalComplex.homotopyCofiber.X φ i ⟶ F.X j

The first projection (homotopyCofiber φ).X i ⟶ F.X j when c.Rel i j.

Equations

• HomologicalComplex.homotopyCofiber.fstX φ i j hij = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.XIsoBiprod φ i j hij).hom CategoryTheory.Limits.biprod.fst

noncomputable def HomologicalComplex.homotopyCofiber.inlX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel j i) : F.X i ⟶ HomologicalComplex.homotopyCofiber.X φ j

The left inclusion F.X i ⟶ (homotopyCofiber φ).X j when c.Rel j i.

Equations

• HomologicalComplex.homotopyCofiber.inlX φ i j hij = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (HomologicalComplex.homotopyCofiber.XIsoBiprod φ j i hij).inv

@[simp]

theorem HomologicalComplex.homotopyCofiber.inlX_fstX_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel j i) {Z : C} (h : F.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ j i hij) h) = h

@[simp]

theorem HomologicalComplex.homotopyCofiber.inlX_fstX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel j i) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij) (HomologicalComplex.homotopyCofiber.fstX φ j i hij) = CategoryTheory.CategoryStruct.id (F.X i)

@[simp]

theorem HomologicalComplex.homotopyCofiber.inlX_sndX_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel j i) {Z : C} (h : G.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ j) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem HomologicalComplex.homotopyCofiber.inlX_sndX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel j i) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij) (HomologicalComplex.homotopyCofiber.sndX φ j) = 0

@[simp]

theorem HomologicalComplex.homotopyCofiber.inrX_fstX_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel i j) {Z : C} (h : F.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ i j hij) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem HomologicalComplex.homotopyCofiber.inrX_fstX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel i j) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) (HomologicalComplex.homotopyCofiber.fstX φ i j hij) = 0

noncomputable def HomologicalComplex.homotopyCofiber.d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) : HomologicalComplex.homotopyCofiber.X φ i ⟶ HomologicalComplex.homotopyCofiber.X φ j

The d field of the homological complex homotopyCofiber φ.

Equations

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

theorem HomologicalComplex.homotopyCofiber.ext_to_X {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel i j) {A : C} {f : A ⟶ HomologicalComplex.homotopyCofiber.X φ i} {g : A ⟶ HomologicalComplex.homotopyCofiber.X φ i} (h₁ : CategoryTheory.CategoryStruct.comp f (HomologicalComplex.homotopyCofiber.fstX φ i j hij) = CategoryTheory.CategoryStruct.comp g (HomologicalComplex.homotopyCofiber.fstX φ i j hij)) (h₂ : CategoryTheory.CategoryStruct.comp f (HomologicalComplex.homotopyCofiber.sndX φ i) = CategoryTheory.CategoryStruct.comp g (HomologicalComplex.homotopyCofiber.sndX φ i)) : f = g

theorem HomologicalComplex.homotopyCofiber.ext_to_X' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (hi : ¬c.Rel i (ComplexShape.next c i)) {A : C} {f : A ⟶ HomologicalComplex.homotopyCofiber.X φ i} {g : A ⟶ HomologicalComplex.homotopyCofiber.X φ i} (h : CategoryTheory.CategoryStruct.comp f (HomologicalComplex.homotopyCofiber.sndX φ i) = CategoryTheory.CategoryStruct.comp g (HomologicalComplex.homotopyCofiber.sndX φ i)) : f = g

theorem HomologicalComplex.homotopyCofiber.ext_from_X {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel j i) {A : C} {f : HomologicalComplex.homotopyCofiber.X φ j ⟶ A} {g : HomologicalComplex.homotopyCofiber.X φ j ⟶ A} (h₁ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij) f = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hij) g) (h₂ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ j) f = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ j) g) : f = g

theorem HomologicalComplex.homotopyCofiber.ext_from_X' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (hi : ¬c.Rel i (ComplexShape.next c i)) {A : C} {f : HomologicalComplex.homotopyCofiber.X φ i ⟶ A} {g : HomologicalComplex.homotopyCofiber.X φ i ⟶ A} (h : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) f = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) g) : f = g

theorem HomologicalComplex.homotopyCofiber.d_fstX_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) {Z : C} (h : F.X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ j k hjk) h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ i j hij) (F.d j k)) h

theorem HomologicalComplex.homotopyCofiber.d_fstX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j) (HomologicalComplex.homotopyCofiber.fstX φ j k hjk) = -CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ i j hij) (F.d j k)

theorem HomologicalComplex.homotopyCofiber.d_sndX_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel i j) {Z : C} (h : G.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ i j hij) (φ.f j) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ i) (G.d i j)) h

theorem HomologicalComplex.homotopyCofiber.d_sndX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel i j) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j) (HomologicalComplex.homotopyCofiber.sndX φ j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ i j hij) (φ.f j) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ i) (G.d i j)

theorem HomologicalComplex.homotopyCofiber.inlX_d_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) {Z : C} (h : HomologicalComplex.homotopyCofiber.X φ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ j i hij) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j) h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (F.d j k) (HomologicalComplex.homotopyCofiber.inlX φ k j hjk) + CategoryTheory.CategoryStruct.comp (φ.f j) (HomologicalComplex.homotopyCofiber.inrX φ j)) h

theorem HomologicalComplex.homotopyCofiber.inlX_d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ j i hij) (HomologicalComplex.homotopyCofiber.d φ i j) = -CategoryTheory.CategoryStruct.comp (F.d j k) (HomologicalComplex.homotopyCofiber.inlX φ k j hjk) + CategoryTheory.CategoryStruct.comp (φ.f j) (HomologicalComplex.homotopyCofiber.inrX φ j)

theorem HomologicalComplex.homotopyCofiber.inlX_d'_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel i j) (hj : ¬c.Rel j (ComplexShape.next c j)) {Z : C} (h : HomologicalComplex.homotopyCofiber.X φ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ j i hij) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j) h) = CategoryTheory.CategoryStruct.comp (φ.f j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ j) h)

theorem HomologicalComplex.homotopyCofiber.inlX_d' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : c.Rel i j) (hj : ¬c.Rel j (ComplexShape.next c j)) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ j i hij) (HomologicalComplex.homotopyCofiber.d φ i j) = CategoryTheory.CategoryStruct.comp (φ.f j) (HomologicalComplex.homotopyCofiber.inrX φ j)

theorem HomologicalComplex.homotopyCofiber.shape {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) (hij : ¬c.Rel i j) : HomologicalComplex.homotopyCofiber.d φ i j = 0

@[simp]

theorem HomologicalComplex.homotopyCofiber.inrX_d_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) {Z : C} (h : HomologicalComplex.homotopyCofiber.X φ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j) h) = CategoryTheory.CategoryStruct.comp (G.d i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ j) h)

@[simp]

theorem HomologicalComplex.homotopyCofiber.inrX_d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) (HomologicalComplex.homotopyCofiber.d φ i j) = CategoryTheory.CategoryStruct.comp (G.d i j) (HomologicalComplex.homotopyCofiber.inrX φ j)

@[simp]

theorem HomologicalComplex.homotopyCofiber_d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (j : ι) : (HomologicalComplex.homotopyCofiber φ).d i j = HomologicalComplex.homotopyCofiber.d φ i j

@[simp]

theorem HomologicalComplex.homotopyCofiber_X {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) : (HomologicalComplex.homotopyCofiber φ).X i = HomologicalComplex.homotopyCofiber.X φ i

noncomputable def HomologicalComplex.homotopyCofiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] : HomologicalComplex C c

The homotopy cofiber of a morphism of homological complexes, also known as the mapping cone.

Equations

• HomologicalComplex.homotopyCofiber φ = HomologicalComplex.mk (fun (i : ι) => HomologicalComplex.homotopyCofiber.X φ i) fun (i j : ι) => HomologicalComplex.homotopyCofiber.d φ i j

@[simp]

theorem HomologicalComplex.homotopyCofiber.inr_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) : (HomologicalComplex.homotopyCofiber.inr φ).f i = HomologicalComplex.homotopyCofiber.inrX φ i

noncomputable def HomologicalComplex.homotopyCofiber.inr {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] : G ⟶ HomologicalComplex.homotopyCofiber φ

The right inclusion G ⟶ homotopyCofiber φ.

Equations

• HomologicalComplex.homotopyCofiber.inr φ = HomologicalComplex.Hom.mk fun (i : ι) => HomologicalComplex.homotopyCofiber.inrX φ i

noncomputable def HomologicalComplex.homotopyCofiber.inrCompHomotopy {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) : Homotopy (CategoryTheory.CategoryStruct.comp φ (HomologicalComplex.homotopyCofiber.inr φ)) 0

The composition φ ≫ mappingCone.inr φ is homotopic to 0.

Equations

• HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc = Homotopy.mk fun (i j : ι) => if hij : c.Rel j i then HomologicalComplex.homotopyCofiber.inlX φ i j hij else 0

theorem HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (i : ι) (j : ι) (hij : c.Rel j i) : (HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).hom i j = HomologicalComplex.homotopyCofiber.inlX φ i j hij

theorem HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (i : ι) (j : ι) (hij : ¬c.Rel j i) : (HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).hom i j = 0

noncomputable def HomologicalComplex.homotopyCofiber.desc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} {K : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) : HomologicalComplex.homotopyCofiber φ ⟶ K

The morphism homotopyCofiber φ ⟶ K that is induced by a morphism α : G ⟶ K and a homotopy hα : Homotopy (φ ≫ α) 0.

Equations

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

theorem HomologicalComplex.homotopyCofiber.desc_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} {K : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (j : ι) (k : ι) (hjk : c.Rel j k) : (HomologicalComplex.homotopyCofiber.desc φ α hα).f j = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.fstX φ j k hjk) (hα.hom k j) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ j) (α.f j)

theorem HomologicalComplex.homotopyCofiber.desc_f' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} {K : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (j : ι) (hj : ¬c.Rel j (ComplexShape.next c j)) : (HomologicalComplex.homotopyCofiber.desc φ α hα).f j = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ j) (α.f j)

@[simp]

theorem HomologicalComplex.homotopyCofiber.inlX_desc_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} {K : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (i : ι) (j : ι) (hjk : c.Rel j i) {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hjk) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homotopyCofiber.desc φ α hα).f j) h) = CategoryTheory.CategoryStruct.comp (hα.hom i j) h

@[simp]

theorem HomologicalComplex.homotopyCofiber.inlX_desc_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} {K : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (i : ι) (j : ι) (hjk : c.Rel j i) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ i j hjk) ((HomologicalComplex.homotopyCofiber.desc φ α hα).f j) = hα.hom i j

@[simp]

theorem HomologicalComplex.homotopyCofiber.inrX_desc_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} {K : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (i : ι) {Z : C} (h : K.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homotopyCofiber.desc φ α hα).f i) h) = CategoryTheory.CategoryStruct.comp (α.f i) h

@[simp]

theorem HomologicalComplex.homotopyCofiber.inrX_desc_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} {K : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (i : ι) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) ((HomologicalComplex.homotopyCofiber.desc φ α hα).f i) = α.f i

@[simp]

theorem HomologicalComplex.homotopyCofiber.inr_desc_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} {K : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) {Z : HomologicalComplex C c} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr φ) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.desc φ α hα) h) = CategoryTheory.CategoryStruct.comp α h

@[simp]

theorem HomologicalComplex.homotopyCofiber.inr_desc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} {K : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr φ) (HomologicalComplex.homotopyCofiber.desc φ α hα) = α

@[simp]

theorem HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_desc_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} {K : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (i : ι) (j : ι) {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).hom i j) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homotopyCofiber.desc φ α hα).f j) h) = CategoryTheory.CategoryStruct.comp (hα.hom i j) h

@[simp]

theorem HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_desc_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} {K : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (i : ι) (j : ι) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).hom i j) ((HomologicalComplex.homotopyCofiber.desc φ α hα).f j) = hα.hom i j

theorem HomologicalComplex.homotopyCofiber.eq_desc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} {K : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (f : HomologicalComplex.homotopyCofiber φ ⟶ K) (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) : f = HomologicalComplex.homotopyCofiber.desc φ (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr φ) f) (Homotopy.trans (Homotopy.ofEq (_ : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr φ) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp φ (HomologicalComplex.homotopyCofiber.inr φ)) f)) (Homotopy.trans (Homotopy.compRight (HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc) f) (Homotopy.ofEq (_ : CategoryTheory.CategoryStruct.comp 0 f = 0))))

theorem HomologicalComplex.homotopyCofiber.descSigma_ext_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [DecidableRel c.Rel] {K : HomologicalComplex C c} (x : (α : G ⟶ K) × Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (y : (α : G ⟶ K) × Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) : x = y ↔ x.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = y.snd.hom i j

noncomputable def HomologicalComplex.homotopyCofiber.descEquiv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (K : HomologicalComplex C c) (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) : (α : G ⟶ K) × Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0 ≃ (HomologicalComplex.homotopyCofiber φ ⟶ K)

Morphisms homotopyCofiber φ ⟶ K are uniquely determined by a morphism α : G ⟶ K and a homotopy from φ ≫ α to 0.

Equations

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

@[inline, reducible]

noncomputable abbrev HomologicalComplex.cylinder {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] : HomologicalComplex C c

The cylinder object of a homological complex K is the homotopy cofiber of the morphism biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K.

Equations

• HomologicalComplex.cylinder K = HomologicalComplex.homotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))

noncomputable def HomologicalComplex.cylinder.ι₀ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] : K ⟶ HomologicalComplex.cylinder K

The left inclusion K ⟶ K.cylinder.

Equations

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

noncomputable def HomologicalComplex.cylinder.ι₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] : K ⟶ HomologicalComplex.cylinder K

The right inclusion K ⟶ K.cylinder.

Equations

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

noncomputable def HomologicalComplex.cylinder.desc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {K : HomologicalComplex C c} [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (φ₀ : K ⟶ F) (φ₁ : K ⟶ F) (h : Homotopy φ₀ φ₁) : HomologicalComplex.cylinder K ⟶ F

The morphism K.cylinder ⟶ F that is induced by two morphisms φ₀ φ₁ : K ⟶ F and a homotopy h : Homotopy φ₀ φ₁.

Equations

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

@[simp]

theorem HomologicalComplex.cylinder.ι₀_desc_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {K : HomologicalComplex C c} [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (φ₀ : K ⟶ F) (φ₁ : K ⟶ F) (h : Homotopy φ₀ φ₁) {Z : HomologicalComplex C c} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₀ K) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.desc φ₀ φ₁ h✝) h) = CategoryTheory.CategoryStruct.comp φ₀ h

@[simp]

theorem HomologicalComplex.cylinder.ι₀_desc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {K : HomologicalComplex C c} [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (φ₀ : K ⟶ F) (φ₁ : K ⟶ F) (h : Homotopy φ₀ φ₁) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₀ K) (HomologicalComplex.cylinder.desc φ₀ φ₁ h) = φ₀

@[simp]

theorem HomologicalComplex.cylinder.ι₁_desc_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {K : HomologicalComplex C c} [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (φ₀ : K ⟶ F) (φ₁ : K ⟶ F) (h : Homotopy φ₀ φ₁) {Z : HomologicalComplex C c} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₁ K) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.desc φ₀ φ₁ h✝) h) = CategoryTheory.CategoryStruct.comp φ₁ h

@[simp]

theorem HomologicalComplex.cylinder.ι₁_desc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {K : HomologicalComplex C c} [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (φ₀ : K ⟶ F) (φ₁ : K ⟶ F) (h : Homotopy φ₀ φ₁) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₁ K) (HomologicalComplex.cylinder.desc φ₀ φ₁ h) = φ₁

noncomputable def HomologicalComplex.cylinder.π {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] : HomologicalComplex.cylinder K ⟶ K

The projection π : K.cylinder ⟶ K.

Equations

• HomologicalComplex.cylinder.π K = HomologicalComplex.cylinder.desc (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id K) (Homotopy.refl (CategoryTheory.CategoryStruct.id K))

@[simp]

theorem HomologicalComplex.cylinder.ι₀_π_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] {Z : HomologicalComplex C c} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₀ K) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K) h) = h

@[simp]

theorem HomologicalComplex.cylinder.ι₀_π {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₀ K) (HomologicalComplex.cylinder.π K) = CategoryTheory.CategoryStruct.id K

@[simp]

theorem HomologicalComplex.cylinder.ι₁_π_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] {Z : HomologicalComplex C c} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₁ K) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K) h) = h

@[simp]

theorem HomologicalComplex.cylinder.ι₁_π {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₁ K) (HomologicalComplex.cylinder.π K) = CategoryTheory.CategoryStruct.id K

@[inline, reducible]

noncomputable abbrev HomologicalComplex.cylinder.inlX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (i : ι) (j : ι) (hij : c.Rel j i) : K.X i ⟶ (HomologicalComplex.cylinder K).X j

The left inclusion K.X i ⟶ K.cylinder.X j when c.Rel j i.

Equations

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

@[inline, reducible]

noncomputable abbrev HomologicalComplex.cylinder.inrX {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (i : ι) : (K ⊞ K).X i ⟶ (HomologicalComplex.cylinder K).X i

The right inclusion (K ⊞ K).X i ⟶ K.cylinder.X i.

Equations

• HomologicalComplex.cylinder.inrX K i = HomologicalComplex.homotopyCofiber.inrX (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K)) i

@[simp]

theorem HomologicalComplex.cylinder.inlX_π_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (i : ι) (j : ι) (hij : c.Rel j i) {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inlX K i j hij) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.cylinder.π K).f j) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem HomologicalComplex.cylinder.inlX_π {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (i : ι) (j : ι) (hij : c.Rel j i) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inlX K i j hij) ((HomologicalComplex.cylinder.π K).f j) = 0

@[simp]

theorem HomologicalComplex.cylinder.inrX_π_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (i : ι) {Z : C} (h : K.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inrX K i) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.cylinder.π K).f i) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id K)).f i) h

@[simp]

theorem HomologicalComplex.cylinder.inrX_π {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (i : ι) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inrX K i) ((HomologicalComplex.cylinder.π K).f i) = (CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id K)).f i

noncomputable def HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] : HomologicalComplex.cylinder K ⟶ HomologicalComplex.cylinder K

A null homotopic map K.cylinder ⟶ K.cylinder which identifies to π K ≫ ι₀ K - 𝟙 _, see nullHomotopicMap_eq.

Equations

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

noncomputable def HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopy {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] : Homotopy (HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap K) 0

The obvious homotopy from nullHomotopicMap K to zero.

Equations

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

theorem HomologicalComplex.cylinder.πCompι₀Homotopy.inlX_nullHomotopy_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (i : ι) (j : ι) (hij : c.Rel j i) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inlX K i j hij) ((HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap K).f j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inlX K i j hij) ((CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K) (HomologicalComplex.cylinder.ι₀ K) - CategoryTheory.CategoryStruct.id (HomologicalComplex.cylinder K)).f j)

theorem HomologicalComplex.cylinder.πCompι₀Homotopy.biprod_lift_id_sub_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] : CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K) = CategoryTheory.Limits.biprod.inl - CategoryTheory.Limits.biprod.inr

theorem HomologicalComplex.cylinder.πCompι₀Homotopy.inrX_nullHomotopy_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (j : ι) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inrX K j) ((HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap K).f j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inrX K j) ((CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K) (HomologicalComplex.cylinder.ι₀ K) - CategoryTheory.CategoryStruct.id (HomologicalComplex.cylinder K)).f j)

theorem HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap_eq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) : HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap K = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K) (HomologicalComplex.cylinder.ι₀ K) - CategoryTheory.CategoryStruct.id (HomologicalComplex.cylinder K)

noncomputable def HomologicalComplex.cylinder.πCompι₀Homotopy {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) : Homotopy (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K) (HomologicalComplex.cylinder.ι₀ K)) (CategoryTheory.CategoryStruct.id (HomologicalComplex.cylinder K))

The homotopy between π K ≫ ι₀ K and 𝟙 K.cylinder.

Equations

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

noncomputable def HomologicalComplex.cylinder.homotopyEquiv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) : HomotopyEquiv (HomologicalComplex.cylinder K) K

The homotopy equivalence between K.cylinder and K.

Equations

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

noncomputable def HomologicalComplex.cylinder.homotopy₀₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) : Homotopy (HomologicalComplex.cylinder.ι₀ K) (HomologicalComplex.cylinder.ι₁ K)

The homotopy between cylinder.ι₀ K and cylinder.ι₁ K.

Equations

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

theorem HomologicalComplex.cylinder.map_ι₀_eq_map_ι₁ {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) [DecidableRel c.Rel] [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] (H : CategoryTheory.Functor (HomologicalComplex C c) D) (hH : CategoryTheory.MorphismProperty.IsInvertedBy (HomologicalComplex.homotopyEquivalences C c) H) : H.toPrefunctor.map (HomologicalComplex.cylinder.ι₀ K) = H.toPrefunctor.map (HomologicalComplex.cylinder.ι₁ K)

theorem Homotopy.map_eq_of_inverts_homotopyEquivalences {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} [DecidableRel c.Rel] {φ₀ : F ⟶ G} {φ₁ : F ⟶ G} (h : Homotopy φ₀ φ₁) (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X i) (F.X i)] [HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F) (-CategoryTheory.CategoryStruct.id F))] {D : Type u_3} [CategoryTheory.Category.{u_5, u_3} D] (H : CategoryTheory.Functor (HomologicalComplex C c) D) (hH : CategoryTheory.MorphismProperty.IsInvertedBy (HomologicalComplex.homotopyEquivalences C c) H) : H.toPrefunctor.map φ₀ = H.toPrefunctor.map φ₁

If a functor inverts homotopy equivalences, it sends homotopic maps to the same map.