English
In a concrete category with a multiequalizer, two elements are equal if their images under all injectors ι I t are equal.
Русский
В конкретной категории с мультиверхним пределом два элемента равны, если их образы под всеми инъекторами ι I t равны.
LaTeX
$$$\\forall t : J.L, Multiequalizer.ι I t x = Multiequalizer.ι I t y \\Rightarrow x=y$$$
Lean4
/-- An auxiliary equivalence to be used in `multiequalizerEquiv` below. -/
def multiequalizerEquivAux {J : MulticospanShape.{w, w'}} (I : MulticospanIndex J C) :
(I.multicospan ⋙ forget C).sections ≃
{ x : ∀ i : J.L, ToType (I.left i) // ∀ i : J.R, I.fst i (x _) = I.snd i (x _) }
where
toFun
x :=
⟨fun _ => x.1 (WalkingMulticospan.left _), fun i =>
by
have a := x.2 (WalkingMulticospan.Hom.fst i)
have b := x.2 (WalkingMulticospan.Hom.snd i)
rw [← b] at a
exact a⟩
invFun
x :=
{ val := fun j =>
match j with
| WalkingMulticospan.left _ => x.1 _
| WalkingMulticospan.right b => I.fst b (x.1 _)
property := by
rintro (a | b) (a' | b') (f | f | f)
· simp
· rfl
· dsimp
exact (x.2 b').symm
· simp }
left_inv := by
intro x; ext (a | b)
· rfl
· rw [← x.2 (WalkingMulticospan.Hom.fst b)]
rfl
right_inv := by
intro x
ext i
rfl
