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 1 and
• mappingCone.snd φ : Cochain (mappingCone φ) G 0.

instance CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat {C : Type u_1} [CategoryTheory.Category.{v, 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)] : HomologicalComplex.HasHomotopyCofiber φ

noncomputable def CochainComplex.mappingCone {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] : HomologicalComplex C (ComplexShape.up ℤ)

The mapping cone of a morphism of cochain complexes indexed by ℤ.

noncomputable def CochainComplex.mappingCone.inl {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] : HomComplex.Cochain F (mappingCone φ) (-1)

The left inclusion in the mapping cone, as a cochain of degree -1.

noncomputable def CochainComplex.mappingCone.inr {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] : G ⟶ mappingCone φ

The right inclusion in the mapping cone.

noncomputable def CochainComplex.mappingCone.fst {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] : HomComplex.Cocycle (mappingCone φ) F 1

The first projection from the mapping cone, as a cocyle of degree 1.

noncomputable def CochainComplex.mappingCone.snd {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] : HomComplex.Cochain (mappingCone φ) G 0

The second projection from the mapping cone, as a cochain of degree 0.

@[simp]

theorem CochainComplex.mappingCone.inl_v_fst_v {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : q + 1 = p) : CategoryTheory.CategoryStruct.comp ((inl φ).v p q ⋯) ((↑(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.{v, 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 ((inl φ).v p q ⋯) (CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v q p hpq) h) = h

@[simp]

theorem CochainComplex.mappingCone.inl_v_snd_v {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + -1 = q) : CategoryTheory.CategoryStruct.comp ((inl φ).v p q hpq) ((snd φ).v q q ⋯) = 0

@[simp]

theorem CochainComplex.mappingCone.inl_v_snd_v_assoc {C : Type u_1} [CategoryTheory.Category.{v, 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 ((inl φ).v p q hpq) (CategoryTheory.CategoryStruct.comp ((snd φ).v q q ⋯) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CochainComplex.mappingCone.inr_f_fst_v {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + 1 = q) : CategoryTheory.CategoryStruct.comp ((inr φ).f p) ((↑(fst φ)).v p q hpq) = 0

@[simp]

theorem CochainComplex.mappingCone.inr_f_fst_v_assoc {C : Type u_1} [CategoryTheory.Category.{v, 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 ((inr φ).f p) (CategoryTheory.CategoryStruct.comp ((↑(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.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (p : ℤ) : CategoryTheory.CategoryStruct.comp ((inr φ).f p) ((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.{v, 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 ((inr φ).f p) (CategoryTheory.CategoryStruct.comp ((snd φ).v p p ⋯) h) = h

@[simp]

theorem CochainComplex.mappingCone.inl_fst {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] : (inl φ).comp ↑(fst φ) ⋯ = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id F)

@[simp]

theorem CochainComplex.mappingCone.inl_snd {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] : (inl φ).comp (snd φ) ⋯ = 0

@[simp]

theorem CochainComplex.mappingCone.inr_fst {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] : (HomComplex.Cochain.ofHom (inr φ)).comp ↑(fst φ) ⋯ = 0

@[simp]

theorem CochainComplex.mappingCone.inr_snd {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] : (HomComplex.Cochain.ofHom (inr φ)).comp (snd φ) ⋯ = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id G)

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.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {d e : ℤ} (γ : HomComplex.Cochain F K d) (he : 1 + d = e) : (inl φ).comp ((↑(fst φ)).comp γ he) ⋯ = γ

@[simp]

theorem CochainComplex.mappingCone.inl_snd_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {d e f : ℤ} (γ : HomComplex.Cochain G K d) (he : 0 + d = e) (hf : -1 + e = f) : (inl φ).comp ((snd φ).comp γ he) hf = 0

@[simp]

theorem CochainComplex.mappingCone.inr_fst_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {d e f : ℤ} (γ : HomComplex.Cochain F K d) (he : 1 + d = e) (hf : 0 + e = f) : (HomComplex.Cochain.ofHom (inr φ)).comp ((↑(fst φ)).comp γ he) hf = 0

@[simp]

theorem CochainComplex.mappingCone.inr_snd_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {d e : ℤ} (γ : HomComplex.Cochain G K d) (he : 0 + d = e) : (HomComplex.Cochain.ofHom (inr φ)).comp ((snd φ).comp γ he) ⋯ = γ

theorem CochainComplex.mappingCone.ext_to {C : Type u_1} [CategoryTheory.Category.{v, 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 ⟶ (mappingCone φ).X i} (h₁ : CategoryTheory.CategoryStruct.comp f ((↑(fst φ)).v i j hij) = CategoryTheory.CategoryStruct.comp g ((↑(fst φ)).v i j hij)) (h₂ : CategoryTheory.CategoryStruct.comp f ((snd φ).v i i ⋯) = CategoryTheory.CategoryStruct.comp g ((snd φ).v i i ⋯)) : f = g

theorem CochainComplex.mappingCone.ext_to_iff {C : Type u_1} [CategoryTheory.Category.{v, 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 ⟶ (mappingCone φ).X i) : f = g ↔ CategoryTheory.CategoryStruct.comp f ((↑(fst φ)).v i j hij) = CategoryTheory.CategoryStruct.comp g ((↑(fst φ)).v i j hij) ∧ CategoryTheory.CategoryStruct.comp f ((snd φ).v i i ⋯) = CategoryTheory.CategoryStruct.comp g ((snd φ).v i i ⋯)

theorem CochainComplex.mappingCone.ext_from {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : j + 1 = i) {A : C} {f g : (mappingCone φ).X j ⟶ A} (h₁ : CategoryTheory.CategoryStruct.comp ((inl φ).v i j ⋯) f = CategoryTheory.CategoryStruct.comp ((inl φ).v i j ⋯) g) (h₂ : CategoryTheory.CategoryStruct.comp ((inr φ).f j) f = CategoryTheory.CategoryStruct.comp ((inr φ).f j) g) : f = g

theorem CochainComplex.mappingCone.ext_from_iff {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : j + 1 = i) {A : C} (f g : (mappingCone φ).X j ⟶ A) : f = g ↔ CategoryTheory.CategoryStruct.comp ((inl φ).v i j ⋯) f = CategoryTheory.CategoryStruct.comp ((inl φ).v i j ⋯) g ∧ CategoryTheory.CategoryStruct.comp ((inr φ).f j) f = CategoryTheory.CategoryStruct.comp ((inr φ).f j) g

theorem CochainComplex.mappingCone.decomp_to {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {i : ℤ} {A : C} (f : A ⟶ (mappingCone φ).X i) (j : ℤ) (hij : i + 1 = j) : ∃ (a : A ⟶ F.X j) (b : A ⟶ G.X i), f = CategoryTheory.CategoryStruct.comp a ((inl φ).v j i ⋯) + CategoryTheory.CategoryStruct.comp b ((inr φ).f i)

theorem CochainComplex.mappingCone.decomp_from {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {j : ℤ} {A : C} (f : (mappingCone φ).X j ⟶ A) (i : ℤ) (hij : j + 1 = i) : ∃ (a : F.X i ⟶ A) (b : G.X j ⟶ A), f = CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v j i hij) a + CategoryTheory.CategoryStruct.comp ((snd φ).v j j ⋯) b

theorem CochainComplex.mappingCone.ext_cochain_to_iff {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : i + 1 = j) {K : CochainComplex C ℤ} {γ₁ γ₂ : HomComplex.Cochain K (mappingCone φ) i} : γ₁ = γ₂ ↔ γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij ∧ γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯

theorem CochainComplex.mappingCone.ext_cochain_from_iff {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : i + 1 = j) {K : CochainComplex C ℤ} {γ₁ γ₂ : HomComplex.Cochain (mappingCone φ) K j} : γ₁ = γ₂ ↔ (inl φ).comp γ₁ ⋯ = (inl φ).comp γ₂ ⋯ ∧ (HomComplex.Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (HomComplex.Cochain.ofHom (inr φ)).comp γ₂ ⋯

theorem CochainComplex.mappingCone.id {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] : (↑(fst φ)).comp (inl φ) ⋯ + (snd φ).comp (HomComplex.Cochain.ofHom (inr φ)) ⋯ = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id (mappingCone φ))

theorem CochainComplex.mappingCone.id_X {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + 1 = q) : CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v p q hpq) ((inl φ).v q p ⋯) + CategoryTheory.CategoryStruct.comp ((snd φ).v p p ⋯) ((inr φ).f p) = CategoryTheory.CategoryStruct.id ((mappingCone φ).X p)

theorem CochainComplex.mappingCone.inl_v_d {C : Type u_1} [CategoryTheory.Category.{v, 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 ((inl φ).v i j hij) ((mappingCone φ).d j i) = CategoryTheory.CategoryStruct.comp (φ.f i) ((inr φ).f i) - CategoryTheory.CategoryStruct.comp (F.d i k) ((inl φ).v k i hik)

theorem CochainComplex.mappingCone.inl_v_d_assoc {C : Type u_1} [CategoryTheory.Category.{v, 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 : (mappingCone φ).X i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((inl φ).v i j hij) (CategoryTheory.CategoryStruct.comp ((mappingCone φ).d j i) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (φ.f i) ((inr φ).f i) - CategoryTheory.CategoryStruct.comp (F.d i k) ((inl φ).v k i hik)) h

theorem CochainComplex.mappingCone.inr_f_d {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (n₁ n₂ : ℤ) : CategoryTheory.CategoryStruct.comp ((inr φ).f n₁) ((mappingCone φ).d n₁ n₂) = CategoryTheory.CategoryStruct.comp (G.d n₁ n₂) ((inr φ).f n₂)

theorem CochainComplex.mappingCone.inr_f_d_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (n₁ n₂ : ℤ) {Z : C} (h : (mappingCone φ).X n₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((inr φ).f n₁) (CategoryTheory.CategoryStruct.comp ((mappingCone φ).d n₁ n₂) h) = CategoryTheory.CategoryStruct.comp (G.d n₁ n₂) (CategoryTheory.CategoryStruct.comp ((inr φ).f n₂) h)

theorem CochainComplex.mappingCone.d_fst_v {C : Type u_1} [CategoryTheory.Category.{v, 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 ((mappingCone φ).d i j) ((↑(fst φ)).v j k hjk) = -CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v i j hij) (F.d j k)

theorem CochainComplex.mappingCone.d_fst_v_assoc {C : Type u_1} [CategoryTheory.Category.{v, 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 ((mappingCone φ).d i j) (CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v j k hjk) h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v i j hij) (F.d j k)) h

@[simp]

theorem CochainComplex.mappingCone.d_fst_v' {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : i + 1 = j) : CategoryTheory.CategoryStruct.comp ((mappingCone φ).d (i - 1) i) ((↑(fst φ)).v i j hij) = -CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v (i - 1) i ⋯) (F.d i j)

@[simp]

theorem CochainComplex.mappingCone.d_fst_v'_assoc {C : Type u_1} [CategoryTheory.Category.{v, 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 ((mappingCone φ).d (i - 1) i) (CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v i j hij) h) = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v (i - 1) i ⋯) (F.d i j)) h

theorem CochainComplex.mappingCone.d_snd_v {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : i + 1 = j) : CategoryTheory.CategoryStruct.comp ((mappingCone φ).d i j) ((snd φ).v j j ⋯) = CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v i j hij) (φ.f j) + CategoryTheory.CategoryStruct.comp ((snd φ).v i i ⋯) (G.d i j)

theorem CochainComplex.mappingCone.d_snd_v_assoc {C : Type u_1} [CategoryTheory.Category.{v, 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 ((mappingCone φ).d i j) (CategoryTheory.CategoryStruct.comp ((snd φ).v j j ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v i j hij) (φ.f j) + CategoryTheory.CategoryStruct.comp ((snd φ).v i i ⋯) (G.d i j)) h

@[simp]

theorem CochainComplex.mappingCone.d_snd_v' {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (n : ℤ) : CategoryTheory.CategoryStruct.comp ((mappingCone φ).d (n - 1) n) ((snd φ).v n n ⋯) = CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v (n - 1) n ⋯) (φ.f n) + CategoryTheory.CategoryStruct.comp ((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.{v, 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 ((mappingCone φ).d (n - 1) n) (CategoryTheory.CategoryStruct.comp ((snd φ).v n n ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v (n - 1) n ⋯) (φ.f n) + CategoryTheory.CategoryStruct.comp ((snd φ).v (n - 1) (n - 1) ⋯) (G.d (n - 1) n)) h

@[simp]

theorem CochainComplex.mappingCone.δ_inl {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] : HomComplex.δ (-1) 0 (inl φ) = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ (inr φ))

@[simp]

theorem CochainComplex.mappingCone.δ_snd {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] : HomComplex.δ 0 1 (snd φ) = -(↑(fst φ)).comp (HomComplex.Cochain.ofHom φ) ⋯

noncomputable def CochainComplex.mappingCone.descCochain {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain F K m) (β : HomComplex.Cochain G K n) (h : m + 1 = n) : HomComplex.Cochain (mappingCone φ) K 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.

@[simp]

theorem CochainComplex.mappingCone.inl_descCochain {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain F K m) (β : HomComplex.Cochain G K n) (h : m + 1 = n) : (inl φ).comp (descCochain φ α β h) ⋯ = α

@[simp]

theorem CochainComplex.mappingCone.inr_descCochain {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain F K m) (β : HomComplex.Cochain G K n) (h : m + 1 = n) : (HomComplex.Cochain.ofHom (inr φ)).comp (descCochain φ α β h) ⋯ = β

@[simp]

theorem CochainComplex.mappingCone.inl_v_descCochain_v {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain F K m) (β : HomComplex.Cochain G K n) (h : m + 1 = n) (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + -1 = p₂) (h₂₃ : p₂ + n = p₃) : CategoryTheory.CategoryStruct.comp ((inl φ).v p₁ p₂ h₁₂) ((descCochain φ α β h).v p₂ p₃ h₂₃) = α.v p₁ p₃ ⋯

@[simp]

theorem CochainComplex.mappingCone.inl_v_descCochain_v_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain F K m) (β : 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 ((inl φ).v p₁ p₂ h₁₂) (CategoryTheory.CategoryStruct.comp ((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.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain F K m) (β : HomComplex.Cochain G K n) (h : m + 1 = n) (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂) : CategoryTheory.CategoryStruct.comp ((inr φ).f p₁) ((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.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain F K m) (β : 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 ((inr φ).f p₁) (CategoryTheory.CategoryStruct.comp ((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.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain F K m) (β : HomComplex.Cochain G K n) (h : m + 1 = n) (n' : ℤ) (hn' : n + 1 = n') : HomComplex.δ n n' (descCochain φ α β h) = (↑(fst φ)).comp (HomComplex.δ m n α + n'.negOnePow • (HomComplex.Cochain.ofHom φ).comp β ⋯) ⋯ + (snd φ).comp (HomComplex.δ n n' β) ⋯

noncomputable def CochainComplex.mappingCone.descCocycle {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain F K m) (β : HomComplex.Cocycle G K n) (h : m + 1 = n) (eq : HomComplex.δ m n α = n.negOnePow • (HomComplex.Cochain.ofHom φ).comp ↑β ⋯) : HomComplex.Cocycle (mappingCone φ) K n

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.

@[simp]

theorem CochainComplex.mappingCone.descCocycle_coe {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain F K m) (β : HomComplex.Cocycle G K n) (h : m + 1 = n) (eq : HomComplex.δ m n α = n.negOnePow • (HomComplex.Cochain.ofHom φ).comp ↑β ⋯) : ↑(descCocycle φ α β h eq) = descCochain φ α (↑β) h

noncomputable def CochainComplex.mappingCone.desc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cochain F K (-1)) (β : G ⟶ K) (eq : HomComplex.δ (-1) 0 α = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)) : mappingCone φ ⟶ K

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 (φ ≫ β).

@[simp]

theorem CochainComplex.mappingCone.ofHom_desc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cochain F K (-1)) (β : G ⟶ K) (eq : HomComplex.δ (-1) 0 α = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)) : HomComplex.Cochain.ofHom (desc φ α β eq) = descCochain φ α (HomComplex.Cochain.ofHom β) ⋯

@[simp]

theorem CochainComplex.mappingCone.inl_v_desc_f {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cochain F K (-1)) (β : G ⟶ K) (eq : HomComplex.δ (-1) 0 α = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)) (p q : ℤ) (h : p + -1 = q) : CategoryTheory.CategoryStruct.comp ((inl φ).v p q h) ((desc φ α β eq).f q) = α.v p q h

@[simp]

theorem CochainComplex.mappingCone.inl_v_desc_f_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cochain F K (-1)) (β : G ⟶ K) (eq : HomComplex.δ (-1) 0 α = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)) (p q : ℤ) (h : p + -1 = q) {Z : C} (h✝ : K.X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((inl φ).v p q h) (CategoryTheory.CategoryStruct.comp ((desc φ α β eq).f q) h✝) = CategoryTheory.CategoryStruct.comp (α.v p q h) h✝

theorem CochainComplex.mappingCone.inl_desc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cochain F K (-1)) (β : G ⟶ K) (eq : HomComplex.δ (-1) 0 α = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)) : (inl φ).comp (HomComplex.Cochain.ofHom (desc φ α β eq)) ⋯ = α

@[simp]

theorem CochainComplex.mappingCone.inr_f_desc_f {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cochain F K (-1)) (β : G ⟶ K) (eq : HomComplex.δ (-1) 0 α = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)) (p : ℤ) : CategoryTheory.CategoryStruct.comp ((inr φ).f p) ((desc φ α β eq).f p) = β.f p

@[simp]

theorem CochainComplex.mappingCone.inr_f_desc_f_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cochain F K (-1)) (β : G ⟶ K) (eq : HomComplex.δ (-1) 0 α = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)) (p : ℤ) {Z : C} (h : K.X p ⟶ Z) : CategoryTheory.CategoryStruct.comp ((inr φ).f p) (CategoryTheory.CategoryStruct.comp ((desc φ α β eq).f p) h) = CategoryTheory.CategoryStruct.comp (β.f p) h

@[simp]

theorem CochainComplex.mappingCone.inr_desc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cochain F K (-1)) (β : G ⟶ K) (eq : HomComplex.δ (-1) 0 α = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)) : CategoryTheory.CategoryStruct.comp (inr φ) (desc φ α β eq) = β

@[simp]

theorem CochainComplex.mappingCone.inr_desc_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cochain F K (-1)) (β : G ⟶ K) (eq : HomComplex.δ (-1) 0 α = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)) {Z : CochainComplex C ℤ} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (inr φ) (CategoryTheory.CategoryStruct.comp (desc φ α β eq) h) = CategoryTheory.CategoryStruct.comp β h

theorem CochainComplex.mappingCone.desc_f {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cochain F K (-1)) (β : G ⟶ K) (eq : HomComplex.δ (-1) 0 α = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)) (p q : ℤ) (hpq : p + 1 = q) : (desc φ α β eq).f p = CategoryTheory.CategoryStruct.comp ((↑(fst φ)).v p q hpq) (α.v q p ⋯) + CategoryTheory.CategoryStruct.comp ((snd φ).v p p ⋯) (β.f p)

noncomputable def CochainComplex.mappingCone.descHomotopy {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (f₁ f₂ : mappingCone φ ⟶ K) (γ₁ : HomComplex.Cochain F K (-2)) (γ₂ : HomComplex.Cochain G K (-1)) (h₁ : (inl φ).comp (HomComplex.Cochain.ofHom f₁) ⋯ = HomComplex.δ (-2) (-1) γ₁ + (HomComplex.Cochain.ofHom φ).comp γ₂ ⋯ + (inl φ).comp (HomComplex.Cochain.ofHom f₂) ⋯) (h₂ : HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp (inr φ) f₁) = HomComplex.δ (-1) 0 γ₂ + HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp (inr φ) f₂)) : Homotopy f₁ f₂

Constructor for homotopies between morphisms from a mapping cone.

noncomputable def CochainComplex.mappingCone.liftCochain {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K F m) (β : HomComplex.Cochain K G n) (h : n + 1 = m) : HomComplex.Cochain K (mappingCone φ) 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.

@[simp]

theorem CochainComplex.mappingCone.liftCochain_fst {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K F m) (β : HomComplex.Cochain K G n) (h : n + 1 = m) : (liftCochain φ α β h).comp (↑(fst φ)) h = α

@[simp]

theorem CochainComplex.mappingCone.liftCochain_snd {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K F m) (β : HomComplex.Cochain K G n) (h : n + 1 = m) : (liftCochain φ α β h).comp (snd φ) ⋯ = β

@[simp]

theorem CochainComplex.mappingCone.liftCochain_v_fst_v {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K F m) (β : HomComplex.Cochain K G n) (h : n + 1 = m) (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + 1 = p₃) : CategoryTheory.CategoryStruct.comp ((liftCochain φ α β h).v p₁ p₂ h₁₂) ((↑(fst φ)).v p₂ p₃ h₂₃) = α.v p₁ p₃ ⋯

@[simp]

theorem CochainComplex.mappingCone.liftCochain_v_fst_v_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K F m) (β : 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 ((liftCochain φ α β h).v p₁ p₂ h₁₂) (CategoryTheory.CategoryStruct.comp ((↑(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.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K F m) (β : HomComplex.Cochain K G n) (h : n + 1 = m) (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂) : CategoryTheory.CategoryStruct.comp ((liftCochain φ α β h).v p₁ p₂ h₁₂) ((snd φ).v p₂ p₂ ⋯) = β.v p₁ p₂ h₁₂

@[simp]

theorem CochainComplex.mappingCone.liftCochain_v_snd_v_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K F m) (β : 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 ((liftCochain φ α β h).v p₁ p₂ h₁₂) (CategoryTheory.CategoryStruct.comp ((snd φ).v p₂ p₂ ⋯) h✝) = CategoryTheory.CategoryStruct.comp (β.v p₁ p₂ h₁₂) h✝

theorem CochainComplex.mappingCone.δ_liftCochain {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K F m) (β : HomComplex.Cochain K G n) (h : n + 1 = m) (m' : ℤ) (hm' : m + 1 = m') : HomComplex.δ n m (liftCochain φ α β h) = -(HomComplex.δ m m' α).comp (inl φ) ⋯ + (HomComplex.δ n m β + α.comp (HomComplex.Cochain.ofHom φ) ⋯).comp (HomComplex.Cochain.ofHom (inr φ)) ⋯

noncomputable def CochainComplex.mappingCone.liftCocycle {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cocycle K F m) (β : HomComplex.Cochain K G n) (h : n + 1 = m) (eq : HomComplex.δ n m β + (↑α).comp (HomComplex.Cochain.ofHom φ) ⋯ = 0) : HomComplex.Cocycle K (mappingCone φ) n

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.

@[simp]

theorem CochainComplex.mappingCone.liftCocycle_coe {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cocycle K F m) (β : HomComplex.Cochain K G n) (h : n + 1 = m) (eq : HomComplex.δ n m β + (↑α).comp (HomComplex.Cochain.ofHom φ) ⋯ = 0) : ↑(liftCocycle φ α β h eq) = liftCochain φ (↑α) β h

noncomputable def CochainComplex.mappingCone.lift {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cocycle K F 1) (β : HomComplex.Cochain K G 0) (eq : HomComplex.δ 0 1 β + (↑α).comp (HomComplex.Cochain.ofHom φ) ⋯ = 0) : K ⟶ mappingCone φ

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.

@[simp]

theorem CochainComplex.mappingCone.ofHom_lift {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cocycle K F 1) (β : HomComplex.Cochain K G 0) (eq : HomComplex.δ 0 1 β + (↑α).comp (HomComplex.Cochain.ofHom φ) ⋯ = 0) : HomComplex.Cochain.ofHom (lift φ α β eq) = liftCochain φ (↑α) β ⋯

@[simp]

theorem CochainComplex.mappingCone.lift_f_fst_v {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cocycle K F 1) (β : HomComplex.Cochain K G 0) (eq : HomComplex.δ 0 1 β + (↑α).comp (HomComplex.Cochain.ofHom φ) ⋯ = 0) (p q : ℤ) (hpq : p + 1 = q) : CategoryTheory.CategoryStruct.comp ((lift φ α β eq).f p) ((↑(fst φ)).v p q hpq) = (↑α).v p q hpq

@[simp]

theorem CochainComplex.mappingCone.lift_f_fst_v_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cocycle K F 1) (β : HomComplex.Cochain K G 0) (eq : HomComplex.δ 0 1 β + (↑α).comp (HomComplex.Cochain.ofHom φ) ⋯ = 0) (p q : ℤ) (hpq : p + 1 = q) {Z : C} (h : F.X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((lift φ α β eq).f p) (CategoryTheory.CategoryStruct.comp ((↑(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.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cocycle K F 1) (β : HomComplex.Cochain K G 0) (eq : HomComplex.δ 0 1 β + (↑α).comp (HomComplex.Cochain.ofHom φ) ⋯ = 0) : (HomComplex.Cochain.ofHom (lift φ α β eq)).comp ↑(fst φ) ⋯ = ↑α

@[simp]

theorem CochainComplex.mappingCone.lift_f_snd_v {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cocycle K F 1) (β : HomComplex.Cochain K G 0) (eq : HomComplex.δ 0 1 β + (↑α).comp (HomComplex.Cochain.ofHom φ) ⋯ = 0) (p q : ℤ) (hpq : p + 0 = q) : CategoryTheory.CategoryStruct.comp ((lift φ α β eq).f p) ((snd φ).v p q hpq) = β.v p q hpq

@[simp]

theorem CochainComplex.mappingCone.lift_f_snd_v_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cocycle K F 1) (β : HomComplex.Cochain K G 0) (eq : HomComplex.δ 0 1 β + (↑α).comp (HomComplex.Cochain.ofHom φ) ⋯ = 0) (p q : ℤ) (hpq : p + 0 = q) {Z : C} (h : G.X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((lift φ α β eq).f p) (CategoryTheory.CategoryStruct.comp ((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.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cocycle K F 1) (β : HomComplex.Cochain K G 0) (eq : HomComplex.δ 0 1 β + (↑α).comp (HomComplex.Cochain.ofHom φ) ⋯ = 0) : (HomComplex.Cochain.ofHom (lift φ α β eq)).comp (snd φ) ⋯ = β

theorem CochainComplex.mappingCone.lift_f {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (α : HomComplex.Cocycle K F 1) (β : HomComplex.Cochain K G 0) (eq : HomComplex.δ 0 1 β + (↑α).comp (HomComplex.Cochain.ofHom φ) ⋯ = 0) (p q : ℤ) (hpq : p + 1 = q) : (lift φ α β eq).f p = CategoryTheory.CategoryStruct.comp ((↑α).v p q hpq) ((inl φ).v q p ⋯) + CategoryTheory.CategoryStruct.comp (β.v p p ⋯) ((inr φ).f p)

noncomputable def CochainComplex.mappingCone.liftHomotopy {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} (f₁ f₂ : K ⟶ mappingCone φ) (α : HomComplex.Cochain K F 0) (β : HomComplex.Cochain K G (-1)) (h₁ : (HomComplex.Cochain.ofHom f₁).comp ↑(fst φ) ⋯ = -HomComplex.δ 0 1 α + (HomComplex.Cochain.ofHom f₂).comp ↑(fst φ) ⋯) (h₂ : (HomComplex.Cochain.ofHom f₁).comp (snd φ) ⋯ = HomComplex.δ (-1) 0 β + α.comp (HomComplex.Cochain.ofHom φ) ⋯ + (HomComplex.Cochain.ofHom f₂).comp (snd φ) ⋯) : Homotopy f₁ f₂

Constructor for homotopies between morphisms to a mapping cone.

@[simp]

theorem CochainComplex.mappingCone.liftCochain_descCochain {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K L : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K F m) (β : HomComplex.Cochain K G n) {n' m' : ℤ} (α' : HomComplex.Cochain F L m') (β' : HomComplex.Cochain G L n') (h : n + 1 = m) (h' : m' + 1 = n') (p : ℤ) (hp : n + n' = p) : (liftCochain φ α β h).comp (descCochain φ α' β' h') hp = α.comp α' ⋯ + β.comp β' hp

theorem CochainComplex.mappingCone.liftCochain_v_descCochain_v {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K L : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K F m) (β : HomComplex.Cochain K G n) {n' m' : ℤ} (α' : HomComplex.Cochain F L m') (β' : 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 ((liftCochain φ α β h).v p₁ p₂ h₁₂) ((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.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] {K L : CochainComplex C ℤ} (α : HomComplex.Cocycle K F 1) (β : HomComplex.Cochain K G 0) (eq : HomComplex.δ 0 1 β + (↑α).comp (HomComplex.Cochain.ofHom φ) ⋯ = 0) (α' : HomComplex.Cochain F L (-1)) (β' : G ⟶ L) (eq' : HomComplex.δ (-1) 0 α' = HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β')) (n n' : ℤ) (hnn' : n + 1 = n') : CategoryTheory.CategoryStruct.comp ((lift φ α β eq).f n) ((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.{v, u_1} C] [CategoryTheory.Category.{v', 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 (mappingCone φ)).X n ≅ (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.

@[simp]

theorem CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Category.{v', 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) : (mapHomologicalComplexXIso' φ H n m hnm).inv = CategoryTheory.CategoryStruct.comp ((↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n m hnm) (H.map ((inl φ).v m n ⋯)) + CategoryTheory.CategoryStruct.comp ((snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯) (H.map ((inr φ).f n))

@[simp]

theorem CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Category.{v', 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) : (mapHomologicalComplexXIso' φ H n m hnm).hom = CategoryTheory.CategoryStruct.comp (H.map ((↑(fst φ)).v n m hnm)) ((inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v m n ⋯) + CategoryTheory.CategoryStruct.comp (H.map ((snd φ).v n n ⋯)) ((inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n)

noncomputable def CochainComplex.mappingCone.mapHomologicalComplexXIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Category.{v', 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 (mappingCone φ)).X n ≅ (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 φ.

theorem CochainComplex.mappingCone.mapHomologicalComplexXIso_eq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Category.{v', 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) : mapHomologicalComplexXIso φ H n = mapHomologicalComplexXIso' φ H n m hnm

noncomputable def CochainComplex.mappingCone.mapHomologicalComplexIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Category.{v', 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 (mappingCone φ) ≅ 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 φ.

theorem CochainComplex.mappingCone.map_inr {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Category.{v', 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 (inr φ)) (mapHomologicalComplexIso φ H).hom = inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)