coconeOfCoconeForget — Mathlib

Lean4

/-- Given a functor `F : J ⥤ TopCat` and a cocone `c : Cocone (F ⋙ forget)`
of the underlying cocone of types, this is a cocone for `F` whose point is
`c.pt` with the supremum of the coinduced topologies by the maps `c.ι.app j`. -/
@[simps pt ι_app]
def coconeOfCoconeForget : Cocone F where
  pt := of (coconePtOfCoconeForget c)
  ι :=
    { app
        j :=
        ofHom
          (ContinuousMap.mk (c.ι.app j)
            (by
              rw [continuous_iff_coinduced_le]
              exact le_iSup (fun j ↦ (F.obj j).str.coinduced (c.ι.app j)) j))
      naturality j j'
        φ := by
        ext
        apply congr_fun (c.ι.naturality φ) }

Похожие утверждения