cokernel_zero_of_nonzero_to_simple

Mathlib.CategoryTheory.Simple

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

Lean4

theorem cokernel_zero_of_nonzero_to_simple {X Y : C} [Simple Y] {f : X ⟶ Y} (w : f ≠ 0) : cokernel.π f = 0 := by
  classical
  by_contra h
  haveI := isIso_of_epi_of_nonzero h
  exact w (eq_zero_of_mono_cokernel f)

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

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

Разделы

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

Аффилиация

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