δ_leftUnshift — Mathlib

English

The δ differential after a rightShift by a interacts with the δ of γ via a neg-one-power twist, as δ n m (γ.rightShift a n hn) = a.negOnePow · (δ n m γ).rightShift a m' hm'.

Русский

δ после rightShift взаимодействует через (-1)^a с δ(γ): δ n m (γ.rightShift a n hn) = a.negOnePow · (δ n m γ).rightShift a m' hm'.

LaTeX

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

Lean4

theorem δ_leftUnshift {a n' : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') (m m' : ℤ) (hm' : m + a = m') :
    δ n m (γ.leftUnshift n hn) = a.negOnePow • (δ n' m' γ).leftUnshift m hm' :=
  by
  obtain ⟨γ', rfl⟩ := (leftShiftAddEquiv K L n a n' hn).surjective γ
  dsimp
  simp only [leftUnshift_leftShift, γ'.δ_leftShift a n' m' hn m hm', leftUnshift_units_smul, smul_smul,
    Int.units_mul_self, one_smul]

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