The bipartite ribbon graph of a permutation triple

A degree-n permutation triple and a finite bipartite ribbon graph carry the same information, and this file builds the graph out of the triple. The edges are the n sheets, the black vertices are the cycles of σ0 and the white ones the cycles of σ1 — fixed points included, so every sheet has exactly one end of each colour — and the cyclic order of the edges around a vertex is the cycle of the corresponding component through them. For a connected triple the result is a dessin d'enfants; disconnected triples give disconnected graphs, and TauCeti.PermutationTriple.isConnected_ribbonGraph is the equivalence.

• TauCeti.PermutationTriple.ribbonGraph: the construction.
• TauCeti.PermutationTriple.facePerm_ribbonGraph: the face permutation of the graph is the third component σinf of the triple, so the faces of the graph are the cycles of σinf.
• TauCeti.PermutationTriple.isConnected_ribbonGraph: the graph is connected exactly when the triple is, the rotation group of the graph being the monodromy group of the triple.
• TauCeti.PermutationTriple.eulerChar_ribbonGraph: the Euler characteristic of the graph, counted as |B| + |W| - |E| + |F|, is the Euler characteristic of the triple, counted as the total number of cycles of the three components less the degree. The two counts agree because the black vertices, the white vertices and the faces are precisely the cycles of σ0, of σ1 and of σinf.

Implementation notes

The construction is @[expose]d. Its edge, black-vertex and white-vertex types are structure fields of TauCeti.BipartiteRibbonGraph, so a consumer cannot so much as state that an edge of t.ribbonGraph is a sheet of t without reducing those fields; the lemmas below then read off the remaining fields.

The black and white vertex types are quotients of Fin n. Their Fintype and DecidableEq instances decide Equiv.Perm.SameCycle by iterating the permutation, so the cell counts of the graph of a concrete triple evaluate by decide and #eval.

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.

def TauCeti.PermutationTriple.ribbonGraph {n : ℕ} (t : PermutationTriple n) : BipartiteRibbonGraph

The finite bipartite ribbon graph of a permutation triple: its edges are the sheets, its black and white vertices are the cycles of σ0 and of σ1, and the cyclic orders around them are σ0 and σ1 themselves. For a connected triple this is the dessin d'enfants of the associated three-point cover.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PermutationTriple.rotB_ribbonGraph {n : ℕ} (t : PermutationTriple n) : t.ribbonGraph.rotB = t.σ0

The cyclic order of the sheets around a black vertex is σ0.

@[simp]

theorem TauCeti.PermutationTriple.rotW_ribbonGraph {n : ℕ} (t : PermutationTriple n) : t.ribbonGraph.rotW = t.σ1

The cyclic order of the sheets around a white vertex is σ1.

@[simp]

theorem TauCeti.PermutationTriple.blackEnd_ribbonGraph {n : ℕ} (t : PermutationTriple n) (i : Fin n) : t.ribbonGraph.blackEnd i = ⟦i⟧

The black end of a sheet is its cycle under σ0.

@[simp]

theorem TauCeti.PermutationTriple.whiteEnd_ribbonGraph {n : ℕ} (t : PermutationTriple n) (i : Fin n) : t.ribbonGraph.whiteEnd i = ⟦i⟧

The white end of a sheet is its cycle under σ1.

@[simp]

theorem TauCeti.PermutationTriple.facePerm_ribbonGraph {n : ℕ} (t : PermutationTriple n) : t.ribbonGraph.facePerm = t.σinf

The faces of the graph are the cycles of the third component: the face permutation is σinf on the nose, the product-one convention of a triple being that of a ribbon graph.

@[simp]

theorem TauCeti.PermutationTriple.rotationGroup_ribbonGraph {n : ℕ} (t : PermutationTriple n) : t.ribbonGraph.rotationGroup = t.monodromyGroup

The rotation group of the graph is the monodromy group of the triple.

@[simp]

theorem TauCeti.PermutationTriple.isConnected_ribbonGraph {n : ℕ} (t : PermutationTriple n) : t.ribbonGraph.IsConnected ↔ t.IsConnected

The graph of a triple is connected exactly when the triple is.

Relabeling

def TauCeti.PermutationTriple.ribbonGraphIsoSmul {n : ℕ} (t : PermutationTriple n) (τ : Equiv.Perm (Fin n)) : t.ribbonGraph.Iso (τ • t).ribbonGraph

Relabeling the sheets by τ is an isomorphism from the ribbon graph of a triple onto the ribbon graph of the relabeled triple. Isomorphic triples therefore have isomorphic graphs, so the construction descends to isomorphism classes.

Equations

• t.ribbonGraphIsoSmul τ = { edge := τ, black := Quotient.congr τ ⋯, white := Quotient.congr τ ⋯, map_blackEnd := ⋯, map_whiteEnd := ⋯, map_rotB := ⋯, map_rotW := ⋯ }

@[simp]

theorem TauCeti.PermutationTriple.ribbonGraphIsoSmul_edge_apply {n : ℕ} (t : PermutationTriple n) (τ : Equiv.Perm (Fin n)) (i : Fin n) : (t.ribbonGraphIsoSmul τ).edge i = τ i

@[simp]

theorem TauCeti.PermutationTriple.ribbonGraphIsoSmul_black_apply {n : ℕ} (t : PermutationTriple n) (τ : Equiv.Perm (Fin n)) (i : Fin n) : (t.ribbonGraphIsoSmul τ).black ⟦i⟧ = ⟦τ i⟧

Relabeling sends a black vertex represented by i to the vertex represented by τ i.

@[simp]

theorem TauCeti.PermutationTriple.ribbonGraphIsoSmul_white_apply {n : ℕ} (t : PermutationTriple n) (τ : Equiv.Perm (Fin n)) (i : Fin n) : (t.ribbonGraphIsoSmul τ).white ⟦i⟧ = ⟦τ i⟧

Relabeling sends a white vertex represented by i to the vertex represented by τ i.

Counting cells

@[simp]

theorem TauCeti.PermutationTriple.card_E_ribbonGraph {n : ℕ} (t : PermutationTriple n) : Fintype.card t.ribbonGraph.E = n

The edges of the graph are the sheets of the triple.

@[simp]

theorem TauCeti.PermutationTriple.card_B_ribbonGraph {n : ℕ} (t : PermutationTriple n) : Fintype.card t.ribbonGraph.B = orbitCount t.σ0

The black vertices of the graph are the cycles of σ0, fixed points included.

@[simp]

theorem TauCeti.PermutationTriple.card_W_ribbonGraph {n : ℕ} (t : PermutationTriple n) : Fintype.card t.ribbonGraph.W = orbitCount t.σ1

The white vertices of the graph are the cycles of σ1, fixed points included.

@[simp]

theorem TauCeti.PermutationTriple.faceCount_ribbonGraph {n : ℕ} (t : PermutationTriple n) : t.ribbonGraph.faceCount = orbitCount t.σinf

The faces of the graph are the cycles of σinf, fixed points included.

@[simp]

theorem TauCeti.PermutationTriple.eulerChar_ribbonGraph {n : ℕ} (t : PermutationTriple n) : t.ribbonGraph.eulerChar = t.eulerChar

The Euler characteristic of the graph is the Euler characteristic of the triple: the two counts agree cell by cell.