baseChange — Mathlib

English

Given an R-algebra S and an S-algebra T with submersive presentations, this constructs the base change from R to T for S.

Русский

Пусть есть R-алгебра S и S-алгебра T c.submersive presentations; конструируется базовое изменение от R к T для S.

LaTeX

$$$\\text{baseChange}(T) : \\text{SubmersivePresentation } T (T \\otimes_R S) ι σ$$$

Lean4

/-- If `P` is a submersive presentation of `S` over `R` and `T` is an `R`-algebra, we
obtain a natural submersive presentation of `T ⊗[R] S` over `T`. -/
noncomputable def baseChange : SubmersivePresentation T (T ⊗[R] S) ι σ
    where
  toPreSubmersivePresentation := P.toPreSubmersivePresentation.baseChange T
  jacobian_isUnit := P.baseChange_jacobian T ▸ P.jacobian_isUnit.map TensorProduct.includeRight

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