The mapping cocone

Given a morphism φ : K ⟶ L of cochain complexes, the mapping cone allows to obtain a triangle K ⟶ L ⟶ mappingCone φ ⟶ .... In this file, we define the mapping cocone, which fits in a rotated triangle: mappingCocone φ ⟶ K ⟶ L ⟶ ....

noncomputable def CochainComplex.mappingCocone {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] : CochainComplex C ℤ

The mapping cocone of a morphism φ : K ⟶ L of cochain complexes: it is (mappingCone φ)⟦(-1 : ℤ)⟧.

noncomputable def CochainComplex.mappingCocone.fst {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] : mappingCocone φ ⟶ K

The first projection mappingCocone φ ⟶ K.

noncomputable def CochainComplex.mappingCocone.snd {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] : HomComplex.Cochain (mappingCocone φ) L (-1)

The second projection in Cochain (mappingCocone φ) L (-1).

noncomputable def CochainComplex.mappingCocone.inl {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] : HomComplex.Cochain K (mappingCocone φ) 0

The left inclusion in Cochain K (mappingCocone φ) 0.

noncomputable def CochainComplex.mappingCocone.inr {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] : HomComplex.Cocycle L (mappingCocone φ) 1

The right inclusion in Cocycle L (mappingCocone φ) 1.

@[simp]

theorem CochainComplex.mappingCocone.inl_v_fst_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] (p : ℤ) : CategoryTheory.CategoryStruct.comp ((inl φ).v p p ⋯) ((fst φ).f p) = CategoryTheory.CategoryStruct.id (K.X p)

@[simp]

theorem CochainComplex.mappingCocone.inl_v_fst_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] (p : ℤ) {Z : C} (h : K.X p ⟶ Z) : CategoryTheory.CategoryStruct.comp ((inl φ).v p p ⋯) (CategoryTheory.CategoryStruct.comp ((fst φ).f p) h) = h

@[simp]

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

@[simp]

theorem CochainComplex.mappingCocone.inl_v_snd_v_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + -1 = q) {Z : C} (h : L.X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((inl φ).v p p ⋯) (CategoryTheory.CategoryStruct.comp ((snd φ).v p q hpq) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

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

@[simp]

theorem CochainComplex.mappingCocone.inr_v_fst_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + 1 = q) {Z : C} (h : K.X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((↑(inr φ)).v p q hpq) (CategoryTheory.CategoryStruct.comp ((fst φ).f q) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CochainComplex.mappingCocone.inr_v_snd_v {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + 1 = q) : CategoryTheory.CategoryStruct.comp ((↑(inr φ)).v p q hpq) ((snd φ).v q p ⋯) = CategoryTheory.CategoryStruct.id (L.X p)

@[simp]

theorem CochainComplex.mappingCocone.inr_v_snd_v_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + 1 = q) {Z : C} (h : L.X p ⟶ Z) : CategoryTheory.CategoryStruct.comp ((↑(inr φ)).v p q hpq) (CategoryTheory.CategoryStruct.comp ((snd φ).v q p ⋯) h) = h

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

noncomputable def CochainComplex.mappingCocone.descCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K M m) (β : HomComplex.Cochain L M n) (h : m + 1 = n) : HomComplex.Cochain (mappingCocone φ) M m

Constructor for cochains from mappingCocone.

@[simp]

theorem CochainComplex.mappingCocone.inl_v_descCochain_v {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K M m) (β : HomComplex.Cochain L M n) (h : m + 1 = n) (p q : ℤ) (hpq : p + m = q) : CategoryTheory.CategoryStruct.comp ((inl φ).v p p ⋯) ((descCochain φ α β h).v p q hpq) = α.v p q hpq

@[simp]

theorem CochainComplex.mappingCocone.inl_v_descCochain_v_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K M m) (β : HomComplex.Cochain L M n) (h : m + 1 = n) (p q : ℤ) (hpq : p + m = q) {Z : C} (h✝ : M.X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((inl φ).v p p ⋯) (CategoryTheory.CategoryStruct.comp ((descCochain φ α β h).v p q hpq) h✝) = CategoryTheory.CategoryStruct.comp (α.v p q hpq) h✝

@[simp]

theorem CochainComplex.mappingCocone.inr_v_descCochain_v {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K M m) (β : HomComplex.Cochain L M n) (h : m + 1 = n) (p q : ℤ) (hpq : p + 1 = q) (r : ℤ) (hr : q + m = r) : CategoryTheory.CategoryStruct.comp ((↑(inr φ)).v p q hpq) ((descCochain φ α β h).v q r hr) = β.v p r ⋯

@[simp]

theorem CochainComplex.mappingCocone.inr_v_descCochain_v_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K M m) (β : HomComplex.Cochain L M n) (h : m + 1 = n) (p q : ℤ) (hpq : p + 1 = q) (r : ℤ) (hr : q + m = r) {Z : C} (h✝ : M.X r ⟶ Z) : CategoryTheory.CategoryStruct.comp ((↑(inr φ)).v p q hpq) (CategoryTheory.CategoryStruct.comp ((descCochain φ α β h).v q r hr) h✝) = CategoryTheory.CategoryStruct.comp (β.v p r ⋯) h✝

