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 FixedPoints.subfield G F
,
the subfield consisting of elements of F
fixed_points by every element of G
.
This subfield is then normal and separable, and in addition (TODO) if G
acts faithfully on F
then finrank (FixedPoints.subfield G F) F = Fintype.card G
.
Main Definitions #
FixedPoints.subfield G F
, the subfield consisting of elements ofF
fixed_points by every element ofG
, whereG
is a group that acts onF
.
The subfield of F fixed by the field endomorphism m
.
Instances For
A typeclass for subrings invariant under a MulSemiringAction
.
Instances
The subfield of fixed points by a monoid action.
Instances For
minpoly G F x
is the minimal polynomial of (x : F)
over FixedPoints.subfield G F
.
Instances For
MulSemiringAction.toAlgHom
is bijective.
Bijection between G and algebra homomorphisms that fix the fixed points