Words for a full symmetric top group

Only the distinguishing-word facts used by the every-base construction are included here.

def Saxl.WordDistinguishing (Q : Type u_1) {ι : Type u_2} {C : Type u_3} [Group Q] [MulAction Q ι] (word : ι → C) : Prop

A colour word has trivial stabilizer under contravariant reindexing.

Equations

• Saxl.WordDistinguishing Q word = ∀ (q : Q), (∀ (i : ι), word (q⁻¹ • i) = word i) → q = 1

theorem Saxl.symmetricTop_wordDistinguishing_iff_injective {C : Type u_1} {D : Type u_2} (word : C → D) : WordDistinguishing (Equiv.Perm C) word ↔ Function.Injective word

For the natural action of the full symmetric group, a word is distinguishing exactly when it has no repeated colour.

theorem Saxl.symmetricTop_wordDistinguishing_iff_bijective {C : Type u_1} [Finite C] (word : C → C) : WordDistinguishing (Equiv.Perm C) word ↔ Function.Bijective word

A self-colouring of a finite coordinate type distinguishes its full symmetric group exactly when it is a bijection.