isZero_extend_X' — Mathlib

English

Let K, L, M be homological complexes over a category with a zero object. For any embedding e and index i' with e.r i' = none, the X-component of K extended by e at i' is a zero object.

Русский

Пусть K, L, M — гомологические комплексы в имеющей нуль-объект категории. При любом вложении e и индексе i' с e.r i' = none компонент X в K, расширенном по e, в позиции i' является нулевым объектом.

LaTeX

$$$e\\,r\\,i' = \\mathrm{none} \\Rightarrow (K\\extend e)\\,X\\,i' \\cong 0$$$

Lean4

theorem isZero_extend_X' (i' : ι') (hi' : e.r i' = none) : IsZero ((K.extend e).X i') :=
  extend.isZero_X K hi'

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