shiftLinearMap — Mathlib

English

There is an additive linear equivalence between Cochain K L n and Cochain K (L⟦a⟧) n' with n' + a = n, induced by rightShiftAddEquiv and the smul compatibility with shift.

Русский

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

LaTeX

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

Lean4

/-- The linear map `Cochain K L n ≃+ Cochain (K⟦a⟧) (L⟦a⟧) n` when the category is `R`-linear. -/
@[simps!]
def shiftLinearMap (n a : ℤ) : Cochain K L n →ₗ[R] Cochain (K⟦a⟧) (L⟦a⟧) n
    where
  toAddHom := shiftAddHom K L n a
  map_smul' _ _ := by dsimp; simp only [shift_smul]

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