Finite bipartite ribbon graphs

A finite bipartite ribbon graph consists of a finite set of edges, finite sets of black and white vertices, an endpoint of each colour for every edge, and a cyclic order on the edges incident to each vertex. The cyclic orders are encoded by two permutations of the common edge set. The two endpoint maps are surjective, which excludes isolated vertices, and requiring each incidence fibre to be a single cycle makes the encoding extensional: there is no unused cyclic-order data away from the incident edges.

The product of the two vertex rotations determines the face permutation, whose orbits are the faces. Gluing a disc into each face gives a closed oriented surface, one for each connected component, and eulerChar is its Euler characteristic |B| + |W| - |E| + |F|. This file also provides morphisms, isomorphisms, automorphisms, connected components, vertex degrees, the two incidence degree-sum formulas, and the copy of a ribbon graph in a higher universe.

References

• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer, 2004, Chapter 1.

structure TauCeti.BipartiteRibbonGraph : Type (u + 1)

A finite bipartite ribbon graph, encoded by its two endpoint maps and the cyclic rotations of the common edge set around black and white vertices.

• E : Type u

  The finite type of edges.

• B : Type u

  The finite type of black vertices.

• W : Type u

  The finite type of white vertices.

• fintypeE : Fintype self.E

  Finiteness of the edge set.

• fintypeB : Fintype self.B

  Finiteness of the black vertex set.

• fintypeW : Fintype self.W

  Finiteness of the white vertex set.

• decidableEqE : DecidableEq self.E

  Decidable equality on edges.

• decidableEqB : DecidableEq self.B

  Decidable equality on black vertices.

• decidableEqW : DecidableEq self.W

  Decidable equality on white vertices.

• blackEnd : self.E → self.B

  The black endpoint of an edge.

• whiteEnd : self.E → self.W

  The white endpoint of an edge.

• rotB : Equiv.Perm self.E

  The cyclic rotation of edges around their black endpoints.

• rotW : Equiv.Perm self.E

  The cyclic rotation of edges around their white endpoints.

• blackEnd_surjective : Function.Surjective self.blackEnd

  Every black vertex is incident to an edge.

• whiteEnd_surjective : Function.Surjective self.whiteEnd

  Every white vertex is incident to an edge.

