δ_rightUnshift — Mathlib

English

The δ differential after a leftUnshift by a is given by a neg-one-power twist of the δ after a shift, connecting leftUnshift and δ.

Русский

δ после leftUnshift на a выражается через (-1)^a и δ после сдвига, устанавливая связь между leftUnshift и δ.

LaTeX

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

Lean4

theorem δ_rightUnshift {a n' : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n) (m m' : ℤ) (hm' : m' + a = m) :
    δ n m (γ.rightUnshift n hn) = a.negOnePow • (δ n' m' γ).rightUnshift m hm' :=
  by
  obtain ⟨γ', rfl⟩ := (rightShiftAddEquiv K L n a n' hn).surjective γ
  dsimp
  simp only [rightUnshift_rightShift, γ'.δ_rightShift a n' m' hn m hm', rightUnshift_units_smul, smul_smul,
    Int.units_mul_self, one_smul]

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