Classification of connected triples in small degrees

Through degree four, the ordered full cycle partitions determine a connected permutation triple up to simultaneous relabeling. Consequently every inhabited ordered passport in these degrees has size one, even without using its monodromy subgroup to distinguish classes.

The cycle-data tables list all three degree-two classes, all seven degree-three classes, and all twenty-six degree-four classes. The degree-four table also determines their genera and geometry types: six classes have genus one, four are Euclidean, three are hyperbolic, and the rest are spherical. Fixed points are included in every displayed partition.

The degree-four representatives realize exactly the cycle data in the table, and every connected degree-four triple is equivalent to one of them. Consequently the table classifies connected triples up to relabeling, determines their Euler characteristics, genera, and geometry types, counts the twenty-six isomorphism classes, and shows that every inhabited ordered passport through degree four contains a single class.

References

• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer 2004, §1.5.

def TauCeti.PermutationTriple.degreeFourCycleData : Finset (Multiset ℕ × Multiset ℕ × Multiset ℕ)

The twenty-six ordered cycle data realized by connected degree-four permutation triples.

Equations

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

theorem TauCeti.PermutationTriple.image_cycleData_four : Finset.image (fun (t : ConnectedTriple 4) => (↑t).cycleData) Finset.univ = degreeFourCycleData

The complete table of ordered full cycle data in degree four.

@[simp]

theorem TauCeti.PermutationTriple.cycleData_mem_degreeFourCycleData (t : ConnectedTriple 4) : (↑t).cycleData ∈ degreeFourCycleData

The ordered full cycle data of every connected degree-four triple appear in the table degreeFourCycleData.

