Loogle!

Result

Found 115 declarations mentioning CategoryTheory.Limits.HasKernels.

• CategoryTheory.Limits.HasKernels 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : Prop
• CategoryTheory.Limits.hasKernels_of_hasEqualizers 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasKernels C
• CategoryTheory.Limits.ker 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] : CategoryTheory.Functor (CategoryTheory.Arrow C) C
• CategoryTheory.Limits.HasKernels.has_limit 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} [self : CategoryTheory.Limits.HasKernels C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Limits.HasKernel f
• CategoryTheory.Limits.HasKernels.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (has_limit : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasKernel f := by infer_instance) : CategoryTheory.Limits.HasKernels C
• CategoryTheory.Limits.ker_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] (f : CategoryTheory.Arrow C) : (CategoryTheory.Limits.ker C).obj f = CategoryTheory.Limits.kernel f.hom
• CategoryTheory.Limits.ker.ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] : CategoryTheory.Limits.ker C ⟶ CategoryTheory.Arrow.leftFunc
• CategoryTheory.Limits.ker.ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] (f : CategoryTheory.Arrow C) : (CategoryTheory.Limits.ker.ι C).app f = CategoryTheory.Limits.kernel.ι f.hom
• CategoryTheory.Limits.ker_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] {f g : CategoryTheory.Arrow C} (u : f ⟶ g) : (CategoryTheory.Limits.ker C).map u = CategoryTheory.Limits.kernel.lift g.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f.hom) (CategoryTheory.Arrow.Hom.left u)) ⋯
• CategoryTheory.Limits.ker.condition 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.ker.ι C) CategoryTheory.Arrow.leftToRight = 0
• CategoryTheory.Limits.ker.condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] {Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C} (h : CategoryTheory.Arrow.rightFunc ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.ker.ι C) (CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow.leftToRight h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Preadditive.hasEqualizers_of_hasKernels 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] : CategoryTheory.Limits.HasEqualizers C
• ModuleCat.hasKernels_moduleCat 📋 Mathlib.Algebra.Category.ModuleCat.Kernels
  {R : Type u} [Ring R] : CategoryTheory.Limits.HasKernels (ModuleCat R)
