Documentation

TauCeti.RingTheory.Localization.FiniteDimensional

Finite-dimensionality of a fraction field over an intermediate field #

Let S be finite as a module over R, and let L be a fraction field of S. Then L is finite-dimensional over any intermediate field K, that is, any field sitting in a tower R → K → L. Mathlib proves this only for the concrete FractionRing R and FractionRing S; the statement here is about abstract fraction fields and an arbitrary intermediate field.

Main results #

Provenance #

Roadmap: EllipticCurves, the Layers 0-1 target Function-field foundations and isogenies (TauCetiRoadmap/EllipticCurves/README.md:1096). This is the fraction-field sentence of Stacks, Lemma 10.161.5 (tag 032I).

Implementation notes #

The proof is elementary and does not use integral-closure theory, only the integrality of a finite module element: V is the K-span of the image of a finite R-generating set of S, it absorbs multiplication by the image of S, and it contains the inverse of every nonzero element of that image because such an element is integral over K and the inverse of a nonzero integral element lies in the algebra it generates. L is then V because every element of L is a quotient of elements of the image of S.

source
theorem TauCeti.IsFractionRing.finiteDimensional_of_finite (R : Type u_1) (S : Type u_2) (K : Type u_3) (L : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] [Field K] [Field L] [Algebra R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] :
FiniteDimensional K L

A fraction field L of a ring S that is finite as an R-module is finite-dimensional over any intermediate field K, that is, any field with R → K → L.

This is the content of Stacks, Lemma 10.161.5 (tag 032I) — "Let M be a finite field extension of the fraction field of S. Then M is also a finite field extension of K" — but the hypotheses here are weaker than that sentence suggests, and deliberately so: K need not be a fraction field of R, and no assumption on R beyond Module.Finite R S is used. No explicit IsDomain S hypothesis is needed either, but that is not extra generality: IsFractionRing S L with L a field already forces algebraMap S L to be injective, and hence S to be a domain. Mathlib covers only the concrete FractionRing R / FractionRing S case.