Loogle!

Result

Found 172 declarations mentioning CategoryTheory.Limits.CokernelCofork.

• CategoryTheory.Limits.CokernelCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) : Type (max u v)
• CategoryTheory.Limits.cokernel.zeroCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.CokernelCofork f
• CategoryTheory.Limits.CokernelCofork.ofπ 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {Z : C} (π : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f π = 0) : CategoryTheory.Limits.CokernelCofork f
• CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_of_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork f} (hc : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Epi f] : CategoryTheory.Limits.IsZero c.pt
• CategoryTheory.Limits.CokernelCofork.IsColimit.ofEpiOfIsZero 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (hf : CategoryTheory.Epi f) (h : CategoryTheory.Limits.IsZero c.pt) : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Limits.ofπCongr 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {P : C} {π π' : Y ⟶ P} {w : CategoryTheory.CategoryStruct.comp f π = 0} (h : π = π') : CategoryTheory.Limits.CokernelCofork.ofπ π w ≅ CategoryTheory.Limits.CokernelCofork.ofπ π' ⋯
• CategoryTheory.Limits.CokernelCofork.IsColimit.isIso_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (hc : CategoryTheory.Limits.IsColimit c) (hf : f = 0) : CategoryTheory.IsIso (CategoryTheory.Limits.Cofork.π c)
• CategoryTheory.Limits.CokernelCofork.mapOfIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CategoryTheory.Limits.CokernelCofork f} (hf : CategoryTheory.Limits.IsColimit cc) (cc' : CategoryTheory.Limits.CokernelCofork f') (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') : cc.pt ⟶ cc'.pt
• CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CategoryTheory.Limits.CokernelCofork f} {cc' : CategoryTheory.Limits.CokernelCofork f'} (hf : CategoryTheory.Limits.IsColimit cc) (hf' : CategoryTheory.Limits.IsColimit cc') (φ : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : cc.pt ≅ cc'.pt
• CategoryTheory.Limits.isCokernelEpiComp 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork f} (i : CategoryTheory.Limits.IsColimit c) {W : C} (g : W ⟶ X) [hg : CategoryTheory.Epi g] {h : W ⟶ Y} (hh : h = CategoryTheory.CategoryStruct.comp g f) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π c) ⋯)
• CategoryTheory.Limits.CokernelCofork.condition 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (s : CategoryTheory.Limits.CokernelCofork f) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Cofork.π s) = 0
• CategoryTheory.Limits.CokernelCofork.isColimitOfIsColimitOfIff' 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork f} (hc : CategoryTheory.Limits.IsColimit c) {X' : C} (f' : X' ⟶ Y) (iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), CategoryTheory.CategoryStruct.comp f φ = 0 ↔ CategoryTheory.CategoryStruct.comp f' φ = 0) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π c) ⋯)
• CategoryTheory.Limits.CokernelCofork.IsColimit.desc' 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {s : CategoryTheory.Limits.CokernelCofork f} (hs : CategoryTheory.Limits.IsColimit s) {W : C} (k : Y ⟶ W) (h : CategoryTheory.CategoryStruct.comp f k = 0) : { l // CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π s) l = k }
• CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CategoryTheory.Limits.CokernelCofork f} {cc' : CategoryTheory.Limits.CokernelCofork f'} (hf : CategoryTheory.Limits.IsColimit cc) (hf' : CategoryTheory.Limits.IsColimit cc') (φ : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : (CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit hf hf' φ).hom = CategoryTheory.Limits.CokernelCofork.mapOfIsColimit hf cc' φ.hom
• CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CategoryTheory.Limits.CokernelCofork f} {cc' : CategoryTheory.Limits.CokernelCofork f'} (hf : CategoryTheory.Limits.IsColimit cc) (hf' : CategoryTheory.Limits.IsColimit cc') (φ : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') : (CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit hf hf' φ).inv = CategoryTheory.Limits.CokernelCofork.mapOfIsColimit hf' cc φ.inv
• CategoryTheory.Limits.IsCokernel.cokernelIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {Z : C} (l : Y ⟶ Z) {s : CategoryTheory.Limits.CokernelCofork f} (hs : CategoryTheory.Limits.IsColimit s) (i : s.pt ≅ Z) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π s) i.hom = l) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ l ⋯)
• CategoryTheory.Limits.CokernelCofork.condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (s : CategoryTheory.Limits.CokernelCofork f) {Z : C} (h : s.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π s) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Limits.CokernelCofork.isColimitOfIsColimitOfIff 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork f} (hc : CategoryTheory.Limits.IsColimit c) {X' Y' : C} (f' : X' ⟶ Y') (e : Y' ≅ Y) (iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), CategoryTheory.CategoryStruct.comp f φ = 0 ↔ CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp e.hom φ) = 0) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.Limits.Cofork.π c)) ⋯)
• CategoryTheory.Limits.CokernelCofork.π_mapOfIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CategoryTheory.Limits.CokernelCofork f} (hf : CategoryTheory.Limits.IsColimit cc) (cc' : CategoryTheory.Limits.CokernelCofork f') (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc) (CategoryTheory.Limits.CokernelCofork.mapOfIsColimit hf cc' φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right φ) (CategoryTheory.Limits.Cofork.π cc')
• CategoryTheory.Limits.CokernelCofork.π_mapOfIsColimit_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CategoryTheory.Limits.CokernelCofork f} (hf : CategoryTheory.Limits.IsColimit cc) (cc' : CategoryTheory.Limits.CokernelCofork f') (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') {Z : C} (h : cc'.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CokernelCofork.mapOfIsColimit hf cc' φ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc') h)
• CategoryTheory.Limits.isCokernelOfComp 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {W : C} (g : W ⟶ X) (h : W ⟶ Y) {c : CategoryTheory.Limits.CokernelCofork h} (i : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Cofork.π c) = 0) (hfg : CategoryTheory.CategoryStruct.comp g f = h) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π c) hf)
• CategoryTheory.Limits.IsCokernel.ofIsoComp 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {Z : C} (l : Z ⟶ Y) (i : X ≅ Z) (h : CategoryTheory.CategoryStruct.comp i.hom l = f) {s : CategoryTheory.Limits.CokernelCofork f} (hs : CategoryTheory.Limits.IsColimit s) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π s) ⋯)
• CategoryTheory.Limits.IsCokernel.ofIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {X' Y' : C} {f' : X' ⟶ Y'} {s : CategoryTheory.Limits.CokernelCofork f} (hs : CategoryTheory.Limits.IsColimit s) (s' : CategoryTheory.Limits.CokernelCofork f') (eX : X ≅ X') (eY : Y ≅ Y') (e : s.pt ≅ s'.pt) (H : CategoryTheory.CategoryStruct.comp eX.hom f' = CategoryTheory.CategoryStruct.comp f eY.hom) (H' : CategoryTheory.CategoryStruct.comp eY.hom (CategoryTheory.Limits.Cofork.π s') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π s) e.hom) : CategoryTheory.Limits.IsColimit s'
• CategoryTheory.Limits.CokernelCofork.π_eq_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (s : CategoryTheory.Limits.CokernelCofork f) : s.ι.app CategoryTheory.Limits.WalkingParallelPair.zero = 0
• CategoryTheory.Limits.isCokernelEpiComp_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork f} (i : CategoryTheory.Limits.IsColimit c) {W : C} (g : W ⟶ X) [hg : CategoryTheory.Epi g] {h : W ⟶ Y} (hh : h = CategoryTheory.CategoryStruct.comp g f) (s : CategoryTheory.Limits.CokernelCofork h) : (CategoryTheory.Limits.isCokernelEpiComp i g hh).desc s = i.desc (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Limits.Cofork.π s) ⋯)
• CategoryTheory.Limits.isColimitAux 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (t : CategoryTheory.Limits.CokernelCofork f) (desc : (s : CategoryTheory.Limits.CokernelCofork f) → t.pt ⟶ s.pt) (fac : ∀ (s : CategoryTheory.Limits.CokernelCofork f), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π t) (desc s) = CategoryTheory.Limits.Cofork.π s) (uniq : ∀ (s : CategoryTheory.Limits.CokernelCofork f) (m : t.pt ⟶ s.pt), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π t) m = CategoryTheory.Limits.Cofork.π s → m = desc s) : CategoryTheory.Limits.IsColimit t
• CategoryTheory.Preadditive.coforkOfCokernelCofork 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork (f - g)) : CategoryTheory.Limits.Cofork f g
• CategoryTheory.Preadditive.cokernelCoforkOfCofork 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Cofork f g) : CategoryTheory.Limits.CokernelCofork (f - g)
• CategoryTheory.Preadditive.epi_of_isZero_cokernel' 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (hc : CategoryTheory.Limits.IsColimit c) (h : CategoryTheory.Limits.IsZero c.pt) : CategoryTheory.Epi f
• CategoryTheory.Preadditive.epi_iff_isZero_cokernel' 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Epi f ↔ CategoryTheory.Limits.IsZero c.pt
• CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork (f - g)} (i : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Preadditive.coforkOfCokernelCofork c)
• CategoryTheory.Preadditive.coforkOfCokernelCofork_pt 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork (f - g)) : (CategoryTheory.Preadditive.coforkOfCokernelCofork c).pt = c.pt
• CategoryTheory.Preadditive.cokernelCoforkOfCofork_ofπ 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} {P : C} (π : Y ⟶ P) (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π) : CategoryTheory.Preadditive.cokernelCoforkOfCofork (CategoryTheory.Limits.Cofork.ofπ π w) = CategoryTheory.Limits.CokernelCofork.ofπ π ⋯
• CategoryTheory.Preadditive.coforkOfCokernelCofork_π 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork (f - g)) : (CategoryTheory.Preadditive.coforkOfCokernelCofork c).π = CategoryTheory.Limits.Cofork.π c
• CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork (f - g)} (i : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cofork f g) : (CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork i).desc s = i.desc (CategoryTheory.Preadditive.cokernelCoforkOfCofork s)
• CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_cocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop) : (CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype f p).cocone = CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯
• CategoryTheory.Limits.BinaryBicone.inlCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y) : CategoryTheory.Limits.CokernelCofork c.inl
• CategoryTheory.Limits.BinaryBicone.inrCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y) : CategoryTheory.Limits.CokernelCofork c.inr
• CategoryTheory.Limits.biprod.inlCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.CokernelCofork CategoryTheory.Limits.biprod.inl
• CategoryTheory.Limits.biprod.inrCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.CokernelCofork CategoryTheory.Limits.biprod.inr
• CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f} (i : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.BinaryBicone X c.pt
• CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitMonoOfCokernel 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f} (i : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).IsBilimit
• CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_pt 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f} (i : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).pt = Y
• CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inl 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f} (i : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).inl = f
• CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_fst 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f} (i : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).fst = CategoryTheory.retraction f
• CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_snd 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f} (i : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).snd = CategoryTheory.Limits.Cofork.π c
• CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inr 📋 Mathlib.CategoryTheory.Preadditive.Biproducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f} (i : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).inr = let c' := CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.Cofork.π c) ⋯; have i' := CategoryTheory.Limits.isCokernelEpiComp i (CategoryTheory.retraction f) ⋯; have i'' := CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork i'; (CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork C ⋯ i'').section_
• ModuleCat.cokernelCocone 📋 Mathlib.Algebra.Category.ModuleCat.Kernels
  {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) : CategoryTheory.Limits.CokernelCofork f
