instHasColimitDiscreteWalkingPairCompPairEval

Mathlib.Algebra.Homology.HomologicalComplexBiprod

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.instHasColimitDiscreteWalkingPairCompPairEval

← MathLib Explorer

English

The colimit exists for the evaluation diagram at each index.

Русский

Существует колимит для диаграммы оценки на каждом индексе.

LaTeX

$$$\\text{HasColimit}((\\mathrm{pair}\\; K\\; L) \\cdot (\\mathrm{eval}\\; C\\; c\\; i))$$$

Lean4

instance (i : ι) : HasColimit ((pair K L) ⋙ (eval C c i)) :=
  by
  have e : _ ≅ pair (K.X i) (L.X i) := diagramIsoPair (pair K L ⋙ eval C c i)
  exact hasColimit_of_iso e

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

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

Разделы

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

Аффилиация

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