Loogle!

Result

Found 58 declarations mentioning CochainComplex.mappingCone.inr.

• CochainComplex.mappingCone.inr 📋 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 φ] : G ⟶ CochainComplex.mappingCone φ
• CochainComplex.mappingCone.inr_descCochain 📋 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) : (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp (CochainComplex.mappingCone.descCochain φ α β h) ⋯ = β
• CochainComplex.mappingCone.inr_snd_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 ℤ} {d e : ℤ} (γ : CochainComplex.HomComplex.Cochain G K d) (he : 0 + d = e) : (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp ((CochainComplex.mappingCone.snd φ).comp γ he) ⋯ = γ
• CochainComplex.mappingCone.δ_inl 📋 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 φ] : CochainComplex.HomComplex.δ (-1) 0 (CochainComplex.mappingCone.inl φ) = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ (CochainComplex.mappingCone.inr φ))
• CochainComplex.mappingCone.inr_snd 📋 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 φ] : (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp (CochainComplex.mappingCone.snd φ) ⋯ = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id G)
• CochainComplex.mappingCone.ext_cochain_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 : i + 1 = j) {K : CochainComplex C ℤ} {γ₁ γ₂ : CochainComplex.HomComplex.Cochain (CochainComplex.mappingCone φ) K j} : γ₁ = γ₂ ↔ (CochainComplex.mappingCone.inl φ).comp γ₁ ⋯ = (CochainComplex.mappingCone.inl φ).comp γ₂ ⋯ ∧ (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp γ₁ ⋯ = (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp γ₂ ⋯
• 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.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.inr_fst 📋 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 φ] : (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp ↑(CochainComplex.mappingCone.fst φ) ⋯ = 0
• CochainComplex.mappingCone.inr_fst_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 ℤ} {d e f : ℤ} (γ : CochainComplex.HomComplex.Cochain F K d) (he : 1 + d = e) (hf : 0 + e = f) : (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp ((↑(CochainComplex.mappingCone.fst φ)).comp γ he) hf = 0
• CochainComplex.mappingCone.inr_desc 📋 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 φ β)) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) (CochainComplex.mappingCone.desc φ α β eq) = β
• 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.δ_liftCochain 📋 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) (m' : ℤ) (hm' : m + 1 = m') : CochainComplex.HomComplex.δ n m (CochainComplex.mappingCone.liftCochain φ α β h) = -(CochainComplex.HomComplex.δ m m' α).comp (CochainComplex.mappingCone.inl φ) ⋯ + (CochainComplex.HomComplex.δ n m β + α.comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯).comp (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)) ⋯
• CochainComplex.mappingCone.inr_f_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 φ] (n₁ n₂ : ℤ) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f n₁) ((CochainComplex.mappingCone φ).d n₁ n₂) = CategoryTheory.CategoryStruct.comp (G.d n₁ n₂) ((CochainComplex.mappingCone.inr φ).f n₂)
• CochainComplex.mappingCone.inr_f_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 : ℤ) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p) ((CochainComplex.mappingCone.desc φ α β eq).f p) = β.f p
• CochainComplex.mappingCone.inr_f_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 φ] (n₁ n₂ : ℤ) {Z : C} (h : (CochainComplex.mappingCone φ).X n₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f n₁) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d n₁ n₂) h) = CategoryTheory.CategoryStruct.comp (G.d n₁ n₂) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f n₂) h)
• CochainComplex.mappingCone.inr_f_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 : ℤ) {Z : C} (h : K.X p ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.desc φ α β eq).f p) h) = CategoryTheory.CategoryStruct.comp (β.f p) h
• CochainComplex.mappingCone.inr_desc_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 φ β)) {Z : CochainComplex C ℤ} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.desc φ α β eq) h) = CategoryTheory.CategoryStruct.comp β h
• 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.id 📋 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 φ] : (↑(CochainComplex.mappingCone.fst φ)).comp (CochainComplex.mappingCone.inl φ) ⋯ + (CochainComplex.mappingCone.snd φ).comp (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)) ⋯ = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone φ))
• 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.descHomotopy 📋 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 ℤ} (f₁ f₂ : CochainComplex.mappingCone φ ⟶ K) (γ₁ : CochainComplex.HomComplex.Cochain F K (-2)) (γ₂ : CochainComplex.HomComplex.Cochain G K (-1)) (h₁ : (CochainComplex.mappingCone.inl φ).comp (CochainComplex.HomComplex.Cochain.ofHom f₁) ⋯ = CochainComplex.HomComplex.δ (-2) (-1) γ₁ + (CochainComplex.HomComplex.Cochain.ofHom φ).comp γ₂ ⋯ + (CochainComplex.mappingCone.inl φ).comp (CochainComplex.HomComplex.Cochain.ofHom f₂) ⋯) (h₂ : CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) f₁) = CochainComplex.HomComplex.δ (-1) 0 γ₂ + CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) f₂)) : Homotopy f₁ f₂
• 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.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.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.map_inr 📋 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 φ)] : CategoryTheory.CategoryStruct.comp ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.inr φ)) (CochainComplex.mappingCone.mapHomologicalComplexIso φ H).hom = CochainComplex.mappingCone.inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
• 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.mappingCone.triangle_mor₂ 📋 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) : (CochainComplex.mappingCone.triangle φ).mor₂ = CochainComplex.mappingCone.inr φ
• CochainComplex.mappingCone.rotateTrianglehIso 📋 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) : (CochainComplex.mappingCone.triangleh φ).rotate ≅ CochainComplex.mappingCone.triangleh (CochainComplex.mappingCone.inr φ)
• CochainComplex.mappingCone.rotateHomotopyEquiv 📋 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) : HomotopyEquiv ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1).obj K) (CochainComplex.mappingCone (CochainComplex.mappingCone.inr φ))
• CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂ 📋 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₁ K₂ L₂ : CochainComplex C ℤ} {φ₁ : K₁ ⟶ L₁} {φ₂ : K₂ ⟶ L₂} {a : K₁ ⟶ K₂} {b : L₁ ⟶ L₂} (H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂)) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ₁) (CochainComplex.mappingCone.mapOfHomotopy H) = CategoryTheory.CategoryStruct.comp b (CochainComplex.mappingCone.inr φ₂)
• CochainComplex.mappingCone.inr_triangleδ 📋 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) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) (CochainComplex.mappingCone.triangle φ).mor₃ = 0
• CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂_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₁ K₂ L₂ : CochainComplex C ℤ} {φ₁ : K₁ ⟶ L₁} {φ₂ : K₂ ⟶ L₂} {a : K₁ ⟶ K₂} {b : L₁ ⟶ L₂} (H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂)) {Z : CochainComplex C ℤ} (h : CochainComplex.mappingCone φ₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ₁) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.mapOfHomotopy H) h) = CategoryTheory.CategoryStruct.comp b (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ₂) h)
• CochainComplex.mappingCone.inr_f_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 : ℤ) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p) ((CochainComplex.mappingCone.triangle φ).mor₃.f p) = 0
• CochainComplex.mappingCone.inr_triangleδ_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) {Z : CochainComplex C ℤ} (h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle φ).obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle φ).mor₃ h) = CategoryTheory.CategoryStruct.comp 0 h
• CochainComplex.mappingCone.inr_f_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 : ℤ) {Z : C} (h : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle φ).obj₁).X p ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.triangle φ).mor₃.f p) h) = CategoryTheory.CategoryStruct.comp 0 h
• CochainComplex.mappingCone.rotateHomotopyEquivComm₂Homotopy 📋 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) : Homotopy (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle φ).mor₃ (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom) (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.inr φ))
• CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃ 📋 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) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom (CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.inr φ)).mor₃ = -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ
• CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_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) {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.inr φ)).obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.inr φ)).mor₃ h) = CategoryTheory.CategoryStruct.comp (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ) h
• CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂ 📋 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) : CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle φ).mor₃) ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.inr φ))
• CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_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) {Z : HomotopyCategory C (ComplexShape.up ℤ)} (h : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (CochainComplex.mappingCone.inr φ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle φ).mor₃) (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.inr φ))) h
• CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv 📋 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) [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.f) (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv = -CochainComplex.mappingCone.inr (CochainComplex.homOfDegreewiseSplit S σ)
• CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc 📋 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) [CategoryTheory.Limits.HasBinaryBiproducts C] {Z : CochainComplex C ℤ} (h : CochainComplex.mappingCone (CochainComplex.homOfDegreewiseSplit S σ) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.f) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv h) = CategoryTheory.CategoryStruct.comp (-CochainComplex.mappingCone.inr (CochainComplex.homOfDegreewiseSplit S σ)) h
• CochainComplex.mappingConeCompTriangle_mor₃ 📋 Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : (CochainComplex.mappingConeCompTriangle f g).mor₃ = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle g).mor₃ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (CochainComplex.mappingCone.inr f))
• CochainComplex.mappingConeCompHomotopyEquiv_comm₁ 📋 Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X₁) g ⋯)) (CochainComplex.mappingConeCompHomotopyEquiv f g).inv = (CochainComplex.mappingConeCompTriangle f g).mor₂
• CochainComplex.mappingConeCompTriangleh_comm₁ 📋 Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangleh f g).mor₂ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingConeCompHomotopyEquiv f g).hom) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.inr (CochainComplex.mappingConeCompTriangle f g).mor₁)
• CochainComplex.mappingConeCompTriangleh_comm₁_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Z : HomotopyCategory C (ComplexShape.up ℤ)} (h : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (CochainComplex.mappingConeCompTriangle f g).mor₁) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangleh f g).mor₂ (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingConeCompHomotopyEquiv f g).hom) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.inr (CochainComplex.mappingConeCompTriangle f g).mor₁)) h
• CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc 📋 Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Z : CochainComplex C ℤ} (h : CochainComplex.mappingCone g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X₁) g ⋯)) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).inv h) = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f g).mor₂ h
• CochainComplex.mappingCone.inr_descShortComplex 📋 Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr S.f) (CochainComplex.mappingCone.descShortComplex S) = S.g
• CochainComplex.mappingCone.inr_descShortComplex_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 ℤ)) {Z : CochainComplex C ℤ} (h : S.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr S.f) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.descShortComplex S) h) = CategoryTheory.CategoryStruct.comp S.g h
• CochainComplex.mappingCone.inr_f_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 ℤ)) (n : ℤ) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr S.f).f n) ((CochainComplex.mappingCone.descShortComplex S).f n) = S.g.f n
• CochainComplex.mappingCone.inr_f_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 ℤ)) (n : ℤ) {Z : C} (h : S.X₃.X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr S.f).f n) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.descShortComplex S).f n) h) = CategoryTheory.CategoryStruct.comp (S.g.f n) h

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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 ?a

   If 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 ?b

4. By 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 find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. 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