v_comp_XIsoOfEq_inv — Mathlib

English

If q' = q, then γ.v(p,q,hpq) composed with the inverse of XiSoOfEq(G,hq') equals γ.v(p,q',hpq).

Русский

Если q' = q, то γ.v(p,q,hpq) ∘ (XIsoOfEq(G,hq')).inv = γ.v(p,q',hpq).

LaTeX

$$$$\gamma_v(p,q,hpq) \circ (\mathrm{XIsoOfEq}\, G\, hq').inv = \gamma_v(p,q',hpq).$$$$

Lean4

@[reassoc]
theorem v_comp_XIsoOfEq_inv (γ : Cochain F G n) (p q q' : ℤ) (hpq : p + n = q) (hq' : q' = q) :
    γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').inv = γ.v p q' (by rw [hq', hpq]) :=
  by
  subst hq'
  simp only [HomologicalComplex.XIsoOfEq, eqToIso_refl, Iso.refl_inv, comp_id]

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