extendScalarsOfIsLocalization — Mathlib

English

Extending an isomorphism of R-modules gives an isomorphism of A-modules, and vice versa.

Русский

Расширение изоморфизма R‑модулей даёт изоморфизм A‑модулей, и наоборот.

LaTeX

$$$\\text{extendScalarsOfIsLocalization}(f) : M \\simeq_A N$$$

Lean4

/-- An `R`-linear isomorphism between `S⁻¹R`-modules is actually `S⁻¹R`-linear. -/
@[simps!]
def extendScalarsOfIsLocalization (f : M ≃ₗ[R] N) : M ≃ₗ[A] N :=
  .ofLinear (LinearMap.extendScalarsOfIsLocalization S A f) (LinearMap.extendScalarsOfIsLocalization S A f.symm)
    (by ext; simp) (by ext; simp)

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