π_of_zero

Mathlib.CategoryTheory.Limits.Shapes.Kernels

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.cokernel.π_of_zero

English

The cokernel projection of a zero morphism is an isomorphism.

Русский

Проекция котокernel нулевого морфизма является изоморфизмом.

LaTeX

$$$IsIso (cokernel.\pi (0 : X ⟶ Y))$$$

Lean4

/-- The cokernel of a zero morphism is an isomorphism -/
theorem π_of_zero : IsIso (cokernel.π (0 : X ⟶ Y)) :=
  coequalizer.π_of_self _

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

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

Разделы

Аффилиация

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