Examples of dessins d'enfants

This file realizes the standard small permutation triples as finite bipartite ribbon graphs and computes their cells. In positive degree n, the cyclic dessin is an n-star: one black vertex, n white vertices, n edges, and one face; in degree zero it is the formal empty dessin, with no edges, vertices, or faces. The dessin of z ↦ 4z(1 - z) is a two-edge segment. The degree-four Euclidean example has one vertex of each colour and two faces, so it lies on a torus. The degree-three symmetric example has one black vertex, two white vertices, and two faces.

The definitions use the general construction from permutation triples. The cell counts below spell out the resulting graphs without choosing representatives for their quotient vertex and face types, and the Euler characteristic and genus computations agree with the corresponding triple invariants. The definitions are computable and exposed, so their invariants also evaluate directly: for instance, torusDessin.genus = 1 holds by decide, and #eval torusDessin.eulerChar returns 0.

References

• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer 2004, §1.3 and §1.5.
• E. Girondo, G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, London Mathematical Society Student Texts 79, Cambridge University Press 2012, §4.2.

The cyclic star

def TauCeti.BipartiteRibbonGraph.cyclicDessin (n : ℕ) : BipartiteRibbonGraph

The dessin of the cyclic triple of degree n. In positive degree it is the n-star.

Equations

• TauCeti.BipartiteRibbonGraph.cyclicDessin n = (TauCeti.PermutationTriple.cyclicTriple n).ribbonGraph

theorem TauCeti.BipartiteRibbonGraph.cyclicDessin_def {n : ℕ} : cyclicDessin n = (PermutationTriple.cyclicTriple n).ribbonGraph

The cyclic dessin is the ribbon graph constructed from the cyclic permutation triple.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_E_cyclicDessin {n : ℕ} : Fintype.card (cyclicDessin n).E = n

The cyclic dessin has n edges.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_B_cyclicDessin {n : ℕ} (hn : n ≠ 0) : Fintype.card (cyclicDessin n).B = 1

In positive degree, the cyclic dessin has one black vertex.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_B_cyclicDessin_zero : Fintype.card (cyclicDessin 0).B = 0

The degree-zero cyclic dessin has no black vertices.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_W_cyclicDessin {n : ℕ} : Fintype.card (cyclicDessin n).W = n

Every edge of the cyclic dessin has its own white vertex.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.faceCount_cyclicDessin {n : ℕ} (hn : n ≠ 0) : (cyclicDessin n).faceCount = 1

In positive degree, the cyclic dessin has one face.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.faceCount_cyclicDessin_zero : (cyclicDessin 0).faceCount = 0

The degree-zero cyclic dessin has no faces.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.isConnected_cyclicDessin_iff {n : ℕ} : (cyclicDessin n).IsConnected ↔ n ≠ 0

The cyclic dessin is connected exactly in positive degree.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.eulerChar_cyclicDessin {n : ℕ} (hn : n ≠ 0) : (cyclicDessin n).eulerChar = 2

In positive degree, the cyclic dessin has Euler characteristic two.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.eulerChar_cyclicDessin_zero : (cyclicDessin 0).eulerChar = 0

The degree-zero cyclic dessin has Euler characteristic zero.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.genus_cyclicDessin {n : ℕ} (hn : n ≠ 0) : (cyclicDessin n).genus = 0

In positive degree, the cyclic dessin has genus zero.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.genus_cyclicDessin_zero : (cyclicDessin 0).genus = 1

The truncated genus formula assigns genus one to the degree-zero cyclic dessin.

The segment dessin

def TauCeti.BipartiteRibbonGraph.segmentDessin : BipartiteRibbonGraph

The two-edge segment dessin associated to the map z ↦ 4z(1 - z).

Equations

• TauCeti.BipartiteRibbonGraph.segmentDessin = TauCeti.PermutationTriple.chebyshevTriple.ribbonGraph

theorem TauCeti.BipartiteRibbonGraph.segmentDessin_def : segmentDessin = PermutationTriple.chebyshevTriple.ribbonGraph

The segment dessin is the ribbon graph constructed from the Chebyshev permutation triple.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_E_segmentDessin : Fintype.card segmentDessin.E = 2

The segment dessin has two edges.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_B_segmentDessin : Fintype.card segmentDessin.B = 2

The segment dessin has two black vertices.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_W_segmentDessin : Fintype.card segmentDessin.W = 1

The segment dessin has one white vertex.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.faceCount_segmentDessin : segmentDessin.faceCount = 1

The segment dessin has one face.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.isConnected_segmentDessin : segmentDessin.IsConnected

The segment dessin is connected.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.eulerChar_segmentDessin : segmentDessin.eulerChar = 2

The segment dessin has Euler characteristic two.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.genus_segmentDessin : segmentDessin.genus = 0

The segment dessin has genus zero.

The torus dessin

def TauCeti.BipartiteRibbonGraph.torusDessin : BipartiteRibbonGraph

The four-edge dessin associated to torusTriple.

Equations

• TauCeti.BipartiteRibbonGraph.torusDessin = TauCeti.PermutationTriple.torusTriple.ribbonGraph

theorem TauCeti.BipartiteRibbonGraph.torusDessin_def : torusDessin = PermutationTriple.torusTriple.ribbonGraph

The torus dessin is the ribbon graph constructed from the Euclidean genus-one triple.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_E_torusDessin : Fintype.card torusDessin.E = 4

The torus dessin has four edges.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_B_torusDessin : Fintype.card torusDessin.B = 1

The torus dessin has one black vertex.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_W_torusDessin : Fintype.card torusDessin.W = 1

The torus dessin has one white vertex.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.faceCount_torusDessin : torusDessin.faceCount = 2

The torus dessin has two faces.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.isConnected_torusDessin : torusDessin.IsConnected

The torus dessin is connected.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.eulerChar_torusDessin : torusDessin.eulerChar = 0

The torus dessin has Euler characteristic zero.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.genus_torusDessin : torusDessin.genus = 1

The torus dessin has genus one.

The symmetric degree-three dessin

def TauCeti.BipartiteRibbonGraph.s3Dessin : BipartiteRibbonGraph

The three-edge dessin associated to the triple with monodromy group S₃.

Equations

• TauCeti.BipartiteRibbonGraph.s3Dessin = TauCeti.PermutationTriple.s3Triple.ribbonGraph

theorem TauCeti.BipartiteRibbonGraph.s3Dessin_def : s3Dessin = PermutationTriple.s3Triple.ribbonGraph

The symmetric degree-three dessin is the ribbon graph constructed from s3Triple.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_E_s3Dessin : Fintype.card s3Dessin.E = 3

The symmetric degree-three dessin has three edges.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_B_s3Dessin : Fintype.card s3Dessin.B = 1

The symmetric degree-three dessin has one black vertex.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.card_W_s3Dessin : Fintype.card s3Dessin.W = 2

The symmetric degree-three dessin has two white vertices.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.faceCount_s3Dessin : s3Dessin.faceCount = 2

The symmetric degree-three dessin has two faces.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.isConnected_s3Dessin : s3Dessin.IsConnected

The symmetric degree-three dessin is connected.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.eulerChar_s3Dessin : s3Dessin.eulerChar = 2

The symmetric degree-three dessin has Euler characteristic two.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.genus_s3Dessin : s3Dessin.genus = 0

The symmetric degree-three dessin has genus zero.