English
Let R be a commutative semiring, A an R-algebra, and M,N be R-modules. For any R-linear map f: M → N, the base-change along A yields an A-linear map baseChange_A(f): A ⊗_R M →_A A ⊗_R N, defined by sending a ⊗ m to a ⊗ f(m). This is the standard extension of scalars of f to A.
Русский
Пусть R — коммутативное полупольцо, A — алгебра над R, и M,N — модули над R. для любой линейной отображения f: M → N над R существует единственный A-линейный отображение baseChange_A(f): A ⊗_R M →_A A ⊗_R N, которое действует на простых тензоров по правилу a ⊗ m ↦ a ⊗ f(m). Это стандартное расширение скаляров.
LaTeX
$$$\\mathrm{baseChange}_A(f): A \\otimes_R M \\to_A A \\otimes_R N$, \\\\quad (a\\otimes_R m) \\mapsto a\\otimes_R f(m).$$
Lean4
/-- `baseChange A f` for `f : M →ₗ[R] N` is the `A`-linear map `A ⊗[R] M →ₗ[A] A ⊗[R] N`.
This "base change" operation is also known as "extension of scalars". -/
def baseChange (f : M →ₗ[R] N) : A ⊗[R] M →ₗ[A] A ⊗[R] N :=
AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) f
