Cycle data of permutation triples

The cycle data of a permutation triple records, in the ordered branch-point convention 0, 1, ∞, the full cycle partition of each component. These are the parts of Mathlib's Equiv.Perm.partition, rather than Equiv.Perm.cycleType: fixed points therefore appear as parts equal to one.

TauCeti.PermutationTriple.cycleData packages the three partitions, computed using Equiv.Perm.computedCycleType, and TauCeti.PermutationTriple.cycleCounts packages their numbers of parts. The latter is expressed using TauCeti.orbitCount, and cycleCounts_eq_card_cycleData identifies the two descriptions. The remaining results record that every partition sums to the degree and that both invariants are unchanged by simultaneous relabeling, transport of the sheet type, inversion of the convention, and isomorphism of triples.

References

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

def TauCeti.PermutationTriple.cycleData {n : ℕ} (t : PermutationTriple n) : Multiset ℕ × Multiset ℕ × Multiset ℕ

The ordered full cycle partitions of the three components of a permutation triple. Fixed points occur as parts equal to one. The executable body is exposed for kernel computations in importing modules; the component equations identify it with Mathlib's partitions.

Equations

• t.cycleData = (t.σ0.computedCycleType, t.σ1.computedCycleType, t.σinf.computedCycleType)

@[simp]

theorem TauCeti.PermutationTriple.cycleData_σ0 {n : ℕ} (t : PermutationTriple n) : t.cycleData.1 = t.σ0.partition.parts

@[simp]

theorem TauCeti.PermutationTriple.cycleData_σ1 {n : ℕ} (t : PermutationTriple n) : t.cycleData.2.1 = t.σ1.partition.parts

@[simp]

theorem TauCeti.PermutationTriple.cycleData_σinf {n : ℕ} (t : PermutationTriple n) : t.cycleData.2.2 = t.σinf.partition.parts

noncomputable def TauCeti.PermutationTriple.cycleCounts {n : ℕ} (t : PermutationTriple n) : ℕ × ℕ × ℕ

The ordered numbers of cycles of the three components, with fixed points included.

Equations

• t.cycleCounts = (TauCeti.orbitCount t.σ0, TauCeti.orbitCount t.σ1, TauCeti.orbitCount t.σinf)

@[simp]

theorem TauCeti.PermutationTriple.cycleCounts_σ0 {n : ℕ} (t : PermutationTriple n) : t.cycleCounts.1 = orbitCount t.σ0

@[simp]

theorem TauCeti.PermutationTriple.cycleCounts_σ1 {n : ℕ} (t : PermutationTriple n) : t.cycleCounts.2.1 = orbitCount t.σ1

@[simp]

theorem TauCeti.PermutationTriple.cycleCounts_σinf {n : ℕ} (t : PermutationTriple n) : t.cycleCounts.2.2 = orbitCount t.σinf

theorem TauCeti.PermutationTriple.cycleCounts_eq_card_cycleData {n : ℕ} (t : PermutationTriple n) : t.cycleCounts = (t.cycleData.1.card, t.cycleData.2.1.card, t.cycleData.2.2.card)

The cycle counts of a triple are the cardinalities of its three full cycle partitions.

theorem TauCeti.PermutationTriple.sum_cycleData {n : ℕ} (t : PermutationTriple n) : (t.cycleData.1.sum, t.cycleData.2.1.sum, t.cycleData.2.2.sum) = (n, n, n)

Each full cycle partition of a degree-n triple sums to n.

@[simp]

theorem TauCeti.PermutationTriple.cycleData_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : (τ • t).cycleData = t.cycleData

Simultaneous relabeling leaves the ordered cycle data unchanged.

@[simp]

theorem TauCeti.PermutationTriple.cycleCounts_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : (τ • t).cycleCounts = t.cycleCounts

Simultaneous relabeling leaves all three cycle counts unchanged.

@[simp]

theorem TauCeti.PermutationTriple.cycleData_transport {n m : ℕ} (e : Fin n ≃ Fin m) (t : PermutationTriple n) : ((transport e) t).cycleData = t.cycleData

Transporting the labels of the sheets leaves the ordered cycle data unchanged.

@[simp]

theorem TauCeti.PermutationTriple.cycleCounts_transport {n m : ℕ} (e : Fin n ≃ Fin m) (t : PermutationTriple n) : ((transport e) t).cycleCounts = t.cycleCounts

Transporting the labels of the sheets leaves all three cycle counts unchanged.

theorem TauCeti.PermutationTriple.cycleData_inv_components {n : ℕ} (t : PermutationTriple n) : (t.σ0⁻¹.partition.parts, t.σ1⁻¹.partition.parts, t.σinf⁻¹.partition.parts) = t.cycleData

Inverting all three components, as in the passage to the opposite composition convention, leaves the ordered cycle data unchanged.

theorem TauCeti.PermutationTriple.cycleCounts_inv_components {n : ℕ} (t : PermutationTriple n) : (orbitCount t.σ0⁻¹, orbitCount t.σ1⁻¹, orbitCount t.σinf⁻¹) = t.cycleCounts

Inverting all three components leaves their ordered numbers of cycles unchanged.

theorem TauCeti.PermutationTriple.cycleData_eq_of_equivalent {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') : t.cycleData = t'.cycleData

Isomorphic permutation triples have the same ordered cycle data.

theorem TauCeti.PermutationTriple.cycleCounts_eq_of_equivalent {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') : t.cycleCounts = t'.cycleCounts

Isomorphic permutation triples have the same ordered numbers of cycles.