d_comp_XIsoOfEq_inv — Mathlib

English

For a morphism f: K ⟶ L between bicomplexes, the horizontal differential commutes with f on each component: (f.f i1).f i2 followed by (L.d i1 i1').f i2 equals (K.d i1 i1').f i2 followed by (f.f i1').f i2.

Русский

Для морфизма f: K ⇢ L между биокомплексами, горизонтальный дифференциал коммютирует с f по каждой компоненте.

LaTeX

$$$\forall i_1,i_1': c_1.Rel i_1 i_1' ,\; (f.f i_1).f i_2 ≫ (L.d i_1 i_1').f i_2 = (K.d i_1 i_1').f i_2 ≫ (f.f i_1').f i_2$$$

Lean4

@[reassoc (attr := simp)]
theorem d_comp_XIsoOfEq_inv (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₃ = p₂) (p₁ : ι) :
    K.d p₁ p₂ ≫ (K.XIsoOfEq h).inv = K.d p₁ p₃ := by subst h; simp

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