extendScalarsOfIsLocalizationEquiv

English

The equivalence between R-linear and A-linear maps preserves composition and inverses; it is a true equivalence of categories.

Русский

Эквивалентность между R-линейными и A-линейными отображениями сохраняет композиции и обратные отображения; это действительная эквивалентность категорий.

LaTeX

$$$\\text{extendScalarsOfIsLocalizationEquiv} : (M \\to_R N) \\simeq (M \\to_A N)$$$

Lean4

/-- The `S⁻¹R`-linear isomorphisms between two `S⁻¹R`-modules are exactly the `R`-linear
isomorphisms. -/
@[simps]
def extendScalarsOfIsLocalizationEquiv : (M ≃ₗ[R] N) ≃ M ≃ₗ[A] N
    where
  toFun e := e.extendScalarsOfIsLocalization S A
  invFun e := e.restrictScalars R
  left_inv e := by ext; simp
  right_inv e := by ext; simp

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