zero_of_comp_mono

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.zero_of_comp_mono

English

If g is mono and f ≫ g = 0, then f = 0.

Русский

Если g моно, и f ∘ g = 0, то f = 0.

LaTeX

$$$\\text{Mono}(g) \\Rightarrow (f \\circ g = 0) \\Rightarrow f = 0$$$

Lean4

theorem zero_of_comp_mono {X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) [Mono g] (h : f ≫ g = 0) : f = 0 :=
  by
  rw [← zero_comp, cancel_mono] at h
  exact h

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

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

Разделы

Аффилиация

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