epiIsCokernelOfKernel

Mathlib.CategoryTheory.Abelian.NonPreadditive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NonPreadditiveAbelian.epiIsCokernelOfKernel

Lean4

/-- In a `NonPreadditiveAbelian` category, an epi is the cokernel of its kernel. More precisely:
If `f` is an epimorphism and `s` is some limit kernel cone on `f`, then `f` is a cokernel
of `Fork.ι s`. -/
def epiIsCokernelOfKernel [Epi f] (s : Fork f 0) (h : IsLimit s) :
    IsColimit (CokernelCofork.ofπ f (KernelFork.condition s)) :=
  IsCokernel.cokernelIso _ _
    (cokernel.ofIsoComp _ _ (Limits.IsLimit.conePointUniqueUpToIso (limit.isLimit _) h)
      (ConeMorphism.w (Limits.IsLimit.uniqueUpToIso (limit.isLimit _) h).hom _))
    (asIso <| Abelian.factorThruCoimage f) (Abelian.coimage.fac f)

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

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

Разделы

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

Аффилиация

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