• CategoryTheory.Limits.CokernelCofork.map 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] : CategoryTheory.Limits.CokernelCofork (G.map f)
• CategoryTheory.Limits.mapZeroCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Limits.cokernel.zeroCokernelCofork f).map G ≅ CategoryTheory.Limits.cokernel.zeroCokernelCofork (G.map f)
• CategoryTheory.Limits.CokernelCofork.mapIsColimit 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (hc : CategoryTheory.Limits.IsColimit c) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G] : CategoryTheory.Limits.IsColimit (c.map G)
• CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] : CategoryTheory.Limits.IsColimit (G.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (c.map G)
• CategoryTheory.Limits.CokernelCofork.map_π 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] : CategoryTheory.Limits.Cofork.π (c.map G) = G.map (CategoryTheory.Limits.Cofork.π c)
• CategoryTheory.Limits.CokernelCofork.map_condition 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] : CategoryTheory.CategoryStruct.comp (G.map f) (G.map (CategoryTheory.Limits.Cofork.π c)) = 0
• CategoryTheory.Limits.CokernelCofork.map_condition_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] {Z : D} (h : G.obj c.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Cofork.π c)) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Abelian.AbelianStruct.cokernelCofork 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.Abelian.AbelianStruct f) : CategoryTheory.Limits.CokernelCofork f
• CategoryTheory.Abelian.BiproductToPushoutIsCokernel.biproductToPushoutCofork 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasPushouts C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.biprod.lift f (-g))
• CategoryTheory.Abelian.AbelianStruct.mk 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} (kernelFork : CategoryTheory.Limits.KernelFork f) (isLimitKernelFork : CategoryTheory.Limits.IsLimit kernelFork) (cokernelCofork : CategoryTheory.Limits.CokernelCofork f) (isColimitCokernelCofork : CategoryTheory.Limits.IsColimit cokernelCofork) (image : C) (imageπ : X ⟶ image) (ι_imageπ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kernelFork) imageπ = 0 := by cat_disch) (imageIsCokernel : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ imageπ ι_imageπ)) (imageι : image ⟶ Y) (imageι_π : CategoryTheory.CategoryStruct.comp imageι (CategoryTheory.Limits.Cofork.π cokernelCofork) = 0 := by cat_disch) (imageIsKernel : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι imageι imageι_π)) (fac : CategoryTheory.CategoryStruct.comp imageπ imageι = f := by cat_disch) : CategoryTheory.Abelian.AbelianStruct f
• AddCommGrpCat.cokernelCocone 📋 Mathlib.Algebra.Category.Grp.Kernels
  {G H : AddCommGrpCat} (f : G ⟶ H) : CategoryTheory.Limits.CokernelCofork f
• CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : S.LeftHomologyData
• CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_K 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).K = S.X₂
• CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_i 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).i = CategoryTheory.CategoryStruct.id S.X₂
• CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_f' 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).f' = S.f
• CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_liftK 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) {T : C} (φ : T ⟶ S.X₂) : (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).liftK φ ⋯ = φ
• CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_H 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).H = c.pt
• CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.ShortComplex.LeftHomologyMapData (CategoryTheory.CategoryStruct.id S) (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg) (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc)
• CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φK 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φK = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).K
• CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_π 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).π = CategoryTheory.Limits.Cofork.π c
• CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φH 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φH = CategoryTheory.Limits.Cofork.π c
• CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : CategoryTheory.ShortComplex.LeftHomologyMapData φ (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁) (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S₂ hg₂ c₂ hc₂)
• CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork_φK 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : (CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φK = φ.τ₂
• CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork_φH 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : (CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φH = f
• CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : S.RightHomologyData
• CategoryTheory.ShortComplex.isoOpcyclesOfIsColimit 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] {cc : CategoryTheory.Limits.CokernelCofork S.f} (hcc : CategoryTheory.Limits.IsColimit cc) : cc.pt ≅ S.opcycles
• CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_H 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).H = c.pt
• CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_Q 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).Q = c.pt
• CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.ShortComplex.RightHomologyMapData (CategoryTheory.CategoryStruct.id S) (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg) (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc)
• CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_g' 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).g' = 0
• CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_p 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).p = CategoryTheory.Limits.Cofork.π c
• CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] {cc : CategoryTheory.Limits.CokernelCofork S.f} (hcc : CategoryTheory.Limits.IsColimit cc) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc) (S.isoOpcyclesOfIsColimit hcc).hom = S.pOpcycles
• CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_ι 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).ι = CategoryTheory.CategoryStruct.id c.pt
• CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φH 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φH = CategoryTheory.Limits.Cofork.π c
• CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φQ 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork S hf hg c hc).φQ = CategoryTheory.Limits.Cofork.π c
• CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] {cc : CategoryTheory.Limits.CokernelCofork S.f} (hcc : CategoryTheory.Limits.IsColimit cc) : CategoryTheory.CategoryStruct.comp S.pOpcycles (S.isoOpcyclesOfIsColimit hcc).inv = CategoryTheory.Limits.Cofork.π cc
• CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] {cc : CategoryTheory.Limits.CokernelCofork S.f} (hcc : CategoryTheory.Limits.IsColimit cc) {Z : C} (h : S.opcycles ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc) (CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom h) = CategoryTheory.CategoryStruct.comp S.pOpcycles h
• CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] {cc : CategoryTheory.Limits.CokernelCofork S.f} (hcc : CategoryTheory.Limits.IsColimit cc) {Z : C} (h : cc.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp S.pOpcycles (CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc) h
• CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : CategoryTheory.ShortComplex.RightHomologyMapData φ (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁) (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S₂ hg₂ c₂ hc₂)
• CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork_φH 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : (CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φH = f
• CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork_φQ 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : (CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φQ = f
• CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork 📋 Mathlib.Algebra.Homology.ShortComplex.Homology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : S.HomologyData
• CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_left 📋 Mathlib.Algebra.Homology.ShortComplex.Homology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc).left = CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc
• CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_right 📋 Mathlib.Algebra.Homology.ShortComplex.Homology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc).right = CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc
• CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_iso 📋 Mathlib.Algebra.Homology.ShortComplex.Homology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc).iso = CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).H
• CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork 📋 Mathlib.Algebra.Homology.ShortComplex.Homology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.CategoryStruct.id S) (CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg) (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc)
• CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork 📋 Mathlib.Algebra.Homology.ShortComplex.Homology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : CategoryTheory.ShortComplex.HomologyMapData φ (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁) (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S₂ hg₂ c₂ hc₂)
• CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork_left 📋 Mathlib.Algebra.Homology.ShortComplex.Homology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : (CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).left = CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm
• CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork_right 📋 Mathlib.Algebra.Homology.ShortComplex.Homology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (comm : CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f) : (CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).right = CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.g'_eq 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {cc : CategoryTheory.Limits.CokernelCofork S.f} (hcc : CategoryTheory.Limits.IsColimit cc) : hcc.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯) = CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom S.fromOpcycles
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : S.HomologyData
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : S.LeftHomologyData
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : S.RightHomologyData
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_H 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac).H = H
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_H 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData S hkf hcc fac).H = H
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : H ≅ S.homology
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_left 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation S hkf hcc fac).left = CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_right 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation S hkf hcc fac).right = CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData S hkf hcc fac
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_iso 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation S hkf hcc fac).iso = CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac).H
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_K 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac).K = kf.pt
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_Q 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData S hkf hcc fac).Q = cc.pt
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_π 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac).π = π
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_ι 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData S hkf hcc fac).ι = ι
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_i 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac).i = CategoryTheory.Limits.Fork.ι kf
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_p 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData S hkf hcc fac).p = CategoryTheory.Limits.Cofork.π cc
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : H ≅ CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : CategoryTheory.CategoryStruct.comp S.homologyπ (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).inv = CategoryTheory.CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).inv π
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).hom S.homologyι = CategoryTheory.CategoryStruct.comp ι (S.isoOpcyclesOfIsColimit hcc).hom
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] {Z : C} (h : H ⟶ Z) : CategoryTheory.CategoryStruct.comp S.homologyπ (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).inv h) = CategoryTheory.CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).inv (CategoryTheory.CategoryStruct.comp π h)
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] {Z : C} (h : S.opcycles ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).hom (CategoryTheory.CategoryStruct.comp S.homologyι h) = CategoryTheory.CategoryStruct.comp ι (CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom h)
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).inv ι = CategoryTheory.CategoryStruct.comp S.homologyι (S.isoOpcyclesOfIsColimit hcc).inv
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : CategoryTheory.CategoryStruct.comp π (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).hom = CategoryTheory.CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).hom S.homologyπ
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] {Z : C} (h : cc.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).inv (CategoryTheory.CategoryStruct.comp ι h) = CategoryTheory.CategoryStruct.comp S.homologyι (CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).inv h)
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] {Z : C} (h : S.homology ⟶ Z) : CategoryTheory.CategoryStruct.comp π (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).hom h) = CategoryTheory.CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).hom (CategoryTheory.CategoryStruct.comp S.homologyπ h)
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage S hkf hcc fac).hom (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)) = CategoryTheory.CategoryStruct.comp ι (S.isoOpcyclesOfIsColimit hcc).hom
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] {Z : C} (h : S.opcycles ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage S hkf hcc fac).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)) h) = CategoryTheory.CategoryStruct.comp ι (CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom h)
• CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc) : S.RightHomologyData
• CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_H 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc) : (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).H = 0
• CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_Q 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc) : (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).Q = cc.pt
• CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc) : (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).p = CategoryTheory.Limits.Cofork.π cc
• CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_ι 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [CategoryTheory.Limits.HasZeroObject C] (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc) : (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).ι = 0
• CategoryTheory.ShortComplex.exact_iff_of_forks 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {cg : CategoryTheory.Limits.KernelFork S.g} (hg : CategoryTheory.Limits.IsLimit cg) {cf : CategoryTheory.Limits.CokernelCofork S.f} (hf : CategoryTheory.Limits.IsColimit cf) : S.Exact ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι cg) (CategoryTheory.Limits.Cofork.π cf) = 0
• CategoryTheory.Limits.CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements 📋 Mathlib.CategoryTheory.Abelian.Refinements
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork f} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (y : A ⟶ Y) : CategoryTheory.CategoryStruct.comp y (CategoryTheory.Limits.Cofork.π c) = 0 ↔ ∃ A' π, ∃ (_ : CategoryTheory.Epi π), ∃ x, CategoryTheory.CategoryStruct.comp π y = CategoryTheory.CategoryStruct.comp x f
• HomologicalComplex.extend.rightHomologyData.cokernelCofork 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j : ι} {i' j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) : CategoryTheory.Limits.CokernelCofork ((K.extend e).d i' j')
• HomologicalComplex.extend.rightHomologyData.isColimitCokernelCofork 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j : ι} {i' j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) (hcocone : CategoryTheory.Limits.IsColimit cocone) : CategoryTheory.Limits.IsColimit (HomologicalComplex.extend.rightHomologyData.cokernelCofork K e hj' hi hi' cocone)
• HomologicalComplex.extend.leftHomologyData.cokernelCofork 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι} {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k) (hk' : c'.next j' = k') (cone : CategoryTheory.Limits.KernelFork (K.d j k)) (hcone : CategoryTheory.Limits.IsLimit cone) (cocone : CategoryTheory.Limits.CokernelCofork (hcone.lift (CategoryTheory.Limits.KernelFork.ofι (K.d i j) ⋯))) : CategoryTheory.Limits.CokernelCofork ((HomologicalComplex.extend.leftHomologyData.isLimitKernelFork K e hj' hk hk' cone hcone).lift (CategoryTheory.Limits.KernelFork.ofι ((K.extend e).d i' j') ⋯))
• HomologicalComplex.extend.rightHomologyData.kernelFork 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι} {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k) (hk' : c'.next j' = k') (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) (hcocone : CategoryTheory.Limits.IsColimit cocone) (cone : CategoryTheory.Limits.KernelFork (hcocone.desc (CategoryTheory.Limits.CokernelCofork.ofπ (K.d j k) ⋯))) : CategoryTheory.Limits.KernelFork ((HomologicalComplex.extend.rightHomologyData.isColimitCokernelCofork K e hj' hi hi' cocone hcocone).desc (CategoryTheory.Limits.CokernelCofork.ofπ ((K.extend e).d j' k') ⋯))
• HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff' 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι} {j' k' : ι'} (hj' : e.f j = j') (hk : c.next j = k) (hk' : c'.next j' = k') (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) (hcocone : CategoryTheory.Limits.IsColimit cocone) ⦃W : C⦄ (f' : cocone.pt ⟶ K.X k) (hf' : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cocone) f' = K.d j k) (f'' : cocone.pt ⟶ (K.extend e).X k') (hf'' : CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cocone) f'') = (K.extend e).d j' k') (φ : W ⟶ cocone.pt) : CategoryTheory.CategoryStruct.comp φ f' = 0 ↔ CategoryTheory.CategoryStruct.comp φ f'' = 0
• HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι} {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k) (hk' : c'.next j' = k') (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) (hcocone : CategoryTheory.Limits.IsColimit cocone) ⦃W : C⦄ (φ : W ⟶ cocone.pt) : CategoryTheory.CategoryStruct.comp φ (hcocone.desc (CategoryTheory.Limits.CokernelCofork.ofπ (K.d j k) ⋯)) = 0 ↔ CategoryTheory.CategoryStruct.comp φ ((HomologicalComplex.extend.rightHomologyData.isColimitCokernelCofork K e hj' hi hi' cocone hcocone).desc (CategoryTheory.Limits.CokernelCofork.ofπ ((K.extend e).d j' k') ⋯)) = 0
• HomologicalComplex.extend.leftHomologyData.isColimitCokernelCofork 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι} {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k) (hk' : c'.next j' = k') (cone : CategoryTheory.Limits.KernelFork (K.d j k)) (hcone : CategoryTheory.Limits.IsLimit cone) (cocone : CategoryTheory.Limits.CokernelCofork (hcone.lift (CategoryTheory.Limits.KernelFork.ofι (K.d i j) ⋯))) (hcocone : CategoryTheory.Limits.IsColimit cocone) : CategoryTheory.Limits.IsColimit (HomologicalComplex.extend.leftHomologyData.cokernelCofork K e hj' hi hi' hk hk' cone hcone cocone)
• HomologicalComplex.extend.rightHomologyData.isLimitKernelFork 📋 Mathlib.Algebra.Homology.Embedding.ExtendHomology
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι} {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k) (hk' : c'.next j' = k') (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) (hcocone : CategoryTheory.Limits.IsColimit cocone) (cone : CategoryTheory.Limits.KernelFork (hcocone.desc (CategoryTheory.Limits.CokernelCofork.ofπ (K.d j k) ⋯))) (hcone : CategoryTheory.Limits.IsLimit cone) : CategoryTheory.Limits.IsLimit (HomologicalComplex.extend.rightHomologyData.kernelFork K e hj' hi hi' hk hk' cocone hcocone cone)
• PresheafOfModules.freeYonedaCoproductsCokernelCofork 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
  {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : CategoryTheory.Limits.CokernelCofork M.toFreeYonedaCoproduct
• CategoryTheory.Limits.sigmaConstCokernelCofork 📋 Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (R : C) {α : Type u_1} {β : Type u_2} (f : α → β) [CategoryTheory.Limits.HasCoproduct fun x => R] [CategoryTheory.Limits.HasCoproduct fun x => R] [CategoryTheory.Limits.HasCoproduct fun x => R] : CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.Sigma.map' f fun x => CategoryTheory.CategoryStruct.id R)
• CategoryTheory.CommSq.cokernelCofork 📋 Mathlib.Algebra.Homology.CommSq
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CategoryTheory.CommSq f g inl inr) : CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.biprod.lift f (-g))
• CategoryTheory.ComposableArrows.IsComplex.cokerToKer' 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) : cc.pt ⟶ kf.pt
• CategoryTheory.ComposableArrows.Exact.cokerIsoKer' 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) : cc.pt ≅ kf.pt
• CategoryTheory.ComposableArrows.Exact.cokerToKer' 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) : cc.pt ⟶ kf.pt
• CategoryTheory.ComposableArrows.Exact.isIso_cokerToKer' 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) : CategoryTheory.IsIso (hS.cokerToKer' k hk cc kf hcc hkf)
• CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer' 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) (hS' : (S.sc hS k ⋯).Exact) : CategoryTheory.Mono (hS.cokerToKer' k hk cc kf hcc hkf)
• CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer' 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) (hS' : (S.sc hS (k + 1) ⋯).Exact) : CategoryTheory.Epi (hS.cokerToKer' k hk cc kf hcc hkf)
• CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) : (hS.cokerIsoKer' k hk cc kf hcc hkf).hom = hS.cokerToKer' k hk cc kf hcc hkf
• CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc) (CategoryTheory.CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf) (CategoryTheory.Limits.Fork.ι kf)) = S.map' (k + 1) (k + 2) ⋯ ⋯
• CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac_assoc 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) {Z : C} (h : S.obj ⟨k + 2, ⋯⟩ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc) (CategoryTheory.CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) h)) = CategoryTheory.CategoryStruct.comp (S.map' (k + 1) (k + 2) ⋯ ⋯) h
• CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) : CategoryTheory.CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf) (hS.cokerIsoKer' k hk cc kf hcc hkf).inv = CategoryTheory.CategoryStruct.id cc.pt
• CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id_assoc 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) {Z : C} (h : cc.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf) (CategoryTheory.CategoryStruct.comp (hS.cokerIsoKer' k hk cc kf hcc hkf).inv h) = h
• CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id_assoc 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) {Z : C} (h : kf.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (hS.cokerIsoKer' k hk cc kf hcc hkf).inv (CategoryTheory.CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf) h) = h
• CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id 📋 Mathlib.Algebra.Homology.ExactSequenceFour
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ) (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc) (hkf : CategoryTheory.Limits.IsLimit kf) : CategoryTheory.CategoryStruct.comp (hS.cokerIsoKer' k hk cc kf hcc hkf).inv (hS.cokerToKer' k hk cc kf hcc hkf) = CategoryTheory.CategoryStruct.id kf.pt
• CategoryTheory.ProjectiveResolution.cokernelCofork 📋 Mathlib.CategoryTheory.Preadditive.Projective.Resolution
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) : CategoryTheory.Limits.CokernelCofork (P.complex.d 1 0)
• CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.cc 📋 Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
  {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι) {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' : κ) (i₀ i₁ i₂ i₃ i₃' : ι) (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : CategoryTheory.Limits.CokernelCofork ((CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X data r hr).d pq pq')
• CategoryTheory.Square.cokernelCofork 📋 Mathlib.Algebra.Homology.Square
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (sq : CategoryTheory.Square C) [CategoryTheory.Limits.HasBinaryBiproduct sq.X₂ sq.X₃] : CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.biprod.lift sq.f₁₂ (-sq.f₁₃))
• SSetPair.cokernelCoforkChainComplex 📋 Mathlib.AlgebraicTopology.SimplicialSet.Homology.Relative
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) : CategoryTheory.Limits.CokernelCofork (SSet.chainComplexMap P.hom R)
• SSetPair.cokernelCoforkChainComplexFunctorLeftToRight 📋 Mathlib.AlgebraicTopology.SimplicialSet.Homology.Relative
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : CategoryTheory.Limits.CokernelCofork (SSetPair.chainComplexFunctorLeftToRight C)
• SSetPair.cokernelCoforkChainComplexX 📋 Mathlib.AlgebraicTopology.SimplicialSet.Homology.Relative
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : SSetPair) (R : C) (n : ℕ) : CategoryTheory.Limits.CokernelCofork ((SSet.chainComplexMap P.hom R).f n)
• SemiNormedGrp.cokernelLift 📋 Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
  {X Y : SemiNormedGrp} (f : X ⟶ Y) (s : CategoryTheory.Limits.CokernelCofork f) : (SemiNormedGrp.cokernelCocone f).pt ⟶ s.pt
