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)
:
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)
theorem
HomologicalComplex.HasHomotopyCofiber.hasBinaryBiproduct
{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)
[self : HomologicalComplex.HasHomotopyCofiber φ]
(i : ι)
(j : ι)
(hij : c.Rel i j)
:
CategoryTheory.Limits.HasBinaryBiproduct (F.X j) (G.X i)
instance
HomologicalComplex.instHasHomotopyCofiberOfHasBinaryBiproducts
{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]
:
Equations
- ⋯ = ⋯
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 (c.next i) then F.X (c.next 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
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 (c.next 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
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)
:
@[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 : ι)
:
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 (c.next i))
{Z : C}
(h : HomologicalComplex.homotopyCofiber.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 : HomologicalComplex C c}
{G : HomologicalComplex C c}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
[DecidableRel c.Rel]
(i : ι)
(hi : ¬c.Rel i (c.next 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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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 : ι)
:
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 (c.next 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 (c.next 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 (c.next 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 (c.next 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)
:
@[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)
:
@[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 : ι)
:
@[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 : ι)
:
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]
:
The homotopy cofiber of a morphism of homological complexes, also known as the mapping cone.
Equations
- One or more equations did not get rendered due to their size.
@[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 : ι)
:
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]
:
The right inclusion G ⟶ homotopyCofiber φ.
Equations
- HomologicalComplex.homotopyCofiber.inr φ = { f := fun (i : ι) => HomologicalComplex.homotopyCofiber.inrX φ i, comm' := ⋯ }
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)
:
The composition φ ≫ mappingCone.inr φ is homotopic to 0.
Equations
- HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc = { hom := fun (i j : ι) => if hij : c.Rel j i then HomologicalComplex.homotopyCofiber.inlX φ i j hij else 0, zero := ⋯, comm := ⋯ }
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)
:
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 (c.next 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)
:
@[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)
:
@[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)
:
@[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.ofEq ⋯).trans
(((HomologicalComplex.homotopyCofiber.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 : HomologicalComplex C c}
{G : HomologicalComplex C c}
[DecidableRel c.Rel]
{φ : F ⟶ G}
{K : HomologicalComplex C c}
(x : (α : G ⟶ K) × Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
(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 : 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.
@[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)]
[HomologicalComplex.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
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 ⟶ K.cylinder
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 ⟶ K.cylinder
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 φ₀ φ₁)
:
K.cylinder ⟶ 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)
:
@[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 φ₀ φ₁)
:
@[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)
:
@[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 φ₀ φ₁)
:
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.cylinder ⟶ 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)
:
@[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))]
:
@[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)
:
@[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))]
:
@[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)]
[HomologicalComplex.HasHomotopyCofiber
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
(i : ι)
(j : ι)
(hij : c.Rel j i)
:
K.X i ⟶ K.cylinder.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.
@[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)]
[HomologicalComplex.HasHomotopyCofiber
(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)
:
@[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 : ι)
:
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))]
:
K.cylinder ⟶ K.cylinder
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))]
:
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 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)]
[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 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)]
[HomologicalComplex.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)]
[HomologicalComplex.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
- HomologicalComplex.cylinder.πCompι₀Homotopy K hc = Homotopy.equivSubZero.symm ((Homotopy.ofEq ⋯).trans (HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopy K))
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 K.cylinder 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)
:
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 : (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy H)
:
H.map (HomologicalComplex.cylinder.ι₀ K) = H.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 : (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy H)
:
H.map φ₀ = H.map φ₁
If a functor inverts homotopy equivalences, it sends homotopic maps to the same map.