Genus of a bipartite ribbon graph

The rotations of a finite bipartite ribbon graph encode a permutation triple after numbering the edges. The comparison of their Euler characteristics gives parity and the connected Euler bound for the graph. Its combinatorial genus is therefore a natural number satisfying χ = 2 - 2g when the graph is connected. It agrees with the genus of any numbered triple, independently of the choice of numbering, and is preserved by graph isomorphisms.

For a connected graph, this is the genus of the oriented combinatorial surface determined by the rotation system; no analytic surface is needed. For a disconnected graph, genus is the truncated quotient ((2 - χ) / 2).toNat, which need not be the surface genus.

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.

def TauCeti.BipartiteRibbonGraph.genus (Γ : BipartiteRibbonGraph) : ℕ

The combinatorial genus of a bipartite ribbon graph. It has its geometric meaning for a connected graph; the defining truncated quotient need not be a genus for a disconnected graph.

Equations

• Γ.genus = ((2 - Γ.eulerChar) / 2).toNat

theorem TauCeti.BipartiteRibbonGraph.genus_def (Γ : BipartiteRibbonGraph) : Γ.genus = ((2 - Γ.eulerChar) / 2).toNat

The genus is obtained from the graph's Euler characteristic.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.genus_toPermutationTriple (Γ : BipartiteRibbonGraph) {n : ℕ} (ν : Γ.E ≃ Fin n) : (Γ.toPermutationTriple ν).genus = Γ.genus

The genus of a numbered ribbon graph is the genus of its permutation triple.

theorem TauCeti.BipartiteRibbonGraph.IsConnected.natCast_genus (Γ : BipartiteRibbonGraph) (hΓ : Γ.IsConnected) : ↑Γ.genus = (2 - Γ.eulerChar) / 2

A connected graph's genus is exactly the quotient (2 - χ) / 2 in the integers.

theorem TauCeti.BipartiteRibbonGraph.IsConnected.two_sub_two_mul_genus (Γ : BipartiteRibbonGraph) (hΓ : Γ.IsConnected) : 2 - 2 * ↑Γ.genus = Γ.eulerChar

The Euler characteristic of a connected bipartite ribbon graph is 2 - 2g.

theorem TauCeti.BipartiteRibbonGraph.Iso.genus_eq (Γ : BipartiteRibbonGraph) {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : Γ.genus = Δ.genus

Isomorphic ribbon graphs have the same combinatorial genus.

@[simp]

theorem TauCeti.PermutationTriple.genus_ribbonGraph {n : ℕ} (t : PermutationTriple n) : t.ribbonGraph.genus = t.genus

Passing from a permutation triple to its ribbon graph preserves the combinatorial genus.