extendScalarsOfIsLocalizationEquiv

English

A simplified variant: (f.extendScalarsOfIsLocalization S A) x = f x for all x.

Русский

Упрощённый вариант: (f.extendScalarsOfIsLocalization S A) x = f x для любого x.

LaTeX

$$$ (f.extendScalarsOfIsLocalization S A) x = f x $$$

Lean4

/-- The `S⁻¹R`-linear maps between two `S⁻¹R`-modules are exactly the `R`-linear maps. -/
@[simps]
def extendScalarsOfIsLocalizationEquiv : (M →ₗ[R] N) ≃ₗ[A] (M →ₗ[A] N)
    where
  toFun := LinearMap.extendScalarsOfIsLocalization S A
  invFun := LinearMap.restrictScalars R
  map_add' := by intros; ext; simp
  map_smul' := by intros; ext; simp
  left_inv := by intro _; ext; simp
  right_inv := by intro _; ext; simp

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