toSSetIsoConst

Mathlib.AlgebraicTopology.SingularSet

URI: https://scilib.ai/kg/mathlib#TopCat.toSSetIsoConst

Lean4

/-- The singular simplicial set of a totally disconnected space is the constant simplicial set. -/
noncomputable def toSSetIsoConst (X : TopCat.{u}) [TotallyDisconnectedSpace X] :
    TopCat.toSSet.obj X ≅ (Functor.const _).obj X :=
  (NatIso.ofComponents
      (fun n ↦
        Equiv.toIso
          ((TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace _ X).symm.trans
            (X.toSSetObjEquiv n).symm))).symm

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

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

Разделы

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

Аффилиация

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