Loogle!

Result

Found 73 declarations mentioning CategoryTheory.Limits.HasEqualizer.

• CategoryTheory.Limits.hasEqualizer_of_self 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f : X ⟶ Y) : CategoryTheory.Limits.HasEqualizer f f
• CategoryTheory.Limits.HasEqualizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) : Prop
• CategoryTheory.Limits.equalizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : C
• CategoryTheory.Limits.equalizer.fork 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : CategoryTheory.Limits.Fork f g
• CategoryTheory.Limits.equalizer.ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : CategoryTheory.Limits.equalizer f g ⟶ X
• CategoryTheory.Limits.equalizer.ι_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} [CategoryTheory.Limits.HasEqualizer f g] : CategoryTheory.Mono (CategoryTheory.Limits.equalizer.ι f g)
• CategoryTheory.Limits.eq_of_epi_equalizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Epi (CategoryTheory.Limits.equalizer.ι f g)] : f = g
• CategoryTheory.Limits.equalizer.ι_of_eq 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} [CategoryTheory.Limits.HasEqualizer f g] (h : f = g) : CategoryTheory.IsIso (CategoryTheory.Limits.equalizer.ι f g)
• CategoryTheory.Limits.hasEqualizer_comp_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  (C : Type u) {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] {Z : C} (h : Y ⟶ Z) [CategoryTheory.Mono h] : CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g h)
• CategoryTheory.Limits.equalizerIsEqualizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Limits.equalizer.ι f g) ⋯)
• CategoryTheory.Limits.splitMonoOfIdempotentEqualizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X : C} {f : X ⟶ X} (hf : CategoryTheory.CategoryStruct.comp f f = f) [CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.id X) f] : CategoryTheory.SplitMono (CategoryTheory.Limits.equalizer.ι (CategoryTheory.CategoryStruct.id X) f)
• CategoryTheory.Limits.equalizer.fork_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : (CategoryTheory.Limits.equalizer.fork f g).ι = CategoryTheory.Limits.equalizer.ι f g
• CategoryTheory.Limits.equalizer.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} [CategoryTheory.Limits.HasEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) : W ⟶ CategoryTheory.Limits.equalizer f g
• CategoryTheory.Limits.hasEqualizer_precomp_of_hasEqualizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {Z : C} (h : Z ⟶ X) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.equalizer.ι f g) h] : CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)
• CategoryTheory.Limits.equalizer.condition 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) g
• CategoryTheory.Limits.equalizer.lift_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} [CategoryTheory.Limits.HasEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.lift k h) (CategoryTheory.Limits.equalizer.ι f g) = k
• CategoryTheory.Limits.equalizer.condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.CategoryStruct.comp g h)
• CategoryTheory.Limits.equalizerComparison 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] : G.obj (CategoryTheory.Limits.equalizer f g) ⟶ CategoryTheory.Limits.equalizer (G.map f) (G.map g)
• CategoryTheory.Limits.equalizer.existsUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} [CategoryTheory.Limits.HasEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) : ∃! l, CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g) = k
• CategoryTheory.Limits.equalizer.lift' 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} [CategoryTheory.Limits.HasEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) : { l // CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g) = k }
• CategoryTheory.Limits.hasEqualizer_precomp_of_equalizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {Z : C} (h : Z ⟶ X) {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) {c : CategoryTheory.Limits.PullbackCone s.ι h} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)
• CategoryTheory.Limits.equalizer.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} [CategoryTheory.Limits.HasEqualizer f g] {W : C} {k l : W ⟶ CategoryTheory.Limits.equalizer f g} (h : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.equalizer.ι f g) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g)) : k = l
• CategoryTheory.Limits.equalizer.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} [CategoryTheory.Limits.HasEqualizer f g] {W : C} {k l : W ⟶ CategoryTheory.Limits.equalizer f g} : k = l ↔ CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.equalizer.ι f g) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g)
• CategoryTheory.Limits.equalizer.lift_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} [CategoryTheory.Limits.HasEqualizer f g] {W : C} (k : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) {Z : C} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.lift k h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) h✝) = CategoryTheory.CategoryStruct.comp k h✝
• CategoryTheory.Limits.equalizer.fork_π_app_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : (CategoryTheory.Limits.equalizer.fork f g).π.app CategoryTheory.Limits.WalkingParallelPair.zero = CategoryTheory.Limits.equalizer.ι f g
• CategoryTheory.Limits.equalizerComparison_comp_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerComparison f g G) (CategoryTheory.Limits.equalizer.ι (G.map f) (G.map g)) = G.map (CategoryTheory.Limits.equalizer.ι f g)
• CategoryTheory.Limits.equalizerComparison_comp_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] {Z : D} (h : G.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerComparison f g G) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι (G.map f) (G.map g)) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.equalizer.ι f g)) h
• CategoryTheory.Limits.map_lift_equalizerComparison 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] {Z : C} {h : Z ⟶ X} (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.equalizer.lift h w)) (CategoryTheory.Limits.equalizerComparison f g G) = CategoryTheory.Limits.equalizer.lift (G.map h) ⋯
• CategoryTheory.Limits.map_lift_equalizerComparison_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] {Z : C} {h : Z ⟶ X} (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) {Z✝ : D} (h✝ : CategoryTheory.Limits.equalizer (G.map f) (G.map g) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.equalizer.lift h w)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerComparison f g G) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.lift (G.map h) ⋯) h✝
• CategoryTheory.Preadditive.hasEqualizer_of_hasKernel 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasKernel (f - g)] : CategoryTheory.Limits.HasEqualizer f g
• CategoryTheory.Preadditive.hasKernel_of_hasEqualizer 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : CategoryTheory.Limits.HasKernel (f - g)
• CategoryTheory.Limits.hasEqualizer_of_hasSplitEqualizer 📋 Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.HasSplitEqualizer f g] : CategoryTheory.Limits.HasEqualizer f g
• CategoryTheory.Limits.PreservesEqualizer.iso 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] : G.obj (CategoryTheory.Limits.equalizer f g) ≅ CategoryTheory.Limits.equalizer (G.map f) (G.map g)
• CategoryTheory.Limits.instIsIsoEqualizerComparison 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] : CategoryTheory.IsIso (CategoryTheory.Limits.equalizerComparison f g G)
• CategoryTheory.Limits.PreservesEqualizer.of_iso_comparison 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] [i : CategoryTheory.IsIso (CategoryTheory.Limits.equalizerComparison f g G)] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G
• CategoryTheory.Limits.isLimitOfHasEqualizerOfPreservesLimit 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (G.map (CategoryTheory.Limits.equalizer.ι f g)) ⋯)
• CategoryTheory.Limits.PreservesEqualizer.iso_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] : (CategoryTheory.Limits.PreservesEqualizer.iso G f g).hom = CategoryTheory.Limits.equalizerComparison f g G
• CategoryTheory.Limits.PreservesEqualizer.iso_inv_ι 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesEqualizer.iso G f g).inv (G.map (CategoryTheory.Limits.equalizer.ι f g)) = CategoryTheory.Limits.equalizer.ι (G.map f) (G.map g)
• CategoryTheory.Limits.equalizerSubobject 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : CategoryTheory.Subobject X
• CategoryTheory.Limits.equalizerSubobjectIso 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.equalizerSubobject f g) ≅ CategoryTheory.Limits.equalizer f g
• CategoryTheory.Limits.equalizerSubobject_factors 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] {W : C} (h : W ⟶ X) (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) : (CategoryTheory.Limits.equalizerSubobject f g).Factors h
• CategoryTheory.Limits.equalizerSubobject_factors_iff 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] {W : C} (h : W ⟶ X) : (CategoryTheory.Limits.equalizerSubobject f g).Factors h ↔ CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g
• CategoryTheory.Limits.pullback_equalizer 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] {W : C} (h : W ⟶ X) [CategoryTheory.Limits.HasPullbacks C] : (CategoryTheory.Subobject.pullback h).obj (CategoryTheory.Limits.equalizerSubobject f g) = CategoryTheory.Limits.equalizerSubobject (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)
• CategoryTheory.Limits.equalizerSubobject_arrow' 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobjectIso f g).inv (CategoryTheory.Limits.equalizerSubobject f g).arrow = CategoryTheory.Limits.equalizer.ι f g
• CategoryTheory.Limits.equalizerSubobject_arrow_comp 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobject f g).arrow f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobject f g).arrow g
• CategoryTheory.Limits.equalizerSubobject_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobjectIso f g).hom (CategoryTheory.Limits.equalizer.ι f g) = (CategoryTheory.Limits.equalizerSubobject f g).arrow
• CategoryTheory.Limits.equalizerSubobject_arrow_comp_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobject f g).arrow (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobject f g).arrow (CategoryTheory.CategoryStruct.comp g h)
• CategoryTheory.Limits.equalizerSubobject_arrow'_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobjectIso f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobject f g).arrow h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) h
• CategoryTheory.Limits.equalizerSubobject_arrow_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobjectIso f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobject f g).arrow h
• CategoryTheory.Limits.Multiequalizer.instHasEqualizerFstPiMapSndPiMap 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.HasEqualizer I.fstPiMap I.sndPiMap
• CategoryTheory.Limits.HasCoreflexiveEqualizers.has_eq 📋 Mathlib.CategoryTheory.Limits.Shapes.Reflexive
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasCoreflexiveEqualizers C] ⦃A B : C⦄ (f g : A ⟶ B) [CategoryTheory.IsCoreflexivePair f g] : CategoryTheory.Limits.HasEqualizer f g
• CategoryTheory.Limits.HasCoreflexiveEqualizers.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Reflexive
  {C : Type u} [CategoryTheory.Category.{v, u} C] (has_eq : ∀ ⦃A B : C⦄ (f g : A ⟶ B) [CategoryTheory.IsCoreflexivePair f g], CategoryTheory.Limits.HasEqualizer f g) : CategoryTheory.Limits.HasCoreflexiveEqualizers C
