ιTruncLE_naturality — Mathlib

English

The inclusion maps are natural with respect to morphisms: the truncLE inclusion commutes with the induced truncLE map.

Русский

Включающие отображения естественны по отношению к морфизмам: диаграмма включения truncLE и индуцированного morphism совпадает по направлению композиции.

LaTeX

$$$\mathrm{truncLEMap}_n(\varphi) \circ L_{\le n} = K_{\le n} \circ \varphi$$$

Lean4

@[reassoc (attr := simp)]
theorem ιTruncLE_naturality (n : ℤ) : truncLEMap φ n ≫ L.ιTruncLE n = K.ιTruncLE n ≫ φ := by
  apply HomologicalComplex.ιTruncLE_naturality

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