coneOfConeForget — Mathlib

Lean4
/-- Given a functor `F : J ⥤ TopCat` and a cone `c : Cone (F ⋙ forget)`
of the underlying functor to types, this is a cone for `F` whose point is
`c.pt` with the infimum of the induced topologies by the maps `c.π.app j`. -/
@[simps pt π_app]
def coneOfConeForget : Cone F where
  pt := of (conePtOfConeForget c)
  π :=
    { app
        j :=
        ofHom
          (ContinuousMap.mk (c.π.app j)
            (by
              rw [continuous_iff_le_induced]
              exact iInf_le (fun j ↦ (F.obj j).str.induced (c.π.app j)) j))
      naturality j j'
        φ := by
        ext
        apply congr_fun (c.π.naturality φ) }
Похожие утверждения