baseChange — Mathlib

English

Given a presentation P of S over R and an R-algebra T, one obtains a natural presentation of T ⊗_R S over T.

Русский

Дано презентацию P S над R и R-алгебру T, получаем естественную презентацию T ⊗_R S над T.

LaTeX

$$$\\mathrm{baseChange}:\\; \\mathrm{Presentation}\\; R\\; S \\; \\iota \\; \\sigma \\; \\to\\; \\mathrm{Presentation}\\; T\\; (T \\otimes_R S)\\; \\iota \\sigma$$$

Lean4

/-- If `P` is a presentation of `S` over `R` and `T` is an `R`-algebra, we
obtain a natural presentation of `T ⊗[R] S` over `T`. -/
@[simps relation]
noncomputable def baseChange : Presentation T (T ⊗[R] S) ι σ
    where
  __ := P.toGenerators.baseChange T
  relation i := MvPolynomial.map (algebraMap R T) (P.relation i)
  span_range_relation_eq_ker := P.span_range_relation_eq_ker_baseChange T

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