Loogle!
Result
Found 131 declarations mentioning CochainComplex.HomComplex.Cochain.v.
- CochainComplex.HomComplex.Cochain.v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + n = q) : F.X p ⟶ G.X q - CochainComplex.HomComplex.Cochain.diff_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (p q : ℤ) (hpq : p + 1 = q) : (CochainComplex.HomComplex.Cochain.diff K).v p q hpq = K.d p q - CochainComplex.HomComplex.δ_neg_one_cochain 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cochain F G (-1)) : CochainComplex.HomComplex.δ (-1) 0 z = CochainComplex.HomComplex.Cochain.ofHom (Homotopy.nullHomotopicMap' fun i j hij => z.v i j ⋯) - CochainComplex.HomComplex.Cochain.congr_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} {z₁ z₂ : CochainComplex.HomComplex.Cochain F G n} (h : z₁ = z₂) (p q : ℤ) (hpq : p + n = q) : z₁.v p q hpq = z₂.v p q hpq - CochainComplex.HomComplex.Cochain.ext 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cochain F G n) (h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq) : z₁ = z₂ - CochainComplex.HomComplex.Cochain.ext_iff 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} {z₁ z₂ : CochainComplex.HomComplex.Cochain F G n} : z₁ = z₂ ↔ ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq - CochainComplex.HomComplex.Cochain.ext₀ 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cochain F G 0) (h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯) : z₁ = z₂ - CochainComplex.HomComplex.Cochain.ext₀_iff 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {z₁ z₂ : CochainComplex.HomComplex.Cochain F G 0} : z₁ = z₂ ↔ ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯ - CochainComplex.HomComplex.Cochain.ofHoms_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) (p : ℤ) : (CochainComplex.HomComplex.Cochain.ofHoms ψ).v p p ⋯ = ψ p - CochainComplex.HomComplex.Cochain.single_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ L.X q) (n : ℤ) (hpq : p + n = q) : (CochainComplex.HomComplex.Cochain.single f n).v p q hpq = f - CochainComplex.HomComplex.Cochain.mk_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (v : (p q : ℤ) → p + n = q → (F.X p ⟶ G.X q)) (p q : ℤ) (hpq : p + n = q) : (CochainComplex.HomComplex.Cochain.mk v).v p q hpq = v p q hpq - CochainComplex.HomComplex.Cochain.ofHom_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) (p : ℤ) : (CochainComplex.HomComplex.Cochain.ofHom φ).v p p ⋯ = φ.f p - CochainComplex.HomComplex.Cochain.comp_zero_cochain_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n) (z₂ : CochainComplex.HomComplex.Cochain G K 0) (p q : ℤ) (hpq : p + n = q) : (z₁.comp z₂ ⋯).v p q hpq = CategoryTheory.CategoryStruct.comp (z₁.v p q hpq) (z₂.v q q ⋯) - CochainComplex.HomComplex.Cochain.zero_cochain_comp_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G 0) (z₂ : CochainComplex.HomComplex.Cochain G K n) (p q : ℤ) (hpq : p + n = q) : (z₁.comp z₂ ⋯).v p q hpq = CategoryTheory.CategoryStruct.comp (z₁.v p p ⋯) (z₂.v p q hpq) - CochainComplex.HomComplex.Cocycle.homOf_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cocycle F G 0) (i : ℤ) : z.homOf.f i = (↑z).v i i ⋯ - CochainComplex.HomComplex.Cochain.comp_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (p₁ p₂ p₃ : ℤ) (h₁ : p₁ + n₁ = p₂) (h₂ : p₂ + n₂ = p₃) : (z₁.comp z₂ h).v p₁ p₃ ⋯ = CategoryTheory.CategoryStruct.comp (z₁.v p₁ p₂ h₁) (z₂.v p₂ p₃ h₂) - CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q q' : ℤ) (hpq : p + n = q) (hq' : q = q') : CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (HomologicalComplex.XIsoOfEq G hq').hom = γ.v p q' ⋯ - CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q q' : ℤ) (hpq : p + n = q) (hq' : q' = q) : CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (HomologicalComplex.XIsoOfEq G hq').inv = γ.v p q' ⋯ - CochainComplex.HomComplex.Cochain.zero_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (p q : ℤ) (hpq : p + n = q) : CochainComplex.HomComplex.Cochain.v 0 p q hpq = 0 - CochainComplex.HomComplex.Cochain.single_v_eq_zero 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ L.X q) (n p' q' : ℤ) (hpq' : p' + n = q') (hp' : p' ≠ p) : (CochainComplex.HomComplex.Cochain.single f n).v p' q' hpq' = 0 - CochainComplex.HomComplex.Cochain.single_v_eq_zero' 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ L.X q) (n p' q' : ℤ) (hpq' : p' + n = q') (hq' : q' ≠ q) : (CochainComplex.HomComplex.Cochain.single f n).v p' q' hpq' = 0 - CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q q' : ℤ) (hpq : p + n = q) (hq' : q = q') {Z : C} (h : G.X q' ⟶ Z) : CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq G hq').hom h) = CategoryTheory.CategoryStruct.comp (γ.v p q' ⋯) h - CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q q' : ℤ) (hpq : p + n = q) (hq' : q' = q) {Z : C} (h : G.X q' ⟶ Z) : CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq G hq').inv h) = CategoryTheory.CategoryStruct.comp (γ.v p q' ⋯) h - CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) (p' p q : ℤ) (hpq : p + 0 = q) : CategoryTheory.CategoryStruct.comp (F.d p' p) ((CochainComplex.HomComplex.Cochain.ofHoms ψ).v p q hpq) = CategoryTheory.CategoryStruct.comp (F.d p' q) (ψ q) - CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) (p q q' : ℤ) (hpq : p + 0 = q) : CategoryTheory.CategoryStruct.comp ((CochainComplex.HomComplex.Cochain.ofHoms ψ).v p q hpq) (G.d q q') = CategoryTheory.CategoryStruct.comp (ψ p) (G.d p q') - CochainComplex.HomComplex.Cochain.d_comp_ofHom_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) (p' p q : ℤ) (hpq : p + 0 = q) : CategoryTheory.CategoryStruct.comp (F.d p' p) ((CochainComplex.HomComplex.Cochain.ofHom φ).v p q hpq) = CategoryTheory.CategoryStruct.comp (F.d p' q) (φ.f q) - CochainComplex.HomComplex.Cochain.ofHom_v_comp_d 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) (p q q' : ℤ) (hpq : p + 0 = q) : CategoryTheory.CategoryStruct.comp ((CochainComplex.HomComplex.Cochain.ofHom φ).v p q hpq) (G.d q q') = CategoryTheory.CategoryStruct.comp (φ.f p) (G.d p q') - CochainComplex.HomComplex.Cochain.neg_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + n = q) : (-z).v p q hpq = -z.v p q hpq - CochainComplex.HomComplex.Cochain.sub_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + n = q) : (z₁ - z₂).v p q hpq = z₁.v p q hpq - z₂.v p q hpq - CochainComplex.HomComplex.Cochain.add_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + n = q) : (z₁ + z₂).v p q hpq = z₁.v p q hpq + z₂.v p q hpq - CochainComplex.HomComplex.Cochain.map_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] [CategoryTheory.Preadditive D] (z : CochainComplex.HomComplex.Cochain K L n) (Φ : CategoryTheory.Functor C D) [Φ.Additive] (p q : ℤ) (hpq : p + n = q) : (z.map Φ).v p q hpq = Φ.map (z.v p q hpq) - CochainComplex.HomComplex.δ_zero_cochain_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cochain F G 0) (p q : ℤ) (hpq : p + 1 = q) : (CochainComplex.HomComplex.δ 0 1 z).v p q hpq = CategoryTheory.CategoryStruct.comp (z.v p p ⋯) (G.d p q) - CategoryTheory.CategoryStruct.comp (F.d p q) (z.v q q ⋯) - CochainComplex.HomComplex.δ_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (n m : ℤ) (hnm : n + 1 = m) (z : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + m = q) (q₁ q₂ : ℤ) (hq₁ : q₁ = q - 1) (hq₂ : p + 1 = q₂) : (CochainComplex.HomComplex.δ n m z).v p q hpq = CategoryTheory.CategoryStruct.comp (z.v p q₁ ⋯) (G.d q₁ q) + m.negOnePow • CategoryTheory.CategoryStruct.comp (F.d p q₂) (z.v q₂ q ⋯) - CochainComplex.HomComplex.Cochain.smul_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} (k : R) (z : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + n = q) : (k • z).v p q hpq = k • z.v p q hpq - CochainComplex.HomComplex.Cochain.units_smul_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Ring R] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ} (k : Rˣ) (z : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + n = q) : (k • z).v p q hpq = k • z.v p q hpq - CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G) (z : { z // CochainComplex.HomComplex.Cochain.ofHom φ₁ = CochainComplex.HomComplex.δ (-1) 0 z + CochainComplex.HomComplex.Cochain.ofHom φ₂ }) (i j : ℤ) : ((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂).symm z).hom i j = if hij : i + -1 = j then (↑z).v i j hij else 0 - CochainComplex.mappingCone.inr_f_snd_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((CochainComplex.mappingCone.inr φ).f p) ((CochainComplex.mappingCone.snd φ).v p p ⋯) = CategoryTheory.CategoryStruct.id (G.X p) - CochainComplex.mappingCone.liftCochain_v_snd_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : ℤ} (α : 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₁₂ - CochainComplex.mappingCone.inr_f_snd_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((CochainComplex.mappingCone.inr φ).f p) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v p p ⋯) h) = h - CochainComplex.mappingCone.inr_f_descCochain_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : ℤ} (α : 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₁₂ - CochainComplex.mappingCone.inl_v_descCochain_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : ℤ} (α : 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₃ ⋯ - CochainComplex.mappingCone.liftCochain_v_snd_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : ℤ} (α : 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✝ - CochainComplex.mappingCone.inr_f_descCochain_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : ℤ} (α : 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✝ - CochainComplex.mappingCone.inl_v_descCochain_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : ℤ} (α : 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✝ - CochainComplex.mappingCone.inl_v_snd_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((CochainComplex.mappingCone.inl φ).v p q hpq) ((CochainComplex.mappingCone.snd φ).v q q ⋯) = 0 - CochainComplex.mappingCone.inl_v_fst_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((CochainComplex.mappingCone.inl φ).v p q ⋯) ((↑(CochainComplex.mappingCone.fst φ)).v q p hpq) = CategoryTheory.CategoryStruct.id (F.X p) - CochainComplex.mappingCone.inl_v_desc_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{C : Type u_1} [CategoryTheory.Category.{v, 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 - CochainComplex.mappingCone.inl_v_fst_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((CochainComplex.mappingCone.inl φ).v p q ⋯) (CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v q p hpq) h) = h - CochainComplex.mappingCone.liftCochain_v_fst_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : ℤ} (α : 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₃ ⋯ - CochainComplex.mappingCone.inl_v_snd_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((CochainComplex.mappingCone.inl φ).v p q hpq) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v q q ⋯) h) = CategoryTheory.CategoryStruct.comp 0 h - CochainComplex.mappingCone.inl_v_desc_f_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{C : Type u_1} [CategoryTheory.Category.{v, 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✝ - CochainComplex.mappingCone.liftCochain_v_fst_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : ℤ} (α : 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✝ - CochainComplex.mappingCone.lift_f_snd_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{C : Type u_1} [CategoryTheory.Category.{v, 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 - CochainComplex.mappingCone.ext_from 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : (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 - CochainComplex.mappingCone.ext_from_iff 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : (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 - CochainComplex.mappingCone.inr_f_fst_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((CochainComplex.mappingCone.inr φ).f p) ((↑(CochainComplex.mappingCone.fst φ)).v p q hpq) = 0 - CochainComplex.mappingCone.lift_f_snd_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{C : Type u_1} [CategoryTheory.Category.{v, 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 - CochainComplex.mappingCone.inr_f_fst_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((CochainComplex.mappingCone.inr φ).f p) (CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v p q hpq) h) = CategoryTheory.CategoryStruct.comp 0 h - CochainComplex.mappingCone.decomp_to 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ⟶ (CochainComplex.mappingCone φ).X i) (j : ℤ) (hij : i + 1 = j) : ∃ a b, f = CategoryTheory.CategoryStruct.comp a ((CochainComplex.mappingCone.inl φ).v j i ⋯) + CategoryTheory.CategoryStruct.comp b ((CochainComplex.mappingCone.inr φ).f i) - CochainComplex.mappingCone.lift_f_fst_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{C : Type u_1} [CategoryTheory.Category.{v, 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 - CochainComplex.mappingCone.ext_to 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ⟶ (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 - CochainComplex.mappingCone.ext_to_iff 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ⟶ (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 ⋯) - CochainComplex.mappingCone.decomp_from 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : (CochainComplex.mappingCone φ).X j ⟶ A) (i : ℤ) (hij : j + 1 = i) : ∃ a b, f = CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v j i hij) a + CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v j j ⋯) b - CochainComplex.mappingCone.lift_f_fst_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{C : Type u_1} [CategoryTheory.Category.{v, 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 - CochainComplex.mappingCone.liftCochain_v_descCochain_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : ℤ} (α : 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₂₃) - CochainComplex.mappingCone.inl_v_d 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((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) - CochainComplex.mappingCone.inl_v_d_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 : (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 - CochainComplex.mappingCone.d_fst_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((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) - CochainComplex.mappingCone.id_X 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((↑(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) - CochainComplex.mappingCone.d_snd_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((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) - CochainComplex.mappingCone.d_fst_v' 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((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) - CochainComplex.mappingCone.d_fst_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((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 - CochainComplex.mappingCone.desc_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{C : Type u_1} [CategoryTheory.Category.{v, 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) - CochainComplex.mappingCone.d_snd_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((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 - CochainComplex.mappingCone.d_fst_v'_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((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 - CochainComplex.mappingCone.lift_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{C : Type u_1} [CategoryTheory.Category.{v, 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) - CochainComplex.mappingCone.d_snd_v' 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((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) - CochainComplex.mappingCone.d_snd_v'_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ((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 - CochainComplex.mappingCone.lift_desc_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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 ℤ} (α : 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) - CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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) : (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) - CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{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) : (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)) - CochainComplex.HomComplex.Cochain.shift_v' 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a p q : ℤ) (hpq : p + n = q) : (γ.shift a).v p q hpq = γ.v (p + a) (q + a) ⋯ - CochainComplex.HomComplex.Cochain.rightShift_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n' + a = n) (p q : ℤ) (hpq : p + n' = q) (p' : ℤ) (hp' : p + n = p') : (γ.rightShift a n' hn').v p q hpq = CategoryTheory.CategoryStruct.comp (γ.v p p' hp') (L.shiftFunctorObjXIso a q p' ⋯).inv - CochainComplex.HomComplex.Cochain.rightUnshift_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) (p q : ℤ) (hpq : p + n = q) (p' : ℤ) (hp' : p + n' = p') : (γ.rightUnshift n hn).v p q hpq = CategoryTheory.CategoryStruct.comp (γ.v p p' hp') (L.shiftFunctorObjXIso a p' q ⋯).hom - CochainComplex.HomComplex.Cochain.leftUnshift_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') (p q : ℤ) (hpq : p + n = q) (p' : ℤ) (hp' : p' + n' = q) : (γ.leftUnshift n hn).v p q hpq = (a * n' + a * (a - 1) / 2).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p' p ⋯).inv (γ.v p' q ⋯) - CochainComplex.HomComplex.Cochain.shift_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a p q : ℤ) (hpq : p + n = q) (p' q' : ℤ) (hp' : p' = p + a) (hq' : q' = q + a) : (γ.shift a).v p q hpq = CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p p' hp').hom (CategoryTheory.CategoryStruct.comp (γ.v p' q' ⋯) (L.shiftFunctorObjXIso a q q' hq').inv) - CochainComplex.HomComplex.Cochain.leftShift_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n') (p q : ℤ) (hpq : p + n' = q) (p' : ℤ) (hp' : p' + n = q) : (γ.leftShift a n' hn').v p q hpq = (a * n' + a * (a - 1) / 2).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p p' ⋯).hom (γ.v p' q hp') - CochainComplex.mappingCone.inl_v_triangle_mor₃_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (p q : ℤ) (hpq : p + -1 = q) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q hpq) ((CochainComplex.mappingCone.triangle φ).mor₃.f q) = -(K.shiftFunctorObjXIso 1 q p ⋯).inv - CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (p q : ℤ) (hpq : p + -1 = q) {Z : C} (h : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle φ).obj₁).X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q hpq) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.triangle φ).mor₃.f q) h) = CategoryTheory.CategoryStruct.comp (-(K.shiftFunctorObjXIso 1 q p ⋯).inv) h - CochainComplex.mappingCone.triangleRotateShortComplexSplitting_r 📋 Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) : (CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ n).r = (CochainComplex.mappingCone.snd φ).v n n ⋯ - CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s 📋 Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) : (CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ n).s = -(CochainComplex.mappingCone.inl φ).v (n + 1) n ⋯ - CochainComplex.homOfDegreewiseSplit_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) (n : ℤ) : (CochainComplex.homOfDegreewiseSplit S σ).f n = (↑(CochainComplex.cocycleOfDegreewiseSplit S σ)).v n (n + 1) ⋯ - CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
{C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (p : ℤ) : (↑(CochainComplex.cocycleOfDegreewiseSplit (CochainComplex.mappingCone.triangleRotateShortComplex φ) (CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ))).v p (p + 1) ⋯ = -φ.f (p + { as := 1 }.as) - CochainComplex.mappingCocone.inl_v_fst_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ((CochainComplex.mappingCocone.inl φ).v p p ⋯) ((CochainComplex.mappingCocone.fst φ).f p) = CategoryTheory.CategoryStruct.id (K.X p) - CochainComplex.mappingCocone.inl_v_descCochain_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.HomComplex.Cochain L M n) (h : m + 1 = n) (p q : ℤ) (hpq : p + m = q) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.inl φ).v p p ⋯) ((CochainComplex.mappingCocone.descCochain φ α β h).v p q hpq) = α.v p q hpq - CochainComplex.mappingCocone.inl_v_fst_f_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ((CochainComplex.mappingCocone.inl φ).v p p ⋯) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.fst φ).f p) h) = h - CochainComplex.mappingCocone.liftCochain_v_fst_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 : ℤ} (α : CochainComplex.HomComplex.Cochain M K n) (β : CochainComplex.HomComplex.Cochain M L m) (h : m + 1 = n) (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.liftCochain φ α β h).v p₁ p₂ h₁₂) ((CochainComplex.mappingCocone.fst φ).f p₂) = α.v p₁ p₂ h₁₂ - CochainComplex.mappingCocone.liftCochain_v_snd_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 : ℤ} (α : CochainComplex.HomComplex.Cochain M K n) (β : CochainComplex.HomComplex.Cochain M L m) (h : m + 1 = n) (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + -1 = p₃) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.liftCochain φ α β h).v p₁ p₂ h₁₂) ((CochainComplex.mappingCocone.snd φ).v p₂ p₃ h₂₃) = β.v p₁ p₃ ⋯ - CochainComplex.mappingCocone.inl_v_descCochain_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.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 ((CochainComplex.mappingCocone.inl φ).v p p ⋯) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.descCochain φ α β h).v p q hpq) h✝) = CategoryTheory.CategoryStruct.comp (α.v p q hpq) h✝ - CochainComplex.mappingCocone.liftCochain_v_fst_f_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 : ℤ} (α : CochainComplex.HomComplex.Cochain M K n) (β : CochainComplex.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 ((CochainComplex.mappingCocone.liftCochain φ α β h).v p₁ p₂ h₁₂) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.fst φ).f p₂) h✝) = CategoryTheory.CategoryStruct.comp (α.v p₁ p₂ h₁₂) h✝ - CochainComplex.mappingCocone.liftCochain_v_snd_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 : ℤ} (α : CochainComplex.HomComplex.Cochain M K n) (β : CochainComplex.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 ((CochainComplex.mappingCocone.liftCochain φ α β h).v p₁ p₂ h₁₂) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.snd φ).v p₂ p₃ h₂₃) h✝) = CategoryTheory.CategoryStruct.comp (β.v p₁ p₃ ⋯) h✝ - CochainComplex.mappingCocone.inl_v_snd_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ((CochainComplex.mappingCocone.inl φ).v p p ⋯) ((CochainComplex.mappingCocone.snd φ).v p q hpq) = 0 - CochainComplex.mappingCocone.inr_v_snd_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq) ((CochainComplex.mappingCocone.snd φ).v q p ⋯) = CategoryTheory.CategoryStruct.id (L.X p) - CochainComplex.mappingCocone.inr_v_snd_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.snd φ).v q p ⋯) h) = h - CochainComplex.mappingCocone.inr_v_descCochain_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.HomComplex.Cochain L M n) (h : m + 1 = n) (p q : ℤ) (hpq : p + 1 = q) (r : ℤ) (hr : q + m = r) : CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq) ((CochainComplex.mappingCocone.descCochain φ α β h).v q r hr) = β.v p r ⋯ - CochainComplex.mappingCocone.inl_v_snd_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ((CochainComplex.mappingCocone.inl φ).v p p ⋯) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.snd φ).v p q hpq) h) = CategoryTheory.CategoryStruct.comp 0 h - CochainComplex.mappingCocone.inr_v_descCochain_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.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 ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.descCochain φ α β h).v q r hr) h✝) = CategoryTheory.CategoryStruct.comp (β.v p r ⋯) h✝ - CochainComplex.mappingCocone.inl_v_desc_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ℤ} (α : CochainComplex.HomComplex.Cochain K M 0) (β : CochainComplex.HomComplex.Cocycle L M 1) (hαβ : CochainComplex.HomComplex.δ 0 1 α + (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) (p : ℤ) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.inl φ).v p p ⋯) ((CochainComplex.mappingCocone.desc φ α β hαβ).f p) = α.v p p ⋯ - CochainComplex.mappingCocone.lift_f_snd_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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) (β : CochainComplex.HomComplex.Cochain M L (-1)) (hαβ : CochainComplex.HomComplex.δ (-1) 0 β + CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) = 0) (p q : ℤ) (hpq : p + -1 = q) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.lift φ α β hαβ).f p) ((CochainComplex.mappingCocone.snd φ).v p q hpq) = β.v p q hpq - CochainComplex.mappingCocone.inr_v_fst_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq) ((CochainComplex.mappingCocone.fst φ).f q) = 0 - CochainComplex.mappingCocone.inl_v_desc_f_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ℤ} (α : CochainComplex.HomComplex.Cochain K M 0) (β : CochainComplex.HomComplex.Cocycle L M 1) (hαβ : CochainComplex.HomComplex.δ 0 1 α + (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) (p : ℤ) {Z : C} (h : M.X p ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.inl φ).v p p ⋯) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.desc φ α β hαβ).f p) h) = CategoryTheory.CategoryStruct.comp (α.v p p ⋯) h - CochainComplex.mappingCocone.lift_f_snd_v_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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) (β : CochainComplex.HomComplex.Cochain M L (-1)) (hαβ : CochainComplex.HomComplex.δ (-1) 0 β + CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) = 0) (p q : ℤ) (hpq : p + -1 = q) {Z : C} (h : L.X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.lift φ α β hαβ).f p) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.snd φ).v p q hpq) h) = CategoryTheory.CategoryStruct.comp (β.v p q hpq) h - CochainComplex.mappingCocone.inr_v_fst_f_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.fst φ).f q) h) = CategoryTheory.CategoryStruct.comp 0 h - CochainComplex.mappingCocone.inr_v_desc_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ℤ} (α : CochainComplex.HomComplex.Cochain K M 0) (β : CochainComplex.HomComplex.Cocycle L M 1) (hαβ : CochainComplex.HomComplex.δ 0 1 α + (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) (p q : ℤ) (hpq : p + 1 = q) : CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq) ((CochainComplex.mappingCocone.desc φ α β hαβ).f q) = (↑β).v p q hpq - CochainComplex.mappingCocone.inr_v_desc_f_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ℤ} (α : CochainComplex.HomComplex.Cochain K M 0) (β : CochainComplex.HomComplex.Cocycle L M 1) (hαβ : CochainComplex.HomComplex.δ 0 1 α + (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) (p q : ℤ) (hpq : p + 1 = q) {Z : C} (h : M.X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.desc φ α β hαβ).f q) h) = CategoryTheory.CategoryStruct.comp ((↑β).v p q hpq) h - CochainComplex.mappingCocone.id_X 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
{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 ((CochainComplex.mappingCocone.fst φ).f p) ((CochainComplex.mappingCocone.inl φ).v p p ⋯) + CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.snd φ).v p q hpq) ((↑(CochainComplex.mappingCocone.inr φ)).v q p ⋯) = CategoryTheory.CategoryStruct.id ((CochainComplex.mappingCocone φ).X p) - CochainComplex.mappingCone.inl_v_descShortComplex_f 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (i j : ℤ) (h : i + -1 = j) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl S.f).v i j h) ((CochainComplex.mappingCone.descShortComplex S).f j) = 0 - CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (i j : ℤ) (h : i + -1 = j) {Z : C} (h✝ : S.X₃.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl S.f).v i j h) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.descShortComplex S).f j) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝ - CochainComplex.cm5b.i_f_comp 📋 Mathlib.Algebra.Homology.Factorizations.CM5b
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ) : CategoryTheory.CategoryStruct.comp ((CochainComplex.cm5b.i f).f n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f n) ((CochainComplex.mappingCone.snd (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K))).v n n ⋯)) = CategoryTheory.Injective.ι (K.X n) - CochainComplex.cm5b.i_f_comp_assoc 📋 Mathlib.Algebra.Homology.Factorizations.CM5b
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ) {Z : C} (h : (CochainComplex.cm5b.I K).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CochainComplex.cm5b.i f).f n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f n) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K))).v n n ⋯) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Injective.ι (K.X n)) h - CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zero 📋 Mathlib.Algebra.Homology.ModelCategory.Lifting
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b) (hsq : (n : ℤ) → ⋯.LiftStruct) (n m : ℤ) (hnm : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm) (p.f m) = 0 - CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero 📋 Mathlib.Algebra.Homology.ModelCategory.Lifting
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b) (hsq : (n : ℤ) → ⋯.LiftStruct) (n m : ℤ) (hnm : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (i.f n) ((↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm) = 0 - CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zero_assoc 📋 Mathlib.Algebra.Homology.ModelCategory.Lifting
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b) (hsq : (n : ℤ) → ⋯.LiftStruct) (n m : ℤ) (hnm : n + 1 = m := by lia) {Z : C} (h : Y.X m ⟶ Z) : CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm) (CategoryTheory.CategoryStruct.comp (p.f m) h) = CategoryTheory.CategoryStruct.comp 0 h - CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero_assoc 📋 Mathlib.Algebra.Homology.ModelCategory.Lifting
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b) (hsq : (n : ℤ) → ⋯.LiftStruct) (n m : ℤ) (hnm : n + 1 = m := by lia) {Z : C} (h : X.X m ⟶ Z) : CategoryTheory.CategoryStruct.comp (i.f n) (CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm) h) = CategoryTheory.CategoryStruct.comp 0 h - CochainComplex.Lifting.π_f_cochain₁_v_ι_f 📋 Mathlib.Algebra.Homology.ModelCategory.Lifting
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b) (hsq : (n : ℤ) → ⋯.LiftStruct) {Q : CochainComplex C ℤ} {π : B ⟶ Q} {hπ : CategoryTheory.CategoryStruct.comp i π = 0} (hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ)) {K : CochainComplex C ℤ} {ι : K ⟶ X} {hι : CategoryTheory.CategoryStruct.comp ι p = 0} (hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι)) (n m : ℤ) (hnm : n + 1 = m) : CategoryTheory.CategoryStruct.comp (π.f n) (CategoryTheory.CategoryStruct.comp ((CochainComplex.Lifting.cochain₁ sq hsq hQ hK).v n m hnm) (ι.f m)) = (↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm - CochainComplex.Lifting.π_f_cochain₁_v_ι_f_assoc 📋 Mathlib.Algebra.Homology.ModelCategory.Lifting
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b) (hsq : (n : ℤ) → ⋯.LiftStruct) {Q : CochainComplex C ℤ} {π : B ⟶ Q} {hπ : CategoryTheory.CategoryStruct.comp i π = 0} (hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ)) {K : CochainComplex C ℤ} {ι : K ⟶ X} {hι : CategoryTheory.CategoryStruct.comp ι p = 0} (hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι)) (n m : ℤ) (hnm : n + 1 = m) {Z : C} (h : X.X m ⟶ Z) : CategoryTheory.CategoryStruct.comp (π.f n) (CategoryTheory.CategoryStruct.comp ((CochainComplex.Lifting.cochain₁ sq hsq hQ hK).v n m hnm) (CategoryTheory.CategoryStruct.comp (ι.f m) h)) = CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm) h - CochainComplex.Lifting.exists_hom 📋 Mathlib.Algebra.Homology.ModelCategory.Lifting
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b) (hsq : (n : ℤ) → ⋯.LiftStruct) {Q : CochainComplex C ℤ} {π : B ⟶ Q} {hπ : CategoryTheory.CategoryStruct.comp i π = 0} (hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ)) {K : CochainComplex C ℤ} {ι : K ⟶ X} {hι : CategoryTheory.CategoryStruct.comp ι p = 0} (hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι)) (n m : ℤ) (hnm : n + 1 = m := by lia) : ∃ φ, CategoryTheory.CategoryStruct.comp (π.f n) (CategoryTheory.CategoryStruct.comp φ (ι.f m)) = (↑(CochainComplex.Lifting.cocycle₁' sq hsq)).v n m hnm - CochainComplex.HomComplex.Cochain.fromSingleMk_v_eq_zero 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) (p' q' : ℤ) (hpq' : p' + n = q') (hp' : p' ≠ p) : (CochainComplex.HomComplex.Cochain.fromSingleMk f h).v p' q' hpq' = 0 - CochainComplex.HomComplex.Cochain.toSingleMk_v_eq_zero 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) (p' q' : ℤ) (hpq' : p' + n = q') (hp' : p' ≠ p) : (CochainComplex.HomComplex.Cochain.toSingleMk f h).v p' q' hpq' = 0 - CochainComplex.HomComplex.Cochain.fromSingleMk_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) : (CochainComplex.HomComplex.Cochain.fromSingleMk f h).v p q h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).hom f - CochainComplex.HomComplex.Cochain.toSingleMk_v 📋 Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) : (CochainComplex.HomComplex.Cochain.toSingleMk f h).v p q h = CategoryTheory.CategoryStruct.comp f (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).inv
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using the Loogle command from the command palette. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?bBy main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→and∀) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.You can filter for definitions vs theorems: Using
⊢ (_ : Type _)finds all definitions which provide data while⊢ (_ : Prop)finds all theorems (and definitions of proofs).
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.
This is Loogle revision 9f11169 serving mathlib revision 69fae59