d_f_comp_d_f — Mathlib

English

If a bicomplex is built from X via ofGradedObject, then its graded object is X when mapped back via toGradedObject.

Русский

Если биокомплекс построен из X через ofGradedObject, то последующее отображение обратно в градуированный объект возвращает X.

LaTeX

$$$\big(\mathrm{HomologicalComplex}_2(C;c_1,c_2)\big).toGradedObject = X$$$

Lean4

@[reassoc (attr := simp)]
theorem d_f_comp_d_f (K : HomologicalComplex₂ C c₁ c₂) (i₁ i₁' i₁'' : I₁) (i₂ : I₂) :
    (K.d i₁ i₁').f i₂ ≫ (K.d i₁' i₁'').f i₂ = 0 := by rw [← comp_f, d_comp_d, zero_f]

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