coconeOfHasStrongEpiMonoFactorisation

Mathlib.CategoryTheory.Subobject.MonoOver

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

Lean4

/-- If a category `C` has strong epi-mono factorization, for any `Y : C` and functor
`F : J ⥤ MonoOver Y`, there is a cocone under F. -/
def coconeOfHasStrongEpiMonoFactorisation (F : J ⥤ MonoOver Y) : Cocone F
    where
  pt :=
    { obj := .mk <| (strongEpiMonoFactorisationSigmaDesc F).m
      property := (strongEpiMonoFactorisationSigmaDesc F).m_mono }
  ι :=
    {
      app
        j :=
        { left := Sigma.ι (fun i ↦ (F.obj i : C)) j ≫ (strongEpiMonoFactorisationSigmaDesc F).e
          right := 𝟙 _ } }

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

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

Разделы

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

Аффилиация

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