d_comp_ofHoms_v — Mathlib

English

The left differential followed by the v-component equals the p-th component followed by the right differential.

Русский

Левый дифференциал плюс компонент v равны компоненте p, затем правый дифференциал.

LaTeX

$$$ F.d(p',p) \\circ (\\operatorname{ofHoms}(\\psi)).v(p,q;hpq) = \\psi(p) \\circ G.d(p,q') $$$

Lean4

@[simp]
theorem d_comp_ofHoms_v (ψ : ∀ (p : ℤ), F.X p ⟶ G.X p) (p' p q : ℤ) (hpq : p + 0 = q) :
    F.d p' p ≫ (ofHoms ψ).v p q hpq = F.d p' q ≫ ψ q :=
  by
  rw [add_zero] at hpq
  subst hpq
  rw [ofHoms_v]

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