isColimitCoconeOfHasStrongEpiMonoFactorisation

Mathlib.CategoryTheory.Subobject.MonoOver

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoOver.isColimitCoconeOfHasStrongEpiMonoFactorisation

Lean4

/-- The cocone `coconeOfHasStrongEpiMonoFactorisation F` is a colimit -/
def isColimitCoconeOfHasStrongEpiMonoFactorisation (F : J ⥤ MonoOver Y) :
    IsColimit (coconeOfHasStrongEpiMonoFactorisation F) where
  desc
    c :=
    { left := (liftStructOfHasStrongEpiMonoFactorisation F c).l
      right := 𝟙 _
      w := by simp only [id_obj, const_obj_obj, Functor.id_map, Discrete.functor_map_id, comp_id];
        exact (liftStructOfHasStrongEpiMonoFactorisation F c).fac_right }

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

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

Разделы

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

Аффилиация

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