map_id — Mathlib

English

Map of the identity on the bicomplex yields the identity on the total complex.

Русский

Отображение от идентичности на би-комплексе даёт идентичность на суммарном комплексе.

LaTeX

$$$\\mathrm{map}(\\mathrm{id}_K) c_{12} = \\mathrm{id}_{K.total c_{12}}$$$

Lean4

@[simp]
theorem map_id : map (𝟙 K) c₁₂ = 𝟙 _ :=
  by
  apply (HomologicalComplex.forget _ _).map_injective
  apply GradedObject.mapMap_id

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