English
For generators P of R → S and an algebra T over R, there is a natural generator family baseChange T P of S → T ⊗R S, defined by val = P.val and σ′(i) = 1 ⊗ P.σ(i); the aeval compatibility with the tensor product structure follows from the construction.
Русский
Для генераторов P семейства R → S и алгебры T над R существует естественная семейство генераторов baseChange T P семейства S → T ⊗R S, заданное как выше; совместимость с aeval следует из построения.
LaTeX
$$$\\exists G : \\text{Generators } T\\,(T \\otimes_R S)\\,ι\\;\\text{ with } G.{val} = P.{val},\\; G.{σ'}(i) = 1 ⊗ P.{σ}(i),\\; G.aeval\\_val\\_σ'(s) = \\text{(aeval equation)}$$$
Lean4
/-- If `P` is a family of generators of `S` over `R` and `T` is an `R`-algebra, we
obtain a natural family of generators of `T ⊗[R] S` over `T`. -/
@[simps! val]
noncomputable def baseChange (T) [CommRing T] [Algebra R T] (P : Generators R S ι) : Generators T (T ⊗[R] S) ι :=
by
apply Generators.ofSurjective (fun x ↦ 1 ⊗ₜ[R] P.val x)
intro x
induction x using TensorProduct.induction_on with
| zero => exact ⟨0, map_zero _⟩
| tmul a b =>
let X := P.σ b
use a • MvPolynomial.map (algebraMap R T) X
simp only [LinearMapClass.map_smul, X, aeval_map_algebraMap]
have : ∀ y : P.Ring, aeval (fun x ↦ (1 ⊗ₜ[R] P.val x : T ⊗[R] S)) y = 1 ⊗ₜ aeval (fun x ↦ P.val x) y :=
by
intro y
induction y using MvPolynomial.induction_on with
| C a =>
rw [aeval_C, aeval_C, TensorProduct.algebraMap_apply, algebraMap_eq_smul_one, smul_tmul, algebraMap_eq_smul_one]
| add p q hp hq => simp [map_add, tmul_add, hp, hq]
| mul_X p i hp => simp [hp]
rw [this, P.aeval_val_σ, smul_tmul', smul_eq_mul, mul_one]
| add x y ex ey =>
obtain ⟨a, ha⟩ := ex
obtain ⟨b, hb⟩ := ey
use (a + b)
rw [map_add, ha, hb]
