rightUnshift_comp — Mathlib

English

The δ differential of a rightUnshift is δ n m (γ.rightUnshift n hn) = a.negOnePow · (δ n' m' γ).rightUnshift m hm'.

Русский

δ-доказ δ_rightUnshift: δ n m (γ.rightUnshift n hn) = a.negOnePow · (δ n' m' γ).rightUnshift m hm'.

LaTeX

$$$\delta n m (\gamma.rightUnshift n hn) = a.negOnePow · (\delta n' m' \gamma).rightUnshift m hm'$$$

Lean4

theorem rightUnshift_comp {m : ℤ} {a : ℤ} (γ' : Cochain L (M⟦a⟧) m) {nm : ℤ} (hnm : n + m = nm) (nm' : ℤ)
    (hnm' : nm + a = nm') (m' : ℤ) (hm' : m + a = m') :
    (γ.comp γ' hnm).rightUnshift nm' hnm' = γ.comp (γ'.rightUnshift m' hm') (by cutsat) :=
  by
  ext p q hpq
  rw [(γ.comp γ' hnm).rightUnshift_v nm' hnm' p q hpq (p + n + m) (by cutsat),
    γ.comp_v γ' hnm p (p + n) (p + n + m) rfl rfl,
    comp_v _ _ (show n + m' = nm' by cutsat) p (p + n) q (by cutsat) (by cutsat),
    γ'.rightUnshift_v m' hm' (p + n) q (by cutsat) (p + n + m) rfl, assoc]

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