English
If A is algebraic over R and the map S → A is injective, then S is algebraic over R.
Русский
Если A алгебраичен над R и отображение S → A инъективно, то S алгебраичен над R.
LaTeX
$$$\mathrm{Algebra.IsAlgebraic}\ R\ A \rightarrow (\mathrm{Injective}(\mathrm{algebraMap}\ S\ A)) \Rightarrow \mathrm{Algebra.IsAlgebraic}\ R\ S$$$
Lean4
/-- A special case of `IsAlgebraic.extendScalars`. This is extracted as a theorem
because in some cases `IsAlgebraic.extendScalars` will just runs out of memory. -/
theorem tower_top_of_subalgebra_le {A B : Subalgebra R S} (hle : A ≤ B) {x : S} (h : IsAlgebraic A x) :
IsAlgebraic B x := by
letI : Algebra A B := (Subalgebra.inclusion hle).toAlgebra
haveI : IsScalarTower A B S := .of_algebraMap_eq fun _ ↦ rfl
exact h.extendScalars (Subalgebra.inclusion_injective hle)
