functor

Mathlib.Topology.Category.Profinite.Extend

URI: https://scilib.ai/kg/mathlib#Profinite.Extend.functor

Lean4

/-- Given a cone in `Profinite`, consisting of finite sets and indexed by a cofiltered category,
we obtain a functor from the indexing category to `StructuredArrow c.pt toProfinite`.
-/
@[simps]
def functor : I ⥤ StructuredArrow c.pt toProfinite
    where
  obj i := StructuredArrow.mk (c.π.app i)
  map
    f :=
    StructuredArrow.homMk (F.map f)
      (c.w f)
        -- We check that the original diagram factors through `Profinite.Extend.functor`.

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

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

Разделы

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

Аффилиация

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