English
The symmetric of the canonical equivalence applied to a localized map equals the localized map of the canonical linear map.
Русский
Обратное симметрично к каноническому эквиваленту, применённое к локализованному отображению, равно локализованному отображению канонического линейного отображения.
LaTeX
$$$$ (\\mathrm{Module.FinitePresentation.linearEquivMap S}).\\mathrm{symm}((\\mathrm{IsLocalizedModule.map} S (\\mathrm{LocalizedModule.mkLinearMap S M}) (\\mathrm{LocalizedModule.mkLinearMap S N}) f)) = (\\mathrm{LocalizedModule.mkLinearMap S (M \\to N))} f. $$$$
Lean4
@[simp]
theorem linearEquivMap_symm_apply [Module.FinitePresentation R M] (f : M →ₗ[R] N) :
(Module.FinitePresentation.linearEquivMap S).symm
((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)) f) =
(LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f :=
IsLocalizedModule.linearEquiv_symm_apply S _ _ f
