Belyi maps, dessins d'enfants, and three-point covers

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

DefinitionAnalytic Belyi pairs are classified by finite covers of the thrice-punctured sphere#

Restricting the Belyi map over ℂ ∖ {0, 1} and filling the punctures are inverse bijections between isomorphism classes of analytic Belyi pairs of degree n and isomorphism classes of connected degree-n covers of ℂ ∖ {0, 1}.

TauCeti.AnalyticBelyiPair.isoClassEquivConnectedCoverClass (n : ℕ) :
  Quotient (TauCeti.AnalyticBelyiPair.isoSetoid n) ≃
    TauCeti.ConnectedCoverClass TauCeti.ThricePuncturedSphere.basePt n
Lean

Formalized in Tau Ceti as TauCeti.AnalyticBelyiPair.isoClassEquivConnectedCoverClass.

Sources
LeanTauCeti.AnalyticBelyiPair.isoClassEquivConnectedCoverClass
Uses 8 · Used by 1
Proof usesThe analytic inverse function theorem · The identity theorem for Riemann surfaces · The isomorphism π₁(S¹) ≃* ℤ is the degree · The open mapping theorem · Osgood's lemma · Riemann's removable singularity theorem on complex curves · Rouché's theorem for a disc, classical form · TauCeti.CoveringSpace
Used byThe superelliptic curve is the analytic Belyi pair of the torus triple

DefinitionConnected covers of ℂ ∖ {0, 1} of degree n up to isomorphism are classified by the isomorphism classes of connected triples of degree n# 

TauCeti.ConnectedCoverClass.isoClassEquiv {n : ℕ} :
  TauCeti.ConnectedCoverClass TauCeti.ThricePuncturedSphere.basePt n ≃ TauCeti.ConnectedIsoClass n
Lean

Formalized in Tau Ceti as TauCeti.ConnectedCoverClass.isoClassEquiv.

Sources
LeanTauCeti.ConnectedCoverClass.isoClassEquiv
Uses 3 · Used by 1
Proof usesThe based Seifert--van Kampen theorem · The isomorphism π₁(S¹) ≃* ℤ is the degree · TauCeti.CoveringSpace
Used byThe superelliptic curve is the analytic Belyi pair of the torus triple

TheoremPolynomial Belyification of algebraic numbers#

Every finite set S of elements algebraic over ℚ in a field K, such as a finite subset of AlgebraicClosure ℚ, is carried into {0, 1} by a nonconstant polynomial q with rational coefficients whose critical values, in every field of characteristic zero, lie in {0, 1}.

TauCeti.exists_polynomial_aeval_mem_criticalValues_subset.{u, u_1} {K : Type u_1} [Field K]
  [Algebra ℚ K] {S : Finset K} (hS : ∀ s ∈ S, IsIntegral ℚ s) :
  ∃ q,
    0 < q.natDegree ∧
      (∀ s ∈ S, (Polynomial.aeval s) q ∈ {0, 1}) ∧
        ∀ (L : Type u) [inst : Field L] [inst_1 : Algebra ℚ L],
          Polynomial.criticalValues L q ⊆ {0, 1}
Lean

Formalized in Tau Ceti as TauCeti.exists_polynomial_aeval_mem_criticalValues_subset.

Sources
LeanTauCeti.exists_polynomial_aeval_mem_criticalValues_subset
Uses 1 · Used by 1
Proof usesBelyi's degree reduction
Used byBelyi's theorem, existence direction

TheoremBelyi's degree reduction#

Every finite set S of elements algebraic over a perfect field F, such as a finite subset of AlgebraicClosure ℚ, is carried into F by a polynomial q ∈ F[X] with q′ ≠ 0, in particular nonconstant, whose critical values in every field extension of F also lie in F.

TauCeti.exists_polynomial_aeval_mem_range.{w, u_1, u_2} {F : Type u_1} [Field F] [PerfectField F]
  {K : Type u_2} [Field K] [Algebra F K] {S : Finset K} (hS : ∀ s ∈ S, IsIntegral F s) :
  ∃ q,
    Polynomial.derivative q ≠ 0 ∧
      (∀ s ∈ S, (Polynomial.aeval s) q ∈ Set.range ⇑(algebraMap F K)) ∧
        ∀ (L : Type w) [inst : Field L] [inst_1 : Algebra F L] (x : L),
          (Polynomial.aeval x) (Polynomial.derivative q) = 0 →
            (Polynomial.aeval x) q ∈ Set.range ⇑(algebraMap F L)
