Loogle!

Result

Found 82 declarations mentioning CategoryTheory.Limits.HasEqualizers.

• CategoryTheory.Limits.HasEqualizers 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop
• CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  (C : Type u) [CategoryTheory.Category.{v, u} C] [∀ {X Y : C} {f g : X ⟶ Y}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)] : CategoryTheory.Limits.HasEqualizers C
• CategoryTheory.Limits.hasStrongEpiImages_of_hasPullbacks_of_hasEqualizers 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasStrongEpiImages C
• CategoryTheory.Limits.image.compIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImage f] [CategoryTheory.IsIso g] : CategoryTheory.Limits.image f ≅ CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.Limits.image.preComp_epi_of_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImage g] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] [CategoryTheory.Epi f] : CategoryTheory.Epi (CategoryTheory.Limits.image.preComp f g)
• CategoryTheory.Limits.image.isIso_precomp_iso 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.IsIso f] [CategoryTheory.Limits.HasImage g] : CategoryTheory.IsIso (CategoryTheory.Limits.image.preComp f g)
• CategoryTheory.Limits.image.eq_fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y} [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasImage f'] [CategoryTheory.Limits.HasEqualizers C] (h : f = f') : CategoryTheory.Limits.image.ι f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.eqToIso h).hom (CategoryTheory.Limits.image.ι f')
• CategoryTheory.Limits.image.compIso_hom_comp_image_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImage f] [CategoryTheory.IsIso g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).hom (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) g
• CategoryTheory.Limits.image.compIso_inv_comp_image_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImage f] [CategoryTheory.IsIso g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).inv (CategoryTheory.Limits.image.ι f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.inv g)
• CategoryTheory.Limits.image.compIso_hom_comp_image_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImage f] [CategoryTheory.IsIso g] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) (CategoryTheory.CategoryStruct.comp g h)
• CategoryTheory.Limits.image.compIso_inv_comp_image_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImage f] [CategoryTheory.IsIso g] {Z✝ : C} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) h)
• CategoryTheory.Limits.image.ι_zero' 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] {X Y : C} {f : X ⟶ Y} (h : f = 0) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Limits.image.ι f = 0
• 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.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
• CategoryTheory.Limits.hasCoequalizers_opposite 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasCoequalizers Cᵒᵖ
• CategoryTheory.Limits.hasEqualizers_opposite 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasEqualizers Cᵒᵖ
• CategoryTheory.Limits.hasEqualizers_of_hasPullbacks_and_binary_products 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Limits.HasEqualizers C
• CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasFiniteLimits C
• CategoryTheory.Limits.has_limits_of_hasEqualizers_and_products 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C
• CategoryTheory.Limits.preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasFiniteProducts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.Limits.PreservesFiniteProducts G] : CategoryTheory.Limits.PreservesFiniteLimits G
• CategoryTheory.Limits.preservesLimits_of_preservesEqualizers_and_products 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasProducts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [∀ (J : Type w), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) G] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w, v, v₂, u, u₂} G
• CategoryTheory.Limits.createsFiniteLimitsOfCreatesEqualizersAndFiniteProducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasEqualizers D] [CategoryTheory.Limits.HasFiniteProducts D] (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.Limits.CreatesFiniteProducts G] : CategoryTheory.Limits.CreatesFiniteLimits G
• CategoryTheory.Limits.createsLimitsOfSizeOfCreatesEqualizersAndProducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasEqualizers D] [CategoryTheory.Limits.HasProducts D] (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [(J : Type w) → CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete J) G] : CategoryTheory.CreatesLimitsOfSize.{w, w, v, v₂, u, u₂} G
• CategoryTheory.Limits.preservesLimit_of_preservesEqualizers_and_product 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) C] [CategoryTheory.Limits.HasEqualizers C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) G] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) G] : CategoryTheory.Limits.PreservesLimitsOfShape J G
• CategoryTheory.Limits.createsLimitsOfShapeOfCreatesEqualizersAndProducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) D] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) D] [CategoryTheory.Limits.HasEqualizers D] (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete J) G] [CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) G] : CategoryTheory.CreatesLimitsOfShape J G
• CategoryTheory.Limits.hasLimit_of_equalizer_and_product 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor F.obj)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => F.obj f.fst.2)] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasLimit F
• CategoryTheory.Limits.limitConeOfEqualizerAndProduct 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor F.obj)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => F.obj f.fst.2)] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.LimitCone F
• CategoryTheory.Limits.hasPullbacks_of_hasBinaryProducts_of_hasEqualizers 📋 Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasPullbacks C
• 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.Abelian.hasEqualizers 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasEqualizers C
• CategoryTheory.Functor.preservesFiniteLimits_of_preservesKernels 📋 Mathlib.CategoryTheory.Preadditive.LeftExact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] : CategoryTheory.Limits.PreservesFiniteLimits F
• CategoryTheory.Limits.instEpiFactorThruImageSubobjectOfHasEqualizers 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Epi (CategoryTheory.Limits.factorThruImageSubobject f)
• CategoryTheory.Limits.imageSubobject_iso_comp 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] {X' : C} (h : X' ⟶ X) [CategoryTheory.IsIso h] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f) = CategoryTheory.Limits.imageSubobject f
• CategoryTheory.Limits.imageSubobjectCompIso 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)) ≅ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f)
• CategoryTheory.Limits.imageSubobject_comp_le_epi_of_epi 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] {X' : C} (h : X' ⟶ X) [CategoryTheory.Epi h] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp h f)] : CategoryTheory.Epi ((CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f)).ofLE (CategoryTheory.Limits.imageSubobject f) ⋯)
• CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).inv (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h
• CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).hom (CategoryTheory.Limits.imageSubobject f).arrow = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow (CategoryTheory.inv h)
• CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] {Z : C} (h✝ : Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow (CategoryTheory.CategoryStruct.comp h h✝)
• CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] {Z : C} (h✝ : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv h) h✝)
• 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.HasDetector.hasSeparator 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.HasDetector C] : CategoryTheory.HasSeparator C
• CategoryTheory.IsDetector.isSeparator 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasEqualizers C] {G : C} : CategoryTheory.IsDetector G → CategoryTheory.IsSeparator G
• CategoryTheory.isSeparator_detector 📋 Mathlib.CategoryTheory.Generator.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.HasDetector C] : CategoryTheory.IsSeparator (CategoryTheory.detector C)
• CategoryTheory.ObjectProperty.IsDetecting.isSeparating 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.Limits.HasEqualizers C] (hP : P.IsDetecting) : P.IsSeparating
• CategoryTheory.ObjectProperty.isDetecting_iff_isSeparating 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Balanced C] : P.IsDetecting ↔ P.IsSeparating
• CategoryTheory.Limits.hasEqualizers_of_hasWideEqualizers 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWideEqualizers C] : CategoryTheory.Limits.HasEqualizers C
• CategoryTheory.Limits.hasCoreflexiveEqualizers_of_hasEqualizers 📋 Mathlib.CategoryTheory.Limits.Shapes.Reflexive
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasCoreflexiveEqualizers C
• HomologicalComplex.image_to_eq_image 📋 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.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {i j : ι} (r : c.Rel i j) : CategoryTheory.Limits.imageSubobject (C.dTo j) = CategoryTheory.Limits.imageSubobject (C.d i j)
• HomologicalComplex.image_eq_image 📋 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.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {i i' j : ι} (r : c.Rel i j) (r' : c.Rel i' j) : CategoryTheory.Limits.imageSubobject (C.d i j) = CategoryTheory.Limits.imageSubobject (C.d i' j)
• CategoryTheory.epi_of_nonzero_to_simple 📋 Mathlib.CategoryTheory.Simple
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] {X Y : C} [CategoryTheory.Simple Y] {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (w : f ≠ 0) : CategoryTheory.Epi f
• CategoryTheory.Over.instHasEqualizers 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasEqualizers (CategoryTheory.Over B)
• RingHom.HasEqualizers.hasEqualizers 📋 Mathlib.Algebra.Category.Ring.Under.Property
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) (hQe : RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.Limits.HasEqualizers ((RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q).Under ⊤ R)
• CategoryTheory.Limits.equalizerPullbackMapIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S) : CategoryTheory.Limits.equalizer (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) ≅ CategoryTheory.Limits.pullback (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.Limits.pullback.fst s v)
• CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).hom (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.Limits.pullback.fst s v)) = CategoryTheory.Limits.equalizer.ι (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
• CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.Limits.pullback.fst s v)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.Limits.pullback.fst s v)) (CategoryTheory.Limits.equalizer.ι f g)
• CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.Limits.pullback.snd s v)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.Limits.pullback.fst s v)) (CategoryTheory.Limits.pullback.snd s v)
• CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst s v) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.Limits.pullback.fst s v)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) h)
• CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S) {Z : C} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd s v) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.Limits.pullback.fst s v)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd s v) h)
• CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S) {Z : C} (h : CategoryTheory.Limits.pullback s v ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.Limits.pullback.fst s v)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) h
• CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.Limits.pullback.fst s v)) (CategoryTheory.Limits.equalizer.ι f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.Limits.pullback.fst s v)
• CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.Limits.pullback.fst s v)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst s v) h)
• CategoryTheory.eq_of_zeroHypercover_target 📋 Mathlib.CategoryTheory.MorphismProperty.Local
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) {J : CategoryTheory.Precoverage C} (𝒰 : J.ZeroHypercover S) [J.IsStableUnderBaseChange] [(CategoryTheory.MorphismProperty.isomorphisms C).IsLocalAtTarget J] (H : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.pullback.map s (𝒰.f i) t (𝒰.f i) f (CategoryTheory.CategoryStruct.id (𝒰.X i)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯ = CategoryTheory.Limits.pullback.map s (𝒰.f i) t (𝒰.f i) g (CategoryTheory.CategoryStruct.id (𝒰.X i)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) : f = g
• CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong 📋 Mathlib.CategoryTheory.MorphismProperty.Descent
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} [(CategoryTheory.MorphismProperty.isomorphisms C).DescendsAlong P] [P.IsStableUnderBaseChange] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasEqualizers C] {S T : C} {f : T ⟶ S} (hf : P f) : (CategoryTheory.Over.pullback f).Faithful
• CategoryTheory.MorphismProperty.eq_of_isomorphisms_descendsAlong 📋 Mathlib.CategoryTheory.MorphismProperty.Descent
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} [(CategoryTheory.MorphismProperty.isomorphisms C).DescendsAlong P] [P.IsStableUnderBaseChange] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S) (hv : P v) (H : CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯ = CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) : f = g
• CategoryTheory.JointlyReflectIsomorphisms.jointlyFaithful 📋 Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
  {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)} (h : CategoryTheory.JointlyReflectIsomorphisms F) [∀ (i : I), CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (F i)] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.JointlyFaithful F
