Algebraic Belyi pairs

A Belyi map is a finite map from a curve to the projective line that is unramified outside t = 0, t = 1 and t = ∞. In the language of function fields, over a field k of characteristic zero, an algebraic Belyi pair is a function field F / k with exact constant field k, together with a finite embedding k(t) ↪ F of the rational function field, such that every place of F lying over a place of k(t) other than the three marked places t = 0, t = 1 and t = ∞ has ramification index 1. The embedding is recorded as an Algebra (RatFunc k) F structure, with F finite over RatFunc k; the degree of the Belyi map is Module.finrank (RatFunc k) F.

The three marked places are the finite places of the monic irreducibles t and t - 1, and the place at infinity (TauCeti.Place.zeroOneInfty). The definition asks only that the branch locus be contained in them: a Belyi map need not ramify over all three points.

In characteristic zero the extension F / k(t) is automatically separable, and so are the residue field extensions at all places. Hence F is an algebraic Belyi pair exactly when every place of k(t) outside the three marked places is unramified in F in Stichtenoth's sense (TauCeti.isAlgebraicBelyiPair_iff). Characteristic zero is also what makes the standard examples behave: in characteristic p the map t ↦ t ^ p is inseparable, and 4t(1 - t) is constant in characteristic 2.

The rational function field itself, with the identity embedding, is the Belyi pair of degree one (TauCeti.isAlgebraicBelyiPair_ratFunc). Being a Belyi pair is invariant under isomorphisms over k(t), and more generally under a commutative square of isomorphisms whose automorphism of k(t) permutes the three marked places (TauCeti.IsAlgebraicBelyiPair.of_equiv_equiv); the six automorphisms permuting them are in TauCeti.FieldTheory.FunctionField.Belyi.BranchPoints. Radical examples y ^ n = c t ^ a (t - 1) ^ b, among them the power maps, are in TauCeti.FieldTheory.FunctionField.Belyi.Radical.

Main definitions

• TauCeti.Place.zeroOneInfty: the places t = 0, t = 1 and t = ∞ of k(t), and TauCeti.Place.markedPlace, the same places numbered 0, 1 and 2.
• TauCeti.IsAlgebraicBelyiPair: F / k(t) is an algebraic Belyi pair.

Main results

• TauCeti.Place.notMem_zeroOneInfty_iff: the unmarked places are those at which t and t - 1 both have order zero.
• TauCeti.isAlgebraicBelyiPair_iff: the characterization by unramified places, and TauCeti.isAlgebraicBelyiPair_iff_branchPlaces_subset: the same statement as containment of the branch places of F / k(t) in the three marked places.
• TauCeti.isAlgebraicBelyiPair_ratFunc: k(t) over itself is an algebraic Belyi pair.
• TauCeti.IsAlgebraicBelyiPair.of_equiv_equiv and TauCeti.IsAlgebraicBelyiPair.of_algEquiv: transport along isomorphisms.
• TauCeti.IsAlgebraicBelyiPair.of_isScalarTower: a finite extension of an algebraic Belyi pair that is unramified over the places outside the three marked fibres is an algebraic Belyi pair.
• TauCeti.isAlgebraicBelyiPair_iff_of_isScalarTower: for a tower k(t) ⊆ E ⊆ F, the branch places of E / k(t) and the places below the branch places of F / E are all marked exactly when F is an algebraic Belyi pair with constant field k.

References

• E. Girondo and G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, LMS Student Texts 79, Cambridge University Press, 2012, Chapter 3.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Definitions 3.1.5 and 3.1.13.

noncomputable def TauCeti.Place.zeroOneInfty (k : Type u_1) [Field k] : Set (Place k (RatFunc k))

The three marked places of the rational function field k(t): the places t = 0 and t = 1 of the monic irreducibles t and t - 1, and the place t = ∞ at infinity. A Belyi map is unramified over every other place.

theorem TauCeti.Place.mem_zeroOneInfty_iff {k : Type u_1} [Field k] {P : Place k (RatFunc k)} : P ∈ zeroOneInfty k ↔ P = adicOfIrreducible ⋯ ∨ P = adicOfIrreducible ⋯ ∨ P = infty k

@[simp]

theorem TauCeti.Place.adicOfIrreducible_X_mem_zeroOneInfty {k : Type u_1} [Field k] : adicOfIrreducible ⋯ ∈ zeroOneInfty k

@[simp]

theorem TauCeti.Place.adicOfIrreducible_X_sub_one_mem_zeroOneInfty {k : Type u_1} [Field k] : adicOfIrreducible ⋯ ∈ zeroOneInfty k

