rightShiftLinearEquiv — Mathlib

English

There is a natural R-linear equivalence between Cochain K L n and Cochain K (L⟦a⟧) n' given n' + a = n, implemented by shifting and right shifting, compatible with smul.

Русский

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

LaTeX

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

Lean4

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

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