• SemiNormedGrp₁.cokernelLift 📋 Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
  {X Y : SemiNormedGrp₁} (f : X ⟶ Y) (s : CategoryTheory.Limits.CokernelCofork f) : (SemiNormedGrp₁.cokernelCocone f).pt ⟶ s.pt
• CategoryTheory.MorphismProperty.cokernels.of_isColimit 📋 Mathlib.CategoryTheory.ObjectProperty.Kernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W : CategoryTheory.MorphismProperty C} {X₁ X₂ : C} (f : X₁ ⟶ X₂) (k : CategoryTheory.Limits.CokernelCofork f) (hk : CategoryTheory.Limits.IsColimit k) (hf : W f) : W.cokernels k.pt
• CategoryTheory.ObjectProperty.prop_of_isColimit_cokernelCofork 📋 Mathlib.CategoryTheory.ObjectProperty.Kernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderCokernels] {X Y : C} {f : X ⟶ Y} {k : CategoryTheory.Limits.CokernelCofork f} (hk : CategoryTheory.Limits.IsColimit k) (hX : P X) (hY : P Y) : P k.pt
• CategoryTheory.Limits.CokernelCofork.mapBifunctor 📋 Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
  {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} (c₁ : CategoryTheory.Limits.CokernelCofork f₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (c₂ : CategoryTheory.Limits.CokernelCofork f₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)] : CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
• CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor 📋 Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
  {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {c₁ : CategoryTheory.Limits.CokernelCofork f₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {c₂ : CategoryTheory.Limits.CokernelCofork f₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₂ 0) (F.obj c₁.pt)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj Y₂)] [CategoryTheory.Limits.HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj X₂)] : CategoryTheory.Limits.IsColimit (c₁.mapBifunctor c₂ F)
• CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor.hom_ext 📋 Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
  {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {c₁ : CategoryTheory.Limits.CokernelCofork f₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {c₂ : CategoryTheory.Limits.CokernelCofork f₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₂ 0) (F.obj c₁.pt)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj Y₂)] {T : C} {f g : (F.obj c₁.pt).obj c₂.pt ⟶ T} (h : CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.Limits.Cofork.π c₁)).app Y₂) (CategoryTheory.CategoryStruct.comp ((F.obj c₁.pt).map (CategoryTheory.Limits.Cofork.π c₂)) f) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.Limits.Cofork.π c₁)).app Y₂) (CategoryTheory.CategoryStruct.comp ((F.obj c₁.pt).map (CategoryTheory.Limits.Cofork.π c₂)) g)) : f = g
• CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor.exists_desc 📋 Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
  {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {c₁ : CategoryTheory.Limits.CokernelCofork f₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {c₂ : CategoryTheory.Limits.CokernelCofork f₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₂ 0) (F.obj c₁.pt)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj Y₂)] [CategoryTheory.Limits.HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj X₂)] (s : CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))) : ∃ l, CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.Limits.Cofork.π c₁)).app Y₂) (CategoryTheory.CategoryStruct.comp ((F.obj c₁.pt).map (CategoryTheory.Limits.Cofork.π c₂)) l) = CategoryTheory.Limits.Cofork.π s
