cokernelIso

Mathlib.CategoryTheory.Limits.Shapes.Kernels

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.IsCokernel.cokernelIso

Lean4

/-- If `s` is any colimit cokernel cocone over `f` and `i` is an isomorphism such that
`s.π ≫ i.hom = l`, then `l` is a cokernel of `f`. -/
def cokernelIso {Z : C} (l : Y ⟶ Z) {s : CokernelCofork f} (hs : IsColimit s) (i : s.pt ≅ Z)
    (h : Cofork.π s ≫ i.hom = l) : IsColimit (CokernelCofork.ofπ l <| show f ≫ l = 0 by simp [← h]) :=
  IsColimit.ofIsoColimit hs <|
    Cocones.ext i fun j => by
      cases j
      · dsimp; rw [← h]; simp
      · exact h

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

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

Разделы

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

Аффилиация

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