English
As above: the fraction ring of a localized structure is algebraic over the base field whenever the localized structure is algebraic over the base ring.
Русский
Как выше: дробная часть локализации алгебраична над базовым полем тогда и только тогда, когда локализованная структура алгебраична над базовой колонией.
LaTeX
$$$\text{Algebra.IsAlgebraic}_K L$$$
Lean4
theorem isAlgebraic_of_isFractionRing {R S} (K L) [CommRing R] [CommRing S] [Field K] [CommRing L] [Algebra R S]
[Algebra R K] [Algebra R L] [Algebra S L] [Algebra K L] [IsScalarTower R S L] [IsScalarTower R K L]
[IsFractionRing S L] [Algebra.IsIntegral R S] : Algebra.IsAlgebraic K L :=
by
constructor
intro x
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective S⁰ x
apply IsIntegral.isAlgebraic
rw [IsLocalization.mk'_eq_mul_mk'_one]
apply RingHom.IsIntegralElem.mul
· apply IsIntegral.tower_top (R := R)
apply IsIntegral.map (IsScalarTower.toAlgHom R S L)
exact Algebra.IsIntegral.isIntegral x
· change IsIntegral _ _
rw [← isAlgebraic_iff_isIntegral, ← IsAlgebraic.invOf_iff, isAlgebraic_iff_isIntegral]
apply IsIntegral.tower_top (R := R)
apply IsIntegral.map (IsScalarTower.toAlgHom R S L)
exact Algebra.IsIntegral.isIntegral (s : S)
