mono_iff_isZero_kernel

Mathlib.CategoryTheory.Preadditive.Basic

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

English

Equivalence: f is mono iff kernel f is zero, in the presence of a kernel.

Русский

Эквивалентность: f моно тогда и только тогда, когда kernel f = 0, при наличии ядра.

LaTeX

$$$\operatorname{Mono}(f) \iff \operatorname{IsZero}(\ker f)$$$

Lean4

theorem mono_iff_isZero_kernel {X Y : C} (f : X ⟶ Y) [HasKernel f] : Mono f ↔ IsZero (kernel f) :=
  mono_iff_isZero_kernel' _ (limit.isLimit _)

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

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

Разделы

Аффилиация

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