isLimitConeOfForget — Mathlib

Lean4
/-- Given a functor `F : J ⥤ TopCat` and a cone `c : Cone (F ⋙ forget)`
of the underlying functor to types, the limit of `F` is `c.pt` equipped
with the infimum of the induced topologies by the maps `c.π.app j`. -/
def isLimitConeOfForget (c : Cone (F ⋙ forget)) (hc : IsLimit c) : IsLimit (coneOfConeForget c) :=
  by
  refine
    IsLimit.ofFaithful forget (ht := hc) (fun s ↦ ofHom (ContinuousMap.mk (hc.lift ((forget).mapCone s)) ?_))
      (fun _ ↦ rfl)
  rw [continuous_iff_coinduced_le]
  dsimp [topologicalSpaceConePtOfConeForget]
  rw [le_iInf_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).mapCone s) j
Похожие утверждения