Fixed field under a group action. #
This is the basis of the Fundamental Theorem of Galois Theory.
Given a (finite) group
G that acts on a field
F, we define
fixed_points G F,
the subfield consisting of elements of
F fixed_points by every element of
This subfield is then normal and separable, and in addition (TODO) if
G acts faithfully on
finrank (fixed_points G F) F = fintype.card G.
Main Definitions #
fixed_points G F, the subfield consisting of elements of
Ffixed_points by every element of
Gis a group that acts on
The subfield of F fixed by the field endomorphism
A typeclass for subrings invariant under a
minpoly G F x is the minimal polynomial of
(x : F) over
fixed_points G F.
Bijection between G and algebra homomorphisms that fix the fixed points