rightHomologyMap'_id

Mathlib.Algebra.Homology.ShortComplex.RightHomology

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

← MathLib Explorer

English

The map rightHomologyMap' evaluated at the identity on S is the identity on the right-homology data.

Русский

Отображение rightHomologyMap' в отношении единицы на S даёт единицу на правой гомологии.

LaTeX

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

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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