English
Let K be a Jacobson Noetherian ring and A a nontrivial K-algebra of finite type. Then every K-subfield of A is finite over K.
Русский
Пусть K — кольцо Якобсона и Ноттерово, A — не тривиальная K-алгебра конечного типа. Тогда любая K-подполе A является конечной над K.
LaTeX
$$$\text{If } K \text{ is Jacobson Noetherian and } A \text{ is a nontrivial } K\text{-algebra of finite type, then for every subfield } F \leq A \text{ with } f(K) \subseteq F, \ [F:K] < \infty.$$$
Lean4
/-- If `K` is a Jacobson Noetherian ring, `A` a nontrivial `K`-algebra of finite type,
then any `K`-subfield of `A` is finite over `K`. -/
theorem finite_of_algHom_finiteType_of_isJacobsonRing {K L A : Type*} [CommRing K] [DivisionRing L] [CommRing A]
[IsJacobsonRing K] [IsNoetherianRing K] [Nontrivial A] [Algebra K L] [Algebra K A] [Algebra.FiniteType K A]
(f : L →ₐ[K] A) : Module.Finite K L :=
by
obtain ⟨m, hm⟩ := Ideal.exists_maximal A
letI := Ideal.Quotient.field m
have := finite_of_finite_type_of_isJacobsonRing K (A ⧸ m)
exact Module.Finite.of_injective ((Ideal.Quotient.mkₐ K m).comp f).toLinearMap (RingHom.injective _)
