Finiteness of the automorphism group of a hyperelliptic function field

Let k be an algebraically closed field of characteristic other than two and F / k a function field of genus g ≥ 2 with a rational subfield k(x) of index two. Every k-automorphism of F preserves k(x) and permutes the 2g + 2 ≥ 6 branch places of k(x); an automorphism whose restriction to k(x) fixes all of them fixes k(x) pointwise, by rigidity in genus zero, so it is the identity or the hyperelliptic involution. Hence Aut(F / k) is finite, of order at most 2 · (2g + 2)!. This is the hyperelliptic case of the finiteness of the automorphism group of a function field of genus at least two.

Main results

• TauCeti.branchPermHom: the action of Aut(F / k) on the branch places of k(x), evaluated by TauCeti.branchPermHom_apply and TauCeti.branchPermHom_symm_apply.
• TauCeti.ker_branchPermHom: its kernel is the group of automorphisms over k(x).
• TauCeti.finite_algEquiv_of_finrank_adjoin_eq_two: Aut(F / k) is finite, and TauCeti.card_algEquiv_le_of_finrank_adjoin_eq_two: of order at most 2 · (2g + 2)!.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Exercise 3.17 and Proposition 6.2.4.

noncomputable def TauCeti.branchPermHom {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : 2 ≤ genus k F) [NeZero 2] {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] [Algebra.IsSeparable (↥k⟮x⟯) F] : Gal(F/k) →* Equiv.Perm ↥(branchPlaces hx)

The action of Aut(F / k) on the branch places of k(x), through the restriction of automorphisms to k(x).

Equations

• TauCeti.branchPermHom hF hex hg hx hdeg = TauCeti.placePermHomOfInvariant (TauCeti.restrictAdjoinHom hF hex hg hx hdeg) ⋯

@[simp]

theorem TauCeti.branchPermHom_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : 2 ≤ genus k F) [NeZero 2] {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] [Algebra.IsSeparable (↥k⟮x⟯) F] (σ : Gal(F/k)) (P : ↥(branchPlaces hx)) : ↑(((branchPermHom hF hex hg hx hdeg) σ) P) = (restrictAdjoinHom hF hex hg hx hdeg) σ • ↑P

The action of an automorphism on a branch place is the action of its restriction to k(x).

@[simp]

theorem TauCeti.branchPermHom_symm_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : 2 ≤ genus k F) [NeZero 2] {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] [Algebra.IsSeparable (↥k⟮x⟯) F] (σ : Gal(F/k)) (P : ↥(branchPlaces hx)) : ↑((Equiv.symm ((branchPermHom hF hex hg hx hdeg) σ)) P) = ((restrictAdjoinHom hF hex hg hx hdeg) σ)⁻¹ • ↑P

The inverse action of an automorphism on a branch place.

theorem TauCeti.ker_branchPermHom {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : 2 ≤ genus k F) [NeZero 2] {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] [Algebra.IsSeparable (↥k⟮x⟯) F] [IsAlgClosed k] : (branchPermHom hF hex hg hx hdeg).ker = k⟮x⟯.fixingSubgroup

The kernel of the action on the branch places is the group of automorphisms over k(x), when k is algebraically closed: an automorphism acting trivially on the branch places restricts to an automorphism of the genus-zero field k(x) fixing 2g + 2 ≥ 3 of its rational places, so it fixes k(x) pointwise by rigidity; conversely an automorphism fixing k(x) pointwise restricts to the identity.

theorem TauCeti.finite_algEquiv_of_finrank_adjoin_eq_two {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : 2 ≤ genus k F) [NeZero 2] {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] [Algebra.IsSeparable (↥k⟮x⟯) F] [IsAlgClosed k] : Finite Gal(F/k)

The automorphism group of a hyperelliptic function field is finite over an algebraically closed field of characteristic other than two: the action on the branch places has finite image, and its kernel is the group of automorphisms over k(x), of order two.

theorem TauCeti.card_algEquiv_le_of_finrank_adjoin_eq_two {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : 2 ≤ genus k F) [NeZero 2] {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] [Algebra.IsSeparable (↥k⟮x⟯) F] [IsAlgClosed k] : Nat.card Gal(F/k) ≤ 2 * (2 * genus k F + 2).factorial

The order of the automorphism group is at most 2 · (2g + 2)!: the quotient by the hyperelliptic involution embeds in the symmetric group of the 2g + 2 branch places.