Automorphisms of a hyperelliptic function field preserve the rational subfield

Let F / k be a function field with exact constants and genus g ≥ 2, and let x ∈ F be transcendental with [F : k(x)] = 2. Since the rational subfield of index two is unique (TauCeti.adjoin_eq_adjoin_of_finrank_adjoin_eq_two), every k-automorphism σ of F carries k(x) onto k(σ x) = k(x). Restriction is therefore a homomorphism Aut(F / k) →* Aut(k(x) / k), whose kernel is the group of automorphisms of F / k(x), of order two when F / k(x) is separable (IntermediateField.natCard_fixingSubgroup_of_finrank_eq_two): it is generated by the hyperelliptic involution, and Aut(F / k) modulo it embeds into Aut(k(x) / k).

Main results

• TauCeti.map_adjoin_eq_self_of_finrank_adjoin_eq_two: every automorphism carries k(x) onto itself.
• TauCeti.ker_restrictAdjoinHom: the kernel of restriction to k(x) is the subgroup fixing k(x), of order two by IntermediateField.natCard_fixingSubgroup_of_finrank_eq_two.

References

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

theorem TauCeti.map_adjoin_eq_self_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) {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) (σ : Gal(F/k)) : IntermediateField.map (↑σ) k⟮x⟯ = k⟮x⟯

Every automorphism preserves the rational subfield of index two: for g ≥ 2 and [F : k(x)] = 2, a k-automorphism σ of F carries k(x) onto itself, because k(σ x) is again a rational subfield of index two.

noncomputable def TauCeti.restrictAdjoinHom {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) {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) : Gal(F/k) →* Gal(↥k⟮x⟯/k)

Restriction to the rational subfield of index two, the homomorphism Aut(F / k) →* Aut(k(x) / k).

Equations

• TauCeti.restrictAdjoinHom hF hex hg hx hdeg = k⟮x⟯.restrictAlgEquivHom ⋯

@[simp]

theorem TauCeti.coe_restrictAdjoinHom_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) {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) (σ : Gal(F/k)) (y : ↥k⟮x⟯) : ↑(((restrictAdjoinHom hF hex hg hx hdeg) σ) y) = σ ↑y

theorem TauCeti.ker_restrictAdjoinHom {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) {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) : (restrictAdjoinHom hF hex hg hx hdeg).ker = k⟮x⟯.fixingSubgroup

The kernel of restriction is the group of automorphisms over k(x): an automorphism of F / k restricts to the identity of k(x) exactly when it fixes k(x) pointwise.