Documentation

TauCeti.Combinatorics.PermutationTriple.Passport.Count

The generating triples of a passport #

A passport records a reference monodromy subgroup P.G together with the three ordered full cycle types of the generating triples it contains. For a passport of nonzero degree whose reference subgroup is pretransitive — the first two conjuncts of TauCeti.PassportSpec.IsAdmissible — the number of isomorphism classes in the passport is the number of P.G-generating triples of S_n with those cycle data, counted up to the action of the normalizer of P.G, which is TauCeti.PassportSpec.passportSize_eq_card_generatingTripleOrbits; the count itself, that of the generating triples before the normalizer action, needs no such hypothesis. This file names that finite set of generating triples and gives its cardinality.

The classes of a cycle type #

One S_n-cycle type can meet several G-classes, and can meet none, so a count of the members of G with a prescribed cycle type is a sum over G-classes rather than a single class size. That index set is TauCeti.Subgroup.classesOfFullCycleType, in TauCeti/GroupTheory/Perm/ConjClass.lean, for a group of permutations in general; TauCeti.Subgroup.mem_iUnionClassesOfFullCycleType there identifies the union of those classes, the set TauCeti.Subgroup.iUnionClassesOfFullCycleType, with the elements of the group of that cycle type.

The generating triples of a passport #

TauCeti.PassportSpec.generatingTriples is the set of product-one triples of permutations whose first two entries generate P.G and whose three cycle types are those of P: the generating triples of the passport, as triples of permutations. The product-one relation makes the third entry a function of the first two (TauCeti.PermutationTriple.ofTwo_σinf_eq_of_product_eq_one), so TauCeti.PassportSpec.generatingTriplesEquiv is the elimination rule identifying that finite set with TauCeti.PassportSpec.GeneratingTriple, the two maps being computed by TauCeti.PassportSpec.generatingTriplesEquiv_apply and TauCeti.PassportSpec.generatingTriplesEquiv_symm_apply, and TauCeti.PassportSpec.card_generatingTriples reads the size of the passport's generating triples off it. This is the finite set that a sum over triples of classes counts, and that the normalizer of P.G acts on.

References #

The generating triples of a passport #

source
noncomputable def TauCeti.PassportSpec.generatingTriples {n : ℕ} (P : PassportSpec n) :
Finset (Equiv.Perm (Fin n) × Equiv.Perm (Fin n) × Equiv.Perm (Fin n))

The product-one triples of S_n of the three cycle types recorded by P whose first two entries generate the reference subgroup: the generating triples of the passport, as triples of permutations.

The third entry is forced by the product-one relation, so each of these is a TauCeti.PermutationTriple.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.PassportSpec.mem_generatingTriples {n : ℕ} {P : PassportSpec n} {p : Equiv.Perm (Fin n) × Equiv.Perm (Fin n) × Equiv.Perm (Fin n)} :
    p ∈ P.generatingTriples ↔ p.2.2 * p.2.1 * p.1 = 1 ∧ Subgroup.closure {p.1, p.2.1} = P.G ∧ (p.1.fullCycleType, p.2.1.fullCycleType, p.2.2.fullCycleType) = (P.lam0, P.lam1, P.laminf)
    source
    noncomputable def TauCeti.PassportSpec.generatingTriplesEquiv {n : ℕ} (P : PassportSpec n) :
    P.GeneratingTriple ≃ ↥P.generatingTriples

    The generating triples of a passport, as product-one triples of permutations: the elimination rule for TauCeti.PassportSpec.generatingTriples, and the source of the counting below. Its two maps are computed by TauCeti.PassportSpec.generatingTriplesEquiv_apply and TauCeti.PassportSpec.generatingTriplesEquiv_symm_apply.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.PassportSpec.generatingTriplesEquiv_apply {n : ℕ} (P : PassportSpec n) (g : P.GeneratingTriple) :
      ↑(P.generatingTriplesEquiv g) = ((↑g).σ0, (↑g).σ1, (↑g).σinf)

      The triple of permutations that TauCeti.PassportSpec.generatingTriplesEquiv attaches to a generating triple of P is the triple of its three components.

      source
      @[simp]
      theorem TauCeti.PassportSpec.generatingTriplesEquiv_symm_apply {n : ℕ} (P : PassportSpec n) (p : ↥P.generatingTriples) :
      ↑(P.generatingTriplesEquiv.symm p) = PermutationTriple.ofTwo (↑p).1 (↑p).2.1

      The generating triple that TauCeti.PassportSpec.generatingTriplesEquiv attaches to a product-one triple of S_n is the triple with the same first two components.

      source
      theorem TauCeti.PassportSpec.card_generatingTriples {n : ℕ} (P : PassportSpec n) :
      Nat.card P.GeneratingTriple = P.generatingTriples.card

      The number of generating triples of a passport, computed on the generating triples of S_n.