Permuting the branch points of an algebraic Belyi pair

The six linear fractional transformations

ρ	0, 1, ∞ go to	m(t)
1	0, 1, ∞	t
swap 0 1	1, 0, ∞	1 - t
swap 1 2	0, ∞, 1	t / (t - 1)
swap 0 2	∞, 1, 0	1 / t
finRotate 3	∞, 0, 1	(t - 1) / t
(finRotate 3)⁻¹	1, ∞, 0	1 / (1 - t)

are the Möbius transformations permuting 0, 1, ∞, defined over the prime field. Numbering 0, 1, ∞ as 0, 1, 2 : Fin 3, the transformation m attached to ρ sends the point numbered ρ i to the point numbered i. Its substitution t ↦ m(t) is the automorphism RatFunc.branchPointAut ρ of k(t), and ρ ↦ RatFunc.branchPointAut ρ is a group homomorphism from the symmetric group on the three branch points; it is constructed with the other linear fractional transformations in TauCeti.FieldTheory.RatFunc.Mobius.

Postcomposing a Belyi map β with m gives the Belyi map m ∘ β on the same curve. Its fibre over the point numbered i is the fibre of β over the point numbered ρ i, so m ∘ β is the reordering of the branch points of β along ρ, in the indexing convention of TauCeti.PermutationTriple.reindexBranchPoints, whose component over i comes from the old component over ρ i. The inversion is visible on the two three-cycles: the reordering finRotate 3, which is 0 → 1 → ∞ → 0, is realised by (t - 1) / t, whose own permutation of the points is 0 → ∞ → 1 → 0.

On function fields, m ∘ β replaces the embedding φ : k(t) → F by φ ∘ m. This file states this along an isomorphism e : F ≃ₐ[k] F' with e (φ (m x)) = φ' x, so that F' may be F itself with the new algebra structure, or any other model of it.

Main results

• TauCeti.Place.map_branchPointAut_markedPlace: RatFunc.branchPointAut ρ carries the marked place numbered i to the marked place numbered ρ i.
• TauCeti.IsAlgebraicBelyiPair.of_branchPointAut: reordering the branch points of an algebraic Belyi pair gives an algebraic Belyi pair.
• TauCeti.finrank_eq_of_branchPointAut: of the same degree.
• TauCeti.Place.restrict_map_eq_markedPlace_iff_of_branchPointAut, TauCeti.Place.ramificationIdx_map_of_branchPointAut and TauCeti.Place.relativeDegree_map_of_branchPointAut: the places over the branch point numbered i of the new pair are those over the branch point numbered ρ i of the old one, with the same ramification indices and relative degrees.
• TauCeti.Place.localData_markedPlace_of_branchPointAut: hence the local data (e, f) over the branch point numbered i of the new pair are those over the branch point numbered ρ i of the old one.

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, §4.4.
• S. K. Lando and A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer, 2004, §1.5.

@[simp]

theorem TauCeti.Place.map_branchPointAut_markedPlace {k : Type u_1} [Field k] (ρ : Equiv.Perm (Fin 3)) (i : Fin 3) : map ((RatFunc.branchPointAut k) ρ) (markedPlace k i) = markedPlace k (ρ i)

The branch-point substitutions permute the marked places: RatFunc.branchPointAut ρ carries the marked place numbered i to the marked place numbered ρ i.

theorem TauCeti.Place.mapsTo_branchPointAut_zeroOneInfty {k : Type u_1} [Field k] (ρ : Equiv.Perm (Fin 3)) : Set.MapsTo (map ((RatFunc.branchPointAut k) ρ)) (zeroOneInfty k) (zeroOneInfty k)

The branch-point substitutions carry the three marked places into themselves.

