toTopCat

Mathlib.Condensed.Light.TopCatAdjunction

URI: https://scilib.ai/kg/mathlib#LightCondSet.toTopCat

Lean4

/-- The object part of the functor `LightCondSet ⥤ TopCat` -/
abbrev toTopCat : TopCat.{u} :=
  TopCat.of (X.val.obj ⟨LightProfinite.of PUnit⟩)

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

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

Разделы

Аффилиация

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