opcyclesMap'_id

Mathlib.Algebra.Homology.ShortComplex.RightHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.opcyclesMap'_id

English

The map opcyclesMap' evaluated at the identity on S is the identity on the Q-component of the right-homology data.

Русский

opcyclesMap'(id_S) h h = id на компоненте Q правая гомология

LaTeX

$$opcyclesMap'(id_S) h h = id$$

Lean4

@[simp]
theorem opcyclesMap'_id (h : S.RightHomologyData) : opcyclesMap' (𝟙 S) h h = 𝟙 _ :=
  (RightHomologyMapData.id h).opcyclesMap'_eq

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

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

Разделы

Аффилиация

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