Ribbon graphs and permutation triples classify each other

Numbering the edges of a finite bipartite ribbon graph turns it into a permutation triple (TauCeti.BipartiteRibbonGraph.toPermutationTriple), and every permutation triple has a ribbon graph (TauCeti.PermutationTriple.ribbonGraph). This file proves that the two constructions are mutually inverse up to the appropriate notion of isomorphism on each side, so that isomorphism classes of ribbon graphs with n edges are the same as isomorphism classes of degree-n permutation triples, automorphisms included.

• TauCeti.PermutationTriple.toPermutationTriple_ribbonGraph: triple → graph → triple returns the original triple on the nose, for the tautological numbering of the edges by Fin n.
• TauCeti.BipartiteRibbonGraph.isoRibbonGraph: graph → triple → graph returns a graph isomorphic to the original, the isomorphism being the chosen numbering on edges.
• TauCeti.BipartiteRibbonGraph.nonempty_iso_iff_equivalent: two numbered graphs are isomorphic exactly when their triples are related by relabeling, and TauCeti.PermutationTriple.nonempty_iso_ribbonGraph_iff is the same statement read on triples.
• TauCeti.BipartiteRibbonGraph.isoClassEquiv: the resulting bijection between isomorphism classes of ribbon graphs with n edges and TauCeti.PermutationTriple.IsoClass n.
• TauCeti.BipartiteRibbonGraph.autEquivAutomorphismGroup: the automorphism group of a numbered graph is the automorphism group of its triple.

Connectedness matches on the two sides (TauCeti.BipartiteRibbonGraph.isConnected_toPermutationTriple and TauCeti.PermutationTriple.isConnected_ribbonGraph), so the bijection restricts to one between isomorphism classes of dessins d'enfants and of connected triples.

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.

@[simp]

theorem TauCeti.PermutationTriple.toPermutationTriple_ribbonGraph {n : ℕ} (t : PermutationTriple n) : t.ribbonGraph.toPermutationTriple (Equiv.refl (Fin n)) = t

Triple → graph → triple is the identity: numbering the edges of the ribbon graph of a triple by the sheets they are recovers the triple. The edge type of t.ribbonGraph is Fin n by construction, so the identity is such a numbering.

