extendScalarsOfSurjectiveEquiv — Mathlib

English

If the map algebraMap R S is surjective, there is a canonical linear equivalence between R-linear maps M → N and S-linear maps M → N: (M →ₗ[R] N) ≃ (M →ₗ[S] N).

Русский

Если алгебраMap R S сюръективна, существует каноническое линейное эквивалентное соответствие между R-линейными отображениями M→N и S-линейными M→N.

LaTeX

$$$ (M\\to_{R} N) \\simeq_{\\!R} (M\\to_{S} N) $$$

Lean4

/-- If `R →+* S` is surjective, then `S`-linear maps between modules are exactly `R`-linear maps. -/
def extendScalarsOfSurjectiveEquiv (h : Surjective (algebraMap R S)) : (M →ₗ[R] N) ≃ₗ[R] (M →ₗ[S] N)
    where
  toFun f := { __ := f, map_smul' := fun r x ↦ by obtain ⟨r, rfl⟩ := h r; simp }
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun f := f.restrictScalars S

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