extendScalarsOfSurjective — Mathlib

English

There is an R → S extension that sends an R-linear map to an S-linear map, defined by extending scalars along Surjective(algebraMap R S).

Русский

Существует переход расширения скаляров, который переводит R-линейное отображение в S-линейное отображение, реализованный через расширение скаляров по сюръективному отображению алгебраMap.

LaTeX

$$$\\mathrm{extendScalarsOfSurjective} : (M \\to_{R} N) \\to (M \\to_{S} N)$$$

Lean4

/-- If `R →+* S` is surjective, then `R`-linear isomorphisms are also `S`-linear. -/
def extendScalarsOfSurjective (h : Surjective (algebraMap R S)) (f : M ≃ₗ[R] N) : M ≃ₗ[S] N
    where
  __ := f
  map_smul' r x := by obtain ⟨r, rfl⟩ := h r; simp

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