isColimitCoconeOfForget — Mathlib

Lean4
/-- Given a functor `F : J ⥤ TopCat` and a cocone `c : Cocone (F ⋙ forget)`
of the underlying cocone of types, the colimit of `F` is `c.pt` equipped
with the supremum of the coinduced topologies by the maps `c.ι.app j`. -/
def isColimitCoconeOfForget (c : Cocone (F ⋙ forget)) (hc : IsColimit c) : IsColimit (coconeOfCoconeForget c) :=
  by
  refine
    IsColimit.ofFaithful forget (ht := hc) (fun s ↦ ofHom (ContinuousMap.mk (hc.desc ((forget).mapCocone s)) ?_))
      (fun _ ↦ rfl)
  rw [continuous_iff_le_induced]
  dsimp [topologicalSpaceCoconePtOfCoconeForget]
  rw [iSup_le_iff]
  intro j
  rw [coinduced_le_iff_le_induced, induced_compose]
  convert continuous_iff_le_induced.1 (s.ι.app j).hom.continuous
  exact hc.fac ((forget).mapCocone s) j
Похожие утверждения