Passport records

A passport record mirrors one row of the LMFDB table of Belyi passports: the stored fields plabel, deg, group, abc, a_s/b_s/c_s, lambdas, g, geomtype, pass_size, num_orbits, maxdegbf, is_primitive, primitivization, aut_group and triples, parsed into Lean data. Two fields carry certificate data besides their stored strings: the primitivization carries a block of sheets, and the automorphism group carries a list of generators.

TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt states what such a row asserts about the passport of a connected triple t, which must be one of the stored triples and on whose sheets the certificate data are read. Each field is tied to the invariant it records:

• deg is the degree, which is also the index of the record type;
• lambdas is the ordered full cycle data of t, fixed points included;
• abc is the order triple of t, in the order 0, 1, ∞, and is not sorted, while the search triple (a_s, b_s, c_s) is abc sorted ascending;
• g is the genus, and geomtype the geometry type, which is computed from abc and is not a function of the genus;
• group is the number j of a transitive-group label nTj of the monodromy group, so a valid record exists only in a degree with reference groups (TauCeti.numTransitiveGroups);
• pass_size is the passport size, the number of isomorphism classes of connected triples in the passport, rather than a count of stored rows;
• is_primitive records primitivity of the monodromy action;
• the primitivization block is a maximal proper block of the monodromy action of t;
• the automorphism-group generators generate the automorphism group of t;
• every stored triple lies in the passport of t.

The aggregations num_orbits and maxdegbf describe which map rows the table contains, and the label and name strings are not interpreted here, so validity imposes no condition on them. The stored primitivization label is tied to the map row it names, through the quotient by the primitivization block, by TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsPrimitivizationOf.

The certified fields other than the certificate data are passport invariants: the theorems below read them from any connected triple sharing a passport with t.

Main definitions

• TauCeti.PermutationTriple.LMFDB.PassportRecord: a parsed passport row.
• TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt: validity of a row for the passport of a stored reference triple.

Main results

• TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.abc_eq_lcm_lambdas: each stored order is the least common multiple of the corresponding stored partition.
• TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.passSize_eq_natCard: the stored passport size counts isomorphism classes.
• TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.exists_hasLabel: the stored group and partitions form a label of every passport containing the reference triple.
• TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.g_eq_genus and its companions: the certified fields are invariants of the passport.

References

• M. Musty, S. Schiavone, J. Sijsling, J. Voight, A database of Belyi maps.
• LMFDB, Belyi maps.

structure TauCeti.PermutationTriple.LMFDB.PassportRecord (n : ℕ) : Type

A row of the LMFDB table of Belyi passports in degree n, with its stored fields parsed into Lean data. The stored degree is the field deg, which validity identifies with n.

Besides the stored fields, the primitivization and the automorphism group carry certificate data: a block of sheets and a list of generators, read on the sheets of a stored triple. The stored triples are recorded in this library's multiplication convention, in which a triple satisfies σinf * σ1 * σ0 = 1.

• plabel : String

  The stored passport label. It is carried as a string and is not interpreted here.

• deg : ℕ

  The stored degree.

• group : ℕ

  The number j of the stored transitive-group label nTj of the monodromy group.

• abc : ℕ × ℕ × ℕ

  The stored orders of the monodromy at 0, 1, and ∞, in that order.

• sortedAbc : ℕ × ℕ × ℕ

  The stored search triple (a_s, b_s, c_s) of orders, sorted ascending.

• lambdas : Multiset ℕ × Multiset ℕ × Multiset ℕ

  The stored full cycle partitions at 0, 1, and ∞, fixed points included.

• g : ℕ

  The stored genus.

• geomtype : GeometryType

  The stored geometry type.

• passSize : ℕ

  The stored passport size.

• numOrbits : ℕ

  The stored number of map rows sharing the passport label.

• maxdegbf : ℕ

  The stored largest orbit size among the map rows sharing the passport label.

• isPrimitive : Bool

  The stored primitivity flag.

• primitivization : String

  The stored label of the primitivization. It is carried as a string.

• primitivizationBlock : Finset (Fin n)

  A block of sheets of the reference triple, certifying the primitivization: its translates form the block system whose quotient is the primitivization.

• autGroup : String

  The stored name of the automorphism group. It is carried as a string.