Lean

Formalized in Tau Ceti as TauCeti.exists_polynomial_aeval_mem_range.

Sources
LeanTauCeti.exists_polynomial_aeval_mem_range
Used by 1
Used byPolynomial Belyification of algebraic numbers

TheoremThe superelliptic curve is the analytic Belyi pair of the torus triple#

an analytic Belyi pair is isomorphic to the superelliptic curve exactly when its monodromy triple is isomorphic to TauCeti.PermutationTriple.torusTriple, for any numbering of its fibre over 1/2.

TauCeti.AnalyticBelyiPair.nonempty_iso_superelliptic_iff {P : TauCeti.AnalyticBelyiPair}
  (ν : ↑(P.restrict ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin 4) :
  Nonempty (P.Iso TauCeti.AnalyticBelyiPair.superelliptic) ↔
    TauCeti.PermutationTriple.IsoClass.mk (⋯.monodromyTriple ν) =
      TauCeti.PermutationTriple.IsoClass.mk TauCeti.PermutationTriple.torusTriple
Lean

Formalized in Tau Ceti as TauCeti.AnalyticBelyiPair.nonempty_iso_superelliptic_iff.

Sources
LeanTauCeti.AnalyticBelyiPair.nonempty_iso_superelliptic_iff
Uses 11
Proof usesAnalytic Belyi pairs are classified by finite covers of the thrice-punctured sphere · The analytic implicit root theorem · The analytic inverse function theorem · Connected covers of ℂ ∖ {0, 1} of degree n up to isomorphism are classified by the isomorphism classes of connected triples of degree n · The identity theorem for Riemann surfaces · The isomorphism π₁(S¹) ≃* ℤ is the degree · The open mapping theorem · Osgood's lemma · Riemann's removable singularity theorem on complex curves · Rouché's theorem for a disc, classical form · TauCeti.CoveringSpace

StructureTauCeti.RiemannSurface.MeromorphicFunction#

A meromorphic function on a Riemann surface X: a holomorphic map X → OnePoint ℂ to the Riemann sphere which is not the constant map ∞. On a connected X these form a field (TauCeti.RiemannSurface.MeromorphicFunction.instField).

TauCeti.RiemannSurface.MeromorphicFunction.{u_1} (X : Type u_1) [TopologicalSpace X]
  [ChartedSpace ℂ X] : Type u_1
Lean

Formalized in Tau Ceti as TauCeti.RiemannSurface.MeromorphicFunction.

Sources
LeanTauCeti.RiemannSurface.MeromorphicFunction

StructureTauCeti.IsAlgebraicBelyiPair#

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.

TauCeti.IsAlgebraicBelyiPair.{u_1, u_2} (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
Lean

Formalized in Tau Ceti as TauCeti.IsAlgebraicBelyiPair.

Sources
LeanTauCeti.IsAlgebraicBelyiPair
Used by 2
Used byBelyi's theorem, existence direction · The Galois conjugate of an algebraic Belyi pair is an algebraic Belyi pair

TheoremThe 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.

TauCeti.IsAlgebraicBelyiPair.of_mapRingEquiv.{u_1, u_2, u_3, u_4} {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') ((TauCeti.RatFunc.mapRingEquiv σ) x))
  [CharZero k] [CharZero k'] [FiniteDimensional (RatFunc k) F] [FiniteDimensional (RatFunc k') F']
  (h : TauCeti.IsAlgebraicBelyiPair k F) : TauCeti.IsAlgebraicBelyiPair k' F'
Lean

Formalized in Tau Ceti as TauCeti.IsAlgebraicBelyiPair.of_mapRingEquiv.

Sources
LeanTauCeti.IsAlgebraicBelyiPair.of_mapRingEquiv
Uses 1
Statement usesTauCeti.IsAlgebraicBelyiPair

StructureTauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt#

The record r is a valid row for the passport of the connected triple t: the triple t is one of the stored triples, the certificate data of r are correct on the sheets of t, and every other certified field is the corresponding invariant of t.

The aggregations numOrbits and maxdegbf, and the strings plabel, primitivization and autGroup, are not constrained.

TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt {n : ℕ}
  (r : TauCeti.PermutationTriple.LMFDB.PassportRecord n) (t : TauCeti.ConnectedTriple n) : Prop
Lean

Formalized in Tau Ceti as TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.

Sources
LeanTauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt

StructureTauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor#

A row is valid for the passport P when its stored degree is the degree, its stored orbit size is its number of stored embedding entries, it stores at least one triple, every stored triple denotes a connected triple with passport P, its stored cycle notation writes the stored triples position by position, the stored partitions are those of P, and the stored genus is the genus of every stored triple.

The labels, the base field, the equations, and the embedding values are not constrained.

TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor {n : ℕ}
  (r : TauCeti.PermutationTriple.LMFDB.BelyiRecord n) (P : TauCeti.PassportSpec n) : Prop
Lean

Formalized in Tau Ceti as TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor.

Sources
LeanTauCeti.PermutationTriple.LMFDB.BelyiRecord.IsValidFor

TheoremBelyi's theorem, existence direction#

over a field k algebraic over ℚ, such as an algebraic closure of ℚ or a number field, every function field F / k with exact constant field k admits a Belyi map: there is β ∈ F transcendental over k such that F over k(t), with t acting as β, is an algebraic Belyi pair.

TauCeti.IsFunctionField.exists_isAlgebraicBelyiPair.{u, v} {k : Type u} {F : Type v} [Field k]
  [CharZero k] [Field F] [Algebra k F] [Algebra.IsAlgebraic ℚ k] (hF : TauCeti.IsFunctionField k F)
  (hc : IsIntegrallyClosedIn k F) :
  ∃ β, ∃ (hβ : Transcendental k β), TauCeti.IsAlgebraicBelyiPair k F
Lean

Formalized in Tau Ceti as TauCeti.IsFunctionField.exists_isAlgebraicBelyiPair.

Other forms

Belyi's theorem, existence direction, for a given function. Formalized in Tau Ceti as TauCeti.IsFunctionField.exists_polynomial_isAlgebraicBelyiPair.

TauCeti.IsFunctionField.exists_polynomial_isAlgebraicBelyiPair.{u, v} {k : Type u} {F : Type v}
  [Field k] [CharZero k] [Field F] [Algebra k F] [Algebra.IsAlgebraic ℚ k]
  (hF : TauCeti.IsFunctionField k F) (hc : IsIntegrallyClosedIn k F) {x : F}
  (hx : Transcendental k x) :
  ∃ q,
    0 < q.natDegree ∧
      ∀ [inst : Algebra (RatFunc k) F] [inst_1 : IsScalarTower k (RatFunc k) F]
        [inst_2 : FiniteDimensional (RatFunc k) F],
        (algebraMap (RatFunc k) F) RatFunc.X =
            (Polynomial.aeval x) (Polynomial.map (algebraMap ℚ k) q) →
          TauCeti.IsAlgebraicBelyiPair k F
Sources
LeanTauCeti.IsFunctionField.exists_isAlgebraicBelyiPair · TauCeti.IsFunctionField.exists_polynomial_isAlgebraicBelyiPair
Uses 5
Statement usesTauCeti.IsAlgebraicBelyiPair
Proof usesDedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · Polynomial Belyification of algebraic numbers · The weak approximation theorem

TheoremThe Riemann–Hurwitz formula for a filled cover#

For a connected cover of degree n, whose monodromy triple has genus g, the total ramification ∑ (e - 1) over the added points satisfies 2 g - 2 = -2 n + ∑ (e - 1). This is the shape of the Riemann–Hurwitz formula for a degree-n branched cover of the Riemann sphere, which has genus 0.

TauCeti.FilledCover.two_mul_genus_sub_two.{u_1} {E : Type u_1} [TopologicalSpace E]
  {p : E → TauCeti.ThricePuncturedSphere} (hp : IsCoveringMap p) {n : ℕ}
  (ν : ↑(p ⁻¹' {TauCeti.ThricePuncturedSphere.basePt}) ≃ Fin n) [PathConnectedSpace E]
  [Fintype (TauCeti.FilledPoint p)] :
  2 * ↑(hp.monodromyTriple ν).genus - 2 = -2 * ↑n + ∑ i, (↑(TauCeti.FilledCover.degree p i) - 1)
Lean

Formalized in Tau Ceti as TauCeti.FilledCover.two_mul_genus_sub_two.

Sources
LeanTauCeti.FilledCover.two_mul_genus_sub_two
Uses 2
Proof usesThe Euler bound for a pair of permutations · The isomorphism π₁(S¹) ≃* ℤ is the degree

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.