forgetCreatesColimit

Mathlib.CategoryTheory.Monad.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Comonad.forgetCreatesColimit

Lean4

/-- The forgetful functor from the Eilenberg-Moore category creates colimits. -/
noncomputable instance forgetCreatesColimit : CreatesColimitsOfSize (forget T) where
  CreatesColimitsOfShape :=
    {
      CreatesColimit := fun {D} =>
        createsColimitOfReflectsIso fun c t =>
          { liftedCocone := ForgetCreatesColimits'.liftedCocone D c t
            validLift := Cocones.ext (Iso.refl _) fun _ => (comp_id _)
            makesColimit := ForgetCreatesColimits'.liftedCoconeIsColimit _ _ _ } }

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

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

Разделы

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

Аффилиация

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