English
If P is a pre-submersive presentation of S over R and T is an R-algebra, then there exists a natural pre-submersive presentation of T ⊗[R] S over T obtained by base-changing P along T.
Русский
Пусть P — предsub-мерсивное представление S над R, и T — алгебра над R. Тогда существует естественное предsub-мерсивное представление T ⊗_R S над T, получаемое по базовому изменению P вдоль T.
LaTeX
$$\\text{baseChange}_T(P) : \\text{PreSubmersivePresentation}(T, T \\otimes_R S)_{\\iota, \\sigma} ,\\text{with data as in the definition: }\\text{toPresentation}(\\text{baseChange}_T(P)) = \\text{toPresentation.baseChange}_T(P),\\text{map}=P.map,\\text{map_inj}=P.map_inj.$$
Lean4
/-- If `P` is a pre-submersive presentation of `S` over `R` and `T` is an `R`-algebra, we
obtain a natural pre-submersive presentation of `T ⊗[R] S` over `T`. -/
noncomputable def baseChange : PreSubmersivePresentation T (T ⊗[R] S) ι σ
where
__ := P.toPresentation.baseChange T
map := P.map
map_inj := P.map_inj
