truncLE'Map_id

Mathlib.Algebra.Homology.Embedding.TruncLE

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.truncLE'Map_id

English

The truncLEMap of the identity morphism is the identity on K.truncLE e.

Русский

TruncLEMap от единицы равен тождественному отображению на K.truncLE e.

LaTeX

$$$\mathrm{truncLEMap}(\mathrm{Id}_K, e) = \mathrm{Id}_{K,\mathrm{truncLE} e}$$$

Lean4

@[simp]
theorem truncLE'Map_id : truncLE'Map (𝟙 K) e = 𝟙 _ :=
  (unopFunctor C c.symm).congr_map (congr_arg Quiver.Hom.op (K.op.truncGE'Map_id e.op))

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

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

Разделы

Аффилиация

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