Documentation

TauCeti.Combinatorics.PermutationTriple.Passport.Class

Classes in a passport #

A passport class is an isomorphism class of connected permutation triples with fixed monodromy subgroup up to conjugacy and fixed ordered cycle partitions. This file collects those classes in a finite set and defines the passport size to be its cardinality.

The ordered cycle partitions determine the Euler characteristic, genus, order triple, and geometry type. The comparison theorems below state this without choosing representatives of isomorphism classes. In particular, a passport is a coarser invariant than an isomorphism class; no uniqueness of a class inside a passport is asserted.

Main declarations #

References #

The finite passport class set #

source
noncomputable def TauCeti.PassportSpec.classSet {n : ℕ} (P : PassportSpec n) :
Finset (ConnectedIsoClass n)

The finite set of isomorphism classes of connected triples having passport P.

The elements are quotient classes themselves, rather than arbitrarily chosen representatives.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.PassportSpec.mem_classSet {n : ℕ} {P : PassportSpec n} {c : ConnectedIsoClass n} :
    c ∈ P.classSet ↔ c.HasPassport P

    Membership in the class set is precisely passport membership.

    source
    noncomputable def TauCeti.PassportSpec.passportSize {n : ℕ} (P : PassportSpec n) :
    ℕ

    The size of a passport is the number of isomorphism classes of connected triples in it.

    Equations
    Instances For
      source
      theorem TauCeti.PassportSpec.passportSize_def {n : ℕ} (P : PassportSpec n) :
      P.passportSize = P.classSet.card

      The passport size is the cardinality of the passport class set.

      source
      theorem TauCeti.PassportSpec.passportSize_pos_iff {n : ℕ} (P : PassportSpec n) :
      0 < P.passportSize ↔ ∃ (t : ConnectedTriple n), HasPassport t P

      A passport has positive size exactly when some connected triple has that passport.

      source
      theorem TauCeti.PassportSpec.passportSize_eq_zero_iff {n : ℕ} (P : PassportSpec n) :
      P.passportSize = 0 ↔ ∀ (t : ConnectedTriple n), ¬HasPassport t P

      A passport has size zero exactly when no connected triple has that passport.

      source
      theorem TauCeti.PassportSpec.passportSize_eq_card_hasPassport {n : ℕ} (P : PassportSpec n) :
      P.passportSize = Nat.card { c : ConnectedIsoClass n // c.HasPassport P }

      The passport size counts the isomorphism classes having that passport.

      source
      theorem TauCeti.PassportSpec.isAdmissible_of_classSet_nonempty {n : ℕ} {P : PassportSpec n} (hP : P.classSet.Nonempty) :
      P.IsAdmissible

      A nonempty passport class set supplies admissible passport data.

      source
      theorem TauCeti.PassportSpec.classSet_eq_empty_of_not_isAdmissible {n : ℕ} {P : PassportSpec n} (hP : ¬P.IsAdmissible) :
      P.classSet = ∅

      An inadmissible passport has no isomorphism classes.

      source
      theorem TauCeti.PassportSpec.passportSize_eq_zero_of_not_isAdmissible {n : ℕ} {P : PassportSpec n} (hP : ¬P.IsAdmissible) :
      P.passportSize = 0

      An inadmissible passport has size zero.

      source
      @[simp]
      theorem TauCeti.PassportSpec.classSet_conjugate {n : ℕ} (P : PassportSpec n) (tau : Equiv.Perm (Fin n)) :
      (P.conjugate tau).classSet = P.classSet

      Conjugating the reference monodromy subgroup does not change the passport class set.

      source
      @[simp]
      theorem TauCeti.PassportSpec.passportSize_conjugate {n : ℕ} (P : PassportSpec n) (tau : Equiv.Perm (Fin n)) :
      (P.conjugate tau).passportSize = P.passportSize

      Conjugating the reference monodromy subgroup does not change the passport size.

      Invariants determined by a passport #

      source
      theorem TauCeti.PassportSpec.cycleData_eq_of_hasPassport {n : ℕ} {P : PassportSpec n} {t t' : ConnectedTriple n} (ht : HasPassport t P) (ht' : HasPassport t' P) :
      (↑t).cycleData = (↑t').cycleData

      Two connected triples in the same passport have identical ordered full cycle partitions.

      source
      theorem TauCeti.PassportSpec.eulerChar_eq_of_hasPassport {n : ℕ} {P : PassportSpec n} {t t' : ConnectedTriple n} (ht : HasPassport t P) (ht' : HasPassport t' P) :
      (↑t).eulerChar = (↑t').eulerChar

      Two connected triples in the same passport have equal Euler characteristic.

      source
      theorem TauCeti.PassportSpec.genus_eq_of_hasPassport {n : ℕ} {P : PassportSpec n} {t t' : ConnectedTriple n} (ht : HasPassport t P) (ht' : HasPassport t' P) :
      (↑t).genus = (↑t').genus

      Two connected triples in the same passport have equal genus.

      source
      theorem TauCeti.PassportSpec.orderTriple_eq_of_hasPassport {n : ℕ} {P : PassportSpec n} {t t' : ConnectedTriple n} (ht : HasPassport t P) (ht' : HasPassport t' P) :
      (↑t).orderTriple = (↑t').orderTriple

      Two connected triples in the same passport have equal ordered triples of permutation orders.

      source
      theorem TauCeti.PassportSpec.geometryType_eq_of_hasPassport {n : ℕ} {P : PassportSpec n} {t t' : ConnectedTriple n} (ht : HasPassport t P) (ht' : HasPassport t' P) :
      (↑t).geometryType = (↑t').geometryType

      Two connected triples in the same passport have the same spherical, Euclidean, or hyperbolic geometry type.