rightHomologyMap_id

Mathlib.Algebra.Homology.ShortComplex.RightHomology

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

English

RightHomology maps commute with opcyclesMap under φ, i.e., rightHomologyι_naturality holds.

Русский

Отображения правой гомологии commute с opcyclesMap при φ: rightHomologyι_naturality

LaTeX

$$$rightHomologyMap\phi \circ S_2.rightHomology\iota = S_1.rightHomology\iota \circ opcyclesMap\phi$$$

Lean4

@[simp]
theorem rightHomologyMap_id [HasRightHomology S] : rightHomologyMap (𝟙 S) = 𝟙 _ :=
  rightHomologyMap'_id _

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

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

Разделы

Аффилиация

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