toTopCatMap

Mathlib.Condensed.TopCatAdjunction

URI: https://scilib.ai/kg/mathlib#CondensedSet.toTopCatMap

Lean4

/-- The map part of the functor `CondensedSet ⥤ TopCat` -/
@[simps!]
def toTopCatMap : X.toTopCat ⟶ Y.toTopCat :=
  TopCat.ofHom
    { toFun := f.val.app ⟨of PUnit⟩
      continuous_toFun := by
        rw [continuous_coinduced_dom]
        apply continuous_sigma
        intro ⟨S, x⟩
        simp only [Function.comp_apply, coinducingCoprod]
        rw [show (fun (a : S) ↦ f.val.app ⟨of PUnit⟩ (X.val.map ((of PUnit.{u + 1}).const a).op x)) = _ from
            funext fun a ↦ NatTrans.naturality_apply f.val ((of PUnit.{u + 1}).const a).op x]
        exact continuous_coinducingCoprod Y _ }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru