Fixed fields of finite automorphism groups of function fields #
If a finite group of automorphisms acts on an algebraic function field F / k, its fixed field
is again an algebraic function field over k. The extension of the fixed field is finite Galois,
and its Galois group is the acting group. This is the field-theoretic input to applying
Riemann--Hurwitz to a quotient by a finite automorphism group.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Section III.7.
theorem
TauCeti.IsFunctionField.fixedField
{k : Type u_1}
{F : Type u_2}
[Field k]
[Field F]
[Algebra k F]
(hF : IsFunctionField k F)
(H : Subgroup Gal(F/k))
[Finite ↥H]
:
The fixed field of a finite group of k-automorphisms of a function field is itself a
function field over k. IsGalois.of_fixed_field makes F Galois over
this field, and FixedPoints.toAlgAutMulEquiv identifies its Galois group
with H.