theorem TauCeti.Place.restrict_map_eq_markedPlace_iff_of_branchPointAut {k : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra (RatFunc k) F] [Algebra (RatFunc k) F'] (ρ : Equiv.Perm (Fin 3)) (e : F ≃ₐ[k] F') (he : ∀ (x : RatFunc k), e ((algebraMap (RatFunc k) F) (((RatFunc.branchPointAut k) ρ) x)) = (algebraMap (RatFunc k) F') x) [IsScalarTower k (RatFunc k) F] [IsScalarTower k (RatFunc k) F'] [Algebra.IsIntegral (RatFunc k) F] [Algebra.IsIntegral (RatFunc k) F'] {P : Place k F} {i : Fin 3} : restrict k (RatFunc k) (map e P) = markedPlace k i ↔ restrict k (RatFunc k) P = markedPlace k (ρ i)

Reordering the branch points keeps the places above them: when e : F ≃ₐ[k] F' replaces the Belyi function t of F by m(t), a place of F lies over the branch point numbered ρ i exactly when its transport to F' lies over the branch point numbered i.

theorem TauCeti.Place.ramificationIdx_map_of_branchPointAut {k : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra (RatFunc k) F] [Algebra (RatFunc k) F'] (ρ : Equiv.Perm (Fin 3)) (e : F ≃ₐ[k] F') (he : ∀ (x : RatFunc k), e ((algebraMap (RatFunc k) F) (((RatFunc.branchPointAut k) ρ) x)) = (algebraMap (RatFunc k) F') x) (P : Place k F) : ramificationIdx (RatFunc k) (map e P) = ramificationIdx (RatFunc k) P

Reordering the branch points keeps the ramification indices: when e : F ≃ₐ[k] F' replaces the Belyi function t of F by m(t), a place of F and its transport to F' have the same ramification index over k(t).

theorem TauCeti.Place.relativeDegree_map_of_branchPointAut {k : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra (RatFunc k) F] [Algebra (RatFunc k) F'] (ρ : Equiv.Perm (Fin 3)) (e : F ≃ₐ[k] F') (he : ∀ (x : RatFunc k), e ((algebraMap (RatFunc k) F) (((RatFunc.branchPointAut k) ρ) x)) = (algebraMap (RatFunc k) F') x) [IsScalarTower k (RatFunc k) F] [IsScalarTower k (RatFunc k) F'] [Algebra.IsIntegral (RatFunc k) F] [Algebra.IsIntegral (RatFunc k) F'] (P : Place k F) : relativeDegree k (RatFunc k) (map e P) = relativeDegree k (RatFunc k) P

Reordering the branch points keeps the relative degrees: when e : F ≃ₐ[k] F' replaces the Belyi function t of F by m(t), a place of F and its transport to F' have the same relative degree over k(t).

theorem TauCeti.Place.localData_markedPlace_of_branchPointAut {k : Type u_2} {F : Type u_3} {F' : Type u_4} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra (RatFunc k) F] [Algebra (RatFunc k) F'] (ρ : Equiv.Perm (Fin 3)) (e : F ≃ₐ[k] F') (he : ∀ (x : RatFunc k), e ((algebraMap (RatFunc k) F) (((RatFunc.branchPointAut k) ρ) x)) = (algebraMap (RatFunc k) F') x) [IsScalarTower k (RatFunc k) F] [IsScalarTower k (RatFunc k) F'] [FiniteDimensional (RatFunc k) F] [FiniteDimensional (RatFunc k) F'] (i : Fin 3) : localData k (RatFunc k) (markedPlace k i) = localData k (RatFunc k) (markedPlace k (ρ i))

Reordering the branch points permutes the local data: when e : F ≃ₐ[k] F' replaces the Belyi function t of F by m(t), the multiset of pairs (e, f) of ramification indices and relative degrees at the places of F' over the branch point numbered i is the one at the places of F over the branch point numbered ρ i.

theorem TauCeti.finrank_eq_of_branchPointAut {k : Type u_1} {F : Type u_2} {F' : Type u_3} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra (RatFunc k) F] [Algebra (RatFunc k) F'] (ρ : Equiv.Perm (Fin 3)) (e : F ≃ₐ[k] F') (he : ∀ (x : RatFunc k), e ((algebraMap (RatFunc k) F) (((RatFunc.branchPointAut k) ρ) x)) = (algebraMap (RatFunc k) F') x) : Module.finrank (RatFunc k) F' = Module.finrank (RatFunc k) F

Reordering the branch points keeps the degree: when e : F ≃ₐ[k] F' replaces the Belyi function t of F by m(t), the degrees of F and F' over k(t) agree.

theorem TauCeti.IsAlgebraicBelyiPair.of_branchPointAut {k : Type u_1} {F : Type u_2} {F' : Type u_3} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra (RatFunc k) F] [Algebra (RatFunc k) F'] (ρ : Equiv.Perm (Fin 3)) (e : F ≃ₐ[k] F') (he : ∀ (x : RatFunc k), e ((algebraMap (RatFunc k) F) (((RatFunc.branchPointAut k) ρ) x)) = (algebraMap (RatFunc k) F') x) [CharZero k] [IsScalarTower k (RatFunc k) F] [IsScalarTower k (RatFunc k) F'] [FiniteDimensional (RatFunc k) F] [FiniteDimensional (RatFunc k) F'] (h : IsAlgebraicBelyiPair k F) : IsAlgebraicBelyiPair k F'

Reordering the branch points of an algebraic Belyi pair: if F is an algebraic Belyi pair with Belyi function t, and e : F ≃ₐ[k] F' sends m(t) to the Belyi function of F', where m is the substitution RatFunc.branchPointAut ρ, then F' is an algebraic Belyi pair.

Taking F' = F with the algebra structure φ ∘ m, this is the postcomposition m ∘ β of the Belyi map β. Its fibres over the marked places are those of β reordered along ρ (TauCeti.Place.restrict_map_eq_markedPlace_iff_of_branchPointAut).