g_shortComplexTruncLEX₃ToTruncGE

English

The composition of the left truncation morphism with the special truncation map equals the projection πTruncGE, i.e., g_shortComplexTruncLEX₃ToTruncGE composes to πTruncGE.

Русский

Условие совместимости: композиция g с особым отображением truncation равна проекции πTruncGE.

LaTeX

$$$ (K.shortComplexTruncLE(n_0)).g \; ;\; K.shortComplexTruncLEX₃ToTruncGE(n_0,n_1,h) = K.πTruncGE(n_1) $$$

Lean4

@[reassoc]
theorem g_shortComplexTruncLEX₃ToTruncGE :
    (K.shortComplexTruncLE n₀).g ≫ K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h = K.πTruncGE n₁ := by
  apply HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE

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