XIsoOfEq_hom_comp_XIsoOfEq_inv — Mathlib

English

For a bicomplex K and equalities h1, h3, the composition of homo- and inv-parts yields the corresponding XIsoOfEq with the composed equality.

Русский

Для биокомплексa K и равенств h1, h3 композицией гомоморфизма и обратной части получается XIsoOfEq с объединённым равенством.

LaTeX

$$$ (K.XIsoOfEq h_1).hom \circ (K.XIsoOfEq h_3).inv = (K.XIsoOfEq (h_1 \text{trans } h_3.\text{symm})).hom $$$

Lean4

@[reassoc (attr := simp)]
theorem XIsoOfEq_hom_comp_XIsoOfEq_inv (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₁₂ : p₁ = p₂) (h₃₂ : p₃ = p₂) :
    (K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq (h₁₂.trans h₃₂.symm)).hom :=
  by
  dsimp [XIsoOfEq]
  simp only [eqToHom_trans]

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