leftShift_add — Mathlib

English

There is an additive equivalence between Cochain K L n and Cochain K (L⟦a⟧) n' whenever n' + a = n, given by the pair of maps rightShift and rightUnshift with inverse behavior. It preserves addition.

Русский

Существует аддитивная эквиваленция между Cochain(K,L,n) и Cochain(K, L⟦a⟧, n') при условии n' + a = n, задаваемая парами отображений rightShift и rightUnshift и сохраняющая сложение.

LaTeX

$$$\\text{rightShiftAddEquiv}(n,a,n',\\!hn'):\\; \\text{Cochain}(K,L,n) \\simeq_+ \\text{Cochain}(K,L⟦a⟧,n'),\\; \\gamma \\mapsto \\gamma.rightShift a n' hn',\\; \\text{inv}=\\gamma.rightUnshift n hn',$$$

Lean4

@[simp]
theorem leftShift_add (a n' : ℤ) (hn' : n + a = n') :
    (γ₁ + γ₂).leftShift a n' hn' = γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn' :=
  by
  ext p q hpq
  dsimp
  simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by cutsat), add_v, comp_add, smul_add]

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