English
The base change of an R-extension of S along a ring T yields an extension over T of the tensor product T ⊗_R S, with Ring given by T ⊗_R P.Ring and the appropriate σ and algebra_map structure induced by the tensor product construction.
Русский
Базовое изменение (base change) расширения над R рассматривается по орбитально-торговой конструкции, давая новое расширение над T над T ⊗_R S, с Ring = T ⊗_R P.Ring и соответствующими σ и algebra_map.
LaTeX
$$$\\text{baseChange}(P,R,S,T):\\ \\mathrm{Extension}\\ T\\ (T\\otimes_R S)$$$
Lean4
/-- The base change of an `R`-extension of `S` to `T` gives a `T`-extension of `T ⊗[R] S`. -/
noncomputable def baseChange {T} [CommRing T] [Algebra R T] (P : Extension R S) : Extension T (T ⊗[R] S)
where
Ring := T ⊗[R] P.Ring
__ :=
ofSurjective (P := T ⊗[R] P.Ring) (Algebra.TensorProduct.map (AlgHom.id T T) (IsScalarTower.toAlgHom _ _ _))
(LinearMap.lTensor_surjective T (g := (IsScalarTower.toAlgHom R P.Ring S).toLinearMap) P.algebraMap_surjective)
