Finite automorphism groups from invariant places

A finite, automorphism-invariant set of sufficiently many rational places detects every automorphism of a function field. Restricting the action to this set embeds the full automorphism group in its symmetric group, and in particular makes it finite. This is the group-theoretic step in the Weierstrass-point argument for finiteness of the automorphism group in genus at least two. The finite invariant set is an explicit input; the result applies to Weierstrass points once their invariance and cardinality are established.

References

• G. D. Villa Salvador, Topics in the Theory of Algebraic Function Fields, Birkhäuser, 2006, Chapter 9.

noncomputable def TauCeti.placePermHomOfInvariant {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {G : Type u_3} [Group G] (φ : G →* Gal(F/k)) {S : Finset (Place k F)} (hS : ∀ (g : G), ∀ P ∈ S, φ g • P ∈ S) : G →* Equiv.Perm ↥S

Restricting the action on places to an invariant finite set gives an action by permutations of that set, along a homomorphism φ into the automorphism group. Taking φ to be the identity gives the action of the automorphism group itself.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.placePermHomOfInvariant_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {G : Type u_3} [Group G] (φ : G →* Gal(F/k)) {S : Finset (Place k F)} (hS : ∀ (g : G), ∀ P ∈ S, φ g • P ∈ S) (g : G) (P : ↥S) : ↑(((placePermHomOfInvariant φ hS) g) P) = φ g • ↑P

Evaluating the restricted permutation recovers the action on places.

@[simp]

theorem TauCeti.placePermHomOfInvariant_symm_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {G : Type u_3} [Group G] (φ : G →* Gal(F/k)) {S : Finset (Place k F)} (hS : ∀ (g : G), ∀ P ∈ S, φ g • P ∈ S) (g : G) (P : ↥S) : ↑((Equiv.symm ((placePermHomOfInvariant φ hS) g)) P) = (φ g)⁻¹ • ↑P

Evaluating the inverse of the restricted permutation.

theorem TauCeti.ker_placePermHomOfInvariant_le {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {G : Type u_3} [Group G] (φ : G →* Gal(F/k)) (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (S : Finset (Place k F)) (hS : ∀ (g : G), ∀ P ∈ S, φ g • P ∈ S) (hrat : ∀ P ∈ S, P.degree = 1) (hcard : 2 * genus k F + 3 ≤ S.card) : (placePermHomOfInvariant φ hS).ker ≤ φ.ker

An invariant set of at least 2g + 3 rational places detects the kernel: an element acting trivially on the set already acts trivially on F.

theorem TauCeti.placePermHomOfInvariant_injective {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (S : Finset (Place k F)) (hS : ∀ (σ : Gal(F/k)), ∀ P ∈ S, σ • P ∈ S) (hrat : ∀ P ∈ S, P.degree = 1) (hcard : 2 * genus k F + 3 ≤ S.card) : Function.Injective ⇑(placePermHomOfInvariant (MonoidHom.id Gal(F/k)) hS)

The restricted action is faithful when the invariant set contains at least 2g + 3 rational places.

theorem TauCeti.finite_algEquiv_of_invariant_rational_places {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (S : Finset (Place k F)) (hS : ∀ (σ : Gal(F/k)), ∀ P ∈ S, σ • P ∈ S) (hrat : ∀ P ∈ S, P.degree = 1) (hcard : 2 * genus k F + 3 ≤ S.card) : Finite Gal(F/k)

An invariant set of at least 2g + 3 rational places forces the full automorphism group to be finite.

theorem TauCeti.card_algEquiv_le_factorial_of_invariant_rational_places {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (S : Finset (Place k F)) (hS : ∀ (σ : Gal(F/k)), ∀ P ∈ S, σ • P ∈ S) (hrat : ∀ P ∈ S, P.degree = 1) (hcard : 2 * genus k F + 3 ≤ S.card) : Nat.card Gal(F/k) ≤ S.card.factorial

The finite invariant set also bounds the automorphism group's order by the order of its symmetric group.