Documentation

TauCeti.Combinatorics.PermutationTriple.Enumeration

Enumeration of connected permutation triples #

Connectedness of a permutation triple is decidable, so the connected triples of a given degree form a computable finset, and so do their isomorphism classes, each class listed as the finset of connected triples it contains — the relabeling orbit, not a chosen representative. This file records both finsets and identifies their members and cardinalities with the corresponding types, and then establishes the number of isomorphism classes of connected triples — equivalently, of connected dessins d'enfants with a given number of edges — in degrees one to three:

degree               1   2   3
connected classes    1   3   7

The three degree-two classes are the double cover of the sphere branched at two of the three branch points, one class for each choice of the unbranched point. The seven degree-three classes are the cyclic cover z ↦ z³ in its three orderings of the branch points (monodromy C₃, one branch point unramified), the S₃-cover TauCeti.PermutationTriple.s3Triple in its three orderings (monodromy S₃), and the genus-one cover with a three-cycle at every branch point (monodromy C₃). The twenty-six degree-four classes are counted by TauCeti.ConnectedIsoClass.card_four in TauCeti.Combinatorics.PermutationTriple.SmallDegrees, as a consequence of their classification by cycle data.

Main definitions #

Main results #

source
def TauCeti.connectedTriples (n : ℕ) :
Finset (PermutationTriple n)

The connected permutation triples of degree n, as a finset.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.mem_connectedTriples {n : ℕ} {t : PermutationTriple n} :
    t ∈ connectedTriples n ↔ t.IsConnected

    The members of TauCeti.connectedTriples n are exactly the connected permutation triples of degree n.

    source
    theorem TauCeti.card_connectedTriples {n : ℕ} :
    (connectedTriples n).card = Fintype.card (ConnectedTriple n)

    The finset of connected triples of degree n has the cardinality of the type TauCeti.ConnectedTriple n.

    source
    def TauCeti.isoClasses (n : ℕ) :
    Finset (Finset (ConnectedTriple n))

    The isomorphism classes of connected permutation triples of degree n, as the finset of relabeling orbits: each class is listed as the finset of connected triples it contains.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.mem_isoClasses {n : ℕ} {s : Finset (ConnectedTriple n)} :
      s ∈ isoClasses n ↔ ∃ (t : ConnectedTriple n), Finset.image (fun (x : Equiv.Perm (Fin n)) => x • t) Finset.univ = s

      The members of TauCeti.isoClasses n are exactly the relabeling orbits of connected triples.

      source
      theorem TauCeti.existsUnique_mem_isoClasses {n : ℕ} (t : ConnectedTriple n) :
      ∃! s : Finset (ConnectedTriple n), s ∈ isoClasses n ∧ t ∈ s

      Every connected triple lies in exactly one of the listed relabeling orbits: the members of TauCeti.isoClasses n partition the connected triples of degree n.

      source
      theorem TauCeti.card_isoClasses {n : ℕ} :
      (isoClasses n).card = Fintype.card (ConnectedIsoClass n)

      The finset of isomorphism classes of degree n has the cardinality of the type TauCeti.ConnectedIsoClass n.

      source
      theorem TauCeti.ConnectedIsoClass.card_one :
      Fintype.card (ConnectedIsoClass 1) = 1

      There is one isomorphism class of connected permutation triples of degree one.

      source
      theorem TauCeti.ConnectedIsoClass.card_two :
      Fintype.card (ConnectedIsoClass 2) = 3

      There are three isomorphism classes of connected permutation triples of degree two.

      source
      theorem TauCeti.ConnectedIsoClass.card_three :
      Fintype.card (ConnectedIsoClass 3) = 7

      There are seven isomorphism classes of connected permutation triples of degree three.