Loogle!

Result

Found 65 declarations mentioning CategoryTheory.Limits.kernelSubobject.

• CategoryTheory.Limits.kernelSubobject 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] : CategoryTheory.Subobject X
• CategoryTheory.Limits.kernelSubobjectIso 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f) ≅ CategoryTheory.Limits.kernel f
• CategoryTheory.Limits.kernelSubobject_comp_mono 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {Z : C} (h : Y ⟶ Z) [CategoryTheory.Mono h] : CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.Limits.kernelSubobject f
• CategoryTheory.Limits.kernelSubobject_comp_le 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {Z : C} (h : Y ⟶ Z) [CategoryTheory.Limits.HasKernel (CategoryTheory.CategoryStruct.comp f h)] : CategoryTheory.Limits.kernelSubobject f ≤ CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.Limits.kernelSubobject_factors 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {W : C} (h : W ⟶ X) (w : CategoryTheory.CategoryStruct.comp h f = 0) : (CategoryTheory.Limits.kernelSubobject f).Factors h
• CategoryTheory.Limits.kernelSubobject_factors_iff 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {W : C} (h : W ⟶ X) : (CategoryTheory.Limits.kernelSubobject f).Factors h ↔ CategoryTheory.CategoryStruct.comp h f = 0
• CategoryTheory.Limits.kernelSubobject_zero 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {A B : C} : CategoryTheory.Limits.kernelSubobject 0 = ⊤
• CategoryTheory.Limits.factorThruKernelSubobject 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {W : C} (h : W ⟶ X) (w : CategoryTheory.CategoryStruct.comp h f = 0) : W ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f)
• CategoryTheory.Limits.kernelSubobjectIsoComp 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {X' : C} (f : X' ⟶ X) [CategoryTheory.IsIso f] (g : X ⟶ Y) [CategoryTheory.Limits.HasKernel g] : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f g)) ≅ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g)
• CategoryTheory.Limits.kernelSubobjectMap 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'} [CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f) ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f')
• CategoryTheory.Limits.factorThruKernelSubobject_comp_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {W : C} (h : W ⟶ X) (w : CategoryTheory.CategoryStruct.comp h f = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruKernelSubobject f h w) (CategoryTheory.Limits.kernelSubobject f).arrow = h
• CategoryTheory.Limits.kernelSubobject_arrow' 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).inv (CategoryTheory.Limits.kernelSubobject f).arrow = CategoryTheory.Limits.kernel.ι f
• CategoryTheory.Limits.kernelSubobjectMap_id 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [CategoryTheory.Limits.HasKernel f] : CategoryTheory.Limits.kernelSubobjectMap (CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk f)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))
• CategoryTheory.Limits.isIso_kernelSubobject_zero_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.IsIso (CategoryTheory.Limits.kernelSubobject 0).arrow
• CategoryTheory.Limits.kernelSubobject_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).hom (CategoryTheory.Limits.kernel.ι f) = (CategoryTheory.Limits.kernelSubobject f).arrow
• CategoryTheory.Limits.kernelSubobject_comp_mono_isIso 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {Z : C} (h : Y ⟶ Z) [CategoryTheory.Mono h] : CategoryTheory.IsIso ((CategoryTheory.Limits.kernelSubobject f).ofLE (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f h)) ⋯)
• CategoryTheory.Limits.factorThruKernelSubobject_comp_kernelSubobjectIso 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {W : C} (h : W ⟶ X) (w : CategoryTheory.CategoryStruct.comp h f = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruKernelSubobject f h w) (CategoryTheory.Limits.kernelSubobjectIso f).hom = CategoryTheory.Limits.kernel.lift f h w
• CategoryTheory.Limits.kernelSubobject_arrow'_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h
• CategoryTheory.Limits.le_kernelSubobject 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] (A : CategoryTheory.Subobject X) (h : CategoryTheory.CategoryStruct.comp A.arrow f = 0) : A ≤ CategoryTheory.Limits.kernelSubobject f
• CategoryTheory.Limits.kernelSubobject_arrow_comp 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow f = 0
• CategoryTheory.Limits.kernelSubobject_arrow_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow h
• CategoryTheory.Limits.kernelSubobjectMap_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'} [CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq) (CategoryTheory.Limits.kernelSubobject f').arrow = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow (CategoryTheory.Arrow.Hom.left sq)
• CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Limits.kernelSubobjectMap_arrow_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'} [CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') {Z : C} (h : X' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f').arrow h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) h)
• CategoryTheory.Limits.kernelSubobjectMap_comp 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'} [CategoryTheory.Limits.HasKernel f'] {X'' Y'' : C} {f'' : X'' ⟶ Y''} [CategoryTheory.Limits.HasKernel f''] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') (sq' : CategoryTheory.Arrow.mk f' ⟶ CategoryTheory.Arrow.mk f'') : CategoryTheory.Limits.kernelSubobjectMap (CategoryTheory.CategoryStruct.comp sq sq') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq) (CategoryTheory.Limits.kernelSubobjectMap sq')
• CategoryTheory.Limits.kernelSubobjectIsoComp_inv_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {X' : C} (f : X' ⟶ X) [CategoryTheory.IsIso f] (g : X ⟶ Y) [CategoryTheory.Limits.HasKernel g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIsoComp f g).inv (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f g)).arrow = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject g).arrow (CategoryTheory.inv f)
• CategoryTheory.Limits.kernelSubobjectIsoComp_hom_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {X' : C} (f : X' ⟶ X) [CategoryTheory.IsIso f] (g : X ⟶ Y) [CategoryTheory.Limits.HasKernel g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIsoComp f g).hom (CategoryTheory.Limits.kernelSubobject g).arrow = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f g)).arrow f
• CategoryTheory.Limits.kernelSubobject_arrow'_apply 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier (CategoryTheory.Limits.kernel f)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject f).arrow) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobjectIso f).inv) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f)) x
• CategoryTheory.Limits.kernelSubobject_arrow_apply 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernel.ι f)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobjectIso f).hom) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject f).arrow) x
• CategoryTheory.Limits.kernelSubobject_arrow_comp_apply 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))) : (CategoryTheory.ConcreteCategory.hom f) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject f).arrow) x) = (CategoryTheory.ConcreteCategory.hom 0) x
• CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'} [CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).hom (CategoryTheory.Limits.kernel.map f f' sq.left sq.right ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq) (CategoryTheory.Limits.kernelSubobjectIso f').hom
• CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'} [CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map f f' sq.left sq.right ⋯) (CategoryTheory.Limits.kernelSubobjectIso f').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).inv (CategoryTheory.Limits.kernelSubobjectMap sq)
• CategoryTheory.Limits.kernelSubobjectMap_arrow_apply 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'} [CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject f').arrow) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobjectMap sq)) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Arrow.Hom.left sq)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject f).arrow) x)
• CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'} [CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') {Z : C} (h : CategoryTheory.Limits.kernel f' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map f f' sq.left sq.right ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f').hom h)
• CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'} [CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') {Z : C} (h : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map f f' sq.left sq.right ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq) h)
• image_le_kernel 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g
• imageToKernel 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g)
• instMonoImageToKernel 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Mono (imageToKernel f g w)
• 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 ⋯)
• subobject_ofLE_as_imageToKernel 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) (h : CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g) : (CategoryTheory.Limits.imageSubobject f).ofLE (CategoryTheory.Limits.kernelSubobject g) h = imageToKernel f g w
• factorThruImageSubobject_comp_imageToKernel 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImageSubobject f) (imageToKernel f g w) = CategoryTheory.Limits.factorThruKernelSubobject g f w
• imageToKernel_arrow 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.Limits.kernelSubobject g).arrow = (CategoryTheory.Limits.imageSubobject f).arrow
• imageToKernel_epi_of_epi_of_zero 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Epi f] : CategoryTheory.Epi (imageToKernel f 0 ⋯)
• imageToKernel_arrow_assoc 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) {Z : V} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject g).arrow h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h
• 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_zero_right 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImages V] {w : CategoryTheory.CategoryStruct.comp f 0 = 0} : imageToKernel f 0 w = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow (CategoryTheory.inv (CategoryTheory.Limits.kernelSubobject 0).arrow)
• 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
• imageToKernel_arrow_apply 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) {F : V → V → Type uF} {carrier : V → Type w} {instFunLike : (X Y : V) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory V F] (x : carrier (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject g).arrow) ((CategoryTheory.ConcreteCategory.hom (imageToKernel f g w)) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.imageSubobject f).arrow) x
• imageToKernel_comp_hom_inv_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.HasEqualizers V] [CategoryTheory.Limits.HasImages V] {Z : V} {i : B ≅ Z} (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f i.hom) (CategoryTheory.CategoryStruct.comp i.inv g) = 0) : imageToKernel (CategoryTheory.CategoryStruct.comp f i.hom) (CategoryTheory.CategoryStruct.comp i.inv g) w = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f i.hom).hom (CategoryTheory.CategoryStruct.comp (imageToKernel f g ⋯) (CategoryTheory.Limits.kernelSubobjectIsoComp i.inv g).inv)
• CategoryTheory.ShortComplex.exact_iff_image_eq_kernel 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.Exact ↔ CategoryTheory.Limits.imageSubobject S.f = CategoryTheory.Limits.kernelSubobject S.g
• CategoryTheory.ShortComplex.Exact.isIso_imageToKernel 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) (hS : S.Exact) : CategoryTheory.IsIso (imageToKernel S.f S.g ⋯)
• CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.Exact ↔ CategoryTheory.Epi (imageToKernel S.f S.g ⋯)
• CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.Exact ↔ CategoryTheory.IsIso (imageToKernel S.f S.g ⋯)
• ModuleCat.toKernelSubobject 📋 Mathlib.Algebra.Category.ModuleCat.Subobject
  {R : Type u} [Ring R] {M N : ModuleCat R} {f : M ⟶ N} : ↥(ModuleCat.Hom.hom f).ker →ₗ[R] ↑(CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))
