lanPresheafIso_hom

Mathlib.Condensed.Discrete.Colimit

URI: https://scilib.ai/kg/mathlib#Condensed.lanPresheafIso_hom

Lean4

@[simp]
theorem lanPresheafIso_hom (hF : IsColimit <| F.mapCocone S.asLimitCone.op) :
    (lanPresheafIso hF).hom = colimit.desc _ (Profinite.Extend.cocone _ _) :=
  by
  simp [lanPresheafIso, Final.colimitIso]
  rfl

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

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

Разделы

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

Аффилиация

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