conePoint

Mathlib.CategoryTheory.Monad.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Monad.ForgetCreatesLimits.conePoint

Lean4

/-- The algebra structure which will be the apex of the new limit cone for `D`. -/
@[simps]
def conePoint : Algebra T where
  A := c.pt
  a := t.lift (newCone D c)
  unit :=
    t.hom_ext fun j =>
      by
      rw [Category.assoc, t.fac, newCone_π_app, ← T.η.naturality_assoc, Functor.id_map, (D.obj j).unit]
      simp
  assoc :=
    t.hom_ext fun j =>
      by
      rw [Category.assoc, Category.assoc, t.fac (newCone D c), newCone_π_app, ← Functor.map_comp_assoc,
        t.fac (newCone D c), newCone_π_app, ← T.μ.naturality_assoc, (D.obj j).assoc, Functor.map_comp, Category.assoc]
      rfl

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

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

Разделы

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

Аффилиация

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