Loogle!

Result

Found 2587 declarations mentioning CategoryTheory.Abelian. Of these, only the first 200 are shown.

• CategoryTheory.Abelian 📋 Mathlib.CategoryTheory.Abelian.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max u v)
• CategoryTheory.Abelian.hasCoequalizers 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasCoequalizers C
• CategoryTheory.Abelian.hasEqualizers 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasEqualizers C
• CategoryTheory.Abelian.hasFiniteColimits 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasFiniteColimits C
• CategoryTheory.Abelian.hasFiniteLimits 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.Abelian.hasPullbacks 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasPullbacks C
• CategoryTheory.Abelian.hasPushouts 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasPushouts C
• CategoryTheory.Abelian.hasZeroObject 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.Abelian.has_finite_products 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Abelian C] : CategoryTheory.Limits.HasFiniteProducts C
• CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C
• CategoryTheory.Abelian.nonPreadditiveAbelian 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.NonPreadditiveAbelian C
• CategoryTheory.Abelian.toPreadditive 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Abelian C] : CategoryTheory.Preadditive C
• CategoryTheory.NonPreadditiveAbelian.abelian 📋 Mathlib.CategoryTheory.Abelian.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] : CategoryTheory.Abelian C
• CategoryTheory.Abelian.coim 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (CategoryTheory.Arrow C) C
• CategoryTheory.Abelian.im 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (CategoryTheory.Arrow C) C
• CategoryTheory.Abelian.hasBinaryBiproducts 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasBinaryBiproducts C
• CategoryTheory.Abelian.hasFiniteBiproducts 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasFiniteBiproducts C
• CategoryTheory.Abelian.has_cokernels 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Abelian C] : CategoryTheory.Limits.HasCokernels C
• CategoryTheory.Abelian.has_kernels 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Abelian C] : CategoryTheory.Limits.HasKernels C
• CategoryTheory.Abelian.toIsNormalEpiCategory 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Abelian C] : CategoryTheory.IsNormalEpiCategory C
• CategoryTheory.Abelian.toIsNormalMonoCategory 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Abelian C] : CategoryTheory.IsNormalMonoCategory C
• CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : CategoryTheory.Limits.StrongEpiMonoFactorisation f
• CategoryTheory.Abelian.imageStrongEpiMonoFactorisation 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : CategoryTheory.Limits.StrongEpiMonoFactorisation f
• CategoryTheory.Abelian.mk' 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteProducts C] (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (CategoryTheory.Abelian.AbelianStruct f)) : CategoryTheory.Abelian C
• CategoryTheory.Abelian.coimIsoIm 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Abelian.coim ≅ CategoryTheory.Abelian.im
• CategoryTheory.Abelian.mk 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [toPreadditive : CategoryTheory.Preadditive C] [toIsNormalMonoCategory : CategoryTheory.IsNormalMonoCategory C] [toIsNormalEpiCategory : CategoryTheory.IsNormalEpiCategory C] [has_finite_products : CategoryTheory.Limits.HasFiniteProducts C] [has_kernels : CategoryTheory.Limits.HasKernels C] [has_cokernels : CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Abelian C
• CategoryTheory.Abelian.coim_obj 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (f : CategoryTheory.Arrow C) : CategoryTheory.Abelian.coim.obj f = CategoryTheory.Abelian.coimage f.hom
• CategoryTheory.Abelian.im_obj 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (f : CategoryTheory.Arrow C) : CategoryTheory.Abelian.im.obj f = CategoryTheory.Abelian.image f.hom
• CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_I 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : (CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).I = CategoryTheory.Abelian.coimage f
• CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_I 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : (CategoryTheory.Abelian.imageStrongEpiMonoFactorisation f).I = CategoryTheory.Abelian.image f
• CategoryTheory.Abelian.epi_pullback_of_epi_f 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Epi f] : CategoryTheory.Epi (CategoryTheory.Limits.pullback.snd f g)
• CategoryTheory.Abelian.epi_pullback_of_epi_g 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Epi g] : CategoryTheory.Epi (CategoryTheory.Limits.pullback.fst f g)
• CategoryTheory.Abelian.mono_pushout_of_mono_f 📋 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.Mono f] : CategoryTheory.Mono (CategoryTheory.Limits.pushout.inr f g)
• CategoryTheory.Abelian.mono_pushout_of_mono_g 📋 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.Mono g] : CategoryTheory.Mono (CategoryTheory.Limits.pushout.inl f g)
• CategoryTheory.Abelian.epi_fst_of_isLimit 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Epi g] {s : CategoryTheory.Limits.PullbackCone f g} (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Epi s.fst
• CategoryTheory.Abelian.epi_snd_of_isLimit 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Epi f] {s : CategoryTheory.Limits.PullbackCone f g} (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Epi s.snd
• CategoryTheory.Abelian.mono_inl_of_isColimit 📋 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.Mono g] {s : CategoryTheory.Limits.PushoutCocone f g} (hs : CategoryTheory.Limits.IsColimit s) : CategoryTheory.Mono s.inl
• CategoryTheory.Abelian.mono_inr_of_isColimit 📋 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.Mono f] {s : CategoryTheory.Limits.PushoutCocone f g} (hs : CategoryTheory.Limits.IsColimit s) : CategoryTheory.Mono s.inr
• CategoryTheory.Abelian.BiproductToPushoutIsCokernel.biproductToPushout 📋 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) : Y ⊞ Z ⟶ CategoryTheory.Limits.pushout f g
• CategoryTheory.Abelian.PullbackToBiproductIsKernel.pullbackToBiproduct 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.pullback f g ⟶ X ⊞ Y
• CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_e 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : (CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).e = CategoryTheory.Abelian.coimage.π f
• CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_m 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : (CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).m = CategoryTheory.Abelian.factorThruCoimage f
• CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_e 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : (CategoryTheory.Abelian.imageStrongEpiMonoFactorisation f).e = CategoryTheory.Abelian.factorThruImage f
• CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_m 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : (CategoryTheory.Abelian.imageStrongEpiMonoFactorisation f).m = CategoryTheory.Abelian.image.ι f
• CategoryTheory.Abelian.coimageIsoImage' 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Abelian.coimage f ≅ CategoryTheory.Limits.image f
• CategoryTheory.Abelian.imageIsoImage 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Abelian.image f ≅ CategoryTheory.Limits.image f
• CategoryTheory.Abelian.epi_fst_of_factor_thru_epi_mono_factorization 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasPullbacks C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g₁ : Y ⟶ W) [CategoryTheory.Epi g₁] (g₂ : W ⟶ Z) [CategoryTheory.Mono g₂] (hg : CategoryTheory.CategoryStruct.comp g₁ g₂ = g) (f' : X ⟶ W) (hf : CategoryTheory.CategoryStruct.comp f' g₂ = f) (t : CategoryTheory.Limits.PullbackCone f g) (ht : CategoryTheory.Limits.IsLimit t) : CategoryTheory.Epi t.fst
• CategoryTheory.Abelian.mono_inl_of_factor_thru_epi_mono_factorization 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasPushouts C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g₁ : X ⟶ W) [CategoryTheory.Epi g₁] (g₂ : W ⟶ Z) [CategoryTheory.Mono g₂] (hg : CategoryTheory.CategoryStruct.comp g₁ g₂ = g) (f' : W ⟶ Y) (hf : CategoryTheory.CategoryStruct.comp g₁ f' = f) (t : CategoryTheory.Limits.PushoutCocone f g) (ht : CategoryTheory.Limits.IsColimit t) : CategoryTheory.Mono t.inl
• 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.PullbackToBiproductIsKernel.pullbackToBiproductFork 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.KernelFork (CategoryTheory.Limits.biprod.desc f (-g))
• CategoryTheory.Abelian.coimIsoIm_hom_app 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : CategoryTheory.Arrow C) : CategoryTheory.Abelian.coimIsoIm.hom.app X = CategoryTheory.Abelian.coimageImageComparison X.hom
• CategoryTheory.Abelian.epi_of_cokernel_π_eq_zero 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) (h : CategoryTheory.Limits.cokernel.π f = 0) : CategoryTheory.Epi f
• CategoryTheory.Abelian.mono_of_kernel_ι_eq_zero 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) (h : CategoryTheory.Limits.kernel.ι f = 0) : CategoryTheory.Mono f
• CategoryTheory.Abelian.coimageIsoImage 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Abelian.coimage f ≅ CategoryTheory.Abelian.image f
• CategoryTheory.Abelian.instEpiFactorThruImage 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : CategoryTheory.Epi (CategoryTheory.Abelian.factorThruImage f)
• CategoryTheory.Abelian.instMonoFactorThruCoimage 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : CategoryTheory.Mono (CategoryTheory.Abelian.factorThruCoimage f)
• CategoryTheory.Abelian.isIso_factorThruCoimage 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Epi f] : CategoryTheory.IsIso (CategoryTheory.Abelian.factorThruCoimage f)
• CategoryTheory.Abelian.isIso_factorThruImage 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Mono f] : CategoryTheory.IsIso (CategoryTheory.Abelian.factorThruImage f)
• CategoryTheory.Abelian.coimIsoIm_inv_app 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : CategoryTheory.Arrow C) : CategoryTheory.Abelian.coimIsoIm.inv.app X = CategoryTheory.inv (CategoryTheory.Abelian.coimageImageComparison X.hom)
• CategoryTheory.Abelian.epiDesc 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] {T : C} (g : X ⟶ T) (hg : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) g = 0) : Y ⟶ T
• CategoryTheory.Abelian.monoLift 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] {T : C} (g : T ⟶ Y) (hg : CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π f) = 0) : T ⟶ X
• CategoryTheory.Abelian.BiproductToPushoutIsCokernel.isColimitBiproductToPushout 📋 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.IsColimit (CategoryTheory.Abelian.BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)
• CategoryTheory.Abelian.PullbackToBiproductIsKernel.isLimitPullbackToBiproduct 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.IsLimit (CategoryTheory.Abelian.PullbackToBiproductIsKernel.pullbackToBiproductFork f g)
• CategoryTheory.Abelian.isColimitMapCoconeOfCokernelCoforkOfπ 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Limits.HasZeroMorphisms D] {X Y : D} (p : X ⟶ Y) [CategoryTheory.Limits.HasKernel p] (F : CategoryTheory.Functor D C) [F.PreservesZeroMorphisms] [CategoryTheory.Epi (F.map p)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair p 0) F] : CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.CokernelCofork.ofπ p ⋯))
• CategoryTheory.Abelian.isLimitMapConeOfKernelForkOfι 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Limits.HasZeroMorphisms D] {X Y : D} (i : X ⟶ Y) [CategoryTheory.Limits.HasCokernel i] (F : CategoryTheory.Functor D C) [F.PreservesZeroMorphisms] [CategoryTheory.Mono (F.map i)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair i 0) F] : CategoryTheory.Limits.IsLimit (F.mapCone (CategoryTheory.Limits.KernelFork.ofι i ⋯))
• CategoryTheory.Abelian.comp_epiDesc 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] {T : C} (g : X ⟶ T) (hg : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) g = 0) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Abelian.epiDesc f g hg) = g
• CategoryTheory.Abelian.monoLift_comp 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] {T : C} (g : T ⟶ Y) (hg : CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π f) = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.monoLift f g hg) f = g
• CategoryTheory.Abelian.ofCoimageImageComparisonIsIso 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)] [CategoryTheory.Limits.HasFiniteProducts C] : CategoryTheory.Abelian C
• CategoryTheory.Abelian.comp_epiDesc_assoc 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] {T : C} (g : X ⟶ T) (hg : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) g = 0) {Z : C} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.epiDesc f g hg) h) = CategoryTheory.CategoryStruct.comp g h
• CategoryTheory.Abelian.monoLift_comp_assoc 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] {T : C} (g : T ⟶ Y) (hg : CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π f) = 0) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.monoLift f g hg) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp g h
• CategoryTheory.Abelian.coim_map 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {f g : CategoryTheory.Arrow C} (u : f ⟶ g) : CategoryTheory.Abelian.coim.map u = CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.kernel.ι f.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left u) (CategoryTheory.Abelian.coimage.π g.hom)) ⋯
• CategoryTheory.Abelian.im_map 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {f g : CategoryTheory.Arrow C} (u : f ⟶ g) : CategoryTheory.Abelian.im.map u = CategoryTheory.Limits.kernel.lift (CategoryTheory.Limits.cokernel.π g.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι f.hom) (CategoryTheory.Arrow.Hom.right u)) ⋯
• CategoryTheory.Abelian.instIsIsoCoimageImageComparison 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)
• CategoryTheory.Abelian.coimageIsoImage'_hom 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Abelian.coimageIsoImage' f).hom = CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.kernel.ι f) (CategoryTheory.Limits.factorThruImage f) ⋯
• CategoryTheory.Abelian.imageIsoImage_inv 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Abelian.imageIsoImage f).inv = CategoryTheory.Limits.kernel.lift (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.Limits.image.ι f) ⋯
• CategoryTheory.Abelian.epiIsCokernelOfKernel 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Epi f] (s : CategoryTheory.Limits.Fork f 0) (h : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ f ⋯)
• CategoryTheory.Abelian.monoIsKernelOfCokernel 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Mono f] (s : CategoryTheory.Limits.Cofork f 0) (h : CategoryTheory.Limits.IsColimit s) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f ⋯)
• CategoryTheory.Abelian.factorThruImage_comp_coimageIsoImage'_inv 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) (CategoryTheory.Abelian.coimageIsoImage' f).inv = CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι f)
• CategoryTheory.Abelian.imageIsoImage_hom_comp_image_ι 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.imageIsoImage f).hom (CategoryTheory.Limits.image.ι f) = CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.π f)
• CategoryTheory.Abelian.coimage.comp_π_eq_zero 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Abelian.coimage.π g) = 0 ↔ CategoryTheory.CategoryStruct.comp f g = 0
• CategoryTheory.Abelian.image.ι_comp_eq_zero 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι f) g = 0 ↔ CategoryTheory.CategoryStruct.comp f g = 0
• CategoryTheory.Abelian.comp_coimage_π_eq_zero 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} {f : P ⟶ Q} {R : C} {g : Q ⟶ R} (h : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Abelian.coimage.π g) = 0
• CategoryTheory.Abelian.image_ι_comp_eq_zero 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} {f : P ⟶ Q} {R : C} {g : Q ⟶ R} (h : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι f) g = 0
• ModuleCat.abelian 📋 Mathlib.Algebra.Category.ModuleCat.Abelian
  {R : Type u} [Ring R] : CategoryTheory.Abelian (ModuleCat R)
