stupidTruncMap_id — Mathlib

English

The map induced by a trivial morphism is the identity on the truncated complex.

Русский

Отображение, порождаемое тождественным морфизмом, есть тождественное на усеченном комплексе.

LaTeX

$$$stupidTruncMap(\mathrm{id}_K, e) = \mathrm{id}_{K.\mathrm{stupidTrunc}(e)}$$$

Lean4

@[simp]
theorem stupidTruncMap_id : stupidTruncMap (𝟙 K) e = 𝟙 _ := by simp [stupidTruncMap, stupidTrunc]

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