Decomposing permutation triples into connected components

Every permutation triple restricts to each orbit of its monodromy group. After numbering the points in every orbit, the original triple is the indexed disjoint sum of these restrictions. Thus the monodromy orbits are precisely the connected summands of a possibly disconnected triple.

The construction uses MulAction.selfEquivSigmaOrbits' for the canonical decomposition of the set of labels into its orbits. The only choices are the finite numberings within the individual orbits; the final reconstruction theorem is an equality because the global numbering is assembled from those same choices.

Main results

• TauCeti.PermutationTriple.restrictToOrbit restricts a triple to one monodromy orbit and numbers that orbit by a finite ordinal.
• TauCeti.PermutationTriple.isConnected_restrictToOrbit proves that every such restriction is connected.
• TauCeti.PermutationTriple.card_monodromyOrbit_smul: relabeling the sheets does not change the number of monodromy orbits.
• TauCeti.PermutationTriple.indexedDisjointSum_restrictToOrbit reconstructs the original triple from all its orbit restrictions.

References

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

Restriction to monodromy orbits

@[reducible, inline]

abbrev TauCeti.PermutationTriple.MonodromyOrbit {n : ℕ} (t : PermutationTriple n) : Type

The finite type indexing the orbits of the monodromy group of a permutation triple.

Equations

• t.MonodromyOrbit = MulAction.orbitRel.Quotient (↥t.monodromyGroup) (Fin n)

noncomputable def TauCeti.PermutationTriple.orbitActionHom {n : ℕ} (t : PermutationTriple n) (O : t.MonodromyOrbit) : ↥t.monodromyGroup →* Equiv.Perm (Fin (MulAction.orbitRel.Quotient.orbit O).ncard)

The action of the monodromy group on one of its orbits, transported to the finite ordinal numbering that is used by restrictToOrbit.

Equations

• t.orbitActionHom O = (Finite.equivFinOfCardEq ⋯).permCongrHom.toMonoidHom.comp (MulAction.toPermHom ↥t.monodromyGroup ↑(MulAction.orbitRel.Quotient.orbit O))

@[simp]

theorem TauCeti.PermutationTriple.orbitActionHom_apply {n : ℕ} (t : PermutationTriple n) (O : t.MonodromyOrbit) (g : ↥t.monodromyGroup) (i : Fin (MulAction.orbitRel.Quotient.orbit O).ncard) : (Finite.equivFinOfCardEq ⋯).symm (((t.orbitActionHom O) g) i) = g • (Finite.equivFinOfCardEq ⋯).symm i

Evaluating the transported orbit action and then undoing the finite numbering recovers the original action on the orbit.

noncomputable def TauCeti.PermutationTriple.restrictToOrbit {n : ℕ} (t : PermutationTriple n) (O : t.MonodromyOrbit) : PermutationTriple (MulAction.orbitRel.Quotient.orbit O).ncard

The restriction of a permutation triple to a monodromy orbit, numbered by Fin O.orbit.ncard.

Equations

• t.restrictToOrbit O = t.mapMonodromy (t.orbitActionHom O)

@[simp]

theorem TauCeti.PermutationTriple.restrictToOrbit_σ0 {n : ℕ} (t : PermutationTriple n) (O : t.MonodromyOrbit) : (t.restrictToOrbit O).σ0 = (t.orbitActionHom O) ⟨t.σ0, ⋯⟩

@[simp]

theorem TauCeti.PermutationTriple.restrictToOrbit_σ1 {n : ℕ} (t : PermutationTriple n) (O : t.MonodromyOrbit) : (t.restrictToOrbit O).σ1 = (t.orbitActionHom O) ⟨t.σ1, ⋯⟩

@[simp]

theorem TauCeti.PermutationTriple.restrictToOrbit_σinf {n : ℕ} (t : PermutationTriple n) (O : t.MonodromyOrbit) : (t.restrictToOrbit O).σinf = (t.orbitActionHom O) ⟨t.σinf, ⋯⟩

theorem TauCeti.PermutationTriple.monodromyGroup_restrictToOrbit {n : ℕ} (t : PermutationTriple n) (O : t.MonodromyOrbit) : (t.restrictToOrbit O).monodromyGroup = (t.orbitActionHom O).range

The monodromy group of an orbit restriction is the image of the original monodromy group on that orbit.

theorem TauCeti.PermutationTriple.isConnected_restrictToOrbit {n : ℕ} (t : PermutationTriple n) (O : t.MonodromyOrbit) : (t.restrictToOrbit O).IsConnected

Every monodromy-orbit restriction is connected.

@[simp]

theorem TauCeti.PermutationTriple.card_monodromyOrbit_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : Nat.card (τ • t).MonodromyOrbit = Nat.card t.MonodromyOrbit

Relabeling the sheets does not change the number of monodromy orbits.

Sheets in one monodromy orbit

@[simp]

theorem TauCeti.PermutationTriple.mk_σ0_apply {n : ℕ} (t : PermutationTriple n) (x : Fin n) : ⟦t.σ0 x⟧ = ⟦x⟧

A sheet and its image under the first component lie in one monodromy orbit.

@[simp]

theorem TauCeti.PermutationTriple.mk_σ1_apply {n : ℕ} (t : PermutationTriple n) (x : Fin n) : ⟦t.σ1 x⟧ = ⟦x⟧

A sheet and its image under the second component lie in one monodromy orbit.

Reconstruction

noncomputable def TauCeti.PermutationTriple.orbitDecompositionEquiv {n : ℕ} (t : PermutationTriple n) : (O : t.MonodromyOrbit) × Fin (MulAction.orbitRel.Quotient.orbit O).ncard ≃ Fin n

The numbering of the disjoint union of the numbered monodromy orbits induced by the canonical orbit decomposition of the original labels.

Equations

• t.orbitDecompositionEquiv = (Equiv.sigmaCongrRight fun (O : t.MonodromyOrbit) => (Finite.equivFinOfCardEq ⋯).symm).trans (MulAction.selfEquivSigmaOrbits' (↥t.monodromyGroup) (Fin n)).symm

@[simp]

theorem TauCeti.PermutationTriple.orbitDecompositionEquiv_apply_val {n : ℕ} (t : PermutationTriple n) (O : t.MonodromyOrbit) (i : Fin (MulAction.orbitRel.Quotient.orbit O).ncard) : t.orbitDecompositionEquiv ⟨O, i⟩ = ↑((Finite.equivFinOfCardEq ⋯).symm i)

The orbit-decomposition numbering agrees with the chosen numbering on each orbit.

@[simp]

theorem TauCeti.PermutationTriple.indexedDisjointSum_restrictToOrbit {n : ℕ} (t : PermutationTriple n) : indexedDisjointSum (fun (O : t.MonodromyOrbit) => t.restrictToOrbit O) t.orbitDecompositionEquiv = t

A permutation triple is the indexed disjoint sum of its restrictions to the orbits of its monodromy group. In particular, every summand is connected by isConnected_restrictToOrbit.