leftUnshift_neg — Mathlib

English

Let γ be a degree-n' cochain from K⟦a⟧ to L. If hn is the equality n + a = n', then applying the negation commutes with the left-unshift operation: (-γ).leftUnshift n hn = - (γ.leftUnshift n hn).

Русский

Пусть γ — косоценный комплекс коэффициентов degree n' из K⟦a⟧ в L и пусть hn = n + a = n'. Тогда отрицание коммутирует с операцией leftUnshift: (-γ).leftUnshift n hn = - (γ.leftUnshift n hn).

LaTeX

$$$(-\gamma).leftUnshift n hn = -\gamma.leftUnshift n hn$$$

Lean4

@[simp]
theorem leftUnshift_neg {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') :
    (-γ).leftUnshift n hn = -γ.leftUnshift n hn :=
  by
  change (leftShiftAddEquiv K L n a n' hn).symm (-γ) = _
  apply map_neg

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