leftHomologyMap_id — Mathlib

English

The leftHomologyMap of the identity morphism is the identity on the left-homology data.

Русский

Отображение leftHomologyMap для идентичности равно тождественному отображению на данных левой гомологии.

LaTeX

$$leftHomologyMap(\mathrm{id}_S) = \mathrm{id}_{S.leftHomology}$$

Lean4

@[simp]
theorem leftHomologyMap_id [HasLeftHomology S] : leftHomologyMap (𝟙 S) = 𝟙 _ :=
  leftHomologyMap'_id _

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