English
If K is an R-algebra and A is a K-algebra with IsScalarTower R K A, and algebra_map R K is injective, then algebraic independence over K implies algebraic independence over R for the same family x.
Русский
Пусть K — алгебра над R, A — K-алгебра, существует тождество скалярного квадрата, и вложение R → K инъективно; тогда если x алгебраически независим над K, то он независим над R.
LaTeX
$$$\\text{Injective }(\\text{algebraMap }R K) \\Rightarrow \\text{AlgIndep}_K x \\Rightarrow \\text{AlgIndep}_R x$$$
Lean4
/-- A set of algebraically independent elements in an algebra `A` over a ring `K` is also
algebraically independent over a subring `R` of `K`. -/
theorem restrictScalars {K : Type*} [CommRing K] [Algebra R K] [Algebra K A] [IsScalarTower R K A]
(hinj : Function.Injective (algebraMap R K)) (ai : AlgebraicIndependent K x) : AlgebraicIndependent R x :=
by
have :
(aeval x : MvPolynomial ι K →ₐ[K] A).toRingHom.comp (MvPolynomial.map (algebraMap R K)) =
(aeval x : MvPolynomial ι R →ₐ[R] A).toRingHom :=
by ext <;> simp [algebraMap_eq_smul_one]
change Injective (aeval x).toRingHom
rw [← this, RingHom.coe_comp]
exact Injective.comp ai (MvPolynomial.map_injective _ hinj)
