forgetMapConeLimitConeIso

Mathlib.CategoryTheory.Monoidal.Internal.Limits

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

Lean4

/-- The image of the proposed limit cone for `F : J ⥤ Mon C` under the forgetful functor
`forget C : Mon C ⥤ C` is isomorphic to the limit cone of `F ⋙ forget C`.
-/
def forgetMapConeLimitConeIso (F : J ⥤ Mon C) : (forget C).mapCone (limitCone F) ≅ limit.cone (F ⋙ forget C) :=
  Cones.ext (Iso.refl _) (by simp)

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

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

Разделы

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

Аффилиация

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