• autGroupGenerators : List (Equiv.Perm (Fin n))

  Generators of the automorphism group of the reference triple, certifying autGroup.

• triples : List (PermutationTriple n)

  The stored permutation triples, in this library's multiplication convention.

structure TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt {n : ℕ} (r : PassportRecord n) (t : ConnectedTriple n) : Prop

The record r is a valid row for the passport of the connected triple t: the triple t is one of the stored triples, the certificate data of r are correct on the sheets of t, and every other certified field is the corresponding invariant of t.

The aggregations numOrbits and maxdegbf, and the strings plabel, primitivization and autGroup, are not constrained.

• deg_eq : r.deg = n

  The stored degree is the degree.

• mem_triples : ↑t ∈ r.triples

  The reference triple is one of the stored triples.

• hasPassport_of_mem_triples (s : PermutationTriple n) : s ∈ r.triples → ∃ (hs : s.IsConnected), PassportSpec.HasPassport ⟨s, hs⟩ t.passportOf

  Every stored triple is connected and lies in the passport of the reference triple.

• lambdas_eq : r.lambdas = (↑t).cycleData

  The stored partitions are the ordered full cycle data.

• abc_eq : r.abc = (↑t).orderTriple

  The stored orders are the order triple, positionally.

• sortedAbc_eq : [r.sortedAbc.1, r.sortedAbc.2.1, r.sortedAbc.2.2] = {r.abc.1, r.abc.2.1, r.abc.2.2}.sort fun (a b : ℕ) => a ≤ b

  The stored search triple is the stored order triple sorted ascending.

• g_eq : r.g = (↑t).genus

  The stored genus is the genus.

• geomtype_eq : r.geomtype = (↑t).geometryType

  The stored geometry type is the geometry type.

• exists_transitiveGroupLabel : ∃ (j : TransitiveGroupIndex n), ↑j + 1 = r.group ∧ TransitiveGroupLabel j (↑t).monodromyGroup

  The stored group number displays a transitive-group label of the monodromy group.

• passSize_eq : r.passSize = t.passportOf.passportSize

  The stored passport size is the passport size.

• isPrimitive_eq_true_iff : r.isPrimitive = true ↔ (↑t).IsPrimitive

  The stored primitivity flag is set exactly for a primitive triple.

• isBlock_primitivizationBlock : MulAction.IsBlock ↥(↑t).monodromyGroup ↑r.primitivizationBlock

  The primitivization block is a block of the monodromy action.

• primitivizationBlock_nonempty : r.primitivizationBlock.Nonempty

  The primitivization block is nonempty.

• deg_eq_one_of_primitivizationBlock_eq_univ : r.primitivizationBlock = Finset.univ → n = 1

  The primitivization block is proper, unless the degree is one.

• eq_or_eq_univ_of_primitivizationBlock_subset (C : Set (Fin n)) : MulAction.IsBlock (↥(↑t).monodromyGroup) C → ↑r.primitivizationBlock ⊆ C → C = ↑r.primitivizationBlock ∨ C = Set.univ

  No block lies strictly between the primitivization block and the set of all sheets.

• closure_autGroupGenerators : Subgroup.closure {τ : Equiv.Perm (Fin n) | τ ∈ r.autGroupGenerators} = (↑t).automorphismGroup

  The automorphism-group generators generate the automorphism group.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.abc_eq_lcm_lambdas {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} (h : r.IsValidAt t) : r.abc = (r.lambdas.1.lcm, r.lambdas.2.1.lcm, r.lambdas.2.2.lcm)

Each stored order is the least common multiple of the stored partition at the same branch point.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.sortedAbc_le {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} (h : r.IsValidAt t) : r.sortedAbc.1 ≤ r.sortedAbc.2.1 ∧ r.sortedAbc.2.1 ≤ r.sortedAbc.2.2

The stored search triple is weakly increasing.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.sortedAbc_perm {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} (h : r.IsValidAt t) : {r.sortedAbc.1, r.sortedAbc.2.1, r.sortedAbc.2.2} = {r.abc.1, r.abc.2.1, r.abc.2.2}

The stored search triple is a rearrangement of the stored order triple.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.geomtype_eq_spherical_iff {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} (h : r.IsValidAt t) : r.geomtype = GeometryType.spherical ↔ 1 < (↑r.abc.1)⁻¹ + (↑r.abc.2.1)⁻¹ + (↑r.abc.2.2)⁻¹

