from_zero_ext

Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

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

English

In a category with a zero object, any two arrows 0 → X are equal.

Русский

В категории с нулевым объектом любые две стрелки 0 → X равны.

LaTeX

$$$\\\\forall X\\\\, f,g : 0 \\to X,\\\\ f = g$$$

Lean4

@[ext]
theorem from_zero_ext {X : C} (f g : 0 ⟶ X) : f = g :=
  (isZero_zero C).eq_of_src _ _

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

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

Разделы

Аффилиация

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