noncomputable def TauCeti.BipartiteRibbonGraph.isoOfToPermutationTripleEq {n : ℕ} {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {ν : Γ.E ≃ Fin n} {μ : Δ.E ≃ Fin n} (h : Γ.toPermutationTriple ν = Δ.toPermutationTriple μ) : Γ.Iso Δ

Two numbered ribbon graphs with the same permutation triple are isomorphic, by matching the edges carrying the same number.

Equations

• TauCeti.BipartiteRibbonGraph.isoOfToPermutationTripleEq h = TauCeti.BipartiteRibbonGraph.Iso.ofEdge (ν.trans μ.symm) ⋯ ⋯

@[simp]

theorem TauCeti.BipartiteRibbonGraph.isoOfToPermutationTripleEq_edge {n : ℕ} {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {ν : Γ.E ≃ Fin n} {μ : Δ.E ≃ Fin n} (h : Γ.toPermutationTriple ν = Δ.toPermutationTriple μ) : (isoOfToPermutationTripleEq h).edge = ν.trans μ.symm

noncomputable def TauCeti.BipartiteRibbonGraph.isoRibbonGraph {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) : Γ.Iso (Γ.toPermutationTriple ν).ribbonGraph

Graph → triple → graph is isomorphic to the identity: a ribbon graph is isomorphic to the ribbon graph of its triple along any numbering ν of its edges, by ν itself.

Equations

• Γ.isoRibbonGraph ν = TauCeti.BipartiteRibbonGraph.isoOfToPermutationTripleEq ⋯

@[simp]

theorem TauCeti.BipartiteRibbonGraph.isoRibbonGraph_edge {n : ℕ} {Γ : BipartiteRibbonGraph} (ν : Γ.E ≃ Fin n) : (Γ.isoRibbonGraph ν).edge = ν

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

Two numbered ribbon graphs are isomorphic exactly when their permutation triples are related by a relabeling of the sheets.

theorem TauCeti.PermutationTriple.nonempty_iso_ribbonGraph_iff {n : ℕ} {t t' : PermutationTriple n} : Nonempty (t.ribbonGraph.Iso t'.ribbonGraph) ↔ t.Equivalent t'

Two permutation triples have isomorphic ribbon graphs exactly when they are related by a relabeling of the sheets.

def TauCeti.BipartiteRibbonGraph.isoSetoid (n : ℕ) : Setoid { Γ : BipartiteRibbonGraph // Fintype.card Γ.E = n }

Isomorphism of bipartite ribbon graphs with n edges, as an equivalence relation.

Equations

• TauCeti.BipartiteRibbonGraph.isoSetoid n = { r := fun (Γ Δ : { Γ : TauCeti.BipartiteRibbonGraph // Fintype.card Γ.E = n }) => Nonempty ((↑Γ).Iso ↑Δ), iseqv := ⋯ }

theorem TauCeti.BipartiteRibbonGraph.isoSetoid_r {n : ℕ} {Γ Δ : { Γ : BipartiteRibbonGraph // Fintype.card Γ.E = n }} : (isoSetoid n) Γ Δ ↔ Nonempty ((↑Γ).Iso ↑Δ)

noncomputable def TauCeti.BipartiteRibbonGraph.isoClassEquiv (n : ℕ) : Quotient (isoSetoid n) ≃ PermutationTriple.IsoClass n

Isomorphism classes of bipartite ribbon graphs with n edges are isomorphism classes of degree-n permutation triples: a class of graphs goes to the class of the triple of any numbering of the edges, and a class of triples goes to the class of the (universe-lifted) ribbon graph of any representative.

Equations

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

theorem TauCeti.BipartiteRibbonGraph.isoClassEquiv_mk {n : ℕ} (Γ : { Γ : BipartiteRibbonGraph // Fintype.card Γ.E = n }) (ν : (↑Γ).E ≃ Fin n) : (isoClassEquiv n) ⟦Γ⟧ = PermutationTriple.IsoClass.mk ((↑Γ).toPermutationTriple ν)

The class of a ribbon graph is the class of its triple along any numbering of its edges.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.isoClassEquiv_mk_equivFinOfCardEq {n : ℕ} (Γ : { Γ : BipartiteRibbonGraph // Fintype.card Γ.E = n }) : (isoClassEquiv n) ⟦Γ⟧ = PermutationTriple.IsoClass.mk ((↑Γ).toPermutationTriple (Fintype.equivFinOfCardEq ⋯))

The class of a ribbon graph is the class of its triple along the canonical numbering Fintype.equivFinOfCardEq of its edges; see isoClassEquiv_mk for an arbitrary numbering.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.isoClassEquiv_symm_mk {n : ℕ} (t : PermutationTriple n) : (isoClassEquiv n).symm (PermutationTriple.IsoClass.mk t) = ⟦⟨t.ribbonGraph.ulift, ⋯⟩⟧

The class of a triple is the class of its (universe-lifted) ribbon graph.

Automorphisms

theorem TauCeti.BipartiteRibbonGraph.permCongr_edge_mem_automorphismGroup {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) (f : Γ.Aut) : ν.permCongr f.edge ∈ (Γ.toPermutationTriple ν).automorphismGroup

The edge permutation of an automorphism, read through a numbering of the edges, is an automorphism of the triple.

noncomputable def TauCeti.BipartiteRibbonGraph.autEquivAutomorphismGroup {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) : Γ.Aut ≃* ↥(Γ.toPermutationTriple ν).automorphismGroup

The automorphism group of a ribbon graph is the automorphism group of its permutation triple, along any numbering of the edges: an automorphism is determined by its action on the edges, and an edge permutation extends to an automorphism exactly when it commutes with both rotations.

Equations

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

@[simp]

theorem TauCeti.BipartiteRibbonGraph.coe_autEquivAutomorphismGroup_apply {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) (f : Γ.Aut) : ↑((Γ.autEquivAutomorphismGroup ν) f) = ν.permCongr f.edge

@[simp]

theorem TauCeti.BipartiteRibbonGraph.autEquivAutomorphismGroup_symm_apply_edge {n : ℕ} (Γ : BipartiteRibbonGraph) (ν : Γ.E ≃ Fin n) (τ : ↥(Γ.toPermutationTriple ν).automorphismGroup) : ((Γ.autEquivAutomorphismGroup ν).symm τ).edge = ν.symm.permCongr ↑τ