English
There is an equivalence between the noncomputable multiequalizer and the concrete multiequalizer, realized via a universal construction that matches left/right projections with the forgetting functor.
Русский
Существует эквивалентность между нефункциональным мультиверхним пределом и конкретным мультиверхним пределом, реализуемая через общую конструкцию, совмещающую левые/правые проекции и забывающую функтор.
LaTeX
$$$\\text{multiequalizerEquiv } I : ToType(\\mathrm{multiequalizer} I) \\simeq { x : \\forall i : J.L, ToType(I.left i) // \\forall i : J.R, I.fst i (x _) = I.snd i (x _) }$$$
Lean4
theorem multiequalizer_ext {J : MulticospanShape.{w, w'}} {I : MulticospanIndex J C} [HasMultiequalizer I]
[PreservesLimit I.multicospan (forget C)] (x y : ToType (multiequalizer I))
(h : ∀ t : J.L, Multiequalizer.ι I t x = Multiequalizer.ι I t y) : x = y :=
by
apply Concrete.limit_ext
rintro (a | b)
· apply h
· rw [← limit.w I.multicospan (WalkingMulticospan.Hom.fst b), ConcreteCategory.comp_apply,
ConcreteCategory.comp_apply]
simp [h]
