Documentation

TauCeti.Combinatorics.RibbonGraph.BranchPoints

Branch-point exchanges on bipartite ribbon graphs #

The exchange swap01 renames the two colours, retaining the cyclic orders at every vertex. The exchange swap1Inf retains the black vertices and replaces the white vertices by faces. Its white endpoint sends an edge e to the old face of rotW e; its white rotation is rotW⁻¹ * facePerm * rotW. Thus its new faces are exactly the old white vertices. Both operations preserve the ribbon orientation: they implement exchanges of branch points, with the product-one convention, rather than reversing all cyclic orders.

Numbering the unchanged edge set identifies these constructions with the corresponding operations on permutation triples. Connectedness and genus are preserved, and the exchanges induce the right action of the permutations of the three branch points on graph isomorphism classes. The second exchange is an involution only up to isomorphism.

Implementation notes #

The graph constructors are exposed because their edge and vertex carriers are data fields: consumers need to use the original edges and black vertices, and the original face quotient as the new white vertices. The characteristic lemmas describe the remaining fields.

References #

source
def TauCeti.BipartiteRibbonGraph.swap01 (Γ : BipartiteRibbonGraph) :
BipartiteRibbonGraph

Exchange black and white vertices, retaining their cyclic orders and the edge set.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.BipartiteRibbonGraph.blackEnd_swap01 (Γ : BipartiteRibbonGraph) (e : Γ.E) :
    Γ.swap01.blackEnd e = Γ.whiteEnd e

    The new black endpoint is the old white endpoint.

    source
    @[simp]
    theorem TauCeti.BipartiteRibbonGraph.whiteEnd_swap01 (Γ : BipartiteRibbonGraph) (e : Γ.E) :
    Γ.swap01.whiteEnd e = Γ.blackEnd e

    The new white endpoint is the old black endpoint.

    source
    @[simp]
    theorem TauCeti.BipartiteRibbonGraph.rotB_swap01 (Γ : BipartiteRibbonGraph) :
    Γ.swap01.rotB = Γ.rotW

    The new black rotation is the old white rotation.

    source
    @[simp]
    theorem TauCeti.BipartiteRibbonGraph.rotW_swap01 (Γ : BipartiteRibbonGraph) :
    Γ.swap01.rotW = Γ.rotB

    The new white rotation is the old black rotation.

    source
    @[simp]
    theorem TauCeti.BipartiteRibbonGraph.swap01_swap01 (Γ : BipartiteRibbonGraph) :
    Γ.swap01.swap01 = Γ

    Exchanging the colours twice returns the original graph, including its carriers.

    source
    noncomputable def TauCeti.BipartiteRibbonGraph.swap1Inf (Γ : BipartiteRibbonGraph) :
    BipartiteRibbonGraph

    Exchange white vertices with faces, keeping the black vertices and the edge set. The endpoint shift by the old white rotation realizes the conjugator in the product-one branch-point exchange.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.BipartiteRibbonGraph.blackEnd_swap1Inf (Γ : BipartiteRibbonGraph) (e : Γ.E) :
      Γ.swap1Inf.blackEnd e = Γ.blackEnd e

      Exchanging white vertices and faces retains the black endpoint.

      source
      @[simp]
      theorem TauCeti.BipartiteRibbonGraph.whiteEnd_swap1Inf (Γ : BipartiteRibbonGraph) (e : Γ.E) :
      Γ.swap1Inf.whiteEnd e = ⟦Γ.rotW e⟧

      The new white endpoint is the old face of the edge after white rotation.

      source
      @[simp]
      theorem TauCeti.BipartiteRibbonGraph.rotB_swap1Inf (Γ : BipartiteRibbonGraph) :
      Γ.swap1Inf.rotB = Γ.rotB

      Exchanging white vertices and faces retains the black rotation.

      source
      @[simp]
      theorem TauCeti.BipartiteRibbonGraph.rotW_swap1Inf (Γ : BipartiteRibbonGraph) :
      Γ.swap1Inf.rotW = Γ.rotW⁻¹ * Γ.facePerm * Γ.rotW

      The new white rotation is the conjugated old face permutation.

      source
      @[simp]
      theorem TauCeti.BipartiteRibbonGraph.facePerm_swap01 (Γ : BipartiteRibbonGraph) :
      Γ.swap01.facePerm = Γ.rotW⁻¹ * Γ.facePerm * Γ.rotW

      The face permutation after colour exchange is the conjugated old face permutation.

      source
      @[simp]
      theorem TauCeti.BipartiteRibbonGraph.facePerm_swap1Inf (Γ : BipartiteRibbonGraph) :
      Γ.swap1Inf.facePerm = Γ.rotW

      After white-face exchange the face permutation is the original white rotation.

      source
      noncomputable def TauCeti.BipartiteRibbonGraph.swap1InfFaceEquivWhite (Γ : BipartiteRibbonGraph) :
      Γ.swap1Inf.Face ≃ Γ.W

      The faces after white-face exchange correspond to the original white vertices.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.BipartiteRibbonGraph.swap1InfFaceEquivWhite_mk (Γ : BipartiteRibbonGraph) (e : Γ.E) :
        Γ.swap1InfFaceEquivWhite ⟦e⟧ = Γ.whiteEnd e

        The new face of an edge corresponds to its old white endpoint.

        source
        @[simp]
        theorem TauCeti.BipartiteRibbonGraph.toPermutationTriple_swap01 (Γ : BipartiteRibbonGraph) {n : ℕ} (ν : Γ.E ≃ Fin n) :
        Γ.swap01.toPermutationTriple ν = (Γ.toPermutationTriple ν).swap01

        Under any numbering of the unchanged edges, colour exchange is the triple exchange.

        source
        @[simp]
        theorem TauCeti.BipartiteRibbonGraph.toPermutationTriple_swap1Inf (Γ : BipartiteRibbonGraph) {n : ℕ} (ν : Γ.E ≃ Fin n) :
        Γ.swap1Inf.toPermutationTriple ν = (Γ.toPermutationTriple ν).swap1Inf

        Under any numbering, white-face exchange realizes the prescribed triple exchange.

        source
        @[simp]
        theorem TauCeti.BipartiteRibbonGraph.isConnected_swap01_iff (Γ : BipartiteRibbonGraph) :
        Γ.swap01.IsConnected ↔ Γ.IsConnected

        Colour exchange preserves connectedness, including the nonempty-edge condition.

        source
        @[simp]
        theorem TauCeti.BipartiteRibbonGraph.isConnected_swap1Inf_iff (Γ : BipartiteRibbonGraph) :
        Γ.swap1Inf.IsConnected ↔ Γ.IsConnected

        White-face exchange preserves connectedness.

        source
        @[simp]
        theorem TauCeti.BipartiteRibbonGraph.eulerChar_swap01 (Γ : BipartiteRibbonGraph) :
        Γ.swap01.eulerChar = Γ.eulerChar

        Colour exchange preserves the Euler characteristic.

        source
        @[simp]
        theorem TauCeti.BipartiteRibbonGraph.eulerChar_swap1Inf (Γ : BipartiteRibbonGraph) :
        Γ.swap1Inf.eulerChar = Γ.eulerChar

        White-face exchange preserves the Euler characteristic.

        source
        @[simp]
        theorem TauCeti.BipartiteRibbonGraph.genus_swap01 (Γ : BipartiteRibbonGraph) :
        Γ.swap01.genus = Γ.genus

        Colour exchange preserves the combinatorial genus.

        source
        @[simp]
        theorem TauCeti.BipartiteRibbonGraph.genus_swap1Inf (Γ : BipartiteRibbonGraph) :
        Γ.swap1Inf.genus = Γ.genus

        White-face exchange preserves the combinatorial genus.

        source
        noncomputable def TauCeti.BipartiteRibbonGraph.swap1InfSwap1InfIso (Γ : BipartiteRibbonGraph) :
        Γ.swap1Inf.swap1Inf.Iso Γ

        Applying white-face exchange twice returns an isomorphic graph. Its edge equivalence undoes the simultaneous conjugation by the black rotation on the numbered triple.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.BipartiteRibbonGraph.swap1InfSwap1InfIso_edge_apply (Γ : BipartiteRibbonGraph) (e : Γ.E) :
          Γ.swap1InfSwap1InfIso.edge e = Γ.rotB⁻¹ e

          The isomorphism after two white-face exchanges maps edges by the inverse black rotation.

          source
          @[simp]
          theorem TauCeti.BipartiteRibbonGraph.swap1InfSwap1InfIso_black_apply (Γ : BipartiteRibbonGraph) (b : Γ.B) :
          Γ.swap1InfSwap1InfIso.black b = b

          The isomorphism after two white-face exchanges fixes every black vertex.

          source
          @[simp]
          theorem TauCeti.BipartiteRibbonGraph.swap1InfSwap1InfIso_white_apply (Γ : BipartiteRibbonGraph) (e : Γ.E) :
          Γ.swap1InfSwap1InfIso.white ⟦e⟧ = Γ.whiteEnd e

          The isomorphism after two white-face exchanges sends the new white vertex represented by an edge to its original white endpoint.

          source
          @[instance_reducible]
          noncomputable instance TauCeti.BipartiteRibbonGraph.instMulActionMulOppositePermFinOfNatNatQuotientSubtypeEqCardEIsoSetoid {n : ℕ} :
          MulAction (Equiv.Perm (Fin 3))ᵐᵒᵖ (Quotient (isoSetoid n))

          Branch-point permutations act on graph isomorphism classes on the right, written as a left action of the opposite group. Transport along isoClassEquiv retains the existing product-one convention and all six triple operations.

          Equations
          source
          @[simp]
          theorem TauCeti.BipartiteRibbonGraph.isoClassEquiv_smul {n : ℕ} (ρ : (Equiv.Perm (Fin 3))ᵐᵒᵖ) (c : Quotient (isoSetoid n)) :
          (isoClassEquiv n) (ρ • c) = ρ • (isoClassEquiv n) c

          The correspondence between graph and triple isomorphism classes respects branch-point exchange, with contravariant composition expressed by the opposite group.

          source
          @[simp]
          theorem TauCeti.BipartiteRibbonGraph.op_swap_zero_one_smul_mk (Γ : BipartiteRibbonGraph) {n : ℕ} (h : Fintype.card Γ.E = n) :
          MulOpposite.op (Equiv.swap 0 1) • ⟦⟨Γ, h⟩⟧ = ⟦⟨Γ.swap01, h⟩⟧

          On a representative, the transposition of 0 and 1 exchanges the two colours.

          source
          @[simp]
          theorem TauCeti.BipartiteRibbonGraph.op_swap_one_two_smul_mk (Γ : BipartiteRibbonGraph) {n : ℕ} (h : Fintype.card Γ.E = n) :
          MulOpposite.op (Equiv.swap 1 2) • ⟦⟨Γ, h⟩⟧ = ⟦⟨Γ.swap1Inf, h⟩⟧

          On a representative, the transposition of 1 and ∞ exchanges white vertices and faces.