leftShiftAddEquiv — Mathlib

English

Alternative presentation of the same additive equivalence between Cochain K L n and Cochain K (L⟦a⟧) n' under n' + a = n, emphasizing the additive structure.

Русский

Альтернативное изложение той же аддитивной эквивалентности между Cochain(K,L,n) и Cochain(K, L⟦a⟧, n') при n' + a = n, подчёркивающее аддитивную структуру.

LaTeX

$$$\\text{RightShiftAddEquiv}(n,a,n',hn')[\\;] = \\text{toFun and invFun as above with additive map preservation.}$$$

Lean4

/-- The additive equivalence `Cochain K L n ≃+ Cochain (K⟦a⟧) L n'` when `n + a = n'`. -/
@[simps]
def leftShiftAddEquiv (n a n' : ℤ) (hn' : n + a = n') : Cochain K L n ≃+ Cochain (K⟦a⟧) L n'
    where
  toFun γ := γ.leftShift a n' hn'
  invFun γ := γ.leftUnshift n hn'
  left_inv γ := by simp only [leftUnshift_leftShift]
  right_inv γ := by simp only [leftShift_leftUnshift]
  map_add' γ γ' := by simp only [leftShift_add]

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