shiftAddHom — Mathlib

English

The additive equivalence between Cochain K L n and Cochain K (L⟦a⟧) n' respects addition in the obvious way: (γ1 + γ2).rightShift a n' hn' = γ1.rightShift a n' hn' + γ2.rightShift a n' hn'.

Русский

Аддитивность эквивалентности между Cochain(K,L,n) и Cochain(K,L⟦a⟧,n') выражается как (γ1 + γ2).rightShift a n' hn' = γ1.rightShift a n' hn' + γ2.rightShift a n' hn'.

LaTeX

$$$\\big(\\gamma_1 + \\gamma_2\\big).rightShift a n' hn' = \\gamma_1.rightShift a n' hn' + \\gamma_2.rightShift a n' hn'$$$

Lean4

/-- The additive map `Cochain K L n →+ Cochain (K⟦a⟧) (L⟦a⟧) n`. -/
@[simps!]
def shiftAddHom (n a : ℤ) : Cochain K L n →+ Cochain (K⟦a⟧) (L⟦a⟧) n :=
  AddMonoidHom.mk' (fun γ => γ.shift a) (by intros; dsimp; simp only [shift_add])

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