map_id — Mathlib

English

The map on homology with identity data is the identity: map (Id_G) (id_A) n = id on H_n(G,A).

Русский

Отображение на гомологию с тождественными данными равно тождественности: map(Id_G)(id_A)(n) = id_{H_n(G,A)}.

LaTeX

$$$\mathrm{map}(\mathrm{Id}_G, \mathrm{id}_A, n) = \mathrm{id}_{\mathrm{H}_n(G,A)}$$$

Lean4

@[simp]
theorem map_id : map (MonoidHom.id G) (𝟙 A) n = 𝟙 _ := by simp [map, groupHomology]

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