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_4, u_1} C]
[CategoryTheory.Preadditive C]
{ι : Type u_3}
[AddRightCancelSemigroup ι]
[One ι]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_fst_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_snd_v
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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.inl_v_snd_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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.inr_f_fst_v
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_fst_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_snd_v
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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.inr_f_snd_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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.inl_fst
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
@[simp]
theorem
CochainComplex.mappingCone.inl_snd
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
@[simp]
theorem
CochainComplex.mappingCone.inr_snd
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i j : ℤ)
(hij : i + 1 = j)
{A : C}
{f 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i j : ℤ)
(hij : i + 1 = j)
{A : C}
(f 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i j : ℤ)
(hij : j + 1 = i)
{A : C}
{f 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i j : ℤ)
(hij : j + 1 = i)
{A : C}
(f 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.decomp_to
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{i : ℤ}
{A : C}
(f : A ⟶ (CochainComplex.mappingCone φ).X i)
(j : ℤ)
(hij : i + 1 = j)
:
∃ (a : A ⟶ F.X j) (b : A ⟶ G.X i),
f = CategoryTheory.CategoryStruct.comp a ((CochainComplex.mappingCone.inl φ).v j i ⋯) + CategoryTheory.CategoryStruct.comp b ((CochainComplex.mappingCone.inr φ).f i)
theorem
CochainComplex.mappingCone.decomp_from
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{j : ℤ}
{A : C}
(f : (CochainComplex.mappingCone φ).X j ⟶ A)
(i : ℤ)
(hij : j + 1 = i)
:
∃ (a : F.X i ⟶ A) (b : G.X j ⟶ A),
f = CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v j i hij) a + CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v j j ⋯) b
theorem
CochainComplex.mappingCone.ext_cochain_to_iff
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i j : ℤ)
(hij : i + 1 = j)
{K : CochainComplex C ℤ}
{γ₁ γ₂ : 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(i j : ℤ)
(hij : i + 1 = j)
{K : CochainComplex C ℤ}
{γ₁ γ₂ : 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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)
theorem
CochainComplex.mappingCone.inl_v_d_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
@[simp]
theorem
CochainComplex.mappingCone.inr_f_d
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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₂)
@[simp]
theorem
CochainComplex.mappingCone.inr_f_d_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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)
theorem
CochainComplex.mappingCone.d_fst_v
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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)
theorem
CochainComplex.mappingCone.d_fst_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
@[simp]
theorem
CochainComplex.mappingCone.d_fst_v'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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)
@[simp]
theorem
CochainComplex.mappingCone.d_fst_v'_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
theorem
CochainComplex.mappingCone.d_snd_v
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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)
theorem
CochainComplex.mappingCone.d_snd_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
@[simp]
theorem
CochainComplex.mappingCone.d_snd_v'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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.d_snd_v'_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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.δ_inl
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
@[simp]
theorem
CochainComplex.mappingCone.δ_snd
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
:
noncomputable def
CochainComplex.mappingCone.descCochain
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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.inl_v_descCochain_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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.inr_f_descCochain_v
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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₁₂
@[simp]
theorem
CochainComplex.mappingCone.inr_f_descCochain_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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✝
theorem
CochainComplex.mappingCone.δ_descCochain
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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' β) ⋯
noncomputable def
CochainComplex.mappingCone.descCocycle
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
@[simp]
theorem
CochainComplex.mappingCone.descCocycle_coe
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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.desc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
@[simp]
theorem
CochainComplex.mappingCone.inl_v_desc_f_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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✝
theorem
CochainComplex.mappingCone.inl_desc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_f_desc_f_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_desc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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.inr_desc_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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)
:
theorem
CochainComplex.mappingCone.desc_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(f₁ 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_fst_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_snd_v
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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₁₂
@[simp]
theorem
CochainComplex.mappingCone.liftCochain_v_snd_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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✝
theorem
CochainComplex.mappingCone.δ_liftCochain
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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 φ)) ⋯
noncomputable def
CochainComplex.mappingCone.liftCocycle
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
@[simp]
theorem
CochainComplex.mappingCone.liftCocycle_coe
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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.lift
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
@[simp]
theorem
CochainComplex.mappingCone.lift_f_fst_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
theorem
CochainComplex.mappingCone.lift_fst
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
@[simp]
theorem
CochainComplex.mappingCone.lift_f_snd_v_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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
theorem
CochainComplex.mappingCone.lift_snd
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K : CochainComplex C ℤ}
(f₁ 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K 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_3, u_1} C]
[CategoryTheory.Preadditive C]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
{K 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)
noncomputable def
CochainComplex.mappingCone.mapHomologicalComplexXIso'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(H : CategoryTheory.Functor C D)
[H.Additive]
[HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)]
(n m : ℤ)
(hnm : n + 1 = m)
:
((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone φ)).X n ≅ (CochainComplex.mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).X n
If H : C ⥤ D is an additive functor and φ is a morphism of cochain complexes
in C, this is the comparison isomorphism (in each degree n) between the image
by H of mappingCone φ and the mapping cone of the image by H of φ.
It is an auxiliary definition for mapHomologicalComplexXIso and
mapHomologicalComplexIso. This definition takes an extra
parameter m : ℤ such that n + 1 = m which may help getting better
definitional properties. See also the equational lemma mapHomologicalComplexXIso_eq.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(H : CategoryTheory.Functor C D)
[H.Additive]
[HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)]
(n m : ℤ)
(hnm : n + 1 = m)
:
(CochainComplex.mappingCone.mapHomologicalComplexXIso' φ H n m hnm).inv = CategoryTheory.CategoryStruct.comp
((↑(CochainComplex.mappingCone.fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n m ⋯)
(H.map ((CochainComplex.mappingCone.inl φ).v m n ⋯)) + CategoryTheory.CategoryStruct.comp
((CochainComplex.mappingCone.snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯)
(H.map ((CochainComplex.mappingCone.inr φ).f n))
@[simp]
theorem
CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(H : CategoryTheory.Functor C D)
[H.Additive]
[HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)]
(n m : ℤ)
(hnm : n + 1 = m)
:
(CochainComplex.mappingCone.mapHomologicalComplexXIso' φ H n m hnm).hom = CategoryTheory.CategoryStruct.comp (H.map ((↑(CochainComplex.mappingCone.fst φ)).v n m ⋯))
((CochainComplex.mappingCone.inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v m n ⋯) + CategoryTheory.CategoryStruct.comp (H.map ((CochainComplex.mappingCone.snd φ).v n n ⋯))
((CochainComplex.mappingCone.inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n)
noncomputable def
CochainComplex.mappingCone.mapHomologicalComplexXIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(H : CategoryTheory.Functor C D)
[H.Additive]
[HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)]
(n : ℤ)
:
((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone φ)).X n ≅ (CochainComplex.mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).X n
If H : C ⥤ D is an additive functor and φ is a morphism of cochain complexes
in C, this is the comparison isomorphism (in each degree) between the image
by H of mappingCone φ and the mapping cone of the image by H of φ.
Equations
Instances For
theorem
CochainComplex.mappingCone.mapHomologicalComplexXIso_eq
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(H : CategoryTheory.Functor C D)
[H.Additive]
[HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)]
(n m : ℤ)
(hnm : n + 1 = m)
:
noncomputable def
CochainComplex.mappingCone.mapHomologicalComplexIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(H : CategoryTheory.Functor C D)
[H.Additive]
[HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)]
:
(H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone φ) ≅ CochainComplex.mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
If H : C ⥤ D is an additive functor and φ is a morphism of cochain complexes
in C, this is the comparison isomorphism between the image by H
of mappingCone φ and the mapping cone of the image by H of φ.
Equations
Instances For
theorem
CochainComplex.mappingCone.map_inr
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{F G : CochainComplex C ℤ}
(φ : F ⟶ G)
[HomologicalComplex.HasHomotopyCofiber φ]
(H : CategoryTheory.Functor C D)
[H.Additive]
[HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)]
:
CategoryTheory.CategoryStruct.comp
((H.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.inr φ))
(CochainComplex.mappingCone.mapHomologicalComplexIso φ H).hom = CochainComplex.mappingCone.inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)