@[simp]

theorem CochainComplex.mappingCocone.inl_comp_descCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K M m) (β : HomComplex.Cochain L M n) (h : m + 1 = n) : (inl φ).comp (descCochain φ α β h) ⋯ = α

@[simp]

theorem CochainComplex.mappingCocone.inr_comp_descCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K M m) (β : HomComplex.Cochain L M n) (h : m + 1 = n) : (↑(inr φ)).comp (descCochain φ α β h) ⋯ = β

theorem CochainComplex.mappingCocone.δ_descCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain K M m) (β : HomComplex.Cochain L M n) (h : m + 1 = n) (n' : ℤ) (hn' : n + 1 = n') : HomComplex.δ m n (descCochain φ α β h) = (HomComplex.Cochain.ofHom (fst φ)).comp (HomComplex.δ m n α + m.negOnePow • (HomComplex.Cochain.ofHom φ).comp β ⋯) ⋯ + (snd φ).comp (HomComplex.δ n n' β) ⋯

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

Constructor for cocycles from mappingCocone.

@[simp]

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

noncomputable def CochainComplex.mappingCocone.desc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : HomComplex.Cochain K M 0) (β : HomComplex.Cocycle L M 1) (hαβ : HomComplex.δ 0 1 α + (HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) : mappingCocone φ ⟶ M

Constructor for morphisms from mappingCocone.

@[simp]

theorem CochainComplex.mappingCocone.ofHom_desc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : HomComplex.Cochain K M 0) (β : HomComplex.Cocycle L M 1) (hαβ : HomComplex.δ 0 1 α + (HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) : HomComplex.Cochain.ofHom (desc φ α β hαβ) = descCochain φ α (↑β) ofHom_desc._proof_2

@[simp]

theorem CochainComplex.mappingCocone.inl_v_desc_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : HomComplex.Cochain K M 0) (β : HomComplex.Cocycle L M 1) (hαβ : HomComplex.δ 0 1 α + (HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) (p : ℤ) : CategoryTheory.CategoryStruct.comp ((inl φ).v p p ⋯) ((desc φ α β hαβ).f p) = α.v p p ⋯

@[simp]

theorem CochainComplex.mappingCocone.inl_v_desc_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : HomComplex.Cochain K M 0) (β : HomComplex.Cocycle L M 1) (hαβ : HomComplex.δ 0 1 α + (HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) (p : ℤ) {Z : C} (h : M.X p ⟶ Z) : CategoryTheory.CategoryStruct.comp ((inl φ).v p p ⋯) (CategoryTheory.CategoryStruct.comp ((desc φ α β hαβ).f p) h) = CategoryTheory.CategoryStruct.comp (α.v p p ⋯) h

@[simp]

theorem CochainComplex.mappingCocone.inr_v_desc_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : HomComplex.Cochain K M 0) (β : HomComplex.Cocycle L M 1) (hαβ : HomComplex.δ 0 1 α + (HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) (p q : ℤ) (hpq : p + 1 = q) : CategoryTheory.CategoryStruct.comp ((↑(inr φ)).v p q hpq) ((desc φ α β hαβ).f q) = (↑β).v p q hpq

@[simp]

theorem CochainComplex.mappingCocone.inr_v_desc_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : HomComplex.Cochain K M 0) (β : HomComplex.Cocycle L M 1) (hαβ : HomComplex.δ 0 1 α + (HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) (p q : ℤ) (hpq : p + 1 = q) {Z : C} (h : M.X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((↑(inr φ)).v p q hpq) (CategoryTheory.CategoryStruct.comp ((desc φ α β hαβ).f q) h) = CategoryTheory.CategoryStruct.comp ((↑β).v p q hpq) h

noncomputable def CochainComplex.mappingCocone.liftCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain M K n) (β : HomComplex.Cochain M L m) (h : m + 1 = n) : HomComplex.Cochain M (mappingCocone φ) n

Constructor for cochains to mappingCocone.

@[simp]

theorem CochainComplex.mappingCocone.liftCochain_v_fst_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain M K n) (β : HomComplex.Cochain M L m) (h : m + 1 = n) (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂) : CategoryTheory.CategoryStruct.comp ((liftCochain φ α β h).v p₁ p₂ h₁₂) ((fst φ).f p₂) = α.v p₁ p₂ h₁₂

