zero_of_epi_comp

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

English

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

Русский

Если f эпи и f ∘ g = 0, то g = 0.

LaTeX

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

Lean4

theorem zero_of_epi_comp {X Y Z : C} (f : X ⟶ Y) {g : Y ⟶ Z} [Epi f] (h : f ≫ g = 0) : g = 0 :=
  by
  rw [← comp_zero, cancel_epi] at h
  exact h

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

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

Разделы

Аффилиация

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