spanCone

Mathlib.Topology.Category.Profinite.Nobeling.Basic

URI: https://scilib.ai/kg/mathlib#Profinite.NobelingProof.spanCone

Lean4

/-- The limit cone on `spanFunctor` with point `C`. -/
noncomputable def spanCone [∀ (s : Finset I) (i : I), Decidable (i ∈ s)] (hC : IsCompact C) : Cone (spanFunctor hC)
    where
  pt := @Profinite.of C _ (by rwa [← isCompact_iff_compactSpace]) _ _
  π :=
    { app := fun s ↦ TopCat.ofHom ⟨ProjRestrict C (· ∈ unop s), continuous_projRestrict _ _⟩
      naturality := by
        intro X Y h
        simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp,
          ← projRestricts_comp_projRestrict C (leOfHom h.unop)]
        rfl }

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

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

Разделы

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

Аффилиация

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