English
If f: X → Y, g,h : Y → Z and w: f ≫ g = f ≫ h, then Nonempty IsLimit (Fork.ofι f w) implies ∀ y, g y = h y → ∃! x : X, f x = y.
Русский
Если f: X → Y, g,h : Y → Z и w: f ≫ g = f ≫ h, то непустой предел (Fork.ofι f w) означает: ∀ y, g y = h y → ∃! x: X, f x = y.
LaTeX
$$$$ \\forall X,Y,Z\\; (f:X\\to Y)\\; (g,h:Y\\to Z)\\; (w:f\\to g=f\\to h)\\; \\Rightarrow \\text{IsLimit Fork.ofι f w} $$$$
Lean4
/-- The converse of `type_equalizer_of_unique`. -/
theorem unique_of_type_equalizer (t : IsLimit (Fork.ofι _ w)) (y : Y) (hy : g y = h y) : ∃! x : X, f x = y :=
by
let y' : PUnit ⟶ Y := fun _ => y
have hy' : y' ≫ g = y' ≫ h := funext fun _ => hy
refine ⟨(Fork.IsLimit.lift' t _ hy').1 ⟨⟩, congr_fun (Fork.IsLimit.lift' t y' _).2 ⟨⟩, ?_⟩
intro x' hx'
suffices (fun _ : PUnit => x') = (Fork.IsLimit.lift' t y' hy').1 by rw [← this]
apply Fork.IsLimit.hom_ext t
funext ⟨⟩
apply hx'.trans (congr_fun (Fork.IsLimit.lift' t _ hy').2 ⟨⟩).symm
