projective_over

Mathlib.CategoryTheory.Preadditive.Projective.Basic

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

English

If C has EnoughProjectives, then for any object X, the over category over X is projective.

Русский

Если в категории C есть достаточно проективных, то категория over X проективна для любого X.

LaTeX

$$$ \\text{EnoughProjectives } C \\Rightarrow \\text{Projective over } X $$$

Lean4

instance projective_over (X : C) : Projective (over X) :=
  (EnoughProjectives.presentation X).some.projective

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

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

Разделы

Аффилиация

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