• CategoryTheory.Limits.hasEqualizer_of_common_retraction 📋 Mathlib.CategoryTheory.Limits.Shapes.Reflexive
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoreflexiveEqualizers C] {A B : C} {f g : A ⟶ B} (r : B ⟶ A) (fr : CategoryTheory.CategoryStruct.comp f r = CategoryTheory.CategoryStruct.id A) (gr : CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.id A) : CategoryTheory.Limits.HasEqualizer f g
• CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair.mk 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} (out : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], CategoryTheory.Limits.HasEqualizer f g) : CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair F
• CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair.out 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.Category.{v₁, u₂} D} (F : CategoryTheory.Functor C D) [self : CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair F] {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g] : CategoryTheory.Limits.HasEqualizer f g
• CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.1 A.A))] : C
• CategoryTheory.Comonad.instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair F] (A : adj.toComonad.Coalgebra) : CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
• CategoryTheory.Comonad.ComonadicityInternal.rightAdjointComparison 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : CategoryTheory.Functor adj.toComonad.Coalgebra C
• CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : CategoryTheory.Comonad.comparison adj ⊣ CategoryTheory.Comonad.ComonadicityInternal.rightAdjointComparison adj
• CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) (B : C) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : ((CategoryTheory.Comonad.comparison adj).obj B ⟶ A) ≃ (B ⟶ CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj A)
• CategoryTheory.Comonad.ComonadicityInternal.instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (B : C) : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B))))
• CategoryTheory.Comonad.ComonadicityInternal.counitFork 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : CategoryTheory.Limits.Fork (F.map (G.map A.a)) (F.map (adj.unit.app (G.obj A.A)))
• CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_unit_app 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (B : C) : (CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).unit.app B = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (CategoryTheory.Comonad.ComonadicityInternal.unitFork adj B)
• CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : (CategoryTheory.Comonad.ComonadicityInternal.counitFork A).pt = F.obj (CategoryTheory.Limits.equalizer (G.map A.a) (adj.unit.app (G.obj A.A)))
• CategoryTheory.Comonad.ComonadicityInternal.counitLimitOfPreservesEqualizer 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F] : CategoryTheory.Limits.IsLimit (CategoryTheory.Comonad.ComonadicityInternal.counitFork A)
• CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (A : adj.toComonad.Coalgebra) : ((CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).counit.app A).f = (CategoryTheory.Comonad.beckEqualizer A).lift (CategoryTheory.Comonad.ComonadicityInternal.counitFork A)
• CategoryTheory.Comonad.ComonadicityInternal.unitFork_ι 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : (CategoryTheory.Comonad.ComonadicityInternal.counitFork A).ι = F.map (CategoryTheory.Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)))
• CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) (B : C) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (f : B ⟶ CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj A) : ((CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv adj A B).symm f).f = (adj.homEquiv B A.A).symm (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))))
• CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) (B : C) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (f : (CategoryTheory.Comonad.comparison adj).obj B ⟶ A) : (CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv adj A B) f = CategoryTheory.Limits.equalizer.lift ((adj.homEquiv B A.A) f.f) ⋯
• CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : (CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).counit = { app := fun Y => (CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv adj Y (CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj Y)).symm (CategoryTheory.CategoryStruct.id (CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj Y)), naturality := ⋯ }
• CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f_aux 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (A : adj.toComonad.Coalgebra) : ((CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).counit.app A).f = (adj.homEquiv (CategoryTheory.Limits.equalizer (G.map A.a) (adj.unit.app (G.obj A.A))) A.A).symm (CategoryTheory.Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)))
• CategoryTheory.Idempotents.isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent 📋 Mathlib.CategoryTheory.Idempotents.Basic
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] : CategoryTheory.IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), CategoryTheory.CategoryStruct.comp p p = p → CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.id X) p
• CategoryTheory.Limits.isPullback_equalizer_prod 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Limits.HasBinaryProduct Y Y] : CategoryTheory.IsPullback (CategoryTheory.Limits.equalizer.ι f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) f) (CategoryTheory.Limits.prod.lift f g) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y))

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