effectiveEpiStructOfRegularEpi

Mathlib.CategoryTheory.EffectiveEpi.RegularEpi

URI: https://scilib.ai/kg/mathlib#CategoryTheory.effectiveEpiStructOfRegularEpi

Lean4

/-- The data of an `EffectiveEpi` structure on a `RegularEpi`. -/
def effectiveEpiStructOfRegularEpi {B X : C} (f : X ⟶ B) [RegularEpi f] : EffectiveEpiStruct f
    where
  desc _ h := Cofork.IsColimit.desc isColimit _ (h _ _ w)
  fac _ _ := Cofork.IsColimit.π_desc' isColimit _ _
  uniq _ _ _ hg := Cofork.IsColimit.hom_ext isColimit (hg.trans (Cofork.IsColimit.π_desc' _ _ _).symm)

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

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

Разделы

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

Аффилиация

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