@[simp]

theorem TauCeti.Place.infty_mem_zeroOneInfty {k : Type u_1} [Field k] : infty k ∈ zeroOneInfty k

@[simp]

theorem TauCeti.Place.adicOfIrreducible_X_sub_C_mem_zeroOneInfty_iff {k : Type u_1} [Field k] {a : k} : adicOfIrreducible ⋯ ∈ zeroOneInfty k ↔ a = 0 ∨ a = 1

The place t = a of k(t) is one of the three marked places exactly when a is 0 or 1.

noncomputable def TauCeti.Place.markedPlace (k : Type u_1) [Field k] : Fin 3 → Place k (RatFunc k)

The three marked places t = 0, t = 1 and t = ∞ of k(t), numbered 0, 1 and 2: the numbering of the branch points used for permutation triples.

@[simp]

theorem TauCeti.Place.markedPlace_zero {k : Type u_1} [Field k] : markedPlace k 0 = adicOfIrreducible ⋯

@[simp]

theorem TauCeti.Place.markedPlace_one {k : Type u_1} [Field k] : markedPlace k 1 = adicOfIrreducible ⋯

@[simp]

theorem TauCeti.Place.markedPlace_two {k : Type u_1} [Field k] : markedPlace k 2 = infty k

theorem TauCeti.Place.range_markedPlace (k : Type u_1) [Field k] : Set.range (markedPlace k) = zeroOneInfty k

The numbered marked places are exactly the three marked places.

theorem TauCeti.Place.notMem_zeroOneInfty_iff {k : Type u_1} [Field k] {P : Place k (RatFunc k)} : P ∉ zeroOneInfty k ↔ P.ord RatFunc.X = 0 ∧ P.ord (RatFunc.X - 1) = 0

The marked places are the zeros and poles of t and t - 1: a place of k(t) is none of t = 0, t = 1 and t = ∞ exactly when both t and t - 1 have order zero there.

theorem TauCeti.Place.valuation_X_mul_X_sub_one_of_notMem_zeroOneInfty {k : Type u_1} [Field k] {P : Place k (RatFunc k)} (hP : P ∉ zeroOneInfty k) : P.valuation (RatFunc.X * (RatFunc.X - 1)) = 1

Away from 0, 1 and ∞, the function t (t - 1) is a unit.

structure TauCeti.IsAlgebraicBelyiPair (k : Type u_1) (F : Type u_2) [Field k] [CharZero k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] : Prop

An algebraic Belyi pair over a field k of characteristic zero: a function field F / k with exact constant field k, finite over the rational function field k(t) through the given Algebra (RatFunc k) F structure, in which every place lying over a place of k(t) other than t = 0, t = 1 and t = ∞ has ramification index 1.

The branch locus is only required to be contained in the three marked places. The base field is pinned to characteristic zero, where F / k(t) is automatically separable; in characteristic p the power map t ↦ t ^ p is inseparable and 4t(1 - t) is constant in characteristic 2.

• isIntegrallyClosedIn : IsIntegrallyClosedIn k F

  The constant field of F is exactly k.

• ramificationIdx_eq_one {P : Place k F} : Place.restrict k (RatFunc k) P ∉ Place.zeroOneInfty k → Place.ramificationIdx (RatFunc k) P = 1

  Every place of F over a place of k(t) other than 0, 1, ∞ is unramified.

theorem TauCeti.isAlgebraicBelyiPair_iff {k : Type u_1} {F : Type u_2} [Field k] [CharZero k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] : IsAlgebraicBelyiPair k F ↔ IsIntegrallyClosedIn k F ∧ ∀ P ∉ Place.zeroOneInfty k, P.IsUnramified

An algebraic Belyi pair is a function field unramified outside 0, 1 and ∞: F is an algebraic Belyi pair exactly when its constant field is k and every place of k(t) other than the three marked places is unramified in F. In characteristic zero the residue field extensions are separable, so being unramified is just having ramification index 1 at every place above, of which there is at least one.

theorem TauCeti.isAlgebraicBelyiPair_iff_branchPlaces_subset {k : Type u_1} {F : Type u_2} [Field k] [CharZero k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] : IsAlgebraicBelyiPair k F ↔ IsIntegrallyClosedIn k F ∧ Place.branchPlaces k F ⊆ Place.zeroOneInfty k

An algebraic Belyi pair is branched only over 0, 1 and ∞: F is an algebraic Belyi pair exactly when its constant field is k and every branch place of F / k(t) is one of the three marked places.

theorem TauCeti.IsAlgebraicBelyiPair.of_equiv_equiv {k : Type u_1} {F : Type u_2} [Field k] [CharZero k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] {F' : Type u_3} [Field F'] [Algebra k F'] [Algebra (RatFunc k) F'] [IsScalarTower k (RatFunc k) F'] [FiniteDimensional (RatFunc k) F'] (h : IsAlgebraicBelyiPair k F) (σ : Gal(RatFunc k/k)) (hσ : Set.MapsTo (Place.map σ) (Place.zeroOneInfty k) (Place.zeroOneInfty k)) (e : F ≃ₐ[k] F') (he : ∀ (x : RatFunc k), e ((algebraMap (RatFunc k) F) x) = (algebraMap (RatFunc k) F') (σ x)) : IsAlgebraicBelyiPair k F'

Transport of Belyi pairs along a commutative square of isomorphisms. Let σ : k(t) ≃ₐ[k] k(t) carry the three marked places into themselves, and let e : F ≃ₐ[k] F' restrict to σ on k(t). If F is an algebraic Belyi pair then so is F'.

For F' = F as fields, this changes the Belyi function t of F into its image under an automorphism of k(t); see TauCeti.IsAlgebraicBelyiPair.of_branchPointAut.

theorem TauCeti.IsAlgebraicBelyiPair.of_algEquiv {k : Type u_1} {F : Type u_2} [Field k] [CharZero k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] {F' : Type u_3} [Field F'] [Algebra k F'] [Algebra (RatFunc k) F'] [IsScalarTower k (RatFunc k) F'] [FiniteDimensional (RatFunc k) F'] (h : IsAlgebraicBelyiPair k F) (e : F ≃ₐ[RatFunc k] F') : IsAlgebraicBelyiPair k F'

Being an algebraic Belyi pair is invariant under isomorphism over k(t).

theorem TauCeti.isAlgebraicBelyiPair_ratFunc (k : Type u_1) [Field k] [CharZero k] : IsAlgebraicBelyiPair k (RatFunc k)

The trivial Belyi pair: the rational function field k(t) over itself, the Belyi map of degree one, is an algebraic Belyi pair.

theorem TauCeti.IsAlgebraicBelyiPair.of_isScalarTower {k : Type u_1} {F : Type u_2} [Field k] [CharZero k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] {E : Type u_4} [Field E] [Algebra k E] [Algebra (RatFunc k) E] [IsScalarTower k (RatFunc k) E] [FiniteDimensional (RatFunc k) E] [Algebra E F] [IsScalarTower k E F] [IsScalarTower (RatFunc k) E F] (hE : IsAlgebraicBelyiPair k E) (hF : IsIntegrallyClosedIn k F) (h : ∀ (P : Place k F), Place.restrict k (RatFunc k) P ∉ Place.zeroOneInfty k → Place.ramificationIdx E P = 1) : IsAlgebraicBelyiPair k F

Composing a Belyi map with a cover unramified over its unmarked fibres: if E / k(t) is an algebraic Belyi pair and F / E is a finite extension, with exact constant field k, in which every place of F over a place of k(t) other than t = 0, t = 1 and t = ∞ is unramified over E, then F / k(t) is an algebraic Belyi pair.

theorem TauCeti.isAlgebraicBelyiPair_iff_of_isScalarTower {k : Type u_1} {F : Type u_2} [Field k] [CharZero k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] {E : Type u_4} [Field E] [Algebra k E] [Algebra (RatFunc k) E] [IsScalarTower k (RatFunc k) E] [FiniteDimensional (RatFunc k) E] [Algebra E F] [IsScalarTower k E F] [IsScalarTower (RatFunc k) E F] : IsAlgebraicBelyiPair k F ↔ IsIntegrallyClosedIn k F ∧ Place.branchPlaces k E ⊆ Place.zeroOneInfty k ∧ (fun (P : Place k E) => Place.restrict k (RatFunc k) P) '' Place.branchPlaces k F ⊆ Place.zeroOneInfty k

Belyi maps through an intermediate cover: for a tower k(t) ⊆ E ⊆ F, the field F is an algebraic Belyi pair exactly when its constant field is k, the branch places of E / k(t) are among 0, 1 and ∞, and so are the places of k(t) below the branch places of F / E. This follows from the branch-value formula Place.branchPlaces_eq_image_union for a composite of finite maps of curves f : X → Y and g : Y → ℙ¹.