Loogle!

Result

Found 148 declarations mentioning CategoryTheory.Limits.Fork.

• CategoryTheory.Limits.Fork 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) : Type (max u v)
• 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.idFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (h : f = g) : CategoryTheory.Limits.Fork f g
• CategoryTheory.Limits.coneOfIsSplitMono 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] (f : X ⟶ Y) [CategoryTheory.IsSplitMono f] : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f)
• CategoryTheory.Limits.Cone.ofFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} (t : CategoryTheory.Limits.Fork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.Fork.ofCone 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} (t : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Fork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)
• CategoryTheory.Limits.Fork.ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g) : t.pt ⟶ X
• CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_self 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f : X ⟶ Y} {c : CategoryTheory.Limits.Fork f f} (h : CategoryTheory.Limits.IsLimit c) : CategoryTheory.IsIso c.ι
• CategoryTheory.Limits.eq_of_epi_fork_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g) [CategoryTheory.Epi t.ι] : f = g
• CategoryTheory.Limits.mono_of_isLimit_fork 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {c : CategoryTheory.Limits.Fork f g} (i : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Mono c.ι
• CategoryTheory.Limits.Fork.IsLimit.mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Mono s.ι
• CategoryTheory.Limits.Fork.ofι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {P : C} (ι : P ⟶ X) (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) : CategoryTheory.Limits.Fork f g
• CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (h₀ : f = g) {c : CategoryTheory.Limits.Fork f g} (h : CategoryTheory.Limits.IsLimit c) : CategoryTheory.IsIso c.ι
• CategoryTheory.Limits.Fork.isoForkOfι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c ≅ CategoryTheory.Limits.Fork.ofι c.ι ⋯
• CategoryTheory.Limits.precompFork 📋 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) (c : CategoryTheory.Limits.PullbackCone s.ι h) : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)
• CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {c : CategoryTheory.Limits.Fork f g} (h : CategoryTheory.Limits.IsLimit c) [CategoryTheory.Epi c.ι] : CategoryTheory.IsIso c.ι
• CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork 📋 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) {c : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.id X) f} (i : CategoryTheory.Limits.IsLimit c) : CategoryTheory.SplitMono c.ι
• CategoryTheory.Limits.Fork.IsLimit.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (k : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) : W ⟶ s.pt
• CategoryTheory.Limits.Fork.condition 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g) : CategoryTheory.CategoryStruct.comp t.ι f = CategoryTheory.CategoryStruct.comp t.ι g
• CategoryTheory.Limits.Fork.IsLimit.homIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : CategoryTheory.Limits.Fork f g} (ht : CategoryTheory.Limits.IsLimit t) (Z : C) : (Z ⟶ t.pt) ≃ { h // CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g }
• CategoryTheory.Limits.Fork.IsLimit.lift_ι' 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (k : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.IsLimit.lift hs k h) s.ι = k
• CategoryTheory.Limits.Fork.IsLimit.lift_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.CategoryStruct.comp (hs.lift t) s.ι = t.ι
• CategoryTheory.Limits.Fork.condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp t.ι (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp t.ι (CategoryTheory.CategoryStruct.comp g h)
• 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.Fork.app_zero_eq_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g) : t.π.app CategoryTheory.Limits.WalkingParallelPair.zero = t.ι
• CategoryTheory.Limits.ForkOfι.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {P : C} {ι ι' : P ⟶ X} (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) (w' : CategoryTheory.CategoryStruct.comp ι' f = CategoryTheory.CategoryStruct.comp ι' g) (h : ι = ι') : CategoryTheory.Limits.Fork.ofι ι w ≅ CategoryTheory.Limits.Fork.ofι ι' w'
• CategoryTheory.Limits.isLimitPrecompFork 📋 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.IsLimit (CategoryTheory.Limits.precompFork h s c)
• CategoryTheory.Limits.Fork.hom_comp_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g} (f✝ : s ⟶ t) : CategoryTheory.CategoryStruct.comp f✝.hom t.ι = s.ι
• CategoryTheory.Limits.Fork.IsLimit.existsUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (k : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) : ∃! l, CategoryTheory.CategoryStruct.comp l s.ι = k
• CategoryTheory.Limits.Fork.IsLimit.lift' 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (k : W ⟶ X) (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g) : { l // CategoryTheory.CategoryStruct.comp l s.ι = k }
• CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (s : CategoryTheory.Limits.Fork f g) : s.π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp s.ι f
• CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (s : CategoryTheory.Limits.Fork f g) : s.π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp s.ι g
• CategoryTheory.Limits.Fork.IsLimit.lift_ι'_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) {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.Fork.IsLimit.lift hs k h) (CategoryTheory.CategoryStruct.comp s.ι h✝) = CategoryTheory.CategoryStruct.comp k h✝
• CategoryTheory.Limits.Fork.equivOfIsos 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} {f' g' : X' ⟶ Y'} (e₀ : X ≅ X') (e₁ : Y ≅ Y') (comm₁ : CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom := by cat_disch) (comm₂ : CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom := by cat_disch) : CategoryTheory.Limits.Fork f g ≌ CategoryTheory.Limits.Fork f' g'
• CategoryTheory.Limits.Fork.IsLimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) {W : C} {k l : W ⟶ s.pt} (h : CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι) : k = l
• CategoryTheory.Limits.Fork.mkHom 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g} (k : s.pt ⟶ t.pt) (w : CategoryTheory.CategoryStruct.comp k t.ι = s.ι) : s ⟶ t
• CategoryTheory.Limits.Fork.IsLimit.lift_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (hs.lift t) (CategoryTheory.CategoryStruct.comp s.ι h) = CategoryTheory.CategoryStruct.comp t.ι h
• CategoryTheory.Limits.Fork.IsLimit.ofExistsUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {t : CategoryTheory.Limits.Fork f g} (hs : ∀ (s : CategoryTheory.Limits.Fork f g), ∃! l, CategoryTheory.CategoryStruct.comp l t.ι = s.ι) : CategoryTheory.Limits.IsLimit t
• CategoryTheory.Limits.Fork.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g} (i : s.pt ≅ t.pt) (w : CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι := by cat_disch) : s ≅ t
• CategoryTheory.Limits.Fork.mkHom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g} (k : s.pt ⟶ t.pt) (w : CategoryTheory.CategoryStruct.comp k t.ι = s.ι) : (CategoryTheory.Limits.Fork.mkHom k w).hom = k
• CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork_retraction 📋 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) {c : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.id X) f} (i : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork C hf i).retraction = i.lift (CategoryTheory.Limits.Fork.ofι f ⋯)
• CategoryTheory.Limits.Fork.hom_comp_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g} (f✝ : s ⟶ t) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp f✝.hom (CategoryTheory.CategoryStruct.comp t.ι h) = CategoryTheory.CategoryStruct.comp s.ι h
• CategoryTheory.Limits.liftPrecomp 📋 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) (s' : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)) : s'.pt ⟶ (CategoryTheory.Limits.precompFork h s c).pt
• CategoryTheory.Limits.Fork.isoForkOfι_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.isoForkOfι.hom.hom = CategoryTheory.CategoryStruct.id c.pt
• CategoryTheory.Limits.Fork.isoForkOfι_inv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.isoForkOfι.inv.hom = CategoryTheory.CategoryStruct.id c.pt
• CategoryTheory.Limits.isEqualizerCompMono 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {c : CategoryTheory.Limits.Fork f g} (i : CategoryTheory.Limits.IsLimit c) {Z : C} (h : Y ⟶ Z) [hm : CategoryTheory.Mono h] : have this := ⋯; CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι c.ι ⋯)
• CategoryTheory.Limits.Fork.ext_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g} (i : s.pt ≅ t.pt) (w : CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι := by cat_disch) : (CategoryTheory.Limits.Fork.ext i w).hom = CategoryTheory.Limits.Fork.mkHom i.hom w
• CategoryTheory.Limits.Fork.app_one_eq_ι_comp_right_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (s : CategoryTheory.Limits.Fork f g) {Z : C} (h : (CategoryTheory.Limits.parallelPair f g).obj CategoryTheory.Limits.WalkingParallelPair.one ⟶ Z) : CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelPair.one) h = CategoryTheory.CategoryStruct.comp s.ι (CategoryTheory.CategoryStruct.comp g h)
• CategoryTheory.Limits.Fork.ext_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g} (i : s.pt ≅ t.pt) (w : CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι := by cat_disch) : (CategoryTheory.Limits.Fork.ext i w).inv = CategoryTheory.Limits.Fork.mkHom i.inv ⋯
• CategoryTheory.Limits.Fork.IsLimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g) (lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι) (uniq : ∀ (s : CategoryTheory.Limits.Fork f g) (m : s.pt ⟶ t.pt), CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = lift s) : CategoryTheory.Limits.IsLimit t
• CategoryTheory.Limits.Fork.ι_postcompose 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g f' g' : X ⟶ Y} {α : CategoryTheory.Limits.parallelPair f g ⟶ CategoryTheory.Limits.parallelPair f' g'} {c : CategoryTheory.Limits.Fork f g} : CategoryTheory.Limits.Fork.ι ((CategoryTheory.Limits.Cone.postcompose α).obj c) = CategoryTheory.CategoryStruct.comp c.ι (α.app CategoryTheory.Limits.WalkingParallelPair.zero)
• CategoryTheory.Limits.Fork.IsLimit.mk' 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g) (create : (s : CategoryTheory.Limits.Fork f g) → { l // CategoryTheory.CategoryStruct.comp l t.ι = s.ι ∧ ∀ {m : s.pt ⟶ t.pt}, CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = l }) : CategoryTheory.Limits.IsLimit t
• CategoryTheory.Limits.Fork.isLimitOfIsos 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {X' Y' : C} (c : CategoryTheory.Limits.Fork f g) (hc : CategoryTheory.Limits.IsLimit c) {f' g' : X' ⟶ Y'} (c' : CategoryTheory.Limits.Fork f' g') (e₀ : X ≅ X') (e₁ : Y ≅ Y') (e : c.pt ≅ c'.pt) (comm₁ : CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom := by cat_disch) (comm₂ : CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom := by cat_disch) (comm₃ : CategoryTheory.CategoryStruct.comp e.hom c'.ι = CategoryTheory.CategoryStruct.comp c.ι e₀.hom := by cat_disch) : CategoryTheory.Limits.IsLimit c'
• CategoryTheory.Limits.Fork.isLimitEquivOfIsos 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} (c : CategoryTheory.Limits.Fork f g) {f' g' : X' ⟶ Y'} (c' : CategoryTheory.Limits.Fork f' g') (e₀ : X ≅ X') (e₁ : Y ≅ Y') (e : c.pt ≅ c'.pt) (comm₁ : CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom := by cat_disch) (comm₂ : CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom := by cat_disch) (comm₃ : CategoryTheory.CategoryStruct.comp e.hom c'.ι = CategoryTheory.CategoryStruct.comp c.ι e₀.hom := by cat_disch) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsLimit c'
• CategoryTheory.Limits.Fork.equalizer_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (s : CategoryTheory.Limits.Fork f g) {W : C} {k l : W ⟶ s.pt} (h : CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι) (j : CategoryTheory.Limits.WalkingParallelPair) : CategoryTheory.CategoryStruct.comp k (s.π.app j) = CategoryTheory.CategoryStruct.comp l (s.π.app j)
• CategoryTheory.Limits.Fork.IsLimit.mk_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} {X Y : C} [CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g) (lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι) (uniq : ∀ (s : CategoryTheory.Limits.Fork f g) (m : s.pt ⟶ t.pt), CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = lift s) (s : CategoryTheory.Limits.Fork f g) : (CategoryTheory.Limits.Fork.IsLimit.mk t lift fac uniq).lift s = lift s
• CategoryTheory.Limits.Fork.equivOfIsos_functor_obj_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} {f' g' : X' ⟶ Y'} (e₀ : X ≅ X') (e₁ : Y ≅ Y') (comm₁ : CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom := by cat_disch) (comm₂ : CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom := by cat_disch) (c : CategoryTheory.Limits.Fork f g) : ((CategoryTheory.Limits.Fork.equivOfIsos e₀ e₁ comm₁ comm₂).functor.obj c).ι = CategoryTheory.CategoryStruct.comp c.ι e₀.hom
• CategoryTheory.Limits.Fork.equivOfIsos_inverse_obj_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C} {f' g' : X' ⟶ Y'} (e₀ : X ≅ X') (e₁ : Y ≅ Y') (comm₁ : CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom := by cat_disch) (comm₂ : CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom := by cat_disch) (c : CategoryTheory.Limits.Fork f' g') : ((CategoryTheory.Limits.Fork.equivOfIsos e₀ e₁ comm₁ comm₂).inverse.obj c).ι = CategoryTheory.CategoryStruct.comp c.ι e₀.inv
• CategoryTheory.Limits.Cone.ofFork_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} (t : CategoryTheory.Limits.Fork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)) (j : CategoryTheory.Limits.WalkingParallelPair) : (CategoryTheory.Limits.Cone.ofFork t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.Limits.Fork.IsLimit.homIso_apply_coe 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : CategoryTheory.Limits.Fork f g} (ht : CategoryTheory.Limits.IsLimit t) (Z : C) (k : Z ⟶ t.pt) : ↑((CategoryTheory.Limits.Fork.IsLimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp k t.ι
• CategoryTheory.Limits.Fork.IsLimit.homIso_symm_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : CategoryTheory.Limits.Fork f g} (ht : CategoryTheory.Limits.IsLimit t) (Z : C) (h : { h // CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g }) : (CategoryTheory.Limits.Fork.IsLimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Fork.IsLimit.lift' ht ↑h ⋯)
• CategoryTheory.Limits.Fork.IsLimit.homIso_natural 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : CategoryTheory.Limits.Fork f g} (ht : CategoryTheory.Limits.IsLimit t) {Z Z' : C} (q : Z' ⟶ Z) (k : Z ⟶ t.pt) : ↑((CategoryTheory.Limits.Fork.IsLimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp q k)) = CategoryTheory.CategoryStruct.comp q ↑((CategoryTheory.Limits.Fork.IsLimit.homIso ht Z) k)
• CategoryTheory.Limits.isoOfι 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (s : CategoryTheory.Limits.Fork f 0) : s ≅ CategoryTheory.Limits.Fork.ofι s.ι ⋯
• CategoryTheory.Preadditive.forkOfKernelFork 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.KernelFork (f - g)) : CategoryTheory.Limits.Fork f g
• CategoryTheory.Preadditive.kernelForkOfFork 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : CategoryTheory.Limits.KernelFork (f - g)
• CategoryTheory.Preadditive.isLimitKernelForkOfFork 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : CategoryTheory.Limits.Fork f g} (i : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Preadditive.kernelForkOfFork c)
• CategoryTheory.Preadditive.kernelForkOfFork_ι 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : CategoryTheory.Limits.Fork.ι (CategoryTheory.Preadditive.kernelForkOfFork c) = c.ι
• CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : CategoryTheory.Limits.KernelFork (f - g)} (i : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Fork f g) : (CategoryTheory.Preadditive.isLimitForkOfKernelFork i).lift s = i.lift (CategoryTheory.Preadditive.kernelForkOfFork s)
• CommRingCat.equalizerFork 📋 Mathlib.Algebra.Category.Ring.Constructions
  {A B : CommRingCat} (f g : A ⟶ B) : CategoryTheory.Limits.Fork f g
