instMonoMap'ComposableArrows₃OfNatNat

Mathlib.Algebra.Homology.HomologySequence

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.HomologySequence.instMonoMap'ComposableArrows₃OfNatNat

English

The single C c i construction preserves finite colimits.

Русский

Конструкция одиночного объекта C c i сохраняет конечные колимиты.

LaTeX

$$$\operatorname{PreservesFiniteColimits}(\mathrm{single}\,C\,c\,i)$$$

Lean4

instance [K.HasHomology i] [K.HasHomology j] : Mono ((composableArrows₃ K i j).map' 0 1) :=
  by
  dsimp
  infer_instance

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

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

Разделы

Аффилиация

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