Deciding connectedness of a permutation triple

A permutation triple is connected when its monodromy group, the subgroup of Equiv.Perm (Fin n) generated by its first two components, acts transitively on the n sheets. Transitivity of a subgroup given by generators carries no Decidable instance as stated, so this file computes the monodromy orbit of each sheet as a finset by closing under the two generators, Finset.orbitFinset, and proves that connectedness is the statement that every such orbit is the whole of Fin n. That statement is a Boolean computation, and it gives the Decidable instance for IsConnected which every enumeration of connected triples filters by. The same closure applied to the group itself presents the monodromy group as a finset of permutations, with its order as the cardinality of that finset.

Main definitions

• TauCeti.PermutationTriple.monodromyOrbitFinset: the monodromy orbit of a sheet, as a finset.
• TauCeti.PermutationTriple.monodromyFinset: the monodromy group, as a finset of permutations.

Main results

• TauCeti.PermutationTriple.coe_monodromyOrbitFinset: the finset is the monodromy orbit.
• TauCeti.PermutationTriple.isConnected_iff_forall_monodromyOrbitFinset_eq_univ: a triple is connected exactly when its degree is nonzero and every sheet's computed orbit is everything.
• the Decidable instance for TauCeti.PermutationTriple.IsConnected.
• TauCeti.PermutationTriple.coe_monodromyFinset, TauCeti.PermutationTriple.card_monodromyFinset: the finset is the monodromy group, and its cardinality is the order of the monodromy group.

def TauCeti.PermutationTriple.generators {n : ℕ} (t : PermutationTriple n) : Finset (Equiv.Perm (Fin n))

The two components generating the monodromy group, as a finset. Its coercion to a set is the generating set of TauCeti.PermutationTriple.monodromyGroup, by Finset.coe_pair.

Equations

• t.generators = {t.σ0, t.σ1}

@[simp]

theorem TauCeti.PermutationTriple.coe_generators {n : ℕ} (t : PermutationTriple n) : ↑t.generators = {t.σ0, t.σ1}

theorem TauCeti.PermutationTriple.closure_generators_eq_monodromyGroup {n : ℕ} (t : PermutationTriple n) : Subgroup.closure ↑t.generators = t.monodromyGroup

Monodromy orbits, computed

def TauCeti.PermutationTriple.monodromyOrbitFinset {n : ℕ} (t : PermutationTriple n) (i : Fin n) : Finset (Fin n)

The monodromy orbit of the sheet i, as a finset: the closure of {i} under the two generating permutations, computed by Finset.orbitFinset.

Equations

• t.monodromyOrbitFinset i = t.generators.orbitFinset i

@[simp]

theorem TauCeti.PermutationTriple.coe_monodromyOrbitFinset {n : ℕ} (t : PermutationTriple n) (i : Fin n) : ↑(t.monodromyOrbitFinset i) = MulAction.orbit (↥t.monodromyGroup) i

The computed monodromy orbit of a sheet is its orbit under the monodromy group.

@[simp]

theorem TauCeti.PermutationTriple.mem_monodromyOrbitFinset {n : ℕ} (t : PermutationTriple n) {i j : Fin n} : j ∈ t.monodromyOrbitFinset i ↔ j ∈ MulAction.orbit (↥t.monodromyGroup) i

theorem TauCeti.PermutationTriple.isConnected_iff_forall_monodromyOrbitFinset_eq_univ {n : ℕ} (t : PermutationTriple n) : t.IsConnected ↔ n ≠ 0 ∧ ∀ (i : Fin n), t.monodromyOrbitFinset i = Finset.univ

A triple is connected exactly when its degree is nonzero and the computed monodromy orbit of every sheet is the whole of Fin n. Both conjuncts are decidable.

@[instance_reducible]

instance TauCeti.PermutationTriple.instDecidableIsConnected {n : ℕ} (t : PermutationTriple n) : Decidable t.IsConnected

Connectedness of a permutation triple is decidable, by computing the monodromy orbits.

Equations

• t.instDecidableIsConnected = decidable_of_iff (n ≠ 0 ∧ ∀ (i : Fin n), t.monodromyOrbitFinset i = Finset.univ) ⋯

The monodromy group, computed

def TauCeti.PermutationTriple.monodromyFinset {n : ℕ} (t : PermutationTriple n) : Finset (Equiv.Perm (Fin n))

The monodromy group of a triple, as a finset of permutations: the closure of {1} under left multiplication by the two generating permutations, computed by Finset.closureFinset.

Equations

• t.monodromyFinset = t.generators.closureFinset

@[simp]

theorem TauCeti.PermutationTriple.mem_monodromyFinset {n : ℕ} (t : PermutationTriple n) {g : Equiv.Perm (Fin n)} : g ∈ t.monodromyFinset ↔ g ∈ t.monodromyGroup

@[simp]

theorem TauCeti.PermutationTriple.coe_monodromyFinset {n : ℕ} (t : PermutationTriple n) : ↑t.monodromyFinset = ↑t.monodromyGroup

The computed finset of permutations is the monodromy group.

@[simp]

theorem TauCeti.PermutationTriple.card_monodromyFinset {n : ℕ} (t : PermutationTriple n) : t.monodromyFinset.card = Nat.card ↥t.monodromyGroup

The order of the monodromy group is the cardinality of the computed finset.