English
There is a canonical IsLocalizedModule structure on the localized endomorphism module, i.e., on mkLinearMap, giving a localization data for the endomorphisms.
Русский
Существует каноническая структура IsLocalizedModule на mkLinearMap, задающая локализационные данные для эндоморфизмов.
LaTeX
$$$\\text{IsLocalizedModule}(S,\\mathrm{mkLinearMap}(S,M)).$$$
Lean4
/-- If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S` is invertible, then
there is a linear map `LocalizedModule S M → M''`.
-/
noncomputable def lift (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) :
LocalizedModule S M →ₗ[R] M'' where
toFun := LocalizedModule.lift' S g h
map_add' := LocalizedModule.lift'_add S g h
map_smul' r x := by rw [LocalizedModule.lift'_smul, RingHom.id_apply]
