leftShiftLinearEquiv — Mathlib

English

There is an additive linear equivalence between Cochain K L n and Cochain (K⟦a⟧) L n' whenever n + a = n'. It is built from leftShiftAddEquiv and the smul rules.

Русский

Существует добавочно-линейное эквивалентное отображение между Cochain K L n и Cochain (K⟦a⟧) L n', если n + a = n'. Оно строится из leftShiftAddEquiv и правил смешивания со скалярами.

LaTeX

$$$\text{leftShiftLinearEquiv}(n,a,n',hn') : Cochain K L n \simeq_{\text{linear}} Cochain (K⟦a⟧) L n'$$$

Lean4

/-- The additive equivalence `Cochain K L n ≃+ Cochain (K⟦a⟧) L n'` when `n + a = n'` and
the category is `R`-linear. -/
@[simps!]
def leftShiftLinearEquiv (n a n' : ℤ) (hn : n + a = n') : Cochain K L n ≃ₗ[R] Cochain (K⟦a⟧) L n' :=
  (leftShiftAddEquiv K L n a n' hn).toLinearEquiv (fun x γ => by dsimp; simp only [leftShift_smul])

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