coe_mapCycles₂

Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

URI: https://scilib.ai/kg/mathlib#groupHomology.coe_mapCycles₂

English

The map on H2 induced by the identity is the identity on H2.

Русский

Отображение на H2, индуцированное тождеством, есть тождество на H2.

LaTeX

$$$ mapShortComplexH2(\mathrm{id}_G)(\mathrm{Id}_{A}) = \mathrm{Id}_{shortComplexH2(A)} $$$

Lean4

@[simp]
theorem coe_mapCycles₂ (x) : (mapCycles₂ f φ x).1 = chainsMap₂ f φ x :=
  rfl

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

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

Разделы

Аффилиация

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