English
For a fork t with legs f,g and a limit ht, there is a natural isomorphism homIso ht Z between morphisms Z → t.pt and pairs h:Z → X with h ≫ f = h ≫ g; this gives the standard bijection in a natural way.
Русский
Для расслоения (fork) t с ножками f,g и предельного ht существует естественное изоморфное отображение homIso ht Z между морфизмами Z → t.pt и парами h: Z → X с условием h ≫ f = h ≫ g.
LaTeX
$$$(Z \to t.pt) \cong \{ h: Z \to X \mid h \;\circ\; f = h \circ g \}.$$$
Lean4
/-- Given a limit cone for the pair `f g : X ⟶ Y`, for any `Z`, morphisms from `Z` to its point are in
bijection with morphisms `h : Z ⟶ X` such that `h ≫ f = h ≫ g`.
Further, this bijection is natural in `Z`: see `Fork.IsLimit.homIso_natural`.
This is a special case of `IsLimit.homIso'`, often useful to construct adjunctions.
-/
@[simps]
def homIso {X Y : C} {f g : X ⟶ Y} {t : Fork f g} (ht : IsLimit t) (Z : C) : (Z ⟶ t.pt) ≃ { h : Z ⟶ X // h ≫ f = h ≫ g }
where
toFun k := ⟨k ≫ t.ι, by simp only [Category.assoc, t.condition]⟩
invFun h := (Fork.IsLimit.lift' ht _ h.prop).1
left_inv _ := Fork.IsLimit.hom_ext ht (Fork.IsLimit.lift' _ _ _).prop
right_inv _ := Subtype.ext (Fork.IsLimit.lift' ht _ _).prop
