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 G : HomologicalComplex C c}
(φ : F ⟶ G)
:
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 : ι) (hij : c.Rel i j) : CategoryTheory.Limits.HasBinaryBiproduct (F.X j) (G.X i)
Instances
instance
HomologicalComplex.instHasHomotopyCofiberOfHasBinaryBiproducts
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{ι : Type u_2}
{c : ComplexShape ι}
{F G : HomologicalComplex C c}
(φ : F ⟶ G)
[CategoryTheory.Limits.HasBinaryBiproducts C]
:
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i : ι)
:
C
The X field of the homological complex homotopyCofiber φ.
Equations
Instances For
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel i j)
[CategoryTheory.Limits.HasBinaryBiproduct (F.X j) (G.X i)]
:
The canonical isomorphism (homotopyCofiber φ).X i ≅ F.X j ⊞ G.X i when c.Rel i j.
Equations
Instances For
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i : ι)
(hi : ¬c.Rel i (c.next i))
:
The canonical isomorphism (homotopyCofiber φ).X i ≅ G.X i when ¬ c.Rel i (c.next i).
Equations
Instances For
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i : ι)
:
The second projection (homotopyCofiber φ).X i ⟶ G.X i.
Equations
Instances For
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i : ι)
:
The right inclusion G.X i ⟶ (homotopyCofiber φ).X i.
Equations
Instances For
@[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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i : ι)
:
@[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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i : ι)
{Z : C}
(h : G.X i ⟶ Z)
:
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i : ι)
(hi : ¬c.Rel i (c.next 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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i : ι)
(hi : ¬c.Rel i (c.next i))
{Z : C}
(h : X φ i ⟶ Z)
:
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel i j)
:
The first projection (homotopyCofiber φ).X i ⟶ F.X j when c.Rel i j.
Equations
Instances For
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel j i)
:
The left inclusion F.X i ⟶ (homotopyCofiber φ).X j when c.Rel j i.
Equations
Instances For
@[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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel j i)
:
CategoryTheory.CategoryStruct.comp (inlX φ i j hij) (fstX φ j i hij) = CategoryTheory.CategoryStruct.id (F.X i)
@[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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel j i)
{Z : C}
(h : F.X i ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (inlX φ i j hij) (CategoryTheory.CategoryStruct.comp (fstX φ j i hij) h) = 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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel j 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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel j i)
{Z : C}
(h : G.X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (inlX φ i j hij) (CategoryTheory.CategoryStruct.comp (sndX φ j) 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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel i j)
:
@[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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel i j)
{Z : C}
(h : F.X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (inrX φ i) (CategoryTheory.CategoryStruct.comp (fstX φ i j hij) h) = CategoryTheory.CategoryStruct.comp 0 h
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
:
The d field of the homological complex homotopyCofiber φ.
Equations
Instances For
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel i j)
{A : C}
{f g : A ⟶ X φ i}
(h₁ : CategoryTheory.CategoryStruct.comp f (fstX φ i j hij) = CategoryTheory.CategoryStruct.comp g (fstX φ i j hij))
(h₂ : CategoryTheory.CategoryStruct.comp f (sndX φ i) = CategoryTheory.CategoryStruct.comp g (sndX φ i))
:
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i : ι)
(hi : ¬c.Rel i (c.next i))
{A : C}
{f g : A ⟶ X φ i}
(h : CategoryTheory.CategoryStruct.comp f (sndX φ i) = CategoryTheory.CategoryStruct.comp g (sndX φ i))
:
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel j i)
{A : C}
{f g : X φ j ⟶ A}
(h₁ : CategoryTheory.CategoryStruct.comp (inlX φ i j hij) f = CategoryTheory.CategoryStruct.comp (inlX φ i j hij) g)
(h₂ : CategoryTheory.CategoryStruct.comp (inrX φ j) f = CategoryTheory.CategoryStruct.comp (inrX φ j) 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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i : ι)
(hi : ¬c.Rel i (c.next i))
{A : C}
{f g : X φ i ⟶ A}
(h : CategoryTheory.CategoryStruct.comp (inrX φ i) f = CategoryTheory.CategoryStruct.comp (inrX φ i) g)
:
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j k : ι)
(hij : c.Rel i j)
(hjk : c.Rel j k)
:
CategoryTheory.CategoryStruct.comp (d φ i j) (fstX φ j k hjk) = -CategoryTheory.CategoryStruct.comp (fstX φ i j hij) (F.d j k)
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[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 (d φ i j) (CategoryTheory.CategoryStruct.comp (fstX φ j k hjk) h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (fstX φ i j hij) (F.d j k)) 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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel i j)
:
CategoryTheory.CategoryStruct.comp (d φ i j) (sndX φ j) = CategoryTheory.CategoryStruct.comp (fstX φ i j hij) (φ.f j) + CategoryTheory.CategoryStruct.comp (sndX φ i) (G.d i j)
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel i j)
{Z : C}
(h : G.X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (d φ i j) (CategoryTheory.CategoryStruct.comp (sndX φ j) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (fstX φ i j hij) (φ.f j) + CategoryTheory.CategoryStruct.comp (sndX φ i) (G.d i 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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j k : ι)
(hij : c.Rel i j)
(hjk : c.Rel j k)
:
CategoryTheory.CategoryStruct.comp (inlX φ j i hij) (d φ i j) = -CategoryTheory.CategoryStruct.comp (F.d j k) (inlX φ k j hjk) + CategoryTheory.CategoryStruct.comp (φ.f j) (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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j k : ι)
(hij : c.Rel i j)
(hjk : c.Rel j k)
{Z : C}
(h : X φ j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (inlX φ j i hij) (CategoryTheory.CategoryStruct.comp (d φ i j) h) = CategoryTheory.CategoryStruct.comp
(-CategoryTheory.CategoryStruct.comp (F.d j k) (inlX φ k j hjk) + CategoryTheory.CategoryStruct.comp (φ.f j) (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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel i j)
(hj : ¬c.Rel j (c.next j))
:
CategoryTheory.CategoryStruct.comp (inlX φ j i hij) (d φ i j) = CategoryTheory.CategoryStruct.comp (φ.f j) (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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : c.Rel i j)
(hj : ¬c.Rel j (c.next j))
{Z : C}
(h : X φ j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (inlX φ j i hij) (CategoryTheory.CategoryStruct.comp (d φ i j) h) = CategoryTheory.CategoryStruct.comp (φ.f j) (CategoryTheory.CategoryStruct.comp (inrX φ j) h)
theorem
HomologicalComplex.homotopyCofiber.shape
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{ι : Type u_2}
{c : ComplexShape ι}
{F G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
(hij : ¬c.Rel i j)
:
@[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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
:
CategoryTheory.CategoryStruct.comp (inrX φ i) (d φ i j) = CategoryTheory.CategoryStruct.comp (G.d i j) (inrX φ j)
@[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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i j : ι)
{Z : C}
(h : X φ j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (inrX φ i) (CategoryTheory.CategoryStruct.comp (d φ i j) h) = CategoryTheory.CategoryStruct.comp (G.d i j) (CategoryTheory.CategoryStruct.comp (inrX φ j) h)
noncomputable def
HomologicalComplex.homotopyCofiber
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{ι : Type u_2}
{c : ComplexShape ι}
{F G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
:
The homotopy cofiber of a morphism of homological complexes, also known as the mapping cone.
Equations
Instances For
@[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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
:
The right inclusion G ⟶ homotopyCofiber φ.
Equations
Instances For
@[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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j)
:
Homotopy (CategoryTheory.CategoryStruct.comp φ (inr φ)) 0
The composition φ ≫ mappingCone.inr φ is homotopic to 0.
Equations
Instances For
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j)
(i j : ι)
(hij : c.Rel j i)
:
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j)
(i j : ι)
(hij : ¬c.Rel j i)
:
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 G K : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(α : G ⟶ K)
(hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
:
The morphism homotopyCofiber φ ⟶ K that is induced by a morphism α : G ⟶ K
and a homotopy hα : Homotopy (φ ≫ α) 0.
Equations
Instances For
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 G K : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(α : G ⟶ K)
(hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
(j k : ι)
(hjk : c.Rel j k)
:
(desc φ α hα).f j = CategoryTheory.CategoryStruct.comp (fstX φ j k hjk) (hα.hom k j) + CategoryTheory.CategoryStruct.comp (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 G K : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(α : G ⟶ K)
(hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
(j : ι)
(hj : ¬c.Rel j (c.next j))
:
@[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 G K : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(α : G ⟶ K)
(hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
(i j : ι)
(hjk : c.Rel j i)
:
@[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 G K : HomologicalComplex C c}
(φ : F ⟶ G)
[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 (inlX φ i j hjk) (CategoryTheory.CategoryStruct.comp ((desc φ α hα).f j) h) = CategoryTheory.CategoryStruct.comp (hα.hom i j) 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 G K : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(α : G ⟶ K)
(hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
(i : ι)
:
@[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 G K : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(α : G ⟶ K)
(hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
(i : ι)
{Z : C}
(h : K.X i ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (inrX φ i) (CategoryTheory.CategoryStruct.comp ((desc φ α hα).f i) h) = CategoryTheory.CategoryStruct.comp (α.f i) 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 G K : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(α : G ⟶ K)
(hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
:
@[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 G K : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(α : G ⟶ K)
(hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
{Z : HomologicalComplex C c}
(h : K ⟶ Z)
:
@[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 G K : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(α : G ⟶ K)
(hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
(hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j)
(i j : ι)
:
CategoryTheory.CategoryStruct.comp ((inrCompHomotopy φ hc).hom i j) ((desc φ α hα).f j) = hα.hom i j
@[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 G K : HomologicalComplex C c}
(φ : F ⟶ G)
[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 ((inrCompHomotopy φ hc).hom i j)
(CategoryTheory.CategoryStruct.comp ((desc φ α hα).f j) h) = CategoryTheory.CategoryStruct.comp (hα.hom i j) h
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 G K : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(f : homotopyCofiber φ ⟶ K)
(hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j)
:
f = desc φ (CategoryTheory.CategoryStruct.comp (inr φ) f)
((Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))
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 G : HomologicalComplex C c}
[DecidableRel c.Rel]
{φ : F ⟶ G}
{K : HomologicalComplex C c}
(x y : (α : G ⟶ K) × Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
:
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 G : HomologicalComplex C c}
(φ : F ⟶ G)
[HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(K : HomologicalComplex C c)
(hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j)
:
Morphisms homotopyCofiber φ ⟶ K are uniquely determined by
a morphism α : G ⟶ K and a homotopy from φ ≫ α to 0.
Equations
Instances For
@[reducible, inline]
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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
:
The cylinder object of a homological complex K is the homotopy cofiber
of the morphism biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K.
Equations
Instances For
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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
:
The left inclusion K ⟶ K.cylinder.
Equations
Instances For
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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
:
The right inclusion K ⟶ K.cylinder.
Equations
Instances For
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 K : HomologicalComplex C c}
[DecidableRel c.Rel]
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(φ₀ φ₁ : K ⟶ F)
(h : Homotopy φ₀ φ₁)
:
The morphism K.cylinder ⟶ F that is induced by two morphisms φ₀ φ₁ : K ⟶ F
and a homotopy h : Homotopy φ₀ φ₁.
Equations
Instances For
@[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 K : HomologicalComplex C c}
[DecidableRel c.Rel]
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(φ₀ φ₁ : K ⟶ F)
(h : Homotopy φ₀ φ₁)
:
@[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 K : HomologicalComplex C c}
[DecidableRel c.Rel]
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(φ₀ φ₁ : K ⟶ F)
(h : Homotopy φ₀ φ₁)
{Z : HomologicalComplex C c}
(h✝ : F ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (ι₀ K) (CategoryTheory.CategoryStruct.comp (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 K : HomologicalComplex C c}
[DecidableRel c.Rel]
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(φ₀ φ₁ : K ⟶ F)
(h : Homotopy φ₀ φ₁)
:
@[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 K : HomologicalComplex C c}
[DecidableRel c.Rel]
[∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(φ₀ φ₁ : K ⟶ F)
(h : Homotopy φ₀ φ₁)
{Z : HomologicalComplex C c}
(h✝ : F ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (ι₁ K) (CategoryTheory.CategoryStruct.comp (desc φ₀ φ₁ h) h✝) = CategoryTheory.CategoryStruct.comp φ₁ 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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
:
The projection π : K.cylinder ⟶ K.
Equations
Instances For
@[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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id 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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
{Z : HomologicalComplex C c}
(h : K ⟶ Z)
:
@[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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id 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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
{Z : HomologicalComplex C c}
(h : K ⟶ Z)
:
@[reducible, inline]
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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(i j : ι)
(hij : c.Rel j i)
:
The left inclusion K.X i ⟶ K.cylinder.X j when c.Rel j i.
Equations
Instances For
@[reducible, inline]
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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(i : ι)
:
The right inclusion (K ⊞ K).X i ⟶ K.cylinder.X i.
Equations
Instances For
@[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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(i j : ι)
(hij : c.Rel j 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)]
[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 (inlX K i j hij) (CategoryTheory.CategoryStruct.comp ((π K).f j) h) = CategoryTheory.CategoryStruct.comp 0 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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(i : ι)
:
@[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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(i : ι)
{Z : C}
(h : K.X i ⟶ Z)
:
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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
:
A null homotopic map K.cylinder ⟶ K.cylinder which identifies to
π K ≫ ι₀ K - 𝟙 _, see nullHomotopicMap_eq.
Equations
Instances For
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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
:
Homotopy (nullHomotopicMap K) 0
The obvious homotopy from nullHomotopicMap K to zero.
Equations
Instances For
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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(i j : ι)
(hij : c.Rel j i)
:
CategoryTheory.CategoryStruct.comp (inlX K i j hij) ((nullHomotopicMap K).f j) = CategoryTheory.CategoryStruct.comp (inlX K i j hij)
((CategoryTheory.CategoryStruct.comp (π K) (ι₀ K) - CategoryTheory.CategoryStruct.id K.cylinder).f j)
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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j)
(j : ι)
:
CategoryTheory.CategoryStruct.comp (inrX K j) ((nullHomotopicMap K).f j) = CategoryTheory.CategoryStruct.comp (inrX K j)
((CategoryTheory.CategoryStruct.comp (π K) (ι₀ K) - CategoryTheory.CategoryStruct.id K.cylinder).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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j)
:
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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j)
:
The homotopy between π K ≫ ι₀ K and 𝟙 K.cylinder.
Equations
Instances For
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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j)
:
The homotopy equivalence between K.cylinder and K.
Equations
Instances For
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)]
[HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j)
:
The homotopy between cylinder.ι₀ K and cylinder.ι₁ K.
Equations
Instances For
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)]
[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 : (homotopyEquivalences C c).IsInvertedBy H)
:
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 G : HomologicalComplex C c}
[DecidableRel c.Rel]
{φ₀ φ₁ : 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 : (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy H)
:
If a functor inverts homotopy equivalences, it sends homotopic maps to the same map.