theorem TauCeti.PermutationTriple.equivalent_iff_cycleData_eq_of_degree_le_four {n : ℕ} (hn : n ≤ 4) (t t' : ConnectedTriple n) : (↑t).Equivalent ↑t' ↔ (↑t).cycleData = (↑t').cycleData

Through degree four, the ordered full cycle partitions classify connected triples up to simultaneous relabeling. The monodromy group is not needed as an additional invariant.

theorem TauCeti.PermutationTriple.image_cycleData_one : Finset.image (fun (t : ConnectedTriple 1) => (↑t).cycleData) Finset.univ = {({1}, {1}, {1})}

The unique ordered cycle datum in degree one.

theorem TauCeti.PermutationTriple.image_cycleData_two : Finset.image (fun (t : ConnectedTriple 2) => (↑t).cycleData) Finset.univ = {({1, 1}, {2}, {2}), ({2}, {1, 1}, {2}), ({2}, {2}, {1, 1})}

The complete table of ordered full cycle data in degree two. The three classes differ by which branch point is unramified.

theorem TauCeti.PermutationTriple.image_cycleData_three : Finset.image (fun (t : ConnectedTriple 3) => (↑t).cycleData) Finset.univ = {({1, 1, 1}, {3}, {3}), ({3}, {1, 1, 1}, {3}), ({3}, {3}, {1, 1, 1}), ({2, 1}, {2, 1}, {3}), ({2, 1}, {3}, {2, 1}), ({3}, {2, 1}, {2, 1}), ({3}, {3}, {3})}

The complete table of ordered full cycle data in degree three. There are three cyclic spherical classes, three nonabelian spherical classes, and one cyclic Euclidean class.

theorem TauCeti.PermutationTriple.eulerChar_eq_ite_of_degree_four (t : ConnectedTriple 4) : (↑t).eulerChar = if (↑t).cycleData ∈ {({2, 2}, {4}, {4}), ({4}, {2, 2}, {4}), ({4}, {4}, {2, 2}), ({3, 1}, {4}, {4}), ({4}, {3, 1}, {4}), ({4}, {4}, {3, 1})} then 0 else 2

A connected degree-four triple has Euler characteristic zero precisely for the six cycle data obtained by placing two full four-cycles beside either two two-cycles or a three-cycle and a fixed point; all other degree-four classes have Euler characteristic two.

theorem TauCeti.PermutationTriple.genus_eq_ite_of_degree_four (t : ConnectedTriple 4) : (↑t).genus = if (↑t).cycleData ∈ {({2, 2}, {4}, {4}), ({4}, {2, 2}, {4}), ({4}, {4}, {2, 2}), ({3, 1}, {4}, {4}), ({4}, {3, 1}, {4}), ({4}, {4}, {3, 1})} then 1 else 0

A connected degree-four triple has genus one precisely for the six cycle data obtained by placing two full four-cycles beside either two two-cycles or a three-cycle and a fixed point; all other degree-four classes have genus zero.

theorem TauCeti.PermutationTriple.geometryType_eq_ite_of_degree_four (t : ConnectedTriple 4) : (↑t).geometryType = if (↑t).cycleData ∈ {({3, 1}, {4}, {4}), ({4}, {3, 1}, {4}), ({4}, {4}, {3, 1})} then GeometryType.hyperbolic else if (↑t).cycleData ∈ {({2, 2}, {4}, {4}), ({4}, {2, 2}, {4}), ({4}, {4}, {2, 2}), ({3, 1}, {3, 1}, {3, 1})} then GeometryType.euclidean else GeometryType.spherical

The exact geometry type of a connected degree-four triple, read from its ordered full cycle data. The three permutations of ([3,1], [4], [4]) are hyperbolic; the three permutations of ([2,2], [4], [4]) and ([3,1], [3,1], [3,1]) are Euclidean; all others are spherical.

theorem TauCeti.PermutationTriple.eulerChar_eq_ite_of_degree_le_three {n : ℕ} (hn : n ≤ 3) (t : ConnectedTriple n) : (↑t).eulerChar = if (↑t).cycleData = ({3}, {3}, {3}) then 0 else 2

Through degree three, the Euler characteristic is zero for the triple with three full three-cycles, and two for every other connected triple.

theorem TauCeti.PermutationTriple.genus_eq_ite_of_degree_le_three {n : ℕ} (hn : n ≤ 3) (t : ConnectedTriple n) : (↑t).genus = if (↑t).cycleData = ({3}, {3}, {3}) then 1 else 0

The unique positive-genus class through degree three is the class with full cycle partition [3] at all three branch points, and it has genus one.

theorem TauCeti.PermutationTriple.geometryType_eq_ite_of_degree_le_three {n : ℕ} (hn : n ≤ 3) (t : ConnectedTriple n) : (↑t).geometryType = if (↑t).cycleData = ({3}, {3}, {3}) then GeometryType.euclidean else GeometryType.spherical

The class with three full three-cycles is Euclidean; every other connected class through degree three is spherical.

theorem TauCeti.ConnectedIsoClass.card_four : Fintype.card (ConnectedIsoClass 4) = 26

There are twenty-six isomorphism classes of connected permutation triples of degree four.

theorem TauCeti.PassportSpec.classSet_eq_singleton_of_degree_le_four {n : ℕ} (hn : n ≤ 4) (P : PassportSpec n) (t : ConnectedTriple n) (ht : HasPassport t P) : P.classSet = {ConnectedIsoClass.mk t}

Through degree four, an inhabited ordered passport consists of exactly one isomorphism class. This is stronger than bounding its size: the class is identified by any member.

theorem TauCeti.PassportSpec.passportSize_eq_one_iff_of_degree_le_four {n : ℕ} (hn : n ≤ 4) (P : PassportSpec n) : P.passportSize = 1 ↔ ∃ (t : ConnectedTriple n), HasPassport t P

Through degree four, a passport has size one exactly when it is inhabited. Admissibility alone is not substituted for existence of a product-one triple.

theorem TauCeti.PassportSpec.passportSize_le_one_of_degree_le_four {n : ℕ} (hn : n ≤ 4) (P : PassportSpec n) : P.passportSize ≤ 1

Every ordered passport in degree at most four has size zero or one.

theorem TauCeti.ConnectedTriple.passportSize_passportOf_of_degree_le_four {n : ℕ} (hn : n ≤ 4) (t : ConnectedTriple n) : t.passportOf.passportSize = 1

The ordered passport of any connected triple through degree four has size one.