toExtendScalars — Mathlib

English

Given a family P of generators for T over R and a ring homomorphism R→R', there is a canonical algebra homomorphism from the polynomial algebra on P over R to the polynomial algebra on P over R' that extends scalars along R→R'.

Русский

Пусть имеется множество порождающих P для T над R и гомоморфизм колец R→R'. Тогда существует канонический алгебраный гомоморфизм из кольца многочленов R[P] в R'[P], получаемый по расширению скаляров вдоль R→R'.

LaTeX

$$$\\text{toExtendScalars}:\\; {R,S,ι}\\to\\text{Hom}(P, P\\extendScalars S)$$$

Lean4

/-- Given families of generators `X ⊆ T`, there is a map `R[X] → S[X]`. -/
@[simps]
noncomputable def toExtendScalars (P : Generators R T ι) : Hom P (P.extendScalars S)
    where
  val := X
  aeval_val i := by simp

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