• CategoryTheory.Limits.Cofork.op 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Cofork f g) : CategoryTheory.Limits.Fork f.op g.op
• CategoryTheory.Limits.Fork.op 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : CategoryTheory.Limits.Cofork f.op g.op
• CategoryTheory.Limits.Cofork.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Cofork f g) : CategoryTheory.Limits.Fork f.unop g.unop
• CategoryTheory.Limits.Fork.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : CategoryTheory.Limits.Cofork f.unop g.unop
• CategoryTheory.Limits.Fork.isLimitEquivIsColimitOp 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsColimit c.op
• CategoryTheory.Limits.Fork.op_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.op.pt = Opposite.op c.pt
• CategoryTheory.Limits.Fork.isLimitEquivIsColimitUnop 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsColimit c.unop
• CategoryTheory.Limits.Fork.op_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.op.π = c.ι.op
• CategoryTheory.Limits.Fork.unop_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.unop.π = c.ι.unop
• CategoryTheory.Limits.Fork.opUnopIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.op.unop ≅ c
• CategoryTheory.Limits.Fork.unopOpIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.unop.op ≅ c
• CategoryTheory.Limits.Fork.op_unop_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.op.unop.ι = c.ι
• CategoryTheory.Limits.Fork.unop_op_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.unop.op.ι = c.ι
• CategoryTheory.Limits.Cofork.ofπOpIsoOfι 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y P : C} {f g : X ⟶ Y} (π π' : Y ⟶ P) (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π) (w' : CategoryTheory.CategoryStruct.comp π'.op f.op = CategoryTheory.CategoryStruct.comp π'.op g.op) (h : π = π') : (CategoryTheory.Limits.Cofork.ofπ π w).op ≅ CategoryTheory.Limits.Fork.ofι π'.op w'
• CategoryTheory.Limits.Cofork.ofπUnopIsoOfι 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y P : Cᵒᵖ} {f g : X ⟶ Y} (π π' : Y ⟶ P) (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π) (w' : CategoryTheory.CategoryStruct.comp π'.unop f.unop = CategoryTheory.CategoryStruct.comp π'.unop g.unop) (h : π = π') : (CategoryTheory.Limits.Cofork.ofπ π w).unop ≅ CategoryTheory.Limits.Fork.ofι π'.unop w'
• CategoryTheory.Limits.Fork.op_ι_app_one 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.op.ι.app CategoryTheory.Limits.WalkingParallelPair.one = (c.π.app CategoryTheory.Limits.WalkingParallelPair.zero).op
• CategoryTheory.Limits.Fork.op_ι_app_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.op.ι.app CategoryTheory.Limits.WalkingParallelPair.zero = (c.π.app CategoryTheory.Limits.WalkingParallelPair.one).op
• CategoryTheory.Limits.Fork.unop_ι_app_one 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.unop.ι.app CategoryTheory.Limits.WalkingParallelPair.one = (c.π.app CategoryTheory.Limits.WalkingParallelPair.zero).unop
• CategoryTheory.Limits.Fork.unop_ι_app_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) : c.unop.ι.app CategoryTheory.Limits.WalkingParallelPair.zero = (c.π.app CategoryTheory.Limits.WalkingParallelPair.one).unop
• CategoryTheory.Limits.Fork.op_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g) (X✝ : CategoryTheory.Limits.WalkingParallelPair) : c.op.ι.app X✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.parallelPairOpIso f g).hom.app X✝) (c.π.app (Opposite.unop (CategoryTheory.Limits.walkingParallelPairOp.obj X✝))).op
• CategoryTheory.Fork.IsLimit.regularMono 📋 Mathlib.CategoryTheory.Limits.Shapes.RegularMono
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : C} {p₁ p₂ : A ⟶ B} {c : CategoryTheory.Limits.Fork p₁ p₂} (h : CategoryTheory.Limits.IsLimit c) : CategoryTheory.RegularMono c.ι
• CategoryTheory.IsSplitEqualizer.asFork 📋 Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {h : W ⟶ X} (t : CategoryTheory.IsSplitEqualizer f g h) : CategoryTheory.Limits.Fork f g
• CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) : (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i).pt = i.pt
• CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) {i : CategoryTheory.Limits.Fork s t} (t₁ : CategoryTheory.Limits.IsLimit c₁) (t₂ : CategoryTheory.Limits.IsLimit c₂) (hi : CategoryTheory.Limits.IsLimit i) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i)
• CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) (x✝ : J) : (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i).π.app x✝ = CategoryTheory.CategoryStruct.comp i.ι (c₁.π.app { as := x✝ })
• CategoryTheory.NonPreadditiveAbelian.epiIsCokernelOfKernel 📋 Mathlib.CategoryTheory.Abelian.NonPreadditive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Epi f] (s : CategoryTheory.Limits.Fork f 0) (h : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ f ⋯)
• CategoryTheory.Abelian.epiIsCokernelOfKernel 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Epi f] (s : CategoryTheory.Limits.Fork f 0) (h : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ f ⋯)
• CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape) [Unique J.L] [Unique J.R] {X Y : C} (f g : X ⟶ Y) : CategoryTheory.Limits.Multifork (CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g) ≌ CategoryTheory.Limits.Fork f g
• CategoryTheory.Limits.Multifork.ofPiFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} {hd : CategoryTheory.Limits.IsLimit d} (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : CategoryTheory.Limits.Multifork I
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork 📋 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.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.Multifork I ≌ CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap
• CategoryTheory.Limits.Multifork.toPiFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (K : CategoryTheory.Limits.Multifork I) : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
• CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Functor (CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (CategoryTheory.Limits.Multifork I)
• CategoryTheory.Limits.Multifork.ofPiFork_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} {hd : CategoryTheory.Limits.IsLimit d} (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : (CategoryTheory.Limits.Multifork.ofPiFork a).pt = a.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Limits.Multifork I ≌ CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
• CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Functor (CategoryTheory.Limits.Multifork I) (CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd))
• CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : (I.ofPiForkFunctor hd).obj a = CategoryTheory.Limits.Multifork.ofPiFork a
• CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (K : CategoryTheory.Limits.Multifork I) : (I.toPiForkFunctor hc hd).obj K = CategoryTheory.Limits.Multifork.toPiFork hc hd K
• CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_functor_obj_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape) [Unique J.L] [Unique J.R] {X Y : C} (f g : X ⟶ Y) (c : CategoryTheory.Limits.Multifork (CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g)) : ((CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork J f g).functor.obj c).ι = c.ι default
• CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape) [Unique J.L] [Unique J.R] {X Y : C} (f g : X ⟶ Y) (c : CategoryTheory.Limits.Fork f g) (a : J.L) : ((CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork J f g).inverse.obj c).ι a = c.ι
• CategoryTheory.Limits.Multifork.ofPiFork_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (i : J.L) : (CategoryTheory.Limits.Multifork.ofPiFork a).ι i = CategoryTheory.CategoryStruct.comp a.ι (c.proj i)
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).inverse = I.ofPiForkFunctor hd
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).functor = I.toPiForkFunctor hc hd
• CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {K₁ K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂) : ((I.toPiForkFunctor hc hd).map f).hom = f.hom
• CategoryTheory.Limits.Multifork.ofPiFork_π_app_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (i : J.R) : (CategoryTheory.Limits.Multifork.ofPiFork a).π.app (CategoryTheory.Limits.WalkingMulticospan.right i) = CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (d.proj i))
• CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {K₁ K₂ : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)} (f : K₁ ⟶ K₂) : ((I.ofPiForkFunctor hd).map f).hom = f.hom
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_pt 📋 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.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.functor.obj K).pt = K.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt 📋 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.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.inverse.obj a).pt = a.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_map_hom 📋 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.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.functor.map f).hom = f.hom
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).unitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multifork I)).obj K).pt) ⋯) ⋯
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app 📋 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.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) (X : CategoryTheory.Limits.WalkingParallelPair) : (I.multiforkEquivPiFork.functor.obj K).π.app X = CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun t => X = t → (K.pt ⟶ (CategoryTheory.Limits.parallelPair (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))).obj X)) (fun h => ⋯ ▸ CategoryTheory.Limits.Fan.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι) (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) X ⋯
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app 📋 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.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) (x✝ : CategoryTheory.Limits.WalkingMulticospan J) : (I.multiforkEquivPiFork.inverse.obj a).π.app x✝ = match x✝ with | CategoryTheory.Limits.WalkingMulticospan.left a_1 => CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) a_1) | CategoryTheory.Limits.WalkingMulticospan.right a_1 => CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (J.fst a_1)) (I.fst a_1))
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_map_hom 📋 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.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.inverse.map f).hom = f.hom
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom 📋 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.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom 📋 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.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).counitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Fork.ext (CategoryTheory.Iso.refl (((I.ofPiForkFunctor hd).comp (I.toPiForkFunctor hc hd)).obj K).pt) ⋯) ⋯
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom 📋 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.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom 📋 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.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Comonad.beckCoalgebraFork 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : CategoryTheory.Limits.Fork (CategoryTheory.Comonad.CofreeEqualizer.topMap X) (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X)
• CategoryTheory.Comonad.beckFork 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : CategoryTheory.Limits.Fork (T.map X.a) (T.δ.app X.A)
• CategoryTheory.Comonad.beckEqualizer_lift 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) (s : CategoryTheory.Limits.Fork (T.map X.a) (T.δ.app X.A)) : (CategoryTheory.Comonad.beckEqualizer X).lift s = CategoryTheory.CategoryStruct.comp s.ι (T.ε.app X.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) (B : C) : CategoryTheory.Limits.Fork (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.PreOneHypercover.forkOfIsColimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d) (F : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.Limits.Fork (F.map (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun x => CategoryTheory.CategoryStruct.comp (E.p₁ x.snd) (c.inj x.fst.1)).op) (F.map (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun x => CategoryTheory.CategoryStruct.comp (E.p₂ x.snd) (c.inj x.fst.2)).op)
• CommRingCat.Under.equalizerFork 📋 Mathlib.Algebra.Category.Ring.Under.Limits
  {R : CommRingCat} {A B : CategoryTheory.Under R} (f g : A ⟶ B) : CategoryTheory.Limits.Fork f g
• CommRingCat.Under.equalizerFork' 📋 Mathlib.Algebra.Category.Ring.Under.Limits
  {R : CommRingCat} {A B : Type u} [CommRing A] [CommRing B] [Algebra (↑R) A] [Algebra (↑R) B] (f g : A →ₐ[↑R] B) : CategoryTheory.Limits.Fork f.toUnder g.toUnder
• CommRingCat.Under.tensorProdEqualizer 📋 Mathlib.Algebra.Category.Ring.Under.Limits
  {R S : CommRingCat} [Algebra ↑R ↑S] {A B : CategoryTheory.Under R} (f g : A ⟶ B) : CategoryTheory.Limits.Fork ((R.tensorProd S).map f) ((R.tensorProd S).map g)
• CommRingCat.Under.equalizerForkTensorProdIso 📋 Mathlib.Algebra.Category.Ring.Under.Limits
  {R S : CommRingCat} [Algebra ↑R ↑S] [Module.Flat ↑R ↑S] {A B : CategoryTheory.Under R} (f g : A ⟶ B) : CommRingCat.Under.tensorProdEqualizer f g ≅ CommRingCat.Under.equalizerFork' (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (CommRingCat.toAlgHom f)) (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (CommRingCat.toAlgHom g))
• CategoryTheory.Subfunctor.equalizer.fork 📋 Mathlib.CategoryTheory.Subfunctor.Equalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)} {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) : CategoryTheory.Limits.Fork f g
• SemiNormedGrp.fork 📋 Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
  {V W : SemiNormedGrp} (f g : V ⟶ W) : CategoryTheory.Limits.Fork f g
