English
There is a canonical isomorphism between maps t.pt → Z and compatible morphisms Y → Z given by the cofงork IsColimit structure; the isomorphism is functorial in Z.
Русский
Существует каноническое изоморфное отображение между отображениями t.pt → Z и допустимыми морфизмами Y → Z, задаваемыми структурой IsColimit Cofork; изоморфизм функториально зависит от Z.
LaTeX
$$$\mathrm{Cofork.IsColimit.homIso}\ ht\ Z: (t.pt \to Z) \cong \{ h: Y \to Z \mid f \circ h = g \circ h \}.$$$
Lean4
/-- Given a colimit cocone for the pair `f g : X ⟶ Y`, for any `Z`, morphisms from the cocone point
to `Z` are in bijection with morphisms `h : Y ⟶ Z` such that `f ≫ h = g ≫ h`.
Further, this bijection is natural in `Z`: see `Cofork.IsColimit.homIso_natural`.
This is a special case of `IsColimit.homIso'`, often useful to construct adjunctions.
-/
@[simps]
def homIso {X Y : C} {f g : X ⟶ Y} {t : Cofork f g} (ht : IsColimit t) (Z : C) :
(t.pt ⟶ Z) ≃ { h : Y ⟶ Z // f ≫ h = g ≫ h }
where
toFun k := ⟨t.π ≫ k, by simp only [← Category.assoc, t.condition]⟩
invFun h := (Cofork.IsColimit.desc' ht _ h.prop).1
left_inv _ := Cofork.IsColimit.hom_ext ht (Cofork.IsColimit.desc' _ _ _).prop
right_inv _ := Subtype.ext (Cofork.IsColimit.desc' ht _ _).prop
