Disjoint sums of permutation triples

Two covers of the thrice-punctured sphere may be laid side by side, and the resulting cover has the disjoint union of their sheets. On the combinatorial side this is the juxtaposition of two permutation triples: TauCeti.PermutationTriple.disjointSum takes a triple of degree m and one of degree n to a triple of degree m + n, acting through finSumFinEquiv by the first triple on the first m labels and by the second on the last n.

Main results

• TauCeti.PermutationTriple.disjointSum: the construction, componentwise Equiv.Perm.finSumPerm.
• TauCeti.PermutationTriple.cycleData_disjointSum, TauCeti.PermutationTriple.cycleCounts_disjointSum: the cycle data of a disjoint sum is the concatenation of the cycle data of its summands, and the cycle counts add.
• TauCeti.PermutationTriple.monodromyGroup_disjointSum_le: the monodromy group of a disjoint sum consists of relabelings acting separately on the two blocks, and each of the two components lies in the monodromy group of the corresponding summand. The inclusion is strict in general — the monodromy group of the disjoint sum of a triple with itself is the diagonal, not the whole product.
• TauCeti.PermutationTriple.not_isConnected_disjointSum: a disjoint sum of two triples of nonzero degree is disconnected.
• TauCeti.PermutationTriple.indexedDisjointSum: the disjoint sum of an indexed family of triples of varying degrees, after a numbering of the disjoint union of their labels.

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.disjointSum {m n : ℕ} (s : PermutationTriple m) (t : PermutationTriple n) : PermutationTriple (m + n)

The disjoint sum of two permutation triples: the triple of degree m + n whose components act by those of s on the first m labels and by those of t on the last n. It is the combinatorial shadow of laying two covers of the thrice-punctured sphere side by side.

Equations

• s.disjointSum t = { σ0 := s.σ0.finSumPerm t.σ0, σ1 := s.σ1.finSumPerm t.σ1, σinf := s.σinf.finSumPerm t.σinf, product_eq_one := ⋯ }

@[simp]

theorem TauCeti.PermutationTriple.disjointSum_σ0 {m n : ℕ} (s : PermutationTriple m) (t : PermutationTriple n) : (s.disjointSum t).σ0 = s.σ0.finSumPerm t.σ0

@[simp]

theorem TauCeti.PermutationTriple.disjointSum_σ1 {m n : ℕ} (s : PermutationTriple m) (t : PermutationTriple n) : (s.disjointSum t).σ1 = s.σ1.finSumPerm t.σ1

@[simp]

theorem TauCeti.PermutationTriple.disjointSum_σinf {m n : ℕ} (s : PermutationTriple m) (t : PermutationTriple n) : (s.disjointSum t).σinf = s.σinf.finSumPerm t.σinf

@[simp]

theorem TauCeti.PermutationTriple.disjointSum_one_one {m n : ℕ} : disjointSum 1 1 = 1

The disjoint sum of two trivial triples is trivial.

@[simp]

theorem TauCeti.PermutationTriple.disjointSum_smul {m n : ℕ} (s : PermutationTriple m) (t : PermutationTriple n) (τ : Equiv.Perm (Fin m)) (υ : Equiv.Perm (Fin n)) : (τ • s).disjointSum (υ • t) = τ.finSumPerm υ • s.disjointSum t

Relabeling the two summands separately relabels their disjoint sum.

Cycle data

@[simp]

theorem TauCeti.PermutationTriple.cycleData_disjointSum {m n : ℕ} (s : PermutationTriple m) (t : PermutationTriple n) : (s.disjointSum t).cycleData = (s.cycleData.1 + t.cycleData.1, s.cycleData.2.1 + t.cycleData.2.1, s.cycleData.2.2 + t.cycleData.2.2)

The full cycle partitions of a disjoint sum are the concatenations of those of the two summands, branch point by branch point.

@[simp]

theorem TauCeti.PermutationTriple.cycleCounts_disjointSum {m n : ℕ} (s : PermutationTriple m) (t : PermutationTriple n) : (s.disjointSum t).cycleCounts = (s.cycleCounts.1 + t.cycleCounts.1, s.cycleCounts.2.1 + t.cycleCounts.2.1, s.cycleCounts.2.2 + t.cycleCounts.2.2)

The cycle counts of a disjoint sum are the sums of the cycle counts of the two summands, branch point by branch point.

Monodromy and connectedness

theorem TauCeti.PermutationTriple.monodromyGroup_disjointSum_le {m n : ℕ} (s : PermutationTriple m) (t : PermutationTriple n) : (s.disjointSum t).monodromyGroup ≤ Subgroup.map (Equiv.Perm.finSumPermHom m n) (s.monodromyGroup.prod t.monodromyGroup)

The monodromy group of a disjoint sum acts separately on the two blocks of labels, through the monodromy groups of the two summands. The inclusion is not an equality in general: the disjoint sum of a triple with itself has diagonal monodromy.

theorem TauCeti.PermutationTriple.apply_castAdd_mem_range_castAdd_of_mem_monodromyGroup {m n : ℕ} (s : PermutationTriple m) (t : PermutationTriple n) {g : Equiv.Perm (Fin (m + n))} (hg : g ∈ (s.disjointSum t).monodromyGroup) (i : Fin m) : g (Fin.castAdd n i) ∈ Set.range (Fin.castAdd n)

Every element of the monodromy group of a disjoint sum preserves the first block of labels, which is the reason the sum is disconnected.

theorem TauCeti.PermutationTriple.not_isConnected_disjointSum {m n : ℕ} (s : PermutationTriple m) (t : PermutationTriple n) (hm : m ≠ 0) (hn : n ≠ 0) : ¬(s.disjointSum t).IsConnected

A disjoint sum of two triples of nonzero degree is disconnected: no relabeling in its monodromy group carries a label of the first block to one of the second.

Indexed disjoint sums

def TauCeti.PermutationTriple.indexedDisjointSum {N : ℕ} {I : Type u_1} {d : I → ℕ} (t : (i : I) → PermutationTriple (d i)) (e : (i : I) × Fin (d i) ≃ Fin N) : PermutationTriple N

The disjoint sum of an indexed family of permutation triples, transported along a numbering of the sigma type of their labels. Unlike binary disjointSum, this construction permits the summand degrees to vary with the index.

Equations

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

@[simp]

theorem TauCeti.PermutationTriple.indexedDisjointSum_σ0 {N : ℕ} {I : Type u_1} {d : I → ℕ} (t : (i : I) → PermutationTriple (d i)) (e : (i : I) × Fin (d i) ≃ Fin N) : (indexedDisjointSum t e).σ0 = e.permCongr (Equiv.Perm.sigmaCongrRight fun (i : I) => (t i).σ0)

@[simp]

theorem TauCeti.PermutationTriple.indexedDisjointSum_σ1 {N : ℕ} {I : Type u_1} {d : I → ℕ} (t : (i : I) → PermutationTriple (d i)) (e : (i : I) × Fin (d i) ≃ Fin N) : (indexedDisjointSum t e).σ1 = e.permCongr (Equiv.Perm.sigmaCongrRight fun (i : I) => (t i).σ1)

@[simp]

theorem TauCeti.PermutationTriple.indexedDisjointSum_σinf {N : ℕ} {I : Type u_1} {d : I → ℕ} (t : (i : I) → PermutationTriple (d i)) (e : (i : I) × Fin (d i) ≃ Fin N) : (indexedDisjointSum t e).σinf = e.permCongr (Equiv.Perm.sigmaCongrRight fun (i : I) => (t i).σinf)