• CategoryTheory.Limits.weakEqualizer.fork 📋 Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y) [CategoryTheory.Limits.HasWeakEqualizer f g] : CategoryTheory.Limits.Fork f g
• CategoryTheory.Limits.Fork.IsWeakLimit.mk 📋 Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g) (lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι) : CategoryTheory.Limits.IsWeakLimit t
• CategoryTheory.Limits.Fork.IsWeakLimit.mk' 📋 Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g) (create : (s : CategoryTheory.Limits.Fork f g) → { l // CategoryTheory.CategoryStruct.comp l t.ι = s.ι }) : CategoryTheory.Limits.IsWeakLimit t
• CategoryTheory.Limits.Fork.IsWeakLimit.mk_lift 📋 Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g) (lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι) (s : CategoryTheory.Limits.Fork f g) : (CategoryTheory.Limits.Fork.IsWeakLimit.mk t lift fac).lift s = lift s
• CategoryTheory.Preadditive.isWeakLimitKernelForkOfFork 📋 Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : CategoryTheory.Limits.Fork f g} (i : CategoryTheory.Limits.IsWeakLimit c) : CategoryTheory.Limits.IsWeakLimit (CategoryTheory.Preadditive.kernelForkOfFork c)
• CategoryTheory.Preadditive.isWeakLimitForkOfKernelFork_lift 📋 Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : CategoryTheory.Limits.KernelFork (f - g)} (i : CategoryTheory.Limits.IsWeakLimit c) (s : CategoryTheory.Limits.Fork f g) : (CategoryTheory.Preadditive.isWeakLimitForkOfKernelFork i).lift s = i.lift (CategoryTheory.Preadditive.kernelForkOfFork s)
• ωCPO.HasEqualizers.equalizer 📋 Mathlib.Order.Category.OmegaCompletePartialOrder
  {X Y : ωCPO} (f g : X ⟶ Y) : CategoryTheory.Limits.Fork f g
• TopCat.Presheaf.SheafConditionEqualizerProducts.fork 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Limits.Fork (TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U) (TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes F U)
• TopCat.Presheaf.SheafConditionEqualizerProducts.fork.isoOfIso 📋 Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} {F : TopCat.Presheaf C X} {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {G : TopCat.Presheaf C X} (α : F ≅ G) : TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U ≅ (CategoryTheory.Limits.Cone.postcompose (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIso U α).inv).obj (TopCat.Presheaf.SheafConditionEqualizerProducts.fork G U)

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