• CategoryTheory.JointlyFaithful.of_jointly_reflects_isIso_of_mono 📋 Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
  {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)} [CategoryTheory.Limits.HasEqualizers C] [∀ (i : I), CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (F i)] (hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [CategoryTheory.Mono f], (∀ (i : I), CategoryTheory.IsIso ((F i).map f)) → CategoryTheory.IsIso f) : CategoryTheory.JointlyFaithful F
• CategoryTheory.ExtremalEpi.mk_of_hasEqualizers 📋 Mathlib.CategoryTheory.ExtremalEpi
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasEqualizers C] (hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), CategoryTheory.CategoryStruct.comp p i = f → ∀ [CategoryTheory.Mono i], CategoryTheory.IsIso i) : CategoryTheory.ExtremalEpi f
• SemiNormedGrp.instHasEqualizers 📋 Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
  : CategoryTheory.Limits.HasEqualizers SemiNormedGrp
• CategoryTheory.Limits.isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair 📋 Mathlib.CategoryTheory.Limits.Indization.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape CategoryTheory.Limits.IsIndObject CategoryTheory.Limits.WalkingParallelPair
• CategoryTheory.ObjectProperty.SerreClassLocalization.hasEqualizers 📋 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.HasEqualizers D
• CategoryTheory.PreGaloisCategory.instHasEqualizers 📋 Mathlib.CategoryTheory.Galois.Basic
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] : CategoryTheory.Limits.HasEqualizers C
• CategoryTheory.PreservesImage.iso 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : CategoryTheory.Limits.image (L.map f) ≅ L.obj (CategoryTheory.Limits.image f)
• CategoryTheory.PreservesImage.factorThruImage_comp_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (L.map f)) (CategoryTheory.PreservesImage.iso L f).hom = L.map (CategoryTheory.Limits.factorThruImage f)
• CategoryTheory.PreservesImage.inv_comp_image_ι_map 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).inv (CategoryTheory.Limits.image.ι (L.map f)) = L.map (CategoryTheory.Limits.image.ι f)
• CategoryTheory.PreservesImage.hom_comp_map_image_ι 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom (L.map (CategoryTheory.Limits.image.ι f)) = CategoryTheory.Limits.image.ι (L.map f)
• CategoryTheory.PreservesImage.factorThruImage_comp_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj (CategoryTheory.Limits.image f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (L.map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom h) = CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.factorThruImage f)) h
• CategoryTheory.PreservesImage.inv_comp_image_ι_map_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (L.map f)) h) = CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.image.ι f)) h
• CategoryTheory.PreservesImage.hom_comp_map_image_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom (CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.image.ι f)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (L.map f)) h
• CategoryTheory.PreservesImage.iso_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : (CategoryTheory.PreservesImage.iso L f).hom = CategoryTheory.Limits.image.lift { I := L.obj (CategoryTheory.Limits.image f), m := L.map (CategoryTheory.Limits.image.ι f), m_mono := ⋯, e := L.map (CategoryTheory.Limits.factorThruImage f), fac := ⋯ }
• CategoryTheory.PreservesImage.iso_inv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : (CategoryTheory.PreservesImage.iso L f).inv = { I := L.obj (CategoryTheory.Limits.image f), m := L.map (CategoryTheory.Limits.image.ι f), m_mono := ⋯, e := L.map (CategoryTheory.Limits.factorThruImage f), fac := ⋯, e_strong_epi := ⋯ }.toMonoIsImage.lift (CategoryTheory.Limits.Image.monoFactorisation (L.map f))
• CategoryTheory.Limits.HasWeakEqualizersOfHasEqualizers 📋 Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasWeakEqualizers C
• ωCPO.instHasEqualizers 📋 Mathlib.Order.Category.OmegaCompletePartialOrder
  : CategoryTheory.Limits.HasEqualizers ωCPO

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