instIsClosedUnderQuotientsIsZeroOfHasZeroMorphisms

Mathlib.CategoryTheory.ObjectProperty.EpiMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsIsZeroOfHasZeroMorphisms

English

With zero morphisms, IsZero is closed under quotients.

Русский

С нулевыми морфизмами IsZero замкнуто по quotient.

LaTeX

$$$\forall C [\mathbf{Category}(C)], [\mathbf{HasZeroMorphisms} C] \Rightarrow \mathrm{IsClosedUnderQuotients}(\mathrm{IsZero}(C)).$$$

Lean4

instance [HasZeroMorphisms C] : IsClosedUnderQuotients (IsZero (C := C)) where prop_of_epi f _ hX := IsZero.of_epi f hX

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

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

Разделы

Аффилиация

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