• CategoryTheory.Limits.CokernelCofork.tensor 📋 Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {X₁ Y₁ : C} {f₁ : X₁ ⟶ Y₁} (c₁ : CategoryTheory.Limits.CokernelCofork f₁) {X₂ Y₂ : C} {f₂ : X₂ ⟶ Y₂} (c₂ : CategoryTheory.Limits.CokernelCofork f₂) [CategoryTheory.Limits.HasBinaryCoproduct (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ X₂)] : CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ Y₂) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y₁ f₂))
• CategoryTheory.Limits.CokernelCofork.isColimitTensor 📋 Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {X₁ Y₁ : C} {f₁ : X₁ ⟶ Y₁} {c₁ : CategoryTheory.Limits.CokernelCofork f₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁) {X₂ Y₂ : C} {f₂ : X₂ ⟶ Y₂} {c₂ : CategoryTheory.Limits.CokernelCofork f₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂) [CategoryTheory.Limits.HasBinaryCoproduct (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ X₂)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₂ 0) (CategoryTheory.MonoidalCategory.tensorLeft c₁.pt)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (CategoryTheory.MonoidalCategory.tensorRight Y₂)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (CategoryTheory.MonoidalCategory.tensorRight X₂)] : CategoryTheory.Limits.IsColimit (c₁.tensor c₂)
• CategoryTheory.Preadditive.RightFreyd.Candidate.cokernelCofork 📋 Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.Preadditive V] [CategoryTheory.Limits.HasBinaryBiproducts V] {u v : CategoryTheory.Arrow V} (f : u ⟶ v) : CategoryTheory.Limits.CokernelCofork ((CategoryTheory.Preadditive.RightFreyd.quotient V).map f)

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