ker_comp

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Hom.ker_comp

English

For morphisms f: X → Y and g: Y → Z, the kernel of the composition f ≫ g is the image under g of the kernel of f.

Русский

Для морфизмов f: X → Y и g: Y → Z ядро композиции f ≫ g равно образу ядра f по g.

LaTeX

$$$ (f \\\\!≫ g).ker = (f.ker).map g $$$

Lean4

theorem _root_.AlgebraicGeometry.Scheme.Hom.ker_comp (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).ker = f.ker.map g :=
  (map_ker f g).symm

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

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

Разделы

Аффилиация

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