instEpi

Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

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

English

In any category with a zero object, every morphism X → 0 is an epimorphism.

Русский

В любой категории с нулевым объектом каждый морфизм X → 0 является эпиморфизмом.

LaTeX

$$$\\\\forall X, \\\\text{the unique } f: X \to 0 \\\\text{ is an epi}$$$

Lean4

instance {X : C} (f : X ⟶ 0) : Epi f where left_cancellation g h _ := by ext

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

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

Разделы

Аффилиация

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