• CategoryTheory.NormalMonoCategory.hasEqualizers 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.IsNormalMonoCategory C] : CategoryTheory.Limits.HasEqualizers C
• CategoryTheory.NormalMonoCategory.hasLimit_parallelPair 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.IsNormalMonoCategory C] {X Y : C} (f g : X ⟶ Y) : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)
• CategoryTheory.NormalMonoCategory.pullback_of_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.IsNormalMonoCategory C] {X Y Z : C} (a : X ⟶ Z) (b : Y ⟶ Z) [CategoryTheory.Mono a] [CategoryTheory.Mono b] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan a b)
• CategoryTheory.NormalMonoCategory.preservesEpimorphisms_of_preservesCokernels 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.IsNormalMonoCategory C] [CategoryTheory.Limits.HasZeroObject C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasZeroObject D] (F : CategoryTheory.Functor D C) [F.PreservesZeroMorphisms] [∀ {X Y : D} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] : F.PreservesEpimorphisms
• CategoryTheory.NormalMonoCategory.epi_of_zero_cancel 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.IsNormalMonoCategory C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0) : CategoryTheory.Epi f
• CategoryTheory.NormalMonoCategory.epi_of_zero_cokernel 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.IsNormalMonoCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) (l : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ 0 ⋯)) : CategoryTheory.Epi f
• CategoryTheory.Abelian.coimageImageComparisonFunctor 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow C)
• CategoryTheory.Abelian.coimageImageComparisonFunctor_obj 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (f : CategoryTheory.Arrow C) : CategoryTheory.Abelian.coimageImageComparisonFunctor.obj f = CategoryTheory.Arrow.mk (CategoryTheory.Abelian.coimageImageComparison f.hom)
• CategoryTheory.Abelian.coimageImageComparisonFunctor_map 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {f g : CategoryTheory.Arrow C} (η : f ⟶ g) : CategoryTheory.Abelian.coimageImageComparisonFunctor.map η = CategoryTheory.Arrow.homMk (CategoryTheory.Limits.cokernel.map (CategoryTheory.Limits.kernel.ι f.hom) (CategoryTheory.Limits.kernel.ι g.hom) (CategoryTheory.Limits.kernel.map f.hom g.hom (CategoryTheory.Arrow.Hom.left η) (CategoryTheory.Arrow.Hom.right η) ⋯) (CategoryTheory.Arrow.Hom.left η) ⋯) (CategoryTheory.Limits.kernel.map (CategoryTheory.Limits.cokernel.π f.hom) (CategoryTheory.Limits.cokernel.π g.hom) (CategoryTheory.Arrow.Hom.right η) (CategoryTheory.Limits.cokernel.map f.hom g.hom (CategoryTheory.Arrow.Hom.left η) (CategoryTheory.Arrow.Hom.right η) ⋯) ⋯) ⋯
• CategoryTheory.NonPreadditiveAbelian.has_kernels 📋 Mathlib.CategoryTheory.Abelian.NonPreadditive
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.NonPreadditiveAbelian C] : CategoryTheory.Limits.HasKernels C
• CategoryTheory.NonPreadditiveAbelian.mk 📋 Mathlib.CategoryTheory.Abelian.NonPreadditive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [toHasZeroMorphisms : CategoryTheory.Limits.HasZeroMorphisms C] [toIsNormalMonoCategory : CategoryTheory.IsNormalMonoCategory C] [toIsNormalEpiCategory : CategoryTheory.IsNormalEpiCategory C] [has_zero_object : CategoryTheory.Limits.HasZeroObject C] [has_kernels : CategoryTheory.Limits.HasKernels C] [has_cokernels : CategoryTheory.Limits.HasCokernels C] [has_finite_products : CategoryTheory.Limits.HasFiniteProducts C] [has_finite_coproducts : CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.NonPreadditiveAbelian 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.OfCoimageImageComparisonIsIso.imageMonoFactorisation 📋 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.Limits.MonoFactorisation f
• 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.OfCoimageImageComparisonIsIso.instIsIsoMImageMonoFactorisationOfHasZeroObjectOfEpi 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.IsIso (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).m
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_I 📋 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.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).I = CategoryTheory.Abelian.image f
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_m 📋 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.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).m = CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.π f)
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e 📋 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.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).e = CategoryTheory.Limits.kernel.lift (CategoryTheory.Limits.cokernel.π f) f ⋯
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.hasImages 📋 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.HasImages C
• 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.OfCoimageImageComparisonIsIso.imageFactorisation 📋 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.ImageFactorisation f
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.isNormalEpiCategory 📋 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.IsNormalEpiCategory C
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.isNormalMonoCategory 📋 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.IsNormalMonoCategory C
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.instIsIsoEImageMonoFactorisationOfHasZeroObjectOfMonoOfCoimageImageComparison 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] [CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)] : CategoryTheory.IsIso (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).e
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e' 📋 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.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).e = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι f)) (CategoryTheory.Abelian.coimageImageComparison f)
• CategoryTheory.ShortComplex.cyclesFunctor 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Functor (CategoryTheory.ShortComplex C) C
• CategoryTheory.ShortComplex.leftHomologyFunctor 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Functor (CategoryTheory.ShortComplex C) C
• CategoryTheory.ShortComplex.cyclesFunctor_obj 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.cyclesFunctor C).obj S = S.cycles
• CategoryTheory.ShortComplex.leftHomologyFunctor_obj 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.leftHomologyFunctor C).obj S = S.leftHomology
• CategoryTheory.ShortComplex.iCyclesNatTrans 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.ShortComplex.cyclesFunctor C ⟶ CategoryTheory.ShortComplex.π₂
• CategoryTheory.ShortComplex.toCyclesNatTrans 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.ShortComplex.π₁ ⟶ CategoryTheory.ShortComplex.cyclesFunctor C
• CategoryTheory.ShortComplex.leftHomologyπNatTrans 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.ShortComplex.cyclesFunctor C ⟶ CategoryTheory.ShortComplex.leftHomologyFunctor C
• CategoryTheory.ShortComplex.iCyclesNatTrans_app 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.iCyclesNatTrans C).app S = S.iCycles
• CategoryTheory.ShortComplex.toCyclesNatTrans_app 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.toCyclesNatTrans C).app S = S.toCycles
• CategoryTheory.ShortComplex.leftHomologyπNatTrans_app 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.leftHomologyπNatTrans C).app S = S.leftHomologyπ
• CategoryTheory.ShortComplex.cyclesFunctor_map 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {X✝ Y✝ : CategoryTheory.ShortComplex C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.ShortComplex.cyclesFunctor C).map φ = CategoryTheory.ShortComplex.cyclesMap φ
• CategoryTheory.ShortComplex.leftHomologyFunctor_map 📋 Mathlib.Algebra.Homology.ShortComplex.LeftHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {X✝ Y✝ : CategoryTheory.ShortComplex C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.ShortComplex.leftHomologyFunctor C).map φ = CategoryTheory.ShortComplex.leftHomologyMap φ
• CategoryTheory.ShortComplex.opcyclesFunctor 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Functor (CategoryTheory.ShortComplex C) C
• CategoryTheory.ShortComplex.rightHomologyFunctor 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Functor (CategoryTheory.ShortComplex C) C
• CategoryTheory.ShortComplex.opcyclesFunctor_obj 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.opcyclesFunctor C).obj S = S.opcycles
• CategoryTheory.ShortComplex.rightHomologyFunctor_obj 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.rightHomologyFunctor C).obj S = S.rightHomology
• CategoryTheory.ShortComplex.fromOpcyclesNatTrans 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.ShortComplex.opcyclesFunctor C ⟶ CategoryTheory.ShortComplex.π₃
• CategoryTheory.ShortComplex.pOpcyclesNatTrans 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.ShortComplex.π₂ ⟶ CategoryTheory.ShortComplex.opcyclesFunctor C
• CategoryTheory.ShortComplex.rightHomologyιNatTrans 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.ShortComplex.rightHomologyFunctor C ⟶ CategoryTheory.ShortComplex.opcyclesFunctor C
• CategoryTheory.ShortComplex.fromOpcyclesNatTrans_app 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.fromOpcyclesNatTrans C).app S = S.fromOpcycles
• CategoryTheory.ShortComplex.pOpcyclesNatTrans_app 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.pOpcyclesNatTrans C).app S = S.pOpcycles
• CategoryTheory.ShortComplex.rightHomologyιNatTrans_app 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.rightHomologyιNatTrans C).app S = S.rightHomologyι
• CategoryTheory.ShortComplex.opcyclesFunctor_map 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {X✝ Y✝ : CategoryTheory.ShortComplex C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.ShortComplex.opcyclesFunctor C).map φ = CategoryTheory.ShortComplex.opcyclesMap φ
• CategoryTheory.ShortComplex.rightHomologyFunctor_map 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {X✝ Y✝ : CategoryTheory.ShortComplex C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.ShortComplex.rightHomologyFunctor C).map φ = CategoryTheory.ShortComplex.rightHomologyMap φ
• CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels Cᵒᵖ] [CategoryTheory.Limits.HasCokernels Cᵒᵖ] : (CategoryTheory.ShortComplex.leftHomologyFunctor C).op ≅ (CategoryTheory.ShortComplex.opFunctor C).comp (CategoryTheory.ShortComplex.rightHomologyFunctor Cᵒᵖ)
• CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels Cᵒᵖ] [CategoryTheory.Limits.HasCokernels Cᵒᵖ] : (CategoryTheory.ShortComplex.rightHomologyFunctor C).op ≅ (CategoryTheory.ShortComplex.opFunctor C).comp (CategoryTheory.ShortComplex.leftHomologyFunctor Cᵒᵖ)
• CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso_hom_app 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels Cᵒᵖ] [CategoryTheory.Limits.HasCokernels Cᵒᵖ] (X : (CategoryTheory.ShortComplex C)ᵒᵖ) : (CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso C).hom.app X = (Opposite.unop X).rightHomologyOpIso.inv
• CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso_inv_app 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels Cᵒᵖ] [CategoryTheory.Limits.HasCokernels Cᵒᵖ] (X : (CategoryTheory.ShortComplex C)ᵒᵖ) : (CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso C).inv.app X = (Opposite.unop X).rightHomologyOpIso.hom
• CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso_hom_app 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels Cᵒᵖ] [CategoryTheory.Limits.HasCokernels Cᵒᵖ] (X : (CategoryTheory.ShortComplex C)ᵒᵖ) : (CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso C).hom.app X = (Opposite.unop X).leftHomologyOpIso.inv
• CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso_inv_app 📋 Mathlib.Algebra.Homology.ShortComplex.RightHomology
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels Cᵒᵖ] [CategoryTheory.Limits.HasCokernels Cᵒᵖ] (X : (CategoryTheory.ShortComplex C)ᵒᵖ) : (CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso C).inv.app X = (Opposite.unop X).leftHomologyOpIso.hom
• CategoryTheory.ShortComplex.cyclesFunctorIso 📋 Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels D] [CategoryTheory.Limits.HasCokernels D] [F.PreservesHomology] : F.mapShortComplex.comp (CategoryTheory.ShortComplex.cyclesFunctor D) ≅ (CategoryTheory.ShortComplex.cyclesFunctor C).comp F
• CategoryTheory.ShortComplex.leftHomologyFunctorIso 📋 Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels D] [CategoryTheory.Limits.HasCokernels D] [F.PreservesHomology] : F.mapShortComplex.comp (CategoryTheory.ShortComplex.leftHomologyFunctor D) ≅ (CategoryTheory.ShortComplex.leftHomologyFunctor C).comp F
• CategoryTheory.ShortComplex.opcyclesFunctorIso 📋 Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels D] [CategoryTheory.Limits.HasCokernels D] [F.PreservesHomology] : F.mapShortComplex.comp (CategoryTheory.ShortComplex.opcyclesFunctor D) ≅ (CategoryTheory.ShortComplex.opcyclesFunctor C).comp F
• CategoryTheory.ShortComplex.rightHomologyFunctorIso 📋 Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasKernels D] [CategoryTheory.Limits.HasCokernels D] [F.PreservesHomology] : F.mapShortComplex.comp (CategoryTheory.ShortComplex.rightHomologyFunctor D) ≅ (CategoryTheory.ShortComplex.rightHomologyFunctor C).comp F
• CategoryTheory.ShortComplex.cyclesFunctor_additive 📋 Mathlib.Algebra.Homology.ShortComplex.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : (CategoryTheory.ShortComplex.cyclesFunctor C).Additive
• CategoryTheory.ShortComplex.leftHomologyFunctor_additive 📋 Mathlib.Algebra.Homology.ShortComplex.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : (CategoryTheory.ShortComplex.leftHomologyFunctor C).Additive
• CategoryTheory.ShortComplex.opcyclesFunctor_additive 📋 Mathlib.Algebra.Homology.ShortComplex.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : (CategoryTheory.ShortComplex.opcyclesFunctor C).Additive
• CategoryTheory.ShortComplex.rightHomologyFunctor_additive 📋 Mathlib.Algebra.Homology.ShortComplex.Preadditive
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : (CategoryTheory.ShortComplex.rightHomologyFunctor C).Additive
• CategoryTheory.Limits.kernelOrderHom 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] (X : C) : (CategoryTheory.Subobject (Opposite.op X))ᵒᵈ →o CategoryTheory.Subobject X
• CategoryTheory.Limits.kernelOrderHom_coe 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] (X : C) (a✝ : CategoryTheory.Subobject (Opposite.op X)) : (CategoryTheory.Limits.kernelOrderHom X) a✝ = CategoryTheory.Subobject.lift (fun x f x_1 => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop)) ⋯ a✝
• imageToKernel' 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Limits.image f ⟶ CategoryTheory.Limits.kernel g
• imageToKernel_epi_of_zero_of_mono 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Mono g] : CategoryTheory.Epi (imageToKernel 0 g ⋯)
• imageSubobjectIso_imageToKernel' 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom (imageToKernel' f g w) = CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.Limits.kernelSubobjectIso g).hom
• imageToKernel'_kernelSubobjectIso 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (imageToKernel' f g w) (CategoryTheory.Limits.kernelSubobjectIso g).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv (imageToKernel f g w)
• imageToKernel_comp_left 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] {Z : V} (h : Z ⟶ A) (w : CategoryTheory.CategoryStruct.comp f g = 0) : imageToKernel (CategoryTheory.CategoryStruct.comp h f) g ⋯ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f)).ofLE (CategoryTheory.Limits.imageSubobject f) ⋯) (imageToKernel f g w)
• imageToKernel_comp_right 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] {D : V} (h : C ⟶ D) (w : CategoryTheory.CategoryStruct.comp f g = 0) : imageToKernel f (CategoryTheory.CategoryStruct.comp g h) ⋯ = CategoryTheory.CategoryStruct.comp (imageToKernel f g w) ((CategoryTheory.Limits.kernelSubobject g).ofLE (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp g h)) ⋯)
• imageToKernel_zero_left 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasZeroObject V] {w : CategoryTheory.CategoryStruct.comp 0 g = 0} : imageToKernel 0 g w = 0
• imageToKernel_epi_comp 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] {Z : V} (h : Z ⟶ A) [CategoryTheory.Epi h] (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h f) g = 0) : imageToKernel (CategoryTheory.CategoryStruct.comp h f) g w = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f)).ofLE (CategoryTheory.Limits.imageSubobject f) ⋯) (imageToKernel f g ⋯)
• imageToKernel_comp_mono 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] {D : V} (h : C ⟶ D) [CategoryTheory.Mono h] (w : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = 0) : imageToKernel f (CategoryTheory.CategoryStruct.comp g h) w = CategoryTheory.CategoryStruct.comp (imageToKernel f g ⋯) ((CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp g h)).isoOfEq (CategoryTheory.Limits.kernelSubobject g) ⋯).inv
• CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology 📋 Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [F.PreservesHomology] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] : CategoryTheory.Limits.PreservesFiniteLimits F
• CategoryTheory.AbelianOfAdjunction.hasKernels 📋 Mathlib.CategoryTheory.Abelian.Transfer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) [G.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteLimits G] (i : F.comp G ≅ CategoryTheory.Functor.id C) : CategoryTheory.Limits.HasKernels C
• HomologicalComplex.kernel_from_eq_kernel 📋 Mathlib.Algebra.Homology.HomologicalComplex
  {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasKernels V] {i j : ι} (r : c.Rel i j) : CategoryTheory.Limits.kernelSubobject (C.dFrom i) = CategoryTheory.Limits.kernelSubobject (C.d i j)
