zero_projective

Mathlib.CategoryTheory.Preadditive.Projective.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Projective.zero_projective

English

If a category has a zero object, the zero object is projective.

Русский

Если в категории существует нулевой объект, то нулевой объект проективен.

LaTeX

$$$ 0 \\text{ is projective. } $$$

Lean4

instance zero_projective [HasZeroObject C] : Projective (0 : C) :=
  (isZero_zero C).projective

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

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

Разделы

Аффилиация

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