lift — Mathlib

English

llift is the linear equivalence between X → M (as an S-module) and (X →₀ R) →ₗ[R] M, built from the base lift.

Русский

llift — линейное эквивалентное отображение между X → M и (X →₀ R) →ₗ[R] M, построенное на основе lift.

LaTeX

$$$$ llift : (X \to M) \simeq_+ ((X \to_0 R) \to_\ell[R] M) $$$$

Lean4

/-- A slight rearrangement from `lsum` gives us
the bijection underlying the free-forgetful adjunction for R-modules.
-/
noncomputable def lift : (X → M) ≃+ ((X →₀ R) →ₗ[R] M) :=
  (AddEquiv.arrowCongr (Equiv.refl X) (ringLmapEquivSelf R ℕ M).toAddEquiv.symm).trans (lsum _ : _ ≃ₗ[ℕ] _).toAddEquiv

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