cone

Mathlib.Topology.Category.Profinite.Extend

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

Lean4

/-- Given a functor `G` from `Profinite` and `S : Profinite`, we obtain a cone on
`(StructuredArrow.proj S toProfinite ⋙ toProfinite ⋙ G)` with cone point `G.obj S`.

Whiskering this cone with `Profinite.Extend.functor c` gives `G.mapCone c` as we check in the
example below.
-/
@[simps]
def cone (S : Profinite) : Cone (StructuredArrow.proj S toProfinite ⋙ toProfinite ⋙ G)
    where
  pt := G.obj S
  π :=
    { app := fun i ↦ G.map i.hom
      naturality := fun _ _ f ↦ (by simp [← map_comp]) }

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

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

Разделы

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

Аффилиация

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