The stored geometry type is spherical exactly when the reciprocals of the stored orders sum to more than one.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.geomtype_eq_euclidean_iff {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} (h : r.IsValidAt t) : r.geomtype = GeometryType.euclidean ↔ (↑r.abc.1)⁻¹ + (↑r.abc.2.1)⁻¹ + (↑r.abc.2.2)⁻¹ = 1

The stored geometry type is Euclidean exactly when the reciprocals of the stored orders sum to one.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.geomtype_eq_hyperbolic_iff {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} (h : r.IsValidAt t) : r.geomtype = GeometryType.hyperbolic ↔ (↑r.abc.1)⁻¹ + (↑r.abc.2.1)⁻¹ + (↑r.abc.2.2)⁻¹ < 1

The stored geometry type is hyperbolic exactly when the reciprocals of the stored orders sum to less than one.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.passSize_eq_natCard {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} (h : r.IsValidAt t) : r.passSize = Nat.card { c : ConnectedIsoClass n // c.HasPassport t.passportOf }

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

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.passSize_eq_passportSize {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} (h : r.IsValidAt t) {P : PassportSpec n} (hP : PassportSpec.HasPassport t P) : r.passSize = P.passportSize

The stored passport size is the size of every passport containing the reference triple.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.passSize_pos {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} (h : r.IsValidAt t) : 0 < r.passSize

The stored passport size is positive.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.exists_hasLabel {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} (h : r.IsValidAt t) {P : PassportSpec n} (hP : PassportSpec.HasPassport t P) : ∃ (L : PassportLabel n), L.groupNumber = r.group ∧ (L.lam0, L.lam1, L.laminf) = r.lambdas ∧ P.HasLabel L

The stored group number and partitions form a label of every passport containing the reference triple.

Passport invariance of the certified fields

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.lambdas_eq_cycleData {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} {P : PassportSpec n} {t' : ConnectedTriple n} (h : r.IsValidAt t) (hP : PassportSpec.HasPassport t P) (ht' : PassportSpec.HasPassport t' P) : r.lambdas = (↑t').cycleData

The stored partitions are the ordered full cycle data of every triple in a passport containing the reference triple.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.abc_eq_orderTriple {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} {P : PassportSpec n} {t' : ConnectedTriple n} (h : r.IsValidAt t) (hP : PassportSpec.HasPassport t P) (ht' : PassportSpec.HasPassport t' P) : r.abc = (↑t').orderTriple

The stored orders are the order triple of every triple in a passport containing the reference triple.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.g_eq_genus {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} {P : PassportSpec n} {t' : ConnectedTriple n} (h : r.IsValidAt t) (hP : PassportSpec.HasPassport t P) (ht' : PassportSpec.HasPassport t' P) : r.g = (↑t').genus

The stored genus is the genus of every triple in a passport containing the reference triple.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.geomtype_eq_geometryType {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} {P : PassportSpec n} {t' : ConnectedTriple n} (h : r.IsValidAt t) (hP : PassportSpec.HasPassport t P) (ht' : PassportSpec.HasPassport t' P) : r.geomtype = (↑t').geometryType

The stored geometry type is the geometry type of every triple in a passport containing the reference triple.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.exists_transitiveGroupLabel_of_hasPassport {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} {P : PassportSpec n} {t' : ConnectedTriple n} (h : r.IsValidAt t) (hP : PassportSpec.HasPassport t P) (ht' : PassportSpec.HasPassport t' P) : ∃ (j : TransitiveGroupIndex n), ↑j + 1 = r.group ∧ TransitiveGroupLabel j (↑t').monodromyGroup

The stored group number displays a transitive-group label of the monodromy group of every triple in a passport containing the reference triple.

theorem TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt.isPrimitive_eq_true_iff_of_hasPassport {n : ℕ} {r : PassportRecord n} {t : ConnectedTriple n} {P : PassportSpec n} {t' : ConnectedTriple n} (h : r.IsValidAt t) (hP : PassportSpec.HasPassport t P) (ht' : PassportSpec.HasPassport t' P) : r.isPrimitive = true ↔ (↑t').IsPrimitive

The stored primitivity flag is set exactly when a triple in a passport containing the reference triple is primitive.