@[simp]

theorem CochainComplex.mappingCocone.liftCochain_v_fst_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain M K n) (β : HomComplex.Cochain M L m) (h : m + 1 = n) (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂) {Z : C} (h✝ : K.X p₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((liftCochain φ α β h).v p₁ p₂ h₁₂) (CategoryTheory.CategoryStruct.comp ((fst φ).f p₂) h✝) = CategoryTheory.CategoryStruct.comp (α.v p₁ p₂ h₁₂) h✝

@[simp]

theorem CochainComplex.mappingCocone.liftCochain_v_snd_v {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain M K n) (β : HomComplex.Cochain M L m) (h : m + 1 = n) (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + -1 = p₃) : CategoryTheory.CategoryStruct.comp ((liftCochain φ α β h).v p₁ p₂ h₁₂) ((snd φ).v p₂ p₃ h₂₃) = β.v p₁ p₃ ⋯

@[simp]

theorem CochainComplex.mappingCocone.liftCochain_v_snd_v_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain M K n) (β : HomComplex.Cochain M L m) (h : m + 1 = n) (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + -1 = p₃) {Z : C} (h✝ : L.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((liftCochain φ α β h).v p₁ p₂ h₁₂) (CategoryTheory.CategoryStruct.comp ((snd φ).v p₂ p₃ h₂₃) h✝) = CategoryTheory.CategoryStruct.comp (β.v p₁ p₃ ⋯) h✝

@[simp]

theorem CochainComplex.mappingCocone.liftCochain_comp_fst {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain M K n) (β : HomComplex.Cochain M L m) (h : m + 1 = n) : (liftCochain φ α β h).comp (HomComplex.Cochain.ofHom (fst φ)) ⋯ = α

@[simp]

theorem CochainComplex.mappingCocone.liftCochain_comp_snd {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain M K n) (β : HomComplex.Cochain M L m) (h : m + 1 = n) : (liftCochain φ α β h).comp (snd φ) ⋯ = β

theorem CochainComplex.mappingCocone.δ_liftCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} {n m : ℤ} (α : HomComplex.Cochain M K n) (β : HomComplex.Cochain M L m) (h : m + 1 = n) (n' : ℤ) (hn' : n + 1 = n') : HomComplex.δ n n' (liftCochain φ α β h) = (HomComplex.δ n n' α).comp (inl φ) ⋯ - (HomComplex.δ m n β + α.comp (HomComplex.Cochain.ofHom φ) ⋯).comp (↑(inr φ)) hn'

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

Constructor for cocycles to mappingCocone.

@[simp]

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

noncomputable def CochainComplex.mappingCocone.lift {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : M ⟶ K) (β : HomComplex.Cochain M L (-1)) (hαβ : HomComplex.δ (-1) 0 β + HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) = 0) : M ⟶ mappingCocone φ

Constructor for morphisms to mappingCocone.

@[simp]

theorem CochainComplex.mappingCocone.ofHom_lift {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : M ⟶ K) (β : HomComplex.Cochain M L (-1)) (hαβ : HomComplex.δ (-1) 0 β + HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) = 0) : HomComplex.Cochain.ofHom (lift φ α β hαβ) = liftCochain φ (HomComplex.Cochain.ofHom α) β lift._proof_1

