The primitivization of a passport record #
The stored primitivization of a row of the LMFDB table of Belyi passports is the label of a row of
the table of Belyi maps. Here that row is read as sharing the passport of the block quotient of the
chosen reference triple; this does not identify a particular quotient map, and it does not assert
that every map of the passport factors through a map of that row.
A valid passport row carries a block of sheets of its reference triple t, and a maximal proper
one (TauCeti.PermutationTriple.LMFDB.PassportRecord.IsValidAt). This file ties the stored label
to the mathematics through that block rather than through a label lookup:
TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsPrimitivizationOf q r t says that the map row q
carries the stored primitivization label of r, and that it is a valid row for the passport of
the quotient of t by the translates of the stored block
(TauCeti.PermutationTriple.blockQuotient).
Geometrically, the cover described by t factors through the cover described by the quotient, and
the fibres of the intermediate map are the translates of the block.
A primitivization is not canonical: a triple can have several maximal block systems. The row q
certifies the one chosen by the stored block, and nothing here asserts that another choice gives
the same passport.
The consequences read the stored fields of the two rows against each other: the stored triples of
q are primitive, because the stored block is maximal; the degree of r is the size of the block
times the degree of q; the stored genus of q is at most that of r; and the stored primitivity
flag of r is set exactly when q has the same degree as r, so that a primitive passport is
its own primitivization in degree.
Main definitions #
TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsPrimitivizationOf: a map row certifies the stored primitivization of a passport row.
Main results #
TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsPrimitivizationOf.isPrimitive_toTriple: the stored triples of the primitivization are primitive.TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsPrimitivizationOf.card_mul_deg: the degree of a passport row is the size of its primitivization block times the degree of its primitivization.TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsPrimitivizationOf.g_le: the primitivization has genus at most that of the passport.TauCeti.PermutationTriple.LMFDB.BelyiRecord.IsPrimitivizationOf.isPrimitive_eq_true_iff: the stored primitivity flag is set exactly when the primitivization has the same degree.
References #
- M. Musty, S. Schiavone, J. Sijsling, J. Voight, A database of Belyi maps.
- LMFDB, Belyi maps.
The map row q certifies the stored primitivization of the passport row r at the connected
triple t: the label of q is the stored primitivization label of r, and, for some numbering of
the translates of the primitivization block of r by the sheets of q, the row q is valid for
the passport of the quotient of t by those translates.
The label of the map row is the stored primitivization label.
- exists_isValidFor : ∃ (e : ↑(MulAction.orbit ↥(↑t).monodromyGroup ↑r.primitivizationBlock) ≃ Fin m), q.IsValidFor (ConnectedTriple.passportOf ⟨(↑t).blockQuotient (↑r.primitivizationBlock) e, ⋯⟩)
The map row is valid for the passport of the quotient by the primitivization block.
Instances For
The stored triples of the primitivization of a valid passport row denote primitive triples: the quotient by a maximal proper block is primitive.
The degree of a valid passport row is the size of its primitivization block times the degree of its primitivization.
The stored genus of the primitivization of a valid passport row is at most the stored genus of the passport row: passing to a block quotient does not increase the genus.
The stored primitivity flag of a valid passport row is set exactly when its primitivization has the same degree, that is, when the primitivization block is a single sheet.