English
Same as 70699; naturality of homEquiv in the right-hand argument, expressed via composition with a map between targets.
Русский
То же, что и выше; естественность гом-эквив относительно перехода между целями через композицию с отображением.
LaTeX
$$$ h.homEquiv^{-1}\bigl(f \circ (\mathrm{const}_J).\mathrm{map} g\bigr) = h.homEquiv^{-1} f \circ g. $$$
Lean4
/-- The map of a cofan is a colimit iff the cofan consisting of the mapped morphisms is a colimit.
This essentially lets us commute `Cofan.mk` with `Functor.mapCocone`.
-/
def isColimitMapCoconeCofanMkEquiv {P : C} (g : ∀ j, f j ⟶ P) :
IsColimit (Functor.mapCocone G (Cofan.mk P g)) ≃
IsColimit (Cofan.mk _ fun j => G.map (g j) : Cofan fun j => G.obj (f j)) :=
by
refine (IsColimit.precomposeHomEquiv ?_ _).symm.trans (IsColimit.equivIsoColimit ?_)
· refine Discrete.natIso fun j => Iso.refl (G.obj (f j.as))
refine Cocones.ext (Iso.refl _) fun j => by dsimp; cases j; simp
