The permutation triple of a bipartite ribbon graph

Numbering the edges of a finite bipartite ribbon graph by Fin n turns its black and white rotations into two permutations of Fin n. Their product determines the third component of a permutation triple. The third component is the transported face permutation, so the construction retains all three kinds of cells of the graph.

Changing the edge numbering simultaneously conjugates the three components. Consequently the isomorphism class of the resulting triple is independent of the numbering. Graph isomorphisms also give equivalent triples, and connected ribbon graphs give connected triples. These facts are the reverse half of the correspondence between permutation triples and dessins.

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.BipartiteRibbonGraph.toPermutationTriple {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) : PermutationTriple n

The permutation triple obtained by numbering the edges of a bipartite ribbon graph. Its first two components are the transported black and white rotations.

Equations

• Γ.toPermutationTriple ν = TauCeti.PermutationTriple.ofTwo (ν.permCongr Γ.rotB) (ν.permCongr Γ.rotW)

@[simp]

theorem TauCeti.BipartiteRibbonGraph.toPermutationTriple_σ0 {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) : (Γ.toPermutationTriple ν).σ0 = ν.permCongr Γ.rotB

The first component of the triple is the black rotation in the chosen numbering.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.toPermutationTriple_σ1 {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) : (Γ.toPermutationTriple ν).σ1 = ν.permCongr Γ.rotW

The second component of the triple is the white rotation in the chosen numbering.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.toPermutationTriple_σinf {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) : (Γ.toPermutationTriple ν).σinf = ν.permCongr Γ.facePerm

The third component of the triple is the face permutation in the chosen numbering.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.monodromyGroup_toPermutationTriple {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) : (Γ.toPermutationTriple ν).monodromyGroup = Subgroup.map (↑ν.permCongrHom) Γ.rotationGroup

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

noncomputable def TauCeti.BipartiteRibbonGraph.rotationGroupEquivMonodromyGroup {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) : ↥Γ.rotationGroup ≃* ↥(Γ.toPermutationTriple ν).monodromyGroup

The rotation group of the graph is isomorphic to the monodromy group of its triple.

Equations

• Γ.rotationGroupEquivMonodromyGroup ν = (Γ.rotationGroup.equivMapOfInjective ↑ν.permCongrHom ⋯).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem TauCeti.BipartiteRibbonGraph.coe_rotationGroupEquivMonodromyGroup {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) (g : ↥Γ.rotationGroup) : ↑((Γ.rotationGroupEquivMonodromyGroup ν) g) = ν.permCongr ↑g

The rotation-group isomorphism acts by conjugating an edge permutation through the chosen numbering.

theorem TauCeti.BipartiteRibbonGraph.isConnected_toPermutationTriple {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) : (Γ.toPermutationTriple ν).IsConnected ↔ Γ.IsConnected

The triple obtained from a ribbon graph is connected exactly when the graph is connected.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.toPermutationTriple_trans {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) (τ : Equiv.Perm (Fin n)) : Γ.toPermutationTriple (ν.trans τ) = τ • Γ.toPermutationTriple ν

Postcomposing an edge numbering by a relabeling simultaneously relabels the resulting permutation triple.

theorem TauCeti.BipartiteRibbonGraph.equivalent_toPermutationTriple {n : ℕ} (Γ : BipartiteRibbonGraph) (ν μ : Γ.E ≃ Fin n) : (Γ.toPermutationTriple ν).Equivalent (Γ.toPermutationTriple μ)

Triples obtained from two numberings of the same graph differ by simultaneous relabeling.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.toPermutationTriple_iso {n : ℕ} {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (ν : Δ.E ≃ Fin n) : Γ.toPermutationTriple (f.edge.trans ν) = Δ.toPermutationTriple ν

Numbering the target of a ribbon-graph isomorphism gives the same triple as pulling that numbering back to the source.

theorem TauCeti.BipartiteRibbonGraph.equivalent_toPermutationTriple_of_iso {n : ℕ} {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (ν : Γ.E ≃ Fin n) (μ : Δ.E ≃ Fin n) : (Γ.toPermutationTriple ν).Equivalent (Δ.toPermutationTriple μ)

Isomorphic ribbon graphs give equivalent triples under arbitrary edge numberings.