homologyMap_id

Mathlib.Algebra.Homology.ShortComplex.Homology

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

English

homologyMap(id S) = id on S.homology.

Русский

homologyMap для(identity) равен(identity) на гомологии S.

LaTeX

$$$\mathrm{homologyMap}(\mathrm{id\,S}) = \mathrm{id}_{S\,\text{homology}}$$$

Lean4

@[simp]
theorem homologyMap_id [HasHomology S] : homologyMap (𝟙 S) = 𝟙 _ :=
  homologyMap'_id _

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

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

Разделы

Аффилиация

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