Stable label data for permutation-triple passports

The stable mathematical part of a passport label consists of its degree, a transitive-group label, and the three ordered full cycle partitions at 0, 1, and ∞. The degree is the index of TauCeti.PassportLabel; the group index is zero-based internally, so an index j is displayed externally as nT(j + 1).

TauCeti.PassportSpec.HasLabel interprets this data on a passport specification. It uses TauCeti.TransitiveGroupLabel, so it compares the reference monodromy subgroup only up to conjugacy in the ambient symmetric group. Consequently the interpretation is unchanged when the reference subgroup of a passport is replaced by a conjugate.

This deliberately does not include a trailing orbit letter: such a letter enumerates Galois orbits inside a passport and is not an intrinsic invariant of the passport.

Main definitions

• TauCeti.PassportLabel: the stable degree, group, and ordered partition data of a label.
• TauCeti.PassportLabel.groupNumber: the one-based group number displayed after T.
• TauCeti.PassportLabel.toPassportSpec: the canonical passport using the reference subgroup.
• TauCeti.PassportSpec.HasLabel: interpretation of label data on a passport specification.

Main results

• TauCeti.PassportSpec.hasLabel_iff_exists_conjugate_eq_toPassportSpec: a passport has a label exactly when a conjugate of it is the canonical reference passport for that label.
• TauCeti.PassportSpec.hasLabel_conjugate_iff: label semantics is independent of the chosen representative of the reference monodromy subgroup.
• TauCeti.PassportSpec.hasLabel_iff_of_hasPassport: a passport containing a connected triple has the label read directly from that triple's monodromy and cycle data.

References

• LMFDB, Belyi map search labels.
• G. Butler and J. McKay, The transitive groups of degree up to eleven.

structure TauCeti.PassportLabel (n : ℕ) : Type

The stable mathematical data in a passport label of degree n.

The transitive-group index is zero-based. Thus group = j represents the externally displayed group label nT(j + 1). The three partitions remain ordered by the branch points 0, 1, and ∞.

• group : TransitiveGroupIndex n

  The zero-based index of the reference transitive group.

• lam0 : Multiset ℕ

  The full cycle partition at 0.

• lam1 : Multiset ℕ

  The full cycle partition at 1.

• laminf : Multiset ℕ

  The full cycle partition at ∞.

theorem TauCeti.PassportLabel.ext {n : ℕ} {x y : PassportLabel n} (group : x.group = y.group) (lam0 : x.lam0 = y.lam0) (lam1 : x.lam1 = y.lam1) (laminf : x.laminf = y.laminf) : x = y

theorem TauCeti.PassportLabel.ext_iff {n : ℕ} {x y : PassportLabel n} : x = y ↔ x.group = y.group ∧ x.lam0 = y.lam0 ∧ x.lam1 = y.lam1 ∧ x.laminf = y.laminf

@[instance_reducible]

instance TauCeti.instDecidableEqPassportLabel {n✝ : ℕ} : DecidableEq (PassportLabel n✝)

Equations

• TauCeti.instDecidableEqPassportLabel = TauCeti.instDecidableEqPassportLabel.decEq

def TauCeti.instDecidableEqPassportLabel.decEq {n✝ : ℕ} (x✝ x✝¹ : PassportLabel n✝) : Decidable (x✝ = x✝¹)

Equations

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

def TauCeti.PassportLabel.groupNumber {n : ℕ} (L : PassportLabel n) : ℕ

The one-based transitive-group number displayed after T in an nTj label.

Equations

• L.groupNumber = ↑L.group + 1

theorem TauCeti.PassportLabel.groupNumber_def {n : ℕ} (L : PassportLabel n) : L.groupNumber = ↑L.group + 1

The displayed group number is one more than the internal zero-based index.

theorem TauCeti.PassportLabel.groupNumber_pos {n : ℕ} (L : PassportLabel n) : 0 < L.groupNumber

The displayed transitive-group number is positive.

theorem TauCeti.PassportLabel.groupNumber_le {n : ℕ} (L : PassportLabel n) : L.groupNumber ≤ numTransitiveGroups n

The displayed transitive-group number does not exceed the number of supported reference groups in its degree.

def TauCeti.PassportLabel.toPassportSpec {n : ℕ} (L : PassportLabel n) : PassportSpec n

