Examples of passports and their enumeration

The degree-one cyclic passport has a singleton branch-point orbit. The torus passport changes under an exchange of branch points, witnessing that passing to the orbit is strictly coarser than equality of ordered passports. The computed passport fibers in degrees one to three have size one; the degree-three check uses the nonabelian symmetric monodromy group. For that passport, the generating count, centralizer order and normalizer order evaluate the normalizer formula as 1 = 6 * 1 / 6.

The passport of the cyclic triple z ↦ zⁿ carries the label nT1 with partitions ([n], [1, …, 1], [n]) in every degree with transitive-group labels. For the isomorphic pair formed by cyclicTriple 4 and its relabeling by swap 0 1, the two passports are equal as passports: they have the same class set and the same label. The attached passport specifications nevertheless differ, because relabeling moves the reference monodromy subgroup to a conjugate subgroup that is not equal to it.

theorem TauCeti.card_passportClasses_one : (passportClasses Finset.univ {1} {1} {1}).card = 1

The degree-one passport has one class, computed with its whole symmetric group.

theorem TauCeti.card_passportClasses_cyclic_two : (passportClasses Finset.univ {2} {1, 1} {2}).card = 1

The degree-two cyclic passport, ramified over 0 and ∞, has one class.

theorem TauCeti.card_passportClasses_symmetric_three : (passportClasses Finset.univ {3} {2, 1} {2, 1}).card = 1

The degree-three passport with symmetric monodromy and ordered partitions ([3], [2, 1], [2, 1]) has one class.

theorem TauCeti.PermutationTriple.passportSize_passportOf_s3Triple : (ConnectedTriple.passportOf ⟨s3Triple, isConnected_s3Triple⟩).passportSize = 1

The passport of the degree-three symmetric triple has size one.

theorem TauCeti.PermutationTriple.passportSize_formula_s3Triple : have P := ConnectedTriple.passportOf ⟨s3Triple, isConnected_s3Triple⟩; P.G.genCountType P.lam0 P.lam1 P.laminf = 6 ∧ Nat.card ↥(Subgroup.centralizer ↑P.G) = 1 ∧ Nat.card ↥(Subgroup.normalizer ↑P.G) = 6 ∧ P.passportSize = 6 * 1 / 6

For the degree-three symmetric passport, the normalizer formula reads 1 = 6 * 1 / 6: there are six generating triples of the prescribed cycle types, the centralizer of the monodromy group is trivial, and its normalizer is the full symmetric group.

theorem TauCeti.PermutationTriple.orbit_orderedPassportOf_cyclicTriple_one : MulAction.orbit (Equiv.Perm (Fin 3))ᵐᵒᵖ (ConnectedTriple.orderedPassportOf ⟨cyclicTriple 1, ⋯⟩) = {ConnectedTriple.orderedPassportOf ⟨cyclicTriple 1, ⋯⟩}

The degree-one cyclic triple has a singleton branch-point orbit of ordered passports.

theorem TauCeti.PermutationTriple.exists_ne_mem_orbit_orderedPassportOf_torusTriple : ∃ Q ∈ MulAction.orbit (Equiv.Perm (Fin 3))ᵐᵒᵖ (ConnectedTriple.orderedPassportOf ⟨torusTriple, isConnected_torusTriple⟩), Q ≠ ConnectedTriple.orderedPassportOf ⟨torusTriple, isConnected_torusTriple⟩

Different ordered passports can have the same branch-point orbit: exchanging 1 and ∞ changes the torus passport from ([4], [4], [2, 2]) to ([4], [2, 2], [4]).

theorem TauCeti.PermutationTriple.hasLabel_passportOf_cyclicTriple {n : ℕ} (h : 0 < numTransitiveGroups n) : (ConnectedTriple.passportOf ⟨cyclicTriple n, ⋯⟩).HasLabel { group := ⟨0, h⟩, lam0 := {n}, lam1 := Multiset.replicate n 1, laminf := {n} }

The passport of the cyclic triple z ↦ zⁿ has label nT1 with ordered partitions ([n], [1, …, 1], [n]), in every degree in which transitive-group labels exist.

theorem TauCeti.PermutationTriple.classSet_passportOf_swap_smul_cyclicTriple_four : (Equiv.swap 0 1 • ⟨cyclicTriple 4, ⋯⟩).passportOf.classSet = (ConnectedTriple.passportOf ⟨cyclicTriple 4, ⋯⟩).classSet

Relabeling cyclicTriple 4 by swap 0 1 does not change its passport class set.

theorem TauCeti.PermutationTriple.hasLabel_passportOf_swap_smul_cyclicTriple_four : (Equiv.swap 0 1 • ⟨cyclicTriple 4, ⋯⟩).passportOf.HasLabel { group := ⟨0, hasLabel_passportOf_swap_smul_cyclicTriple_four._proof_1⟩, lam0 := {4}, lam1 := {1, 1, 1, 1}, laminf := {4} }

The relabeling of cyclicTriple 4 by swap 0 1 has the same passport label as cyclicTriple 4: the group 4T1 with ordered partitions ([4], [1, 1, 1, 1], [4]).

theorem TauCeti.PermutationTriple.passportOf_swap_smul_cyclicTriple_four_ne : (Equiv.swap 0 1 • ⟨cyclicTriple 4, ⋯⟩).passportOf ≠ ConnectedTriple.passportOf ⟨cyclicTriple 4, ⋯⟩

The passport specifications attached to cyclicTriple 4 and to its relabeling by swap 0 1 are different: relabeling replaces the reference subgroup generated by finRotate 4 with the subgroup generated by c[0, 2, 3, 1], which does not contain finRotate 4. Equality of passports is therefore equality up to conjugating the reference subgroup, as in classSet_passportOf_swap_smul_cyclicTriple_four.