• HomologicalComplex.kernel_eq_kernel 📋 Mathlib.Algebra.Homology.HomologicalComplex
  {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasKernels V] {i j j' : ι} (r : c.Rel i j) (r' : c.Rel i j') : CategoryTheory.Limits.kernelSubobject (C.d i j) = CategoryTheory.Limits.kernelSubobject (C.d i j')
• CategoryTheory.ShortComplex.cyclesFunctor_linear 📋 Mathlib.Algebra.Homology.ShortComplex.Linear
  {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.cyclesFunctor C)
• CategoryTheory.ShortComplex.leftHomologyFunctor_linear 📋 Mathlib.Algebra.Homology.ShortComplex.Linear
  {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.leftHomologyFunctor C)
• CategoryTheory.ShortComplex.opcyclesFunctor_linear 📋 Mathlib.Algebra.Homology.ShortComplex.Linear
  {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.opcyclesFunctor C)
• CategoryTheory.ShortComplex.rightHomologyFunctor_linear 📋 Mathlib.Algebra.Homology.ShortComplex.Linear
  {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.rightHomologyFunctor C)
• CategoryTheory.Limits.kerIsKernel 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Kernels
  (C : Type u_2) [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.ker.ι C) ⋯)
• CategoryTheory.ObjectProperty.SerreClassLocalization.hasKernels 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Limits.HasKernels D
• CategoryTheory.ObjectProperty.instHasKernelsFullSubcategoryOfIsClosedUnderKernels 📋 Mathlib.CategoryTheory.ObjectProperty.Kernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderKernels] [CategoryTheory.Limits.HasKernels C] : CategoryTheory.Limits.HasKernels P.FullSubcategory
• CategoryTheory.ObjectProperty.preservesKernels_ι 📋 Mathlib.CategoryTheory.ObjectProperty.Kernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasKernels C] [P.IsClosedUnderKernels] ⦃X Y : P.FullSubcategory⦄ (f : X ⟶ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) P.ι
• CategoryTheory.ObjectProperty.preservesEpimorphisms_ι_of_isNormalMonoCategory 📋 Mathlib.CategoryTheory.Abelian.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.IsNormalMonoCategory C] [CategoryTheory.Limits.HasZeroObject C] [P.ContainsZero] [P.IsClosedUnderCokernels] : P.ι.PreservesEpimorphisms
• CategoryTheory.ObjectProperty.preservesMonomorphisms_ι_of_isNormalEpiCategory 📋 Mathlib.CategoryTheory.Abelian.Subcategory
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.IsNormalEpiCategory C] [CategoryTheory.Limits.HasZeroObject C] [P.ContainsZero] [P.IsClosedUnderKernels] : P.ι.PreservesMonomorphisms
• CategoryTheory.Limits.HasWeakKernelsOfHasKernels 📋 Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] : CategoryTheory.Limits.HasWeakKernels C
• CategoryTheory.instDivisionRingEndOfHasKernelsOfSimple 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] : DivisionRing (CategoryTheory.End X)
• CategoryTheory.mono_of_nonzero_from_simple 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] {X Y : C} [CategoryTheory.Simple X] {f : X ⟶ Y} (w : f ≠ 0) : CategoryTheory.Mono f
• CategoryTheory.fieldEndOfFiniteDimensional 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C) [CategoryTheory.Simple X] [I : FiniteDimensional 𝕜 (X ⟶ X)] : Field (CategoryTheory.End X)
• CategoryTheory.isIso_of_hom_simple 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] {X Y : C} [CategoryTheory.Simple X] [CategoryTheory.Simple Y] {f : X ⟶ Y} (w : f ≠ 0) : CategoryTheory.IsIso f
• CategoryTheory.isIso_iff_nonzero 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] {X Y : C} [CategoryTheory.Simple X] [CategoryTheory.Simple Y] (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ f ≠ 0
• CategoryTheory.finrank_hom_simple_simple_eq_zero_of_not_iso 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [DivisionRing 𝕜] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Linear 𝕜 C] {X Y : C} [CategoryTheory.Simple X] [CategoryTheory.Simple Y] (h : ∀ (a : X ≅ Y), False) : Module.finrank 𝕜 (X ⟶ Y) = 0
• CategoryTheory.finrank_endomorphism_simple_eq_one 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C) [CategoryTheory.Simple X] [FiniteDimensional 𝕜 (X ⟶ X)] : Module.finrank 𝕜 (X ⟶ X) = 1
• CategoryTheory.finrank_hom_simple_simple_le_one 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C) [FiniteDimensional 𝕜 (X ⟶ X)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : Module.finrank 𝕜 (X ⟶ Y) ≤ 1
• CategoryTheory.finrank_hom_simple_simple 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C) [∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : Module.finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0
• CategoryTheory.finrank_hom_simple_simple_eq_one_iff 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C) [FiniteDimensional 𝕜 (X ⟶ X)] [FiniteDimensional 𝕜 (X ⟶ Y)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : Module.finrank 𝕜 (X ⟶ Y) = 1 ↔ Nonempty (X ≅ Y)
• CategoryTheory.finrank_hom_simple_simple_eq_zero_iff 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C) [FiniteDimensional 𝕜 (X ⟶ X)] [FiniteDimensional 𝕜 (X ⟶ Y)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : Module.finrank 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty (X ≅ Y)
• CategoryTheory.endomorphism_simple_eq_smul_id 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] [FiniteDimensional 𝕜 (X ⟶ X)] (f : X ⟶ X) : ∃ c, c • CategoryTheory.CategoryStruct.id X = f
• FDRep.instHasKernels 📋 Mathlib.RepresentationTheory.FDRep
  {k : Type u} {G : Type v} [Field k] [Monoid G] : CategoryTheory.Limits.HasKernels (FDRep k G)

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 ce5dd8c