The canonical passport specification represented by a label, using the supplier's reference subgroup for its group component.

Equations

• L.toPassportSpec = { G := TauCeti.referenceSubgroup n L.group, lam0 := L.lam0, lam1 := L.lam1, laminf := L.laminf }

@[simp]

theorem TauCeti.PassportLabel.toPassportSpec_G {n : ℕ} (L : PassportLabel n) : L.toPassportSpec.G = referenceSubgroup n L.group

@[simp]

theorem TauCeti.PassportLabel.toPassportSpec_lam0 {n : ℕ} (L : PassportLabel n) : L.toPassportSpec.lam0 = L.lam0

@[simp]

theorem TauCeti.PassportLabel.toPassportSpec_lam1 {n : ℕ} (L : PassportLabel n) : L.toPassportSpec.lam1 = L.lam1

@[simp]

theorem TauCeti.PassportLabel.toPassportSpec_laminf {n : ℕ} (L : PassportLabel n) : L.toPassportSpec.laminf = L.laminf

def TauCeti.PassportSpec.HasLabel {n : ℕ} (P : PassportSpec n) (L : PassportLabel n) : Prop

A passport specification has label L when its reference subgroup has L's transitive-group label and its three ordered full cycle partitions are those recorded by L.

This predicate interprets the stable mathematical fields of a passport label. It does not assert that the passport is admissible and does not interpret any external orbit letter.

Equations

• P.HasLabel L = (TauCeti.TransitiveGroupLabel L.group P.G ∧ P.lam0 = L.lam0 ∧ P.lam1 = L.lam1 ∧ P.laminf = L.laminf)

theorem TauCeti.PassportSpec.hasLabel_iff {n : ℕ} (P : PassportSpec n) (L : PassportLabel n) : P.HasLabel L ↔ TransitiveGroupLabel L.group P.G ∧ P.lam0 = L.lam0 ∧ P.lam1 = L.lam1 ∧ P.laminf = L.laminf

The defining characterization of passport label semantics.

@[simp]

theorem TauCeti.PassportLabel.hasLabel_toPassportSpec {n : ℕ} (L : PassportLabel n) : L.toPassportSpec.HasLabel L

The canonical reference passport of a label has that label.

theorem TauCeti.PassportSpec.hasLabel_iff_exists_conjugate_eq_toPassportSpec {n : ℕ} (P : PassportSpec n) (L : PassportLabel n) : P.HasLabel L ↔ ∃ (τ : Equiv.Perm (Fin n)), P.conjugate τ = L.toPassportSpec

A passport has a label exactly when conjugating its reference subgroup can turn it into the canonical reference passport carrying that label data.

@[simp]

theorem TauCeti.PassportSpec.hasLabel_conjugate_iff {n : ℕ} (P : PassportSpec n) (L : PassportLabel n) (τ : Equiv.Perm (Fin n)) : (P.conjugate τ).HasLabel L ↔ P.HasLabel L

Replacing a passport's reference monodromy subgroup by a conjugate does not change its label.

theorem TauCeti.PassportSpec.hasLabel_iff_of_hasPassport {n : ℕ} {t : ConnectedTriple n} {P : PassportSpec n} (htP : HasPassport t P) (L : PassportLabel n) : P.HasLabel L ↔ TransitiveGroupLabel L.group (↑t).monodromyGroup ∧ (↑t).cycleData.1 = L.lam0 ∧ (↑t).cycleData.2.1 = L.lam1 ∧ (↑t).cycleData.2.2 = L.laminf

Read a label from any connected triple belonging to the passport: its group component is the transitive-group label of the monodromy group, and its partition components are the triple's ordered full cycle data.

@[simp]

theorem TauCeti.ConnectedTriple.passportOf_hasLabel_iff {n : ℕ} (t : ConnectedTriple n) (L : PassportLabel n) : t.passportOf.HasLabel L ↔ TransitiveGroupLabel L.group (↑t).monodromyGroup ∧ (↑t).cycleData.1 = L.lam0 ∧ (↑t).cycleData.2.1 = L.lam1 ∧ (↑t).cycleData.2.2 = L.laminf

The label of an attached passport is read directly from the connected triple's monodromy group and ordered full cycle data.