English
Let M,N be finitely presented R-modules and l : M' ≃ₗ[R] N' a linear equivalence. There exist r ∈ S, hr ∈ S, and l' a localized equivalence such that a certain equality of localized lifts holds.
Русский
Пусть M,N конечной презентации, l — линейное эквивалентное отображение между локализациями; существует r ∈ S, hr ∈ S и l' локализованное эквивалентное отображение так, чтобы диаграмма лифтинга выравнялась.
LaTeX
$$$$ \\exists r \\in S, \\exists hr, \\exists l' : \\mathrm{LocalizedModule}((\\text{powers } r)) M \\simeq \\mathrm{LocalizedModule}((\\text{powers } r)) N,\\quad (\\mathrm{LocalizedModule.lift}((\\text{powers } r))\\, g) \\circ l' = l \\circ (\\mathrm{LocalizedModule.lift}((\\text{powers } r))\\, f). $$$$
Lean4
instance [Module.FinitePresentation R M] : IsLocalizedModule S (LocalizedModule.map S (M := M) (N := N)) :=
Module.FinitePresentation.isLocalizedModule_mapExtendScalars _ _ _ _
