English
Let c be a limit cone of a diagram F: J ⥤ TopCat. Then the topology on the cone point c.pt is the initial topology with respect to the projections c.π.app j to each F.obj j; equivalently, it is the infimum of the induced topologies from all factors.
Русский
Пусть c является предельным конусом диаграммы F: J ⥤ TopCat. Тогда топология на точке конуса c.pt равна начальной топологии относительно проекций c.π.app j к каждому F.obj j; эквивалентно, этоInf всех индуцированных топологий от факторов.
LaTeX
$$$ c.pt.str = \inf_j (F.obj j).str.induced (c.π.app j) $$$
Lean4
theorem induced_of_isLimit : c.pt.str = ⨅ j, (F.obj j).str.induced (c.π.app j) :=
by
let c' := coneOfConeForget ((forget).mapCone c)
let hc' : IsLimit c' := isLimitConeOfForget _ (isLimitOfPreserves forget hc)
let e := IsLimit.conePointUniqueUpToIso hc' hc
have he (j : J) : e.inv ≫ c'.π.app j = c.π.app j := IsLimit.conePointUniqueUpToIso_inv_comp hc' hc j
apply (homeoOfIso e.symm).induced_eq.symm.trans
dsimp [coneOfConeForget_pt, c', topologicalSpaceConePtOfConeForget]
conv_rhs => simp only [← he]
simp [← induced_compose, homeoOfIso, c']
