hasColimit_of_hasColimitπ

Mathlib.Algebra.Homology.ShortComplex.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.hasColimit_of_hasColimitπ

English

If F : J ⥤ ShortComplex C has colimits after composing with π₁, π₂, π₃, then F has a colimit.

Русский

Пусть F : J ⥤ ShortComplex C имеет колимиты после композиции с π₁, π₂, π₃; тогда F имеет колимит.

LaTeX

$$$ \text{HasColimit } F $$$

Lean4

instance hasColimit_of_hasColimitπ : HasColimit F :=
  ⟨⟨⟨_, isColimitColimitCocone _⟩⟩⟩

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

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

Разделы

Аффилиация

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