Finite subfields in a common overfield #
Finite fields have a unique subfield of each possible degree inside a fixed
finite overfield. The form needed for constant extensions is an inclusion of
the ranges of two specified embeddings: if the degree of A / C divides the
degree of B / C, then the image of A lies in the image of B.
The proof is elementary and keeps the embeddings explicit. The image of B
already supplies #B roots of X ^ (#B) - X; the polynomial has at most
#B roots. Divisibility of extension degrees then shows that every element
of the image of A is another root of the same polynomial.
theorem
BGS.HasseWeil.finiteField_fieldRange_le_of_finrank_dvd
{C : Type u_1}
{A : Type u_2}
{B : Type u_3}
{Ω : Type u_4}
[Field C]
[Field A]
[Field B]
[Field Ω]
[Algebra C A]
[Algebra C B]
[Algebra C Ω]
[Finite C]
[Finite A]
[Finite B]
[Finite Ω]
(f : A →ₐ[C] Ω)
(g : B →ₐ[C] Ω)
(hdiv : Module.finrank C A ∣ Module.finrank C B)
:
In a common finite overfield, the image of a finite field of degree d
is contained in the image of one of degree n whenever d ∣ n over the
same finite base field.