πTruncGE_naturality — Mathlib

English

The projection maps are natural with respect to morphisms: the canonical map to the truncGE commutes with truncGE maps.

Русский

Проекции естественны по отношению к морфизмам: каноническое отображение к усечению ≥ n коммутирует с truncGEMap.

LaTeX

$$$K.\pi_{\ge n} \circ \mathrm{truncGEMap}_n(\varphi) = \varphi \circ L.\pi_{\ge n}$$$

Lean4

@[reassoc (attr := simp)]
theorem πTruncGE_naturality (n : ℤ) : K.πTruncGE n ≫ truncGEMap φ n = φ ≫ L.πTruncGE n := by
  apply HomologicalComplex.πTruncGE_naturality

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