d_comm — Mathlib

English

For each i1,i1',i2,i2', the horizontal and vertical differentials commute in a bicomplex: d1 ∘ d2 = d2 ∘ d1 at the appropriate indices.

Русский

Для каждой пары индексов горизонтальные и вертикальные дифференциалы коммютируют: соответствующие квадратные диаграммы сходятся.

LaTeX

$$$\forall i_1,i_1',i_2,i_2',\; (K.d i_1 i_1').f i_2 \circ (K.X i_1').d i_2 i_2' = (K.X i_1).d i_2 i_2' \circ (K.d i_1 i_1').f i_2'$$$

Lean4

@[reassoc]
theorem d_comm (K : HomologicalComplex₂ C c₁ c₂) (i₁ i₁' : I₁) (i₂ i₂' : I₂) :
    (K.d i₁ i₁').f i₂ ≫ (K.X i₁').d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ (K.d i₁ i₁').f i₂' := by simp

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