@[simp]

theorem CochainComplex.mappingCocone.lift_f_fst_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : M ⟶ K) (β : HomComplex.Cochain M L (-1)) (hαβ : HomComplex.δ (-1) 0 β + HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) = 0) (p : ℤ) : CategoryTheory.CategoryStruct.comp ((lift φ α β hαβ).f p) ((fst φ).f p) = α.f p

@[simp]

theorem CochainComplex.mappingCocone.lift_f_fst_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : M ⟶ K) (β : HomComplex.Cochain M L (-1)) (hαβ : HomComplex.δ (-1) 0 β + HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) = 0) (p : ℤ) {Z : C} (h : K.X p ⟶ Z) : CategoryTheory.CategoryStruct.comp ((lift φ α β hαβ).f p) (CategoryTheory.CategoryStruct.comp ((fst φ).f p) h) = CategoryTheory.CategoryStruct.comp (α.f p) h

@[simp]

theorem CochainComplex.mappingCocone.lift_fst {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : M ⟶ K) (β : HomComplex.Cochain M L (-1)) (hαβ : HomComplex.δ (-1) 0 β + HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) = 0) : CategoryTheory.CategoryStruct.comp (lift φ α β hαβ) (fst φ) = α

@[simp]

theorem CochainComplex.mappingCocone.lift_fst_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : M ⟶ K) (β : HomComplex.Cochain M L (-1)) (hαβ : HomComplex.δ (-1) 0 β + HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) = 0) {Z : CochainComplex C ℤ} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (lift φ α β hαβ) (CategoryTheory.CategoryStruct.comp (fst φ) h) = CategoryTheory.CategoryStruct.comp α h

@[simp]

theorem CochainComplex.mappingCocone.lift_f_snd_v {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : M ⟶ K) (β : HomComplex.Cochain M L (-1)) (hαβ : HomComplex.δ (-1) 0 β + HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) = 0) (p q : ℤ) (hpq : p + -1 = q) : CategoryTheory.CategoryStruct.comp ((lift φ α β hαβ).f p) ((snd φ).v p q hpq) = β.v p q hpq

@[simp]

theorem CochainComplex.mappingCocone.lift_f_snd_v_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ} (α : M ⟶ K) (β : HomComplex.Cochain M L (-1)) (hαβ : HomComplex.δ (-1) 0 β + HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) = 0) (p q : ℤ) (hpq : p + -1 = q) {Z : C} (h : L.X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((lift φ α β hαβ).f p) (CategoryTheory.CategoryStruct.comp ((snd φ).v p q hpq) h) = CategoryTheory.CategoryStruct.comp (β.v p q hpq) h

noncomputable def CochainComplex.mappingCocone.triangle {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)

Given a morphism φ : K ⟶ L of cochain complexes, this is the triangle mappingCocone φ ⟶ K ⟶ L ⟶ ....

@[simp]

theorem CochainComplex.mappingCocone.triangle_obj₂ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasBinaryBiproducts C] : (triangle φ).obj₂ = K

@[simp]

theorem CochainComplex.mappingCocone.triangle_obj₃ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasBinaryBiproducts C] : (triangle φ).obj₃ = L

@[simp]

theorem CochainComplex.mappingCocone.triangle_mor₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasBinaryBiproducts C] : (triangle φ).mor₁ = fst φ

@[simp]

theorem CochainComplex.mappingCocone.triangle_mor₂ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasBinaryBiproducts C] : (triangle φ).mor₂ = φ

@[simp]

theorem CochainComplex.mappingCocone.triangle_obj₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasBinaryBiproducts C] : (triangle φ).obj₁ = mappingCocone φ

noncomputable def CochainComplex.mappingCocone.rotateTriangleIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) [CategoryTheory.Limits.HasBinaryBiproducts C] : (triangle φ).rotate ≅ mappingCone.triangle φ

Rotating the triangle mappingCocone.triangle φ gives a triangle that is isomorphic to mappingCone.triangle φ.