• FGModuleCat.instAbelian 📋 Mathlib.Algebra.Category.FGModuleCat.Abelian
  {k : Type u} [Ring k] [IsNoetherianRing k] : CategoryTheory.Abelian (FGModuleCat k)
• AddCommGrpCat.instAbelian 📋 Mathlib.Algebra.Category.Grp.Abelian
  : CategoryTheory.Abelian AddCommGrpCat
• CategoryTheory.categoryWithHomology_of_abelian 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.CategoryWithHomology C
• CategoryTheory.ShortComplex.instAbelian 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Abelian (CategoryTheory.ShortComplex C)
• CategoryTheory.ShortComplex.HomologyData.ofAbelian 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.HomologyData
• CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.LeftHomologyData
• CategoryTheory.ShortComplex.RightHomologyData.ofAbelian 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.RightHomologyData
• CategoryTheory.ShortComplex.instIsNormalEpiCategory 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.IsNormalEpiCategory (CategoryTheory.ShortComplex C)
• CategoryTheory.ShortComplex.instIsNormalMonoCategory 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.IsNormalMonoCategory (CategoryTheory.ShortComplex C)
• CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_K 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).K = CategoryTheory.Limits.kernel S.g
• CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_Q 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).Q = CategoryTheory.Limits.cokernel S.f
• CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_i 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).i = CategoryTheory.Limits.kernel.ι S.g
• CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_p 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).p = CategoryTheory.Limits.cokernel.π S.f
• CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).H = CategoryTheory.Abelian.coimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f))
• CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).H = CategoryTheory.Abelian.image (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f))
• CategoryTheory.ShortComplex.abelianImageToKernel 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.Abelian.image S.f ⟶ CategoryTheory.Limits.kernel S.g
• CategoryTheory.ShortComplex.cokernelToAbelianCoimage 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.Limits.cokernel S.f ⟶ CategoryTheory.Abelian.coimage S.g
• CategoryTheory.ShortComplex.instEpiCokernelToAbelianCoimage 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.Epi S.cokernelToAbelianCoimage
• CategoryTheory.ShortComplex.instMonoAbelianImageToKernel 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.Mono S.abelianImageToKernel
• CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.homology ≅ CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)
• CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.CategoryStruct.comp S.abelianImageToKernel (CategoryTheory.Limits.kernel.ι S.g) = CategoryTheory.Abelian.image.ι S.f
• CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π S.f) S.cokernelToAbelianCoimage = CategoryTheory.Abelian.coimage.π S.g
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq 📋 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} (hkf : CategoryTheory.Limits.IsLimit kf) : hkf.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯) = CategoryTheory.CategoryStruct.comp S.toCycles (S.isoCyclesOfIsLimit hkf).inv
• 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.LeftHomologyData.ofAbelian_π 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).π = CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)))
• CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_ι 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).ι = CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)))
• CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {Z : C} (h : S.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp S.abelianImageToKernel (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι S.f) h
• CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {Z : C} (h : CategoryTheory.Abelian.coimage S.g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π S.f) (CategoryTheory.CategoryStruct.comp S.cokernelToAbelianCoimage h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π S.g) h
• CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.CategoryStruct.comp S.homologyIsoImageICyclesCompPOpcycles.hom (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)) = S.homologyι
• CategoryTheory.ShortComplex.abelianImageToKernelIsKernel 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.abelianImageToKernel ⋯)
• CategoryTheory.ShortComplex.cokernelToAbelianCoimageIsCokernel 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.cokernelToAbelianCoimage ⋯)
• 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.homologyIsoImageICyclesCompPOpcycles_ι_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {Z : C} (h : S.opcycles ⟶ Z) : CategoryTheory.CategoryStruct.comp S.homologyIsoImageICyclesCompPOpcycles.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)) h) = CategoryTheory.CategoryStruct.comp S.homologyι h
• 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.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.CategoryStruct.comp S.abelianImageToKernel (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)) = 0
• CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)) S.cokernelToAbelianCoimage = 0
• 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.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {Z : C} (h : CategoryTheory.Limits.cokernel S.f ⟶ Z) : CategoryTheory.CategoryStruct.comp S.abelianImageToKernel (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π S.f) h)) = CategoryTheory.CategoryStruct.comp 0 h
• 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.instAbelianOpposite 📋 Mathlib.CategoryTheory.Abelian.Opposite
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Abelian Cᵒᵖ
• CategoryTheory.imageOpUnop 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : Opposite.unop (CategoryTheory.Limits.image f.op) ≅ CategoryTheory.Limits.image f
• CategoryTheory.imageOpOp 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : Opposite.op (CategoryTheory.Limits.image f) ≅ CategoryTheory.Limits.image f.op
• CategoryTheory.imageUnopUnop 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : Opposite.unop (CategoryTheory.Limits.image g) ≅ CategoryTheory.Limits.image g.unop
• CategoryTheory.imageUnopOp 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : Opposite.op (CategoryTheory.Limits.image g.unop) ≅ CategoryTheory.Limits.image g
• CategoryTheory.cokernelOpUnop 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : Opposite.unop (CategoryTheory.Limits.cokernel f.op) ≅ CategoryTheory.Limits.kernel f
• CategoryTheory.kernelOpUnop 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : Opposite.unop (CategoryTheory.Limits.kernel f.op) ≅ CategoryTheory.Limits.cokernel f
• CategoryTheory.cokernelOpOp 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Limits.cokernel f.op ≅ Opposite.op (CategoryTheory.Limits.kernel f)
• CategoryTheory.kernelOpOp 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Limits.kernel f.op ≅ Opposite.op (CategoryTheory.Limits.cokernel f)
• CategoryTheory.cokernelUnopUnop 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryTheory.Limits.cokernel g.unop ≅ Opposite.unop (CategoryTheory.Limits.kernel g)
• CategoryTheory.kernelUnopUnop 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryTheory.Limits.kernel g.unop ≅ Opposite.unop (CategoryTheory.Limits.cokernel g)
• CategoryTheory.cokernelUnopOp 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : Opposite.op (CategoryTheory.Limits.cokernel g.unop) ≅ CategoryTheory.Limits.kernel g
• CategoryTheory.kernelUnopOp 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : Opposite.op (CategoryTheory.Limits.kernel g.unop) ≅ CategoryTheory.Limits.cokernel g
• CategoryTheory.cokernelOpOp_hom 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.cokernelOpOp f).hom = CategoryTheory.Limits.cokernel.desc f.op (CategoryTheory.Limits.kernel.ι f).op ⋯
• CategoryTheory.kernelOpOp_inv 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.kernelOpOp f).inv = CategoryTheory.Limits.kernel.lift f.op (CategoryTheory.Limits.cokernel.π f).op ⋯
• CategoryTheory.cokernelOpUnop_hom 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.cokernelOpUnop f).hom = CategoryTheory.Limits.kernel.lift f (CategoryTheory.Limits.cokernel.π f.op).unop ⋯
• CategoryTheory.kernelOpUnop_inv 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.kernelOpUnop f).inv = CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.kernel.ι f.op).unop ⋯
• CategoryTheory.cokernelOpUnop_inv 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.cokernelOpUnop f).inv = (CategoryTheory.Limits.cokernel.desc f.op (CategoryTheory.Limits.kernel.ι f).op ⋯).unop
• CategoryTheory.kernelOpUnop_hom 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.kernelOpUnop f).hom = (CategoryTheory.Limits.kernel.lift f.op (CategoryTheory.Limits.cokernel.π f).op ⋯).unop
• CategoryTheory.imageUnopOp_inv_comp_op_factorThruImage 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.imageUnopOp g).inv (CategoryTheory.Limits.factorThruImage g.unop).op = CategoryTheory.Limits.image.ι g
• CategoryTheory.image_ι_op_comp_imageUnopOp_hom 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι g.unop).op (CategoryTheory.imageUnopOp g).hom = CategoryTheory.Limits.factorThruImage g
• CategoryTheory.factorThruImage_comp_imageUnopOp_inv 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage g) (CategoryTheory.imageUnopOp g).inv = (CategoryTheory.Limits.image.ι g.unop).op
• CategoryTheory.imageUnopOp_hom_comp_image_ι 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.imageUnopOp g).hom (CategoryTheory.Limits.image.ι g) = (CategoryTheory.Limits.factorThruImage g.unop).op
• CategoryTheory.cokernelUnopUnop_hom 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.cokernelUnopUnop g).hom = CategoryTheory.Limits.cokernel.desc g.unop (CategoryTheory.Limits.kernel.ι g).unop ⋯
• CategoryTheory.kernelUnopUnop_inv 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.kernelUnopUnop g).inv = CategoryTheory.Limits.kernel.lift g.unop (CategoryTheory.Limits.cokernel.π g).unop ⋯
• CategoryTheory.cokernelOpOp_inv 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.cokernelOpOp f).inv = (CategoryTheory.Limits.kernel.lift f (CategoryTheory.Limits.cokernel.π f.op).unop ⋯).op
• CategoryTheory.kernelOpOp_hom 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.kernelOpOp f).hom = (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.kernel.ι f.op).unop ⋯).op
• CategoryTheory.cokernelUnopOp_hom 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.cokernelUnopOp g).hom = CategoryTheory.Limits.kernel.lift g (CategoryTheory.Limits.cokernel.π g.unop).op ⋯
• CategoryTheory.kernelUnopOp_inv 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.kernelUnopOp g).inv = CategoryTheory.Limits.cokernel.desc g (CategoryTheory.Limits.kernel.ι g.unop).op ⋯
• CategoryTheory.cokernelUnopUnop_inv 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.cokernelUnopUnop g).inv = (CategoryTheory.Limits.kernel.lift g (CategoryTheory.Limits.cokernel.π g.unop).op ⋯).unop
• CategoryTheory.kernelUnopUnop_hom 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.kernelUnopUnop g).hom = (CategoryTheory.Limits.cokernel.desc g (CategoryTheory.Limits.kernel.ι g.unop).op ⋯).unop
• CategoryTheory.cokernelUnopOp_inv 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.cokernelUnopOp g).inv = (CategoryTheory.Limits.cokernel.desc g.unop (CategoryTheory.Limits.kernel.ι g).unop ⋯).op
• CategoryTheory.kernelUnopOp_hom 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.kernelUnopOp g).hom = (CategoryTheory.Limits.kernel.lift g.unop (CategoryTheory.Limits.cokernel.π g).unop ⋯).op
• CategoryTheory.cokernel.π_op 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Limits.cokernel.π f.op).unop = CategoryTheory.CategoryStruct.comp (CategoryTheory.cokernelOpUnop f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) (CategoryTheory.eqToHom ⋯))
• CategoryTheory.kernel.ι_unop 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.Limits.kernel.ι g.unop).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g) (CategoryTheory.kernelUnopOp g).inv)
• CategoryTheory.cokernel.π_unop 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.Limits.cokernel.π g.unop).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.cokernelUnopOp g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.eqToHom ⋯))
• CategoryTheory.kernel.ι_op 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Limits.kernel.ι f.op).unop = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.kernelOpUnop f).inv)
• CategoryTheory.ShortComplex.cokernelSequence 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.ShortComplex C
• CategoryTheory.ShortComplex.kernelSequence 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.ShortComplex C
• CategoryTheory.ShortComplex.cokernelSequence_exact 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.cokernelSequence f).Exact
• CategoryTheory.ShortComplex.kernelSequence_exact 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.kernelSequence f).Exact
• CategoryTheory.ShortComplex.cokernelSequence_X₁ 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.cokernelSequence f).X₁ = X
• CategoryTheory.ShortComplex.cokernelSequence_X₂ 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.cokernelSequence f).X₂ = Y
• CategoryTheory.ShortComplex.kernelSequence_X₂ 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.kernelSequence f).X₂ = X
• CategoryTheory.ShortComplex.kernelSequence_X₃ 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.kernelSequence f).X₃ = Y
• CategoryTheory.ShortComplex.cokernelSequence_f 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.cokernelSequence f).f = f
• CategoryTheory.ShortComplex.kernelSequence_g 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.kernelSequence f).g = f
• CategoryTheory.ShortComplex.cokernelSequence_X₃ 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.cokernelSequence f).X₃ = CategoryTheory.Limits.cokernel f
• CategoryTheory.ShortComplex.kernelSequence_X₁ 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.kernelSequence f).X₁ = CategoryTheory.Limits.kernel f
• CategoryTheory.ShortComplex.instEpiGCokernelSequence 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Epi (CategoryTheory.ShortComplex.cokernelSequence f).g
• CategoryTheory.ShortComplex.instMonoFKernelSequence 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Mono (CategoryTheory.ShortComplex.kernelSequence f).f
• CategoryTheory.ShortComplex.cokernelSequence_g 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.cokernelSequence f).g = CategoryTheory.Limits.cokernel.π f
• CategoryTheory.ShortComplex.kernelSequence_f 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.ShortComplex.kernelSequence f).f = CategoryTheory.Limits.kernel.ι f
• CategoryTheory.ShortComplex.Exact.descToInjective 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) {J : C} (f : S.X₂ ⟶ J) [CategoryTheory.Injective J] (hf : CategoryTheory.CategoryStruct.comp S.f f = 0) : S.X₃ ⟶ J
• CategoryTheory.ShortComplex.Exact.liftFromProjective 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) {P : C} (f : P ⟶ S.X₂) [CategoryTheory.Projective P] (hf : CategoryTheory.CategoryStruct.comp f S.g = 0) : P ⟶ S.X₁

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