English
If c is a colimit cocone of F, then the topology on c.pt is the supremum of the coinduced topologies from each F.obj j via c.ι.app j.
Русский
Если c является колимитным коконом диаграммы F, то топология на точке кокона равна наибольшей (супремуму) из коиндуцированных топологий по каждому F.obj j через c.ι.app j.
LaTeX
$$$ c.pt.str = \bigvee_j (F.obj j).str.coinduced (c.ι.app j) $$$
Lean4
theorem coinduced_of_isColimit : c.pt.str = ⨆ j, (F.obj j).str.coinduced (c.ι.app j) :=
by
let c' := coconeOfCoconeForget ((forget).mapCocone c)
let hc' : IsColimit c' := isColimitCoconeOfForget _ (isColimitOfPreserves forget hc)
let e := IsColimit.coconePointUniqueUpToIso hc' hc
have he (j : J) : c'.ι.app j ≫ e.hom = c.ι.app j := IsColimit.comp_coconePointUniqueUpToIso_hom hc' hc j
apply (homeoOfIso e).coinduced_eq.symm.trans
dsimp [coconeOfCoconeForget_pt, c', topologicalSpaceCoconePtOfCoconeForget]
simp only [coinduced_iSup]
conv_rhs => simp only [← he]
rfl
