Documentation

TauCeti.Combinatorics.PermutationTriple.Primitivity.Defs

Primitivity of a permutation triple #

This module supplies the primitivity predicate for permutation triples. The finite decision procedure and its correctness theorem use this predicate to state what their test decides.

source
def TauCeti.PermutationTriple.IsPrimitive {n : ℕ} (t : PermutationTriple n) :
Prop

The monodromy action is pretransitive and has only trivial blocks of sheets. This uses Mathlib's IsPreprimitive, which also holds for an empty set of sheets.

Equations
Instances For
    source
    theorem TauCeti.PermutationTriple.isPrimitive_iff {n : ℕ} (t : PermutationTriple n) :
    t.IsPrimitive ↔ MulAction.IsPreprimitive (↥t.monodromyGroup) (Fin n)

    Primitivity of a triple is preprimitivity of its monodromy action.