truncGEMap_comp

Mathlib.Algebra.Homology.Embedding.TruncGE

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

English

The truncGEMap respects composition in the ambient category.

Русский

TruncGEMap сохраняет композицию в окружающей категории.

LaTeX

$$$truncGEMap(\phi \;\phi', e) = truncGEMap(\phi,e) \circ truncGEMap(\phi',e)$$$

Lean4

@[reassoc, simp]
theorem truncGEMap_comp : truncGEMap (φ ≫ φ') e = truncGEMap φ e ≫ truncGEMap φ' e := by simp [truncGEMap, truncGE]

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

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

Разделы

Аффилиация

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