Loogle!

Result

Found 70 declarations mentioning CategoryTheory.Limits.equalizer.

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.isoSourceOfSelf 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
{C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f : X ⟶ Y) : CategoryTheory.Limits.equalizer f f ≅ X
CategoryTheory.Limits.equalizer.ι_of_self 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
{C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Limits.equalizer.ι f f)
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.equalizer.isoSourceOfSelf_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
{C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f : X ⟶ Y) : (CategoryTheory.Limits.equalizer.isoSourceOfSelf f).hom = CategoryTheory.Limits.equalizer.ι f f
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.isoSourceOfSelf_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
{C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f : X ⟶ Y) : (CategoryTheory.Limits.equalizer.isoSourceOfSelf f).inv = CategoryTheory.Limits.equalizer.lift (CategoryTheory.CategoryStruct.id X) ⋯
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.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.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.Limits.equalizer_as_kernel 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] : CategoryTheory.Limits.equalizer.ι f 0 = CategoryTheory.Limits.kernel.ι f
CategoryTheory.instIsRegularMonoι 📋 Mathlib.CategoryTheory.Limits.Shapes.RegularMono
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (g h : X ⟶ Y) [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)] : CategoryTheory.IsRegularMono (CategoryTheory.Limits.equalizer.ι g h)
CategoryTheory.RegularMono.equalizer 📋 Mathlib.CategoryTheory.Limits.Shapes.RegularMono
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (g h : X ⟶ Y) [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)] : CategoryTheory.RegularMono (CategoryTheory.Limits.equalizer.ι g h)
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.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.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 📋 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'_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.isoEqualizer 📋 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.multiequalizer I ≅ CategoryTheory.Limits.equalizer I.fstPiMap I.sndPiMap
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.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_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_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.Limits.Types.equalizerIso 📋 Mathlib.CategoryTheory.Limits.Types.Equalizers
{Y Z : Type u} (g h : Y ⟶ Z) : CategoryTheory.Limits.equalizer g h ≅ { x // (CategoryTheory.ConcreteCategory.hom g) x = (CategoryTheory.ConcreteCategory.hom h) x }
CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype 📋 Mathlib.CategoryTheory.Limits.Types.Equalizers
{Y Z : Type u} (g h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.equalizerIso g h).hom (TypeCat.ofHom Subtype.val) = CategoryTheory.Limits.equalizer.ι g h
CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι 📋 Mathlib.CategoryTheory.Limits.Types.Equalizers
{Y Z : Type u} (g h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.equalizerIso g h).inv (CategoryTheory.Limits.equalizer.ι g h) = TypeCat.ofHom Subtype.val
CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype_apply 📋 Mathlib.CategoryTheory.Limits.Types.Equalizers
{Y Z : Type u} (g h : Y ⟶ Z) (x : CategoryTheory.Limits.equalizer g h) : ↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.equalizerIso g h).hom) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.equalizer.ι g h)) x
CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι_apply 📋 Mathlib.CategoryTheory.Limits.Types.Equalizers
{Y Z : Type u} (g h : Y ⟶ Z) (x : { x // (CategoryTheory.ConcreteCategory.hom g) x = (CategoryTheory.ConcreteCategory.hom h) x }) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.equalizer.ι g h)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.equalizerIso g h).inv) x) = ↑x
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))
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)
AlgebraicGeometry.instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat 📋 Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
{X Y : AlgebraicGeometry.Scheme} [QuasiSeparatedSpace ↥Y] (f g : X ⟶ Y) : AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.equalizer.ι f g)
AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace 📋 Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
{X Y : AlgebraicGeometry.Scheme} [CompactSpace ↥X] [QuasiSeparatedSpace ↥Y] (f g : X ⟶ Y) : CompactSpace ↥(CategoryTheory.Limits.equalizer f g)
AlgebraicGeometry.Scheme.instIsClosedImmersionιOfIsSeparated 📋 Mathlib.AlgebraicGeometry.Morphisms.Separated
{X Y : AlgebraicGeometry.Scheme} (f g : X ⟶ Y) [Y.IsSeparated] : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.equalizer.ι f g)
AlgebraicGeometry.isClosedImmersion_equalizer_ι_left 📋 Mathlib.AlgebraicGeometry.Morphisms.Separated
{S : AlgebraicGeometry.Scheme} {X Y : CategoryTheory.Over S} [AlgebraicGeometry.IsSeparated Y.hom] (f g : X ⟶ Y) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.equalizer.ι f g))
AlgebraicGeometry.IsImmersion.instιScheme 📋 Mathlib.AlgebraicGeometry.Morphisms.Immersion
{X Y : AlgebraicGeometry.Scheme} (f g : X ⟶ Y) : AlgebraicGeometry.IsImmersion (CategoryTheory.Limits.equalizer.ι f g)
CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv 📋 Mathlib.CategoryTheory.Galois.Basic
{C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X Y : C} (f g : X ⟶ Y) : (F.obj (CategoryTheory.Limits.equalizer f g)).obj ≃ { x // (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map g)) x }
CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply 📋 Mathlib.CategoryTheory.Galois.Basic
{C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X Y : C} {f g : X ⟶ Y} (x : (F.obj X).obj) (h : (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map g)) x) : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Limits.equalizer.ι f g))) ((CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv F f g).symm ⟨x, h⟩) = x
CategoryTheory.regularTopology.equalizerCondition_iff_isIso_lift 📋 Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)) : CategoryTheory.regularTopology.EqualizerCondition P ↔ ∀ (X B : C) (π : X ⟶ B) [CategoryTheory.EffectiveEpi π] [inst : CategoryTheory.Limits.HasPullback π π], CategoryTheory.IsIso (CategoryTheory.Limits.equalizer.lift (P.map π.op) ⋯)
CategoryTheory.regularTopology.mapToEqualizer_eq_comp 📋 Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)) {X B : C} (π : X ⟶ B) [CategoryTheory.Limits.HasPullback π π] : CategoryTheory.regularTopology.mapToEqualizer P π (CategoryTheory.Limits.pullback.fst π π) (CategoryTheory.Limits.pullback.snd π π) ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.lift (P.map π.op) ⋯) (CategoryTheory.Limits.Types.equalizerIso (P.map (CategoryTheory.Limits.pullback.fst π π).op) (P.map (CategoryTheory.Limits.pullback.snd π π).op)).hom

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.
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