v_comp_XIsoOfEq_hom — Mathlib

English

Let γ be a degree n cochain. If q = q', then γ.v(p,q,hpq) composed with the hom component of the XiSoOfEq iso equals γ.v(p,q',hpq').

Русский

Пусть γ — когейн степени n. При q = q'имеется: γ.v(p,q,hpq) ∘ hom(XIsoOfEq G hq') = γ.v(p,q',hpq').

LaTeX

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

Lean4

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

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