limitConeIsLimit

Mathlib.Topology.Category.Profinite.Basic

URI: https://scilib.ai/kg/mathlib#Profinite.limitConeIsLimit

Lean4

/-- The limit cone `Profinite.limitCone F` is indeed a limit cone. -/
def limitConeIsLimit {J : Type v} [SmallCategory J] (F : J ⥤ Profinite.{max u v}) : Limits.IsLimit (limitCone F)
    where
  lift S := (CompHaus.limitConeIsLimit.{v, u} (F ⋙ profiniteToCompHaus)).lift (profiniteToCompHaus.mapCone S)
  uniq S _ h := (CompHaus.limitConeIsLimit.{v, u} _).uniq (profiniteToCompHaus.mapCone S) _ h

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

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

Разделы

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

Аффилиация

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