• isCycleOn_rotB (b : self.B) : self.rotB.IsCycleOn (self.blackEnd ⁻¹' {b})

  The black rotation is a single cycle on every black incidence fibre.

• isCycleOn_rotW (w : self.W) : self.rotW.IsCycleOn (self.whiteEnd ⁻¹' {w})

  The white rotation is a single cycle on every white incidence fibre.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.blackEnd_rotB (Γ : BipartiteRibbonGraph) (e : Γ.E) : Γ.blackEnd (Γ.rotB e) = Γ.blackEnd e

The black rotation preserves black endpoints.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.whiteEnd_rotW (Γ : BipartiteRibbonGraph) (e : Γ.E) : Γ.whiteEnd (Γ.rotW e) = Γ.whiteEnd e

The white rotation preserves white endpoints.

theorem TauCeti.BipartiteRibbonGraph.blackEnd_eq_blackEnd_iff (Γ : BipartiteRibbonGraph) {e e' : Γ.E} : Γ.blackEnd e = Γ.blackEnd e' ↔ Γ.rotB.SameCycle e e'

Two edges share their black end exactly when they lie in one cycle of the black rotation: the black vertices are the cycles of rotB.

theorem TauCeti.BipartiteRibbonGraph.whiteEnd_eq_whiteEnd_iff (Γ : BipartiteRibbonGraph) {e e' : Γ.E} : Γ.whiteEnd e = Γ.whiteEnd e' ↔ Γ.rotW.SameCycle e e'

Two edges share their white end exactly when they lie in one cycle of the white rotation: the white vertices are the cycles of rotW.

Permutations, faces, and connected components

def TauCeti.BipartiteRibbonGraph.facePerm (Γ : BipartiteRibbonGraph) : Equiv.Perm Γ.E

The face permutation of a bipartite ribbon graph. The inverse matches the product-one convention facePerm * rotW * rotB = 1.

Equations

• Γ.facePerm = (Γ.rotW * Γ.rotB)⁻¹

theorem TauCeti.BipartiteRibbonGraph.facePerm_def (Γ : BipartiteRibbonGraph) : Γ.facePerm = (Γ.rotW * Γ.rotB)⁻¹

The face permutation is the inverse of the product of the two vertex rotations.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.facePerm_mul_rotW_mul_rotB (Γ : BipartiteRibbonGraph) : Γ.facePerm * Γ.rotW * Γ.rotB = 1

The face permutation follows the product-one convention facePerm * rotW * rotB = 1.

@[reducible, inline]

abbrev TauCeti.BipartiteRibbonGraph.Face (Γ : BipartiteRibbonGraph) : Type u

A face is an orbit of the face permutation on edges.

Equations

• Γ.Face = Quotient (Equiv.Perm.SameCycle.setoid Γ.facePerm)

@[instance_reducible]

instance TauCeti.BipartiteRibbonGraph.instFintypeFace (Γ : BipartiteRibbonGraph) : Fintype Γ.Face

The faces of a finite bipartite ribbon graph form a finite type, computably: lying in the same face is decided by iterating the face permutation.

Equations

• Γ.instFintypeFace = Quotient.fintype (Equiv.Perm.SameCycle.setoid Γ.facePerm)

def TauCeti.BipartiteRibbonGraph.rotationGroup (Γ : BipartiteRibbonGraph) : Subgroup (Equiv.Perm Γ.E)

The subgroup of edge permutations generated by the two vertex rotations.

Equations

• Γ.rotationGroup = Subgroup.closure {Γ.rotB, Γ.rotW}

theorem TauCeti.BipartiteRibbonGraph.closure_pair_eq_rotationGroup (Γ : BipartiteRibbonGraph) : Subgroup.closure {Γ.rotB, Γ.rotW} = Γ.rotationGroup

The rotation group is generated by the two vertex rotations.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.rotB_mem_rotationGroup (Γ : BipartiteRibbonGraph) : Γ.rotB ∈ Γ.rotationGroup

The black rotation lies in the rotation group.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.rotW_mem_rotationGroup (Γ : BipartiteRibbonGraph) : Γ.rotW ∈ Γ.rotationGroup

The white rotation lies in the rotation group.

@[reducible, inline]

abbrev TauCeti.BipartiteRibbonGraph.ConnectedComponent (Γ : BipartiteRibbonGraph) : Type u

A connected component is an orbit of the group generated by the two vertex rotations.

Equations

• Γ.ConnectedComponent = MulAction.orbitRel.Quotient (↥Γ.rotationGroup) Γ.E

@[instance_reducible]

noncomputable instance TauCeti.BipartiteRibbonGraph.instFintypeConnectedComponent (Γ : BipartiteRibbonGraph) : Fintype Γ.ConnectedComponent

The connected components of a finite bipartite ribbon graph form a finite type.

Equations

• Γ.instFintypeConnectedComponent = Fintype.ofFinite Γ.ConnectedComponent

def TauCeti.BipartiteRibbonGraph.IsConnected (Γ : BipartiteRibbonGraph) : Prop

A bipartite ribbon graph is connected when it has an edge and its two rotations act jointly transitively on the edge set.

Equations

• Γ.IsConnected = (Nonempty Γ.E ∧ MulAction.IsPretransitive (↥Γ.rotationGroup) Γ.E)

theorem TauCeti.BipartiteRibbonGraph.isConnected_def (Γ : BipartiteRibbonGraph) : Γ.IsConnected ↔ Nonempty Γ.E ∧ MulAction.IsPretransitive (↥Γ.rotationGroup) Γ.E

Connectedness of a bipartite ribbon graph: it has an edge, and the two rotations act jointly transitively on the edges.

theorem TauCeti.BipartiteRibbonGraph.isConnected_iff_card_connectedComponent_eq_one (Γ : BipartiteRibbonGraph) : Γ.IsConnected ↔ Fintype.card Γ.ConnectedComponent = 1

A ribbon graph is connected exactly when it has one connected component.

Degrees and Euler characteristic

def TauCeti.BipartiteRibbonGraph.blackDegree (Γ : BipartiteRibbonGraph) (b : Γ.B) : ℕ

The degree of a black vertex is the number of incident edges.

Equations

• Γ.blackDegree b = Fintype.card { e : Γ.E // Γ.blackEnd e = b }

theorem TauCeti.BipartiteRibbonGraph.blackDegree_def (Γ : BipartiteRibbonGraph) (b : Γ.B) : Γ.blackDegree b = Fintype.card { e : Γ.E // Γ.blackEnd e = b }

The degree of a black vertex is the number of edges whose black end it is.

def TauCeti.BipartiteRibbonGraph.whiteDegree (Γ : BipartiteRibbonGraph) (w : Γ.W) : ℕ

The degree of a white vertex is the number of incident edges.

Equations

• Γ.whiteDegree w = Fintype.card { e : Γ.E // Γ.whiteEnd e = w }

theorem TauCeti.BipartiteRibbonGraph.whiteDegree_def (Γ : BipartiteRibbonGraph) (w : Γ.W) : Γ.whiteDegree w = Fintype.card { e : Γ.E // Γ.whiteEnd e = w }

The degree of a white vertex is the number of edges whose white end it is.

theorem TauCeti.BipartiteRibbonGraph.blackDegree_pos (Γ : BipartiteRibbonGraph) (b : Γ.B) : 0 < Γ.blackDegree b

Every black vertex has positive degree.

theorem TauCeti.BipartiteRibbonGraph.whiteDegree_pos (Γ : BipartiteRibbonGraph) (w : Γ.W) : 0 < Γ.whiteDegree w

Every white vertex has positive degree.

theorem TauCeti.BipartiteRibbonGraph.sum_blackDegree (Γ : BipartiteRibbonGraph) : ∑ b : Γ.B, Γ.blackDegree b = Fintype.card Γ.E

The sum of the black vertex degrees is the number of edges.

theorem TauCeti.BipartiteRibbonGraph.sum_whiteDegree (Γ : BipartiteRibbonGraph) : ∑ w : Γ.W, Γ.whiteDegree w = Fintype.card Γ.E

The sum of the white vertex degrees is the number of edges.

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

The number of faces, counting every orbit of the face permutation.

Equations

• Γ.faceCount = Fintype.card Γ.Face

theorem TauCeti.BipartiteRibbonGraph.faceCount_def (Γ : BipartiteRibbonGraph) : Γ.faceCount = Fintype.card Γ.Face

The number of faces is the number of orbits of the face permutation.

def TauCeti.BipartiteRibbonGraph.eulerChar (Γ : BipartiteRibbonGraph) : ℤ

The Euler characteristic |B| + |W| + F - |E| of the closed oriented surface obtained by gluing a disc into each face of the ribbon graph (a disjoint union of closed surfaces when the graph is disconnected).

Equations

• Γ.eulerChar = ↑(Fintype.card Γ.B) + ↑(Fintype.card Γ.W) + ↑Γ.faceCount - ↑(Fintype.card Γ.E)

theorem TauCeti.BipartiteRibbonGraph.eulerChar_def (Γ : BipartiteRibbonGraph) : Γ.eulerChar = ↑(Fintype.card Γ.B) + ↑(Fintype.card Γ.W) + ↑Γ.faceCount - ↑(Fintype.card Γ.E)

The Euler characteristic counts vertices of both colours and faces against edges.

Morphisms and isomorphisms

structure TauCeti.BipartiteRibbonGraph.Hom (Γ : BipartiteRibbonGraph) (Δ : BipartiteRibbonGraph) : Type (max u u_1)

A morphism of bipartite ribbon graphs maps edges and both colours of vertices, preserving incidences and intertwining both rotations.

• edge : Γ.E → Δ.E

  The map on edges.

• black : Γ.B → Δ.B

  The map on black vertices.

• white : Γ.W → Δ.W

  The map on white vertices.

• map_blackEnd (e : Γ.E) : Δ.blackEnd (self.edge e) = self.black (Γ.blackEnd e)

  Black incidence is preserved.

• map_whiteEnd (e : Γ.E) : Δ.whiteEnd (self.edge e) = self.white (Γ.whiteEnd e)

  White incidence is preserved.

• map_rotB : Function.Semiconj self.edge ⇑Γ.rotB ⇑Δ.rotB

  The black rotations are intertwined.

• map_rotW : Function.Semiconj self.edge ⇑Γ.rotW ⇑Δ.rotW

  The white rotations are intertwined.

def TauCeti.BipartiteRibbonGraph.Hom.id (Γ : BipartiteRibbonGraph) : Γ.Hom Γ

The identity morphism of a bipartite ribbon graph.

Equations

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

def TauCeti.BipartiteRibbonGraph.Hom.comp {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {Θ : BipartiteRibbonGraph} (g : Δ.Hom Θ) (f : Γ.Hom Δ) : Γ.Hom Θ

Composition of morphisms of bipartite ribbon graphs.

Equations

• g.comp f = { edge := g.edge ∘ f.edge, black := g.black ∘ f.black, white := g.white ∘ f.white, map_blackEnd := ⋯, map_whiteEnd := ⋯, map_rotB := ⋯, map_rotW := ⋯ }

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Hom.id_edge_apply {Γ : BipartiteRibbonGraph} (e : Γ.E) : (id Γ).edge e = e

The identity morphism fixes every edge.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Hom.id_black_apply {Γ : BipartiteRibbonGraph} (b : Γ.B) : (id Γ).black b = b

The identity morphism fixes every black vertex.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Hom.id_white_apply {Γ : BipartiteRibbonGraph} (w : Γ.W) : (id Γ).white w = w

The identity morphism fixes every white vertex.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Hom.comp_edge_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {Θ : BipartiteRibbonGraph} (g : Δ.Hom Θ) (f : Γ.Hom Δ) (e : Γ.E) : (g.comp f).edge e = g.edge (f.edge e)

A composite morphism maps an edge by the two edge maps in turn.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Hom.comp_black_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {Θ : BipartiteRibbonGraph} (g : Δ.Hom Θ) (f : Γ.Hom Δ) (b : Γ.B) : (g.comp f).black b = g.black (f.black b)

A composite morphism maps a black vertex by the two black-vertex maps in turn.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Hom.comp_white_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {Θ : BipartiteRibbonGraph} (g : Δ.Hom Θ) (f : Γ.Hom Δ) (w : Γ.W) : (g.comp f).white w = g.white (f.white w)

A composite morphism maps a white vertex by the two white-vertex maps in turn.

theorem TauCeti.BipartiteRibbonGraph.Hom.ext {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {f g : Γ.Hom Δ} (hedge : f.edge = g.edge) : f = g

A morphism is determined by its edge map: every vertex is the end of an edge.

theorem TauCeti.BipartiteRibbonGraph.Hom.ext_iff {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {f g : Γ.Hom Δ} : f = g ↔ f.edge = g.edge

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Hom.id_comp {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Hom Δ) : (id Δ).comp f = f

The identity morphism is a left identity for composition.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Hom.comp_id {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Hom Δ) : f.comp (id Γ) = f

The identity morphism is a right identity for composition.

theorem TauCeti.BipartiteRibbonGraph.Hom.comp_assoc {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {Θ : BipartiteRibbonGraph} {Ξ : BipartiteRibbonGraph} (h : Θ.Hom Ξ) (g : Δ.Hom Θ) (f : Γ.Hom Δ) : h.comp (g.comp f) = (h.comp g).comp f

Composition of morphisms is associative.

structure TauCeti.BipartiteRibbonGraph.Iso (Γ : BipartiteRibbonGraph) (Δ : BipartiteRibbonGraph) : Type (max u u_1)

An isomorphism of bipartite ribbon graphs is an equivalence on edges and on each colour of vertices that preserves incidences and intertwines both rotations.

• edge : Γ.E ≃ Δ.E

  The equivalence on edges.

• black : Γ.B ≃ Δ.B

  The equivalence on black vertices.

• white : Γ.W ≃ Δ.W

  The equivalence on white vertices.

• map_blackEnd (e : Γ.E) : Δ.blackEnd (self.edge e) = self.black (Γ.blackEnd e)

  Black incidence is preserved.

• map_whiteEnd (e : Γ.E) : Δ.whiteEnd (self.edge e) = self.white (Γ.whiteEnd e)

  White incidence is preserved.

• map_rotB : Function.Semiconj ⇑self.edge ⇑Γ.rotB ⇑Δ.rotB

  The black rotations are intertwined.

• map_rotW : Function.Semiconj ⇑self.edge ⇑Γ.rotW ⇑Δ.rotW

  The white rotations are intertwined.

def TauCeti.BipartiteRibbonGraph.Iso.toHom {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : Γ.Hom Δ

The morphism underlying an isomorphism of bipartite ribbon graphs.

Equations

• f.toHom = { edge := ⇑f.edge, black := ⇑f.black, white := ⇑f.white, map_blackEnd := ⋯, map_whiteEnd := ⋯, map_rotB := ⋯, map_rotW := ⋯ }

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.toHom_edge_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (e : Γ.E) : f.toHom.edge e = f.edge e

The morphism underlying an isomorphism has the same edge map.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.toHom_black_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (b : Γ.B) : f.toHom.black b = f.black b

The morphism underlying an isomorphism has the same black-vertex map.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.toHom_white_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (w : Γ.W) : f.toHom.white w = f.white w

The morphism underlying an isomorphism has the same white-vertex map.

def TauCeti.BipartiteRibbonGraph.Iso.refl (Γ : BipartiteRibbonGraph) : Γ.Iso Γ

The identity isomorphism.

Equations

• TauCeti.BipartiteRibbonGraph.Iso.refl Γ = { edge := Equiv.refl Γ.E, black := Equiv.refl Γ.B, white := Equiv.refl Γ.W, map_blackEnd := ⋯, map_whiteEnd := ⋯, map_rotB := ⋯, map_rotW := ⋯ }

def TauCeti.BipartiteRibbonGraph.Iso.symm {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : Δ.Iso Γ

The inverse of a ribbon-graph isomorphism.

Equations

• f.symm = { edge := f.edge.symm, black := f.black.symm, white := f.white.symm, map_blackEnd := ⋯, map_whiteEnd := ⋯, map_rotB := ⋯, map_rotW := ⋯ }

def TauCeti.BipartiteRibbonGraph.Iso.trans {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {Θ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (g : Δ.Iso Θ) : Γ.Iso Θ

Composition of ribbon-graph isomorphisms.

Equations

• f.trans g = { edge := f.edge.trans g.edge, black := f.black.trans g.black, white := f.white.trans g.white, map_blackEnd := ⋯, map_whiteEnd := ⋯, map_rotB := ⋯, map_rotW := ⋯ }

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.refl_edge_apply {Γ : BipartiteRibbonGraph} (e : Γ.E) : (refl Γ).edge e = e

The identity isomorphism fixes every edge.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.refl_black_apply {Γ : BipartiteRibbonGraph} (b : Γ.B) : (refl Γ).black b = b

The identity isomorphism fixes every black vertex.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.refl_white_apply {Γ : BipartiteRibbonGraph} (w : Γ.W) : (refl Γ).white w = w

The identity isomorphism fixes every white vertex.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.symm_edge_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (e : Δ.E) : f.symm.edge e = f.edge.symm e

The inverse isomorphism maps edges by the inverse edge equivalence.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.symm_black_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (b : Δ.B) : f.symm.black b = f.black.symm b

The inverse isomorphism maps black vertices by the inverse black-vertex equivalence.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.symm_white_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (w : Δ.W) : f.symm.white w = f.white.symm w

The inverse isomorphism maps white vertices by the inverse white-vertex equivalence.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.trans_edge_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {Θ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (g : Δ.Iso Θ) (e : Γ.E) : (f.trans g).edge e = g.edge (f.edge e)

A composite isomorphism maps an edge by the two edge equivalences in turn.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.trans_black_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {Θ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (g : Δ.Iso Θ) (b : Γ.B) : (f.trans g).black b = g.black (f.black b)

A composite isomorphism maps a black vertex by the two black-vertex equivalences in turn.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.trans_white_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {Θ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (g : Δ.Iso Θ) (w : Γ.W) : (f.trans g).white w = g.white (f.white w)

A composite isomorphism maps a white vertex by the two white-vertex equivalences in turn.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.permCongr_rotB {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : f.edge.permCongr Γ.rotB = Δ.rotB

Relabeling by a ribbon-graph isomorphism conjugates the black rotation to the target's.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.permCongr_rotW {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : f.edge.permCongr Γ.rotW = Δ.rotW

Relabeling by a ribbon-graph isomorphism conjugates the white rotation to the target's.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.permCongr_facePerm {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : f.edge.permCongr Γ.facePerm = Δ.facePerm

Relabeling by a ribbon-graph isomorphism conjugates the face permutation to the target's.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.map_rotationGroup {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : Subgroup.map (↑f.edge.permCongrHom) Γ.rotationGroup = Δ.rotationGroup

Conjugating by an isomorphism carries the source rotation group onto the target one.

def TauCeti.BipartiteRibbonGraph.Iso.rotationGroupEquiv {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : ↥Γ.rotationGroup ≃* ↥Δ.rotationGroup

An isomorphism conjugates the groups generated by the two vertex rotations.

Equations

• f.rotationGroupEquiv = TauCeti.Subgroup.congrOfMapEq f.edge.permCongrHom ⋯

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.coe_rotationGroupEquiv_apply {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (g : ↥Γ.rotationGroup) : ↑(f.rotationGroupEquiv g) = f.edge.permCongr ↑g

The induced equivalence of rotation groups conjugates a permutation by the edge equivalence.

def TauCeti.BipartiteRibbonGraph.Iso.connectedComponentEquiv {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : Γ.ConnectedComponent ≃ Δ.ConnectedComponent

An isomorphism relabels the connected components of a bipartite ribbon graph.

Equations

• f.connectedComponentEquiv = TauCeti.MulAction.orbitRelQuotientCongr f.rotationGroupEquiv f.edge ⋯

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.connectedComponentEquiv_mk {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (e : Γ.E) : f.connectedComponentEquiv (Quotient.mk'' e) = Quotient.mk'' (f.edge e)

The relabelling of connected components sends the component of an edge to the component of its image.

theorem TauCeti.BipartiteRibbonGraph.Iso.isConnected_iff {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : Γ.IsConnected ↔ Δ.IsConnected

Connectedness is invariant under isomorphism.

def TauCeti.BipartiteRibbonGraph.Iso.faceEquiv {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : Γ.Face ≃ Δ.Face

An isomorphism relabels the faces of a bipartite ribbon graph.

Equations

• f.faceEquiv = Quotient.congr f.edge ⋯

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.faceEquiv_mk {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (e : Γ.E) : f.faceEquiv (Quotient.mk'' e) = Quotient.mk'' (f.edge e)

The relabelling of faces sends the face of an edge to the face of its image.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.blackDegree_eq {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (b : Γ.B) : Δ.blackDegree (f.black b) = Γ.blackDegree b

An isomorphism preserves the degree of each black vertex.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.whiteDegree_eq {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (w : Γ.W) : Δ.whiteDegree (f.white w) = Γ.whiteDegree w

An isomorphism preserves the degree of each white vertex.

theorem TauCeti.BipartiteRibbonGraph.Iso.faceCount_eq {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : Γ.faceCount = Δ.faceCount

Isomorphic bipartite ribbon graphs have the same number of faces.

theorem TauCeti.BipartiteRibbonGraph.Iso.eulerChar_eq {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : Γ.eulerChar = Δ.eulerChar

Isomorphic bipartite ribbon graphs have the same Euler characteristic.

theorem TauCeti.BipartiteRibbonGraph.Iso.ext {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {f g : Γ.Iso Δ} (hedge : f.edge = g.edge) : f = g

An isomorphism is determined by its edge equivalence: every vertex is the end of an edge.

theorem TauCeti.BipartiteRibbonGraph.Iso.ext_iff {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {f g : Γ.Iso Δ} : f = g ↔ f.edge = g.edge

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.refl_trans {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : (refl Γ).trans f = f

The identity isomorphism is a left identity for composition.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.trans_refl {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : f.trans (refl Δ) = f

The identity isomorphism is a right identity for composition.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.symm_trans_self {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : f.symm.trans f = refl Δ

Composing the inverse of an isomorphism with it gives the identity.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.trans_symm_self {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (f : Γ.Iso Δ) : f.trans f.symm = refl Γ

Composing an isomorphism with its inverse gives the identity.

theorem TauCeti.BipartiteRibbonGraph.Iso.trans_assoc {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} {Θ : BipartiteRibbonGraph} {Ξ : BipartiteRibbonGraph} (f : Γ.Iso Δ) (g : Δ.Iso Θ) (h : Θ.Iso Ξ) : (f.trans g).trans h = f.trans (g.trans h)

Composition of isomorphisms is associative.

noncomputable def TauCeti.BipartiteRibbonGraph.Iso.ofEdge {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (φ : Γ.E ≃ Δ.E) (hB : Function.Semiconj ⇑φ ⇑Γ.rotB ⇑Δ.rotB) (hW : Function.Semiconj ⇑φ ⇑Γ.rotW ⇑Δ.rotW) : Γ.Iso Δ

An edge bijection intertwining both rotations is the edge map of an isomorphism. The vertex maps are forced, the vertices of each colour being the cycles of the corresponding rotation.

Equations

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

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Iso.ofEdge_edge {Γ : BipartiteRibbonGraph} {Δ : BipartiteRibbonGraph} (φ : Γ.E ≃ Δ.E) (hB : Function.Semiconj ⇑φ ⇑Γ.rotB ⇑Δ.rotB) (hW : Function.Semiconj ⇑φ ⇑Γ.rotW ⇑Δ.rotW) : (ofEdge φ hB hW).edge = φ

The isomorphism built from an edge bijection has that bijection as its edge map.

@[reducible, inline]

abbrev TauCeti.BipartiteRibbonGraph.Aut (Γ : BipartiteRibbonGraph) : Type u

The group of automorphisms of a bipartite ribbon graph.

Equations

• Γ.Aut = Γ.Iso Γ

@[instance_reducible]

instance TauCeti.BipartiteRibbonGraph.instGroupAut (Γ : BipartiteRibbonGraph) : Group Γ.Aut

The automorphisms of a bipartite ribbon graph form a group under composition.

Equations

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

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Aut.one_edge (Γ : BipartiteRibbonGraph) : Iso.edge 1 = 1

The identity automorphism acts trivially on edges.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Aut.mul_edge {Γ : BipartiteRibbonGraph} (f g : Γ.Aut) : (f * g).edge = f.edge * g.edge

Automorphisms multiply by composing their edge permutations.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.Aut.inv_edge {Γ : BipartiteRibbonGraph} (f : Γ.Aut) : f⁻¹.edge = f.edge⁻¹

The inverse automorphism acts on edges by the inverse permutation.

Universe lifting

def TauCeti.BipartiteRibbonGraph.ulift (Γ : BipartiteRibbonGraph) : BipartiteRibbonGraph

The copy of a ribbon graph in a higher universe, with edges and vertices of both colours wrapped in ULift.

Equations

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

@[simp]

theorem TauCeti.BipartiteRibbonGraph.ulift_blackEnd_up (Γ : BipartiteRibbonGraph) (e : Γ.E) : Γ.ulift.blackEnd { down := e } = { down := Γ.blackEnd e }

A lifted edge has the lifted black end.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.ulift_whiteEnd_up (Γ : BipartiteRibbonGraph) (e : Γ.E) : Γ.ulift.whiteEnd { down := e } = { down := Γ.whiteEnd e }

A lifted edge has the lifted white end.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.ulift_rotB_up (Γ : BipartiteRibbonGraph) (e : Γ.E) : Γ.ulift.rotB { down := e } = { down := Γ.rotB e }

The black rotation of the lifted graph lifts the black rotation.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.ulift_rotW_up (Γ : BipartiteRibbonGraph) (e : Γ.E) : Γ.ulift.rotW { down := e } = { down := Γ.rotW e }

The white rotation of the lifted graph lifts the white rotation.

theorem TauCeti.BipartiteRibbonGraph.card_E_ulift (Γ : BipartiteRibbonGraph) : Fintype.card Γ.ulift.E = Fintype.card Γ.E

The number of edges is unchanged by universe lifting.

def TauCeti.BipartiteRibbonGraph.uliftIso (Γ : BipartiteRibbonGraph) : Γ.ulift.Iso Γ

A ribbon graph is isomorphic to its copy in a higher universe, by ULift.down.

Equations

• Γ.uliftIso = { edge := Equiv.ulift, black := Equiv.ulift, white := Equiv.ulift, map_blackEnd := ⋯, map_whiteEnd := ⋯, map_rotB := ⋯, map_rotW := ⋯ }

@[simp]

theorem TauCeti.BipartiteRibbonGraph.uliftIso_edge_apply (Γ : BipartiteRibbonGraph) (e : Γ.ulift.E) : Γ.uliftIso.edge e = e.down

The universe-lifting isomorphism sends a lifted edge to the edge it wraps.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.uliftIso_black_apply (Γ : BipartiteRibbonGraph) (b : Γ.ulift.B) : Γ.uliftIso.black b = b.down

The universe-lifting isomorphism sends a lifted black vertex to the vertex it wraps.

@[simp]

theorem TauCeti.BipartiteRibbonGraph.uliftIso_white_apply (Γ : BipartiteRibbonGraph) (w : Γ.ulift.W) : Γ.uliftIso.white w = w.down

The universe-lifting isomorphism sends a lifted white vertex to the vertex it wraps.