• ModuleCat.toKernelSubobject_arrow 📋 Mathlib.Algebra.Category.ModuleCat.Subobject
  {R : Type u} [Ring R] {M N : ModuleCat R} {f : M ⟶ N} (x : ↥(ModuleCat.Hom.hom f).ker) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject f).arrow) (ModuleCat.toKernelSubobject x) = ↑x
• 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')
• imageToKernel_unop 📋 Mathlib.Algebra.Homology.Opposite
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.Abelian V] {X Y Z : Vᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : imageToKernel g.unop f.unop ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso g.unop ≪≫ (CategoryTheory.imageUnopUnop g).symm).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.factorThruImage g) ⋯).unop (CategoryTheory.Limits.kernelSubobjectIso f.unop ≪≫ CategoryTheory.kernelUnopUnop f).inv)
• imageToKernel_op 📋 Mathlib.Algebra.Homology.Opposite
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.Abelian V] {X Y Z : V} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : imageToKernel g.op f.op ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso g.op ≪≫ (CategoryTheory.imageOpOp g).symm).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.factorThruImage g) ⋯).op (CategoryTheory.Limits.kernelSubobjectIso f.op ≪≫ CategoryTheory.kernelOpOp f).inv)
• AlgebraicTopology.NormalizedMooreComplex.objX_add_one 📋 Mathlib.AlgebraicTopology.MooreComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : AlgebraicTopology.NormalizedMooreComplex.objX X (n + 1) = Finset.univ.inf fun k => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)

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