truncLEMap_id

Mathlib.Algebra.Homology.Embedding.TruncLE

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.truncLEMap_id

English

For any j, if e.f j = j', then QuasiIsoAt (K.πTruncGE e) j'.

Русский

Для любого j, если e.f j = j', то QuasiIsoAt(K.πTruncGE e) j'.

LaTeX

$$$\forall j, j',\; (e.f j = j') \Rightarrow \text{QuasiIsoAt}\bigl(K.\pi_{\mathrm{TruncGE}}(e), j'\bigr)$$$

Lean4

@[simp]
theorem truncLEMap_id : truncLEMap (𝟙 K) e = 𝟙 _ :=
  (unopFunctor C c'.symm).congr_map (congr_arg Quiver.Hom.op (K.op.truncGEMap_id e.op))

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

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

Разделы

Аффилиация

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