limitCone

Mathlib.CategoryTheory.Monoidal.Internal.Limits

URI: https://scilib.ai/kg/mathlib#Mon.limitCone

Lean4

/-- Implementation of `Mon.hasLimits`: a limiting cone over a functor `F : J ⥤ Mon C`.
-/
@[simps]
def limitCone (F : J ⥤ Mon C) : Cone F where
  pt := limit F
  π :=
    { app := fun j => .mk' (limit.π (F ⋙ Mon.forget C) j)
      naturality := fun j j' f => by ext; exact (limit.cone (F ⋙ Mon.forget C)).π.naturality f }

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

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

Разделы

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

Аффилиация

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