instBiproduct

Mathlib.CategoryTheory.Preadditive.Projective.Basic

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

← MathLib Explorer

English

(The same) The biproduct of projective objects P and Q is projective.

Русский

Повтор: бипродукт проективных объектов проективен.

LaTeX

$$$ \\text{Projective}(P \\;\\oplus\\; Q) $$$

Lean4

instance {β : Type v} (g : β → C) [HasZeroMorphisms C] [HasBiproduct g] [∀ b, Projective (g b)] : Projective (⨁ g) where
  factors f e epi := ⟨biproduct.desc fun b => factorThru (biproduct.ι g b ≫ f) e, by cat_disch⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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