Deciding primitivity of a permutation triple

A monodromy action is preprimitive when it is pretransitive and preserves no nontrivial block of sheets. The finite tests below enumerate every subset of sheets and every element of the computed monodromy group. Testing just the two generators would be unsound: the condition that a translate of a block is equal or disjoint need not survive products of generators.

The Boolean tests agree with Mathlib's MulAction.IsBlock and MulAction.IsPreprimitive.

def TauCeti.PermutationTriple.isBlockBool {n : ℕ} (t : PermutationTriple n) (B : Finset (Fin n)) : Bool

Decide whether a set of sheets is a block by testing every monodromy permutation.

Equations

• t.isBlockBool B = decide (∀ g ∈ t.monodromyFinset, g • B = B ∨ Disjoint (g • B) B)

@[simp]

theorem TauCeti.PermutationTriple.isBlockBool_eq_true_iff {n : ℕ} (t : PermutationTriple n) (B : Finset (Fin n)) : t.isBlockBool B = true ↔ MulAction.IsBlock ↥t.monodromyGroup ↑B

The finite block test agrees with Mathlib's block predicate for the monodromy action.

def TauCeti.PermutationTriple.isPrimitiveBool {n : ℕ} (t : PermutationTriple n) : Bool

Decide primitivity by checking transitivity and every subset of the sheets for a nontrivial block.

Equations

• t.isPrimitiveBool = decide ((∀ (i : Fin n), t.monodromyOrbitFinset i = Finset.univ) ∧ ∀ (B : Finset (Fin n)), t.isBlockBool B = true → B.card ≤ 1 ∨ B = Finset.univ)

@[simp]

theorem TauCeti.PermutationTriple.isPrimitiveBool_eq_true_iff {n : ℕ} (t : PermutationTriple n) : t.isPrimitiveBool = true ↔ t.IsPrimitive

The finite primitivity test agrees with primitivity of the triple.

@[instance_reducible]

instance TauCeti.PermutationTriple.instDecidableIsPrimitive {n : ℕ} (t : PermutationTriple n) : Decidable t.IsPrimitive

Primitivity of the monodromy action is decidable by the finite block test.

Equations

• t.instDecidableIsPrimitive = decidable_of_iff (t.isPrimitiveBool = true) ⋯