epi_of_isZero_cokernel

Mathlib.CategoryTheory.Preadditive.Basic

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

← MathLib Explorer

English

Same as above; another form of the lemma expressing epi from zero cokernel'

Русский

То же самое; другая форма леммы: эпиморфизм из нулевого cokernel'

LaTeX

$$$\operatorname{Epi}(f) $ через $\operatorname{IsZero}(\operatorname{cokernel}(f))$$$

Lean4

theorem epi_of_isZero_cokernel {X Y : C} (f : X ⟶ Y) [HasCokernel f] (h : IsZero (cokernel f)) : Epi f :=
  epi_of_isZero_cokernel' _ (cokernelIsCokernel _) h

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

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

Разделы

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

Аффилиация

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