image_le_kernel

Mathlib.Algebra.Homology.ImageToKernel

URI: https://scilib.ai/kg/mathlib#image_le_kernel

English

The morphism imageToKernel f g w is mono for any f, g with w: f ≫ g = 0.

Русский

Гомоморфизм imageToKernel f g w является монотоморфизмом при любых f, g с w: f ∘ g = 0.

LaTeX

$$Mono (imageToKernel f g w)$$

Lean4

theorem image_le_kernel (w : f ≫ g = 0) : imageSubobject f ≤ kernelSubobject g :=
  imageSubobject_le_mk _ _ (kernel.lift _ _ w) (by simp)

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

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

Разделы

Аффилиация

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