epi_of_cokernel_zero

Mathlib.CategoryTheory.Preadditive.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Preadditive.epi_of_cokernel_zero

← MathLib Explorer

English

If the cokernel of f is zero, then f is epi.

Русский

Если кофактор f равен нулю, то f эпиморфизм.

LaTeX

$$$\operatorname{cokernel}(f) = 0 \Rightarrow \operatorname{Epi}(f)$$$

Lean4

theorem epi_of_cokernel_zero {X Y : C} {f : X ⟶ Y} [HasColimit (parallelPair f 0)] (w : cokernel.π f = 0) : Epi f :=
  epi_of_cancel_zero f fun g h => by rw [← cokernel.π_desc f g h, w, Limits.zero_comp]

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

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

Разделы

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

Аффилиация

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