lift — Mathlib

English

The lift and iso interact as (lift ∘ iso) = lift with g.

Русский

Лифт и изоморфизм взаимодействуют так, что (lift ∘ iso) = lift с g.

LaTeX

$$$$ (\mathrm{lift}~S~f~g~h) \circ (\mathrm{iso}~S~f) = \mathrm{LocalizedModule.lift}~S~g~h. $$$$

Lean4

/-- If `M'` is a localized module and `g` is a linear map `M → M''` such that all scalar multiplication
by `s : S` is invertible, then there is a linear map `M' → M''`.
-/
noncomputable def lift (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) : M' →ₗ[R] M'' :=
  (LocalizedModule.lift S g h).comp (iso S f).symm.toLinearMap

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