English
If A is finite type over R and S is larger with an algebra structure and IsScalarTower, then A is finite type over S.
Русский
Если A имеет конечную презентацию над R и S является более широким полем/кольцом, то A имеет конечную презентацию над S.
LaTeX
$$$\\text{Algebra.FiniteType R A} \\to \\text{Algebra.FiniteType S A}$ under IsScalarTower$$
Lean4
theorem of_restrictScalars_finiteType [Algebra S A] [IsScalarTower R S A] [hA : FiniteType R A] : FiniteType S A :=
by
obtain ⟨s, hS⟩ := hA.out
refine ⟨⟨s, eq_top_iff.2 fun b => ?_⟩⟩
have le : adjoin R (s : Set A) ≤ Subalgebra.restrictScalars R (adjoin S s) :=
by
apply (Algebra.adjoin_le _ : adjoin R (s : Set A) ≤ Subalgebra.restrictScalars R (adjoin S ↑s))
simp only [Subalgebra.coe_restrictScalars]
exact Algebra.subset_adjoin
exact le (eq_top_iff.1 hS b)
