The mapping cone of a morphism of cochain complexes #
In this file, we study the homotopy cofiber HomologicalComplex.homotopyCofiber
of a morphism φ : F ⟶ G of cochain complexes indexed by ℤ. In this case,
we redefine it as CochainComplex.mappingCone φ. The API involves definitions
mappingCone.inl φ : Cochain F (mappingCone φ) (-1),mappingCone.inr φ : G ⟶ mappingCone φ,mappingCone.fst φ : Cocycle (mappingCone φ) F 1andmappingCone.snd φ : Cochain (mappingCone φ) G 0.
instance
CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{ι : Type u_2}
[AddRightCancelSemigroup ι]
[One ι]
{F : CochainComplex C ι}
{G : CochainComplex C ι}
(φ : F ⟶ G)
[∀ (p : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X (p + 1)) (G.X p)]
:
Equations
- ⋯ = ⋯
noncomputable def
CochainComplex.mappingCone
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
The mapping cone of a morphism of cochain complexes indexed by ℤ.
Instances For
noncomputable def
CochainComplex.mappingCone.inl
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
The left inclusion in the mapping cone, as a cochain of degree -1.
Equations
- CochainComplex.mappingCone.inl φ = CochainComplex.HomComplex.Cochain.mk fun (p q : ℤ) (hpq : p + -1 = q) => HomologicalComplex.homotopyCofiber.inlX φ p q ⋯
Instances For
noncomputable def
CochainComplex.mappingCone.inr
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
The right inclusion in the mapping cone.
Instances For
noncomputable def
CochainComplex.mappingCone.fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
The first projection from the mapping cone, as a cocyle of degree 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CochainComplex.mappingCone.snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
The second projection from the mapping cone, as a cochain of degree 0.
Equations
Instances For
@[simp]
theorem
CochainComplex.mappingCone.inl_v_fst_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(p : ℤ)
(q : ℤ)
(hpq : q + 1 = p)
{Z : C}
(h : F.X p ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q ⋯)
(CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v q p hpq) h) = h
@[simp]
theorem
CochainComplex.mappingCone.inl_v_fst_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(p : ℤ)
(q : ℤ)
(hpq : q + 1 = p)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q ⋯)
((↑(CochainComplex.mappingCone.fst φ)).v q p hpq) = CategoryTheory.CategoryStruct.id (F.X p)
@[simp]
theorem
CochainComplex.mappingCone.inl_v_snd_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(p : ℤ)
(q : ℤ)
(hpq : p + -1 = q)
{Z : C}
(h : G.X q ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q hpq)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v q q ⋯) h) = CategoryTheory.CategoryStruct.comp 0 h
@[simp]
theorem
CochainComplex.mappingCone.inl_v_snd_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(p : ℤ)
(q : ℤ)
(hpq : p + -1 = q)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q hpq)
((CochainComplex.mappingCone.snd φ).v q q ⋯) = 0
@[simp]
theorem
CochainComplex.mappingCone.inr_f_fst_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(p : ℤ)
(q : ℤ)
(hpq : p + 1 = q)
{Z : C}
(h : F.X q ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
(CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v p q hpq) h) = CategoryTheory.CategoryStruct.comp 0 h
@[simp]
theorem
CochainComplex.mappingCone.inr_f_fst_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(p : ℤ)
(q : ℤ)
(hpq : p + 1 = q)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
((↑(CochainComplex.mappingCone.fst φ)).v p q hpq) = 0
@[simp]
theorem
CochainComplex.mappingCone.inr_f_snd_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(p : ℤ)
{Z : C}
(h : G.X p ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v p p ⋯) h) = h
@[simp]
theorem
CochainComplex.mappingCone.inr_f_snd_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(p : ℤ)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
((CochainComplex.mappingCone.snd φ).v p p ⋯) = CategoryTheory.CategoryStruct.id (G.X p)
@[simp]
theorem
CochainComplex.mappingCone.inl_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
@[simp]
theorem
CochainComplex.mappingCone.inl_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
(CochainComplex.mappingCone.inl φ).comp (CochainComplex.mappingCone.snd φ) ⋯ = 0
@[simp]
theorem
CochainComplex.mappingCone.inr_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
@[simp]
theorem
CochainComplex.mappingCone.inr_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
In order to obtain identities of cochains involving inl, inr, fst and snd,
it is often convenient to use an ext lemma, and use simp lemmas like inl_v_f_fst_v,
but it is sometimes possible to get identities of cochains by using rewrites of
identities of cochains like inl_fst. Then, similarly as in category theory,
if we associate the compositions of cochains to the right as much as possible,
it is also interesting to have reassoc variants of lemmas, like inl_fst_assoc.
@[simp]
theorem
CochainComplex.mappingCone.inl_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{d : ℤ}
{e : ℤ}
(γ : CochainComplex.HomComplex.Cochain F K d)
(he : 1 + d = e)
:
(CochainComplex.mappingCone.inl φ).comp ((↑(CochainComplex.mappingCone.fst φ)).comp γ he) ⋯ = γ
@[simp]
theorem
CochainComplex.mappingCone.inl_snd_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{d : ℤ}
{e : ℤ}
{f : ℤ}
(γ : CochainComplex.HomComplex.Cochain G K d)
(he : 0 + d = e)
(hf : -1 + e = f)
:
(CochainComplex.mappingCone.inl φ).comp ((CochainComplex.mappingCone.snd φ).comp γ he) hf = 0
@[simp]
theorem
CochainComplex.mappingCone.inr_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{d : ℤ}
{e : ℤ}
{f : ℤ}
(γ : CochainComplex.HomComplex.Cochain F K d)
(he : 1 + d = e)
(hf : 0 + e = f)
:
(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp
((↑(CochainComplex.mappingCone.fst φ)).comp γ he) hf = 0
@[simp]
theorem
CochainComplex.mappingCone.inr_snd_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{d : ℤ}
{e : ℤ}
(γ : CochainComplex.HomComplex.Cochain G K d)
(he : 0 + d = e)
:
(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp
((CochainComplex.mappingCone.snd φ).comp γ he) ⋯ = γ
theorem
CochainComplex.mappingCone.ext_to
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(hij : i + 1 = j)
{A : C}
{f : A ⟶ (CochainComplex.mappingCone φ).X i}
{g : A ⟶ (CochainComplex.mappingCone φ).X i}
(h₁ : CategoryTheory.CategoryStruct.comp f ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) = CategoryTheory.CategoryStruct.comp g ((↑(CochainComplex.mappingCone.fst φ)).v i j hij))
(h₂ : CategoryTheory.CategoryStruct.comp f ((CochainComplex.mappingCone.snd φ).v i i ⋯) = CategoryTheory.CategoryStruct.comp g ((CochainComplex.mappingCone.snd φ).v i i ⋯))
:
f = g
theorem
CochainComplex.mappingCone.ext_to_iff
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(hij : i + 1 = j)
{A : C}
(f : A ⟶ (CochainComplex.mappingCone φ).X i)
(g : A ⟶ (CochainComplex.mappingCone φ).X i)
:
f = g ↔ CategoryTheory.CategoryStruct.comp f ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) = CategoryTheory.CategoryStruct.comp g ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) ∧ CategoryTheory.CategoryStruct.comp f ((CochainComplex.mappingCone.snd φ).v i i ⋯) = CategoryTheory.CategoryStruct.comp g ((CochainComplex.mappingCone.snd φ).v i i ⋯)
theorem
CochainComplex.mappingCone.ext_from
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(hij : j + 1 = i)
{A : C}
{f : (CochainComplex.mappingCone φ).X j ⟶ A}
{g : (CochainComplex.mappingCone φ).X j ⟶ A}
(h₁ : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j ⋯) f = CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j ⋯) g)
(h₂ : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f j) f = CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f j) g)
:
f = g
theorem
CochainComplex.mappingCone.ext_from_iff
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(hij : j + 1 = i)
{A : C}
(f : (CochainComplex.mappingCone φ).X j ⟶ A)
(g : (CochainComplex.mappingCone φ).X j ⟶ A)
:
f = g ↔ CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j ⋯) f = CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j ⋯) g ∧ CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f j) f = CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f j) g
theorem
CochainComplex.mappingCone.ext_cochain_to_iff
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(hij : i + 1 = j)
{K : CochainComplex C ℤ}
{γ₁ : CochainComplex.HomComplex.Cochain K (CochainComplex.mappingCone φ) i}
{γ₂ : CochainComplex.HomComplex.Cochain K (CochainComplex.mappingCone φ) i}
:
γ₁ = γ₂ ↔ γ₁.comp (↑(CochainComplex.mappingCone.fst φ)) hij = γ₂.comp (↑(CochainComplex.mappingCone.fst φ)) hij ∧ γ₁.comp (CochainComplex.mappingCone.snd φ) ⋯ = γ₂.comp (CochainComplex.mappingCone.snd φ) ⋯
theorem
CochainComplex.mappingCone.ext_cochain_from_iff
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(hij : i + 1 = j)
{K : CochainComplex C ℤ}
{γ₁ : CochainComplex.HomComplex.Cochain (CochainComplex.mappingCone φ) K j}
{γ₂ : CochainComplex.HomComplex.Cochain (CochainComplex.mappingCone φ) K j}
:
γ₁ = γ₂ ↔ (CochainComplex.mappingCone.inl φ).comp γ₁ ⋯ = (CochainComplex.mappingCone.inl φ).comp γ₂ ⋯ ∧ (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp γ₁ ⋯ = (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp γ₂ ⋯
theorem
CochainComplex.mappingCone.id
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
(↑(CochainComplex.mappingCone.fst φ)).comp (CochainComplex.mappingCone.inl φ) ⋯ + (CochainComplex.mappingCone.snd φ).comp (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ))
⋯ = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone φ))
theorem
CochainComplex.mappingCone.id_X
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(p : ℤ)
(q : ℤ)
(hpq : p + 1 = q)
:
CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v p q hpq)
((CochainComplex.mappingCone.inl φ).v q p ⋯) + CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v p p ⋯)
((CochainComplex.mappingCone.inr φ).f p) = CategoryTheory.CategoryStruct.id ((CochainComplex.mappingCone φ).X p)
theorem
CochainComplex.mappingCone.inl_v_d_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(k : ℤ)
(hij : i + -1 = j)
(hik : k + -1 = i)
{Z : C}
(h : (CochainComplex.mappingCone φ).X i ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j hij)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d j i) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (φ.f i) ((CochainComplex.mappingCone.inr φ).f i) - CategoryTheory.CategoryStruct.comp (F.d i k) ((CochainComplex.mappingCone.inl φ).v k i hik))
h
theorem
CochainComplex.mappingCone.inl_v_d
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(k : ℤ)
(hij : i + -1 = j)
(hik : k + -1 = i)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j hij)
((CochainComplex.mappingCone φ).d j i) = CategoryTheory.CategoryStruct.comp (φ.f i) ((CochainComplex.mappingCone.inr φ).f i) - CategoryTheory.CategoryStruct.comp (F.d i k) ((CochainComplex.mappingCone.inl φ).v k i hik)
@[simp]
theorem
CochainComplex.mappingCone.inr_f_d_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(n₁ : ℤ)
(n₂ : ℤ)
{Z : C}
(h : (CochainComplex.mappingCone φ).X n₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f n₁)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d n₁ n₂) h) = CategoryTheory.CategoryStruct.comp (G.d n₁ n₂)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f n₂) h)
@[simp]
theorem
CochainComplex.mappingCone.inr_f_d
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(n₁ : ℤ)
(n₂ : ℤ)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f n₁) ((CochainComplex.mappingCone φ).d n₁ n₂) = CategoryTheory.CategoryStruct.comp (G.d n₁ n₂) ((CochainComplex.mappingCone.inr φ).f n₂)
theorem
CochainComplex.mappingCone.d_fst_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(k : ℤ)
(hij : i + 1 = j)
(hjk : j + 1 = k)
{Z : C}
(h : F.X k ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d i j)
(CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v j k hjk) h) = CategoryTheory.CategoryStruct.comp
(-CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) (F.d j k)) h
theorem
CochainComplex.mappingCone.d_fst_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(k : ℤ)
(hij : i + 1 = j)
(hjk : j + 1 = k)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d i j)
((↑(CochainComplex.mappingCone.fst φ)).v j k hjk) = -CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) (F.d j k)
@[simp]
theorem
CochainComplex.mappingCone.d_fst_v'_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(hij : i + 1 = j)
{Z : C}
(h : F.X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d (i - 1) i)
(CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) h) = CategoryTheory.CategoryStruct.comp
(-CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v (i - 1) i ⋯) (F.d i j)) h
@[simp]
theorem
CochainComplex.mappingCone.d_fst_v'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(hij : i + 1 = j)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d (i - 1) i)
((↑(CochainComplex.mappingCone.fst φ)).v i j hij) = -CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v (i - 1) i ⋯) (F.d i j)
theorem
CochainComplex.mappingCone.d_snd_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(hij : i + 1 = j)
{Z : C}
(h : G.X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d i j)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v j j ⋯) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) (φ.f j) + CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v i i ⋯) (G.d i j))
h
theorem
CochainComplex.mappingCone.d_snd_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i : ℤ)
(j : ℤ)
(hij : i + 1 = j)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d i j) ((CochainComplex.mappingCone.snd φ).v j j ⋯) = CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) (φ.f j) + CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v i i ⋯) (G.d i j)
@[simp]
theorem
CochainComplex.mappingCone.d_snd_v'_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(n : ℤ)
{Z : C}
(h : G.X n ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d (n - 1) n)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v n n ⋯) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v (n - 1) n ⋯) (φ.f n) + CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v (n - 1) (n - 1) ⋯) (G.d (n - 1) n))
h
@[simp]
theorem
CochainComplex.mappingCone.d_snd_v'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(n : ℤ)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d (n - 1) n)
((CochainComplex.mappingCone.snd φ).v n n ⋯) = CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v (n - 1) n ⋯) (φ.f n) + CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v (n - 1) (n - 1) ⋯) (G.d (n - 1) n)
@[simp]
theorem
CochainComplex.mappingCone.δ_inl
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
@[simp]
theorem
CochainComplex.mappingCone.δ_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
noncomputable def
CochainComplex.mappingCone.descCochain
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain F K m)
(β : CochainComplex.HomComplex.Cochain G K n)
(h : m + 1 = n)
:
Given φ : F ⟶ G, this is the cochain in Cochain (mappingCone φ) K n that is
constructed from two cochains α : Cochain F K m (with m + 1 = n) and β : Cochain F K n.
Equations
- CochainComplex.mappingCone.descCochain φ α β h = (↑(CochainComplex.mappingCone.fst φ)).comp α ⋯ + (CochainComplex.mappingCone.snd φ).comp β ⋯
Instances For
@[simp]
theorem
CochainComplex.mappingCone.inl_descCochain
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain F K m)
(β : CochainComplex.HomComplex.Cochain G K n)
(h : m + 1 = n)
:
(CochainComplex.mappingCone.inl φ).comp (CochainComplex.mappingCone.descCochain φ α β h) ⋯ = α
@[simp]
theorem
CochainComplex.mappingCone.inr_descCochain
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain F K m)
(β : CochainComplex.HomComplex.Cochain G K n)
(h : m + 1 = n)
:
(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp
(CochainComplex.mappingCone.descCochain φ α β h) ⋯ = β
@[simp]
theorem
CochainComplex.mappingCone.inl_v_descCochain_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain F K m)
(β : CochainComplex.HomComplex.Cochain G K n)
(h : m + 1 = n)
(p₁ : ℤ)
(p₂ : ℤ)
(p₃ : ℤ)
(h₁₂ : p₁ + -1 = p₂)
(h₂₃ : p₂ + n = p₃)
{Z : C}
(h : K.X p₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p₁ p₂ h₁₂)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.descCochain φ α β h✝).v p₂ p₃ h₂₃) h) = CategoryTheory.CategoryStruct.comp (α.v p₁ p₃ ⋯) h
@[simp]
theorem
CochainComplex.mappingCone.inl_v_descCochain_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain F K m)
(β : CochainComplex.HomComplex.Cochain G K n)
(h : m + 1 = n)
(p₁ : ℤ)
(p₂ : ℤ)
(p₃ : ℤ)
(h₁₂ : p₁ + -1 = p₂)
(h₂₃ : p₂ + n = p₃)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p₁ p₂ h₁₂)
((CochainComplex.mappingCone.descCochain φ α β h).v p₂ p₃ h₂₃) = α.v p₁ p₃ ⋯
@[simp]
theorem
CochainComplex.mappingCone.inr_f_descCochain_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain F K m)
(β : CochainComplex.HomComplex.Cochain G K n)
(h : m + 1 = n)
(p₁ : ℤ)
(p₂ : ℤ)
(h₁₂ : p₁ + n = p₂)
{Z : C}
(h : K.X p₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p₁)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.descCochain φ α β h✝).v p₁ p₂ h₁₂) h) = CategoryTheory.CategoryStruct.comp (β.v p₁ p₂ h₁₂) h
@[simp]
theorem
CochainComplex.mappingCone.inr_f_descCochain_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain F K m)
(β : CochainComplex.HomComplex.Cochain G K n)
(h : m + 1 = n)
(p₁ : ℤ)
(p₂ : ℤ)
(h₁₂ : p₁ + n = p₂)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p₁)
((CochainComplex.mappingCone.descCochain φ α β h).v p₁ p₂ h₁₂) = β.v p₁ p₂ h₁₂
theorem
CochainComplex.mappingCone.δ_descCochain
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain F K m)
(β : CochainComplex.HomComplex.Cochain G K n)
(h : m + 1 = n)
(n' : ℤ)
(hn' : n + 1 = n')
:
CochainComplex.HomComplex.δ n n' (CochainComplex.mappingCone.descCochain φ α β h) = (↑(CochainComplex.mappingCone.fst φ)).comp
(CochainComplex.HomComplex.δ m n α + n'.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp β ⋯) ⋯ + (CochainComplex.mappingCone.snd φ).comp (CochainComplex.HomComplex.δ n n' β) ⋯
@[simp]
theorem
CochainComplex.mappingCone.descCocycle_coe
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain F K m)
(β : CochainComplex.HomComplex.Cocycle G K n)
(h : m + 1 = n)
(eq : CochainComplex.HomComplex.δ m n α = n.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯)
:
↑(CochainComplex.mappingCone.descCocycle φ α β h eq) = CochainComplex.mappingCone.descCochain φ α (↑β) h
noncomputable def
CochainComplex.mappingCone.descCocycle
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain F K m)
(β : CochainComplex.HomComplex.Cocycle G K n)
(h : m + 1 = n)
(eq : CochainComplex.HomComplex.δ m n α = n.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯)
:
Given φ : F ⟶ G, this is the cocycle in Cocycle (mappingCone φ) K n that is
constructed from α : Cochain F K m (with m + 1 = n) and β : Cocycle F K n,
when a suitable cocycle relation is satisfied.
Equations
- CochainComplex.mappingCone.descCocycle φ α β h eq = CochainComplex.HomComplex.Cocycle.mk (CochainComplex.mappingCone.descCochain φ α (↑β) h) (n + 1) ⋯ ⋯
Instances For
noncomputable def
CochainComplex.mappingCone.desc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cochain F K (-1))
(β : G ⟶ K)
(eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
:
Given φ : F ⟶ G, this is the morphism mappingCone φ ⟶ K that is constructed
from a cochain α : Cochain F K (-1) and a morphism β : G ⟶ K such that
δ (-1) 0 α = Cochain.ofHom (φ ≫ β).
Equations
Instances For
@[simp]
theorem
CochainComplex.mappingCone.ofHom_desc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cochain F K (-1))
(β : G ⟶ K)
(eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
:
@[simp]
theorem
CochainComplex.mappingCone.inl_v_desc_f_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cochain F K (-1))
(β : G ⟶ K)
(eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
(p : ℤ)
(q : ℤ)
(h : p + -1 = q)
{Z : C}
(h : K.X q ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q h✝)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.desc φ α β eq).f q) h) = CategoryTheory.CategoryStruct.comp (α.v p q h✝) h
@[simp]
theorem
CochainComplex.mappingCone.inl_v_desc_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cochain F K (-1))
(β : G ⟶ K)
(eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
(p : ℤ)
(q : ℤ)
(h : p + -1 = q)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q h)
((CochainComplex.mappingCone.desc φ α β eq).f q) = α.v p q h
theorem
CochainComplex.mappingCone.inl_desc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cochain F K (-1))
(β : G ⟶ K)
(eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
:
(CochainComplex.mappingCone.inl φ).comp
(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.desc φ α β eq)) ⋯ = α
@[simp]
theorem
CochainComplex.mappingCone.inr_f_desc_f_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cochain F K (-1))
(β : G ⟶ K)
(eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
(p : ℤ)
{Z : C}
(h : K.X p ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.desc φ α β eq).f p) h) = CategoryTheory.CategoryStruct.comp (β.f p) h
@[simp]
theorem
CochainComplex.mappingCone.inr_f_desc_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cochain F K (-1))
(β : G ⟶ K)
(eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
(p : ℤ)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
((CochainComplex.mappingCone.desc φ α β eq).f p) = β.f p
@[simp]
theorem
CochainComplex.mappingCone.inr_desc_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cochain F K (-1))
(β : G ⟶ K)
(eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
{Z : CochainComplex C ℤ}
(h : K ⟶ Z)
:
@[simp]
theorem
CochainComplex.mappingCone.inr_desc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cochain F K (-1))
(β : G ⟶ K)
(eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
:
theorem
CochainComplex.mappingCone.desc_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cochain F K (-1))
(β : G ⟶ K)
(eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
(p : ℤ)
(q : ℤ)
(hpq : p + 1 = q)
:
(CochainComplex.mappingCone.desc φ α β eq).f p = CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v p q hpq) (α.v q p ⋯) + CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v p p ⋯) (β.f p)
noncomputable def
CochainComplex.mappingCone.descHomotopy
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(f₁ : CochainComplex.mappingCone φ ⟶ K)
(f₂ : CochainComplex.mappingCone φ ⟶ K)
(γ₁ : CochainComplex.HomComplex.Cochain F K (-2))
(γ₂ : CochainComplex.HomComplex.Cochain G K (-1))
(h₁ : (CochainComplex.mappingCone.inl φ).comp (CochainComplex.HomComplex.Cochain.ofHom f₁) ⋯ = CochainComplex.HomComplex.δ (-2) (-1) γ₁ + (CochainComplex.HomComplex.Cochain.ofHom φ).comp γ₂ ⋯ + (CochainComplex.mappingCone.inl φ).comp (CochainComplex.HomComplex.Cochain.ofHom f₂) ⋯)
(h₂ : CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) f₁) = CochainComplex.HomComplex.δ (-1) 0 γ₂ + CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) f₂))
:
Homotopy f₁ f₂
Constructor for homotopies between morphisms from a mapping cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CochainComplex.mappingCone.liftCochain
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain K F m)
(β : CochainComplex.HomComplex.Cochain K G n)
(h : n + 1 = m)
:
Given φ : F ⟶ G, this is the cochain in Cochain (mappingCone φ) K n that is
constructed from two cochains α : Cochain F K m (with m + 1 = n) and β : Cochain F K n.
Equations
- CochainComplex.mappingCone.liftCochain φ α β h = α.comp (CochainComplex.mappingCone.inl φ) ⋯ + β.comp (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)) ⋯
Instances For
@[simp]
theorem
CochainComplex.mappingCone.liftCochain_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain K F m)
(β : CochainComplex.HomComplex.Cochain K G n)
(h : n + 1 = m)
:
(CochainComplex.mappingCone.liftCochain φ α β h).comp (↑(CochainComplex.mappingCone.fst φ)) h = α
@[simp]
theorem
CochainComplex.mappingCone.liftCochain_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain K F m)
(β : CochainComplex.HomComplex.Cochain K G n)
(h : n + 1 = m)
:
(CochainComplex.mappingCone.liftCochain φ α β h).comp (CochainComplex.mappingCone.snd φ) ⋯ = β
@[simp]
theorem
CochainComplex.mappingCone.liftCochain_v_fst_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain K F m)
(β : CochainComplex.HomComplex.Cochain K G n)
(h : n + 1 = m)
(p₁ : ℤ)
(p₂ : ℤ)
(p₃ : ℤ)
(h₁₂ : p₁ + n = p₂)
(h₂₃ : p₂ + 1 = p₃)
{Z : C}
(h : F.X p₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h✝).v p₁ p₂ h₁₂)
(CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v p₂ p₃ h₂₃) h) = CategoryTheory.CategoryStruct.comp (α.v p₁ p₃ ⋯) h
@[simp]
theorem
CochainComplex.mappingCone.liftCochain_v_fst_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain K F m)
(β : CochainComplex.HomComplex.Cochain K G n)
(h : n + 1 = m)
(p₁ : ℤ)
(p₂ : ℤ)
(p₃ : ℤ)
(h₁₂ : p₁ + n = p₂)
(h₂₃ : p₂ + 1 = p₃)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂)
((↑(CochainComplex.mappingCone.fst φ)).v p₂ p₃ h₂₃) = α.v p₁ p₃ ⋯
@[simp]
theorem
CochainComplex.mappingCone.liftCochain_v_snd_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain K F m)
(β : CochainComplex.HomComplex.Cochain K G n)
(h : n + 1 = m)
(p₁ : ℤ)
(p₂ : ℤ)
(h₁₂ : p₁ + n = p₂)
{Z : C}
(h : G.X p₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h✝).v p₁ p₂ h₁₂)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v p₂ p₂ ⋯) h) = CategoryTheory.CategoryStruct.comp (β.v p₁ p₂ h₁₂) h
@[simp]
theorem
CochainComplex.mappingCone.liftCochain_v_snd_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain K F m)
(β : CochainComplex.HomComplex.Cochain K G n)
(h : n + 1 = m)
(p₁ : ℤ)
(p₂ : ℤ)
(h₁₂ : p₁ + n = p₂)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂)
((CochainComplex.mappingCone.snd φ).v p₂ p₂ ⋯) = β.v p₁ p₂ h₁₂
theorem
CochainComplex.mappingCone.δ_liftCochain
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain K F m)
(β : CochainComplex.HomComplex.Cochain K G n)
(h : n + 1 = m)
(m' : ℤ)
(hm' : m + 1 = m')
:
CochainComplex.HomComplex.δ n m (CochainComplex.mappingCone.liftCochain φ α β h) = -(CochainComplex.HomComplex.δ m m' α).comp (CochainComplex.mappingCone.inl φ) ⋯ + (CochainComplex.HomComplex.δ n m β + α.comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯).comp
(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)) ⋯
@[simp]
theorem
CochainComplex.mappingCone.liftCocycle_coe
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cocycle K F m)
(β : CochainComplex.HomComplex.Cochain K G n)
(h : n + 1 = m)
(eq : CochainComplex.HomComplex.δ n m β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
:
↑(CochainComplex.mappingCone.liftCocycle φ α β h eq) = CochainComplex.mappingCone.liftCochain φ (↑α) β h
noncomputable def
CochainComplex.mappingCone.liftCocycle
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cocycle K F m)
(β : CochainComplex.HomComplex.Cochain K G n)
(h : n + 1 = m)
(eq : CochainComplex.HomComplex.δ n m β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
:
Given φ : F ⟶ G, this is the cocycle in Cocycle K (mappingCone φ) n that is
constructed from α : Cochain K F m (with n + 1 = m) and β : Cocycle K G n,
when a suitable cocycle relation is satisfied.
Equations
- CochainComplex.mappingCone.liftCocycle φ α β h eq = CochainComplex.HomComplex.Cocycle.mk (CochainComplex.mappingCone.liftCochain φ (↑α) β h) m h ⋯
Instances For
noncomputable def
CochainComplex.mappingCone.lift
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cocycle K F 1)
(β : CochainComplex.HomComplex.Cochain K G 0)
(eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
:
Given φ : F ⟶ G, this is the morphism K ⟶ mappingCone φ that is constructed
from a cocycle α : Cochain K F 1 and a cochain β : Cochain K G 0
when a suitable cocycle relation is satisfied.
Equations
- CochainComplex.mappingCone.lift φ α β eq = (CochainComplex.mappingCone.liftCocycle φ α β CochainComplex.mappingCone.lift.proof_2 eq).homOf
Instances For
@[simp]
theorem
CochainComplex.mappingCone.ofHom_lift
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cocycle K F 1)
(β : CochainComplex.HomComplex.Cochain K G 0)
(eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
:
@[simp]
theorem
CochainComplex.mappingCone.lift_f_fst_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cocycle K F 1)
(β : CochainComplex.HomComplex.Cochain K G 0)
(eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
(p : ℤ)
(q : ℤ)
(hpq : p + 1 = q)
{Z : C}
(h : F.X q ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.lift φ α β eq).f p)
(CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v p q hpq) h) = CategoryTheory.CategoryStruct.comp ((↑α).v p q hpq) h
@[simp]
theorem
CochainComplex.mappingCone.lift_f_fst_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cocycle K F 1)
(β : CochainComplex.HomComplex.Cochain K G 0)
(eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
(p : ℤ)
(q : ℤ)
(hpq : p + 1 = q)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.lift φ α β eq).f p)
((↑(CochainComplex.mappingCone.fst φ)).v p q hpq) = (↑α).v p q hpq
theorem
CochainComplex.mappingCone.lift_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cocycle K F 1)
(β : CochainComplex.HomComplex.Cochain K G 0)
(eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
:
(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.lift φ α β eq)).comp
↑(CochainComplex.mappingCone.fst φ) ⋯ = ↑α
@[simp]
theorem
CochainComplex.mappingCone.lift_f_snd_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cocycle K F 1)
(β : CochainComplex.HomComplex.Cochain K G 0)
(eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
(p : ℤ)
(q : ℤ)
(hpq : p + 0 = q)
{Z : C}
(h : G.X q ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.lift φ α β eq).f p)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v p q hpq) h) = CategoryTheory.CategoryStruct.comp (β.v p q hpq) h
@[simp]
theorem
CochainComplex.mappingCone.lift_f_snd_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cocycle K F 1)
(β : CochainComplex.HomComplex.Cochain K G 0)
(eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
(p : ℤ)
(q : ℤ)
(hpq : p + 0 = q)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.lift φ α β eq).f p)
((CochainComplex.mappingCone.snd φ).v p q hpq) = β.v p q hpq
theorem
CochainComplex.mappingCone.lift_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cocycle K F 1)
(β : CochainComplex.HomComplex.Cochain K G 0)
(eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
:
(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.lift φ α β eq)).comp
(CochainComplex.mappingCone.snd φ) ⋯ = β
theorem
CochainComplex.mappingCone.lift_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cocycle K F 1)
(β : CochainComplex.HomComplex.Cochain K G 0)
(eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
(p : ℤ)
(q : ℤ)
(hpq : p + 1 = q)
:
(CochainComplex.mappingCone.lift φ α β eq).f p = CategoryTheory.CategoryStruct.comp ((↑α).v p q hpq) ((CochainComplex.mappingCone.inl φ).v q p ⋯) + CategoryTheory.CategoryStruct.comp (β.v p p ⋯) ((CochainComplex.mappingCone.inr φ).f p)
noncomputable def
CochainComplex.mappingCone.liftHomotopy
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(f₁ : K ⟶ CochainComplex.mappingCone φ)
(f₂ : K ⟶ CochainComplex.mappingCone φ)
(α : CochainComplex.HomComplex.Cochain K F 0)
(β : CochainComplex.HomComplex.Cochain K G (-1))
(h₁ : (CochainComplex.HomComplex.Cochain.ofHom f₁).comp ↑(CochainComplex.mappingCone.fst φ) ⋯ = -CochainComplex.HomComplex.δ 0 1 α + (CochainComplex.HomComplex.Cochain.ofHom f₂).comp ↑(CochainComplex.mappingCone.fst φ) ⋯)
(h₂ : (CochainComplex.HomComplex.Cochain.ofHom f₁).comp (CochainComplex.mappingCone.snd φ) ⋯ = CochainComplex.HomComplex.δ (-1) 0 β + α.comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ + (CochainComplex.HomComplex.Cochain.ofHom f₂).comp (CochainComplex.mappingCone.snd φ) ⋯)
:
Homotopy f₁ f₂
Constructor for homotopies between morphisms to a mapping cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CochainComplex.mappingCone.liftCochain_descCochain
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain K F m)
(β : CochainComplex.HomComplex.Cochain K G n)
{n' : ℤ}
{m' : ℤ}
(α' : CochainComplex.HomComplex.Cochain F L m')
(β' : CochainComplex.HomComplex.Cochain G L n')
(h : n + 1 = m)
(h' : m' + 1 = n')
(p : ℤ)
(hp : n + n' = p)
:
(CochainComplex.mappingCone.liftCochain φ α β h).comp (CochainComplex.mappingCone.descCochain φ α' β' h') hp = α.comp α' ⋯ + β.comp β' ⋯
theorem
CochainComplex.mappingCone.liftCochain_v_descCochain_v
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
{n : ℤ}
{m : ℤ}
(α : CochainComplex.HomComplex.Cochain K F m)
(β : CochainComplex.HomComplex.Cochain K G n)
{n' : ℤ}
{m' : ℤ}
(α' : CochainComplex.HomComplex.Cochain F L m')
(β' : CochainComplex.HomComplex.Cochain G L n')
(h : n + 1 = m)
(h' : m' + 1 = n')
(p : ℤ)
(hp : n + n' = p)
(p₁ : ℤ)
(p₂ : ℤ)
(p₃ : ℤ)
(h₁₂ : p₁ + n = p₂)
(h₂₃ : p₂ + n' = p₃)
(q : ℤ)
(hq : p₁ + m = q)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂)
((CochainComplex.mappingCone.descCochain φ α' β' h').v p₂ p₃ h₂₃) = CategoryTheory.CategoryStruct.comp (α.v p₁ q hq) (α'.v q p₃ ⋯) + CategoryTheory.CategoryStruct.comp (β.v p₁ p₂ h₁₂) (β'.v p₂ p₃ h₂₃)
theorem
CochainComplex.mappingCone.lift_desc_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{F : CochainComplex C ℤ}
{G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(α : CochainComplex.HomComplex.Cocycle K F 1)
(β : CochainComplex.HomComplex.Cochain K G 0)
(eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0)
(α' : CochainComplex.HomComplex.Cochain F L (-1))
(β' : G ⟶ L)
(eq' : CochainComplex.HomComplex.δ (-1) 0 α' = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β'))
(n : ℤ)
(n' : ℤ)
(hnn' : n + 1 = n')
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.lift φ α β eq).f n)
((CochainComplex.mappingCone.desc φ α' β' eq').f n) = CategoryTheory.CategoryStruct.comp ((↑α).v n n' hnn') (α'.v n' n ⋯) + CategoryTheory.CategoryStruct.comp (β.v n n ⋯) (β'.f n)