Galois conjugation of algebraic Belyi pairs

Let σ : k ≃+* k' be an isomorphism of fields of characteristic zero, for instance an element of the absolute Galois group of ℚ acting on an algebraic closure. The conjugate of an algebraic Belyi pair F / k(t) along σ is the same field F, with its structure maps from k and from k(t) precomposed with σ⁻¹ and with the coefficient map of σ⁻¹, and with the same distinguished function t. This is the function-field form of base change of a Belyi map along σ. Here a conjugate is described by any field F' over k'(t) together with a ring isomorphism τ : F ≃+* F' carrying k(t) onto k'(t) by the coefficient map RatFunc.mapRingEquiv σ; for the conjugate structure on F itself, τ is the identity.

The coefficient map fixes t and t - 1, so the bijection it induces between the places of k(t) and those of k'(t) fixes each of the three marked places t = 0, t = 1 and t = ∞ (TauCeti.Place.equivOfRingEquiv_mapRingEquiv_markedPlace); the marked places are k-rational, which is why conjugation preserves them. Consequently conjugation carries algebraic Belyi pairs to algebraic Belyi pairs (TauCeti.IsAlgebraicBelyiPair.of_mapRingEquiv) of the same degree (TauCeti.finrank_eq_of_mapRingEquiv, in TauCeti.FieldTheory.RatFunc.Map). Place by place, τ carries the places of F over the marked place numbered i bijectively onto the places of F' over the marked place numbered i (TauCeti.Place.restrict_equivOfRingEquiv_eq_markedPlace_iff), with the same ramification indices (TauCeti.Place.ramificationIdx_equivOfRingEquiv_of_comm) and residue degrees (TauCeti.Place.degree_equivOfRingEquiv).

Conjugation does not in general preserve the isomorphism class of a Belyi pair: the action of the absolute Galois group on isomorphism classes, its orbits and stabilizers, and the field of moduli are built on top of this transport.

Main results

• TauCeti.Place.equivOfRingEquiv_mapRingEquiv_markedPlace: conjugation fixes the marked places.
• TauCeti.IsAlgebraicBelyiPair.of_mapRingEquiv: the conjugate of an algebraic Belyi pair is an algebraic Belyi pair.
• TauCeti.Place.restrict_equivOfRingEquiv_eq_markedPlace_iff: conjugation keeps the fibres over the marked places.

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.
• B. Köck, Belyi's theorem revisited, Beiträge zur Algebra und Geometrie 45 (2004), 253–265.

@[simp]

theorem TauCeti.Place.equivOfRingEquiv_mapRingEquiv_markedPlace {k : Type u_1} {k' : Type u_2} [Field k] [Field k'] (σ : k ≃+* k') (i : Fin 3) : (equivOfRingEquiv σ (RatFunc.mapRingEquiv σ) ⋯) (markedPlace k i) = markedPlace k' i

Conjugation fixes the marked places: the bijection between the places of k(t) and those of k'(t) induced by the coefficient map of σ : k ≃+* k' carries the marked place numbered i to the marked place numbered i.

@[simp]

theorem TauCeti.Place.equivOfRingEquiv_mapRingEquiv_mem_zeroOneInfty_iff {k : Type u_1} {k' : Type u_2} [Field k] [Field k'] (σ : k ≃+* k') {P : Place k (RatFunc k)} : (equivOfRingEquiv σ (RatFunc.mapRingEquiv σ) ⋯) P ∈ zeroOneInfty k' ↔ P ∈ zeroOneInfty k

Conjugation preserves the three marked places as a set.

theorem TauCeti.Place.restrict_equivOfRingEquiv_eq_markedPlace_iff {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] [Algebra (RatFunc k) F] [Algebra (RatFunc k') F'] [IsScalarTower k (RatFunc k) F] [IsScalarTower k' (RatFunc k') F'] (σ : k ≃+* k') (τ : F ≃+* F') (hτ : ∀ (x : RatFunc k), τ ((algebraMap (RatFunc k) F) x) = (algebraMap (RatFunc k') F') ((RatFunc.mapRingEquiv σ) x)) [Algebra.IsIntegral (RatFunc k) F] [Algebra.IsIntegral (RatFunc k') F'] {P : Place k F} {i : Fin 3} : restrict k' (RatFunc k') ((equivOfRingEquiv σ τ ⋯) P) = markedPlace k' i ↔ restrict k (RatFunc k) P = markedPlace k i

Conjugation keeps the fibres over the marked places: if τ : F ≃+* F' carries k(t) onto k'(t) by the coefficient map of σ, then a place of F lies over the marked place numbered i exactly when its transport along τ lies over the marked place numbered i.

theorem TauCeti.IsAlgebraicBelyiPair.of_mapRingEquiv {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra k' F'] [Algebra (RatFunc k) F] [Algebra (RatFunc k') F'] [IsScalarTower k (RatFunc k) F] [IsScalarTower k' (RatFunc k') F'] (σ : k ≃+* k') (τ : F ≃+* F') (hτ : ∀ (x : RatFunc k), τ ((algebraMap (RatFunc k) F) x) = (algebraMap (RatFunc k') F') ((RatFunc.mapRingEquiv σ) x)) [CharZero k] [CharZero k'] [FiniteDimensional (RatFunc k) F] [FiniteDimensional (RatFunc k') F'] (h : IsAlgebraicBelyiPair k F) : IsAlgebraicBelyiPair k' F'

The Galois conjugate of an algebraic Belyi pair is an algebraic Belyi pair: if F is an algebraic Belyi pair over k, and τ : F ≃+* F' carries k(t) onto k'(t) by the coefficient map of σ : k ≃+* k', then F' is an algebraic Belyi pair over k'.

Taking F' = F with its structure maps precomposed with σ⁻¹ and τ the identity, this is the conjugation of a Belyi pair by an automorphism σ of the constants.