Prime symmetry subgroup

For two labels the symmetry group is the full permutation group; for every other number of labels it is the alternating group. The prime configuration model uses this construction at prime cardinality.

def NRR.primeSymmetrySubgroup (p : ℕ) : Subgroup (Equiv.Perm (Fin p))

The permutation subgroup used for prime symmetry: all permutations for two labels and even permutations otherwise.

Equations

• NRR.primeSymmetrySubgroup p = if p = 2 then ⊤ else alternatingGroup (Fin p)

@[reducible, inline]

abbrev NRR.PrimeSymmetry (p : ℕ) : Subgroup (Equiv.Perm (Fin p))

The group of prime symmetries acting on the labelled coordinates.

Equations

• NRR.PrimeSymmetry p = NRR.primeSymmetrySubgroup p

def NRR.PrimeSymmetry.toPerm (p : ℕ) : ↥(PrimeSymmetry p) →* Equiv.Perm (Fin p)

Faithful inclusion of the selected subgroup into all label permutations.

Equations

• NRR.PrimeSymmetry.toPerm p = (NRR.primeSymmetrySubgroup p).subtype

@[simp]

theorem NRR.PrimeSymmetry.toPerm_apply (p : ℕ) (g : ↥(PrimeSymmetry p)) : (toPerm p) g = ↑g

theorem NRR.PrimeSymmetry.toPerm_injective (p : ℕ) : Function.Injective ⇑(toPerm p)

theorem NRR.primeSymmetrySubgroup_eq_top (p : ℕ) (h2 : p = 2) : primeSymmetrySubgroup p = ⊤

theorem NRR.primeSymmetrySubgroup_eq_alternating (p : ℕ) (h2 : p ≠ 2) : primeSymmetrySubgroup p = alternatingGroup (Fin p)

theorem NRR.PrimeSymmetry.exists_map_label {p : ℕ} (hp : Nat.Prime p) (i j : Fin p) : ∃ (g : ↥(PrimeSymmetry p)), ((toPerm p) g) i = j

The chosen prime symmetry group acts transitively on the labels.