English
The symmetric of linearEquivMapExtendScalars applied to a localized map equals the localized map of the symmetric extension.
Русский
Обратное к ExtendScalars равно локализованному отображению симметричного расширения.
LaTeX
$$$$ (\\mathrm{Module.FinitePresentation.linearEquivMapExtendScalars S}).\\mathrm{symm}((\\mathrm{IsLocalizedModule.mapExtendScalars S (\\mathrm{LocalizedModule.mkLinearMap S M}) (\\mathrm{LocalizedModule.mkLinearMap S N}) (\\mathrm{Localization} S)) f) = (\\mathrm{LocalizedModule.mkLinearMap S (M \\to N))} f. $$$$
Lean4
theorem linearEquivMapExtendScalars_apply [Module.FinitePresentation R M] (f : M →ₗ[R] N) :
Module.FinitePresentation.linearEquivMapExtendScalars S ((LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f) =
(IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)
(Localization S))
f :=
IsLocalizedModule.linearEquiv_apply S _ _ f
