Connected ribbon graphs and connected permutation triples

Isomorphism classes of connected finite bipartite ribbon graphs with n edges are equivalent to TauCeti.ConnectedIsoClass n. These graphs are the combinatorial dessins d'enfants, so counting their isomorphism classes reduces to counting connected triples. The equivalence restricts TauCeti.BipartiteRibbonGraph.isoClassEquiv, with the same comparison of automorphism groups given by TauCeti.BipartiteRibbonGraph.autEquivAutomorphismGroup.

The equations connectedIsoClassEquiv_mk and connectedIsoClassEquiv_symm_mk describe the classification on representatives. Edge numberings are arbitrary, and the inverse uses universe lifting so that graphs in any universe are classified. In degree zero both carriers are empty, since connectedness requires a nonempty edge set.

The restriction uses Mathlib's Equiv.subtypeQuotientEquivQuotientSubtype to commute invariant subtypes with quotients.

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.connectedIsoSetoid (n : ℕ) : Setoid { Γ : { Γ : BipartiteRibbonGraph // Fintype.card Γ.E = n } // (↑Γ).IsConnected }

Isomorphism of connected bipartite ribbon graphs with n edges. The inner subtype records the edge count; the outer subtype records connectedness.

Equations

• TauCeti.BipartiteRibbonGraph.connectedIsoSetoid n = Setoid.comap Subtype.val (TauCeti.BipartiteRibbonGraph.isoSetoid n)

@[simp]

theorem TauCeti.BipartiteRibbonGraph.connectedIsoSetoid_mk_eq_mk_iff {n : ℕ} {Γ Δ : { Γ : { Γ : BipartiteRibbonGraph // Fintype.card Γ.E = n } // (↑Γ).IsConnected }} : ⟦Γ⟧ = ⟦Δ⟧ ↔ Nonempty ((↑↑Γ).Iso ↑↑Δ)

Two connected ribbon graphs have the same quotient class exactly when they are isomorphic.

noncomputable def TauCeti.BipartiteRibbonGraph.connectedIsoClassEquiv (n : ℕ) : Quotient (connectedIsoSetoid n) ≃ ConnectedIsoClass n

Isomorphism classes of connected ribbon graphs are the isomorphism classes of connected permutation triples.

Equations

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

theorem TauCeti.BipartiteRibbonGraph.connectedIsoClassEquiv_mk {n : ℕ} (Γ : { Γ : { Γ : BipartiteRibbonGraph // Fintype.card Γ.E = n } // (↑Γ).IsConnected }) (ν : (↑↑Γ).E ≃ Fin n) : (connectedIsoClassEquiv n) ⟦Γ⟧ = ConnectedIsoClass.mk ⟨(↑↑Γ).toPermutationTriple ν, ⋯⟩

A connected graph determines the connected triple class of any numbering of its edges.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.connectedIsoClassEquiv_mk_equivFinOfCardEq {n : ℕ} (Γ : { Γ : { Γ : BipartiteRibbonGraph // Fintype.card Γ.E = n } // (↑Γ).IsConnected }) : (connectedIsoClassEquiv n) ⟦Γ⟧ = ConnectedIsoClass.mk ⟨(↑↑Γ).toPermutationTriple (Fintype.equivFinOfCardEq ⋯), ⋯⟩

The connected graph class evaluated using the canonical numbering of its edges.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.forget_connectedIsoClassEquiv {n : ℕ} (c : Quotient (connectedIsoSetoid n)) : ((connectedIsoClassEquiv n) c).forget = (isoClassEquiv n) (Quotient.map Subtype.val ⋯ c)

Forgetting connectedness commutes with the classification of all ribbon graphs.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.connectedIsoClassEquiv_symm_mk {n : ℕ} (t : ConnectedTriple n) : (connectedIsoClassEquiv n).symm (ConnectedIsoClass.mk t) = ⟦⟨⟨(↑t).ribbonGraph.ulift, ⋯⟩, ⋯⟩⟧

The connected class of a triple determines the class of its universe-lifted ribbon graph.