The cyclic reference permutation groups

In every degree n the first label nT1 is the cyclic group Cₙ, acting regularly on Fin n by rotation. In degrees three to five the reference subgroup is defined as the closure of finRotate n, and in degrees one and two it is the whole symmetric group, which the rotation also generates. We record this uniformly as referenceSubgroup n ⟨0, _⟩ = zpowers (finRotate n) and identify the reference subgroup with Multiplicative (ZMod n), the rotation corresponding to Multiplicative.ofAdd 1. Every permutation group with label nT1 is therefore abstractly cyclic of order n.

Main declarations

• TauCeti.referenceSubgroup_index_zero_eq_zpowers: the reference subgroup of nT1 is generated by finRotate n.
• TauCeti.natCard_referenceSubgroup_index_zero, TauCeti.isCyclic_referenceSubgroup_index_zero: the reference subgroup of nT1 is cyclic of order n.
• TauCeti.referenceSubgroupIndexZeroMulEquivZMod: the reference subgroup of nT1 is isomorphic to Multiplicative (ZMod n), sending finRotate n to Multiplicative.ofAdd 1. It is built from Mathlib's zmodMulEquivOfGenerator.
• TauCeti.TransitiveGroupLabel.nonempty_mulEquiv_zmod_index_zero: a permutation group with label nT1 is isomorphic to Multiplicative (ZMod n).

theorem TauCeti.referenceSubgroup_index_zero_eq_zpowers {n : ℕ} (h : 0 < numTransitiveGroups n) : referenceSubgroup n ⟨0, h⟩ = Subgroup.zpowers (finRotate n)

The reference subgroup of the first label nT1 is the cyclic group generated by the rotation finRotate n, in every degree in which labels exist.

theorem TauCeti.finRotate_mem_referenceSubgroup_index_zero {n : ℕ} (h : 0 < numTransitiveGroups n) : finRotate n ∈ referenceSubgroup n ⟨0, h⟩

The rotation finRotate n lies in the reference subgroup of nT1.

theorem TauCeti.natCard_referenceSubgroup_index_zero {n : ℕ} (h : 0 < numTransitiveGroups n) : Nat.card ↥(referenceSubgroup n ⟨0, h⟩) = n

The reference subgroup of nT1 has order n.

theorem TauCeti.isCyclic_referenceSubgroup_index_zero {n : ℕ} (h : 0 < numTransitiveGroups n) : IsCyclic ↥(referenceSubgroup n ⟨0, h⟩)

The reference subgroup of nT1 is cyclic.

noncomputable def TauCeti.referenceSubgroupIndexZeroMulEquivZMod {n : ℕ} (h : 0 < numTransitiveGroups n) : ↥(referenceSubgroup n ⟨0, h⟩) ≃* Multiplicative (ZMod n)

The reference subgroup of nT1 is cyclic of order n: it is isomorphic to Multiplicative (ZMod n), with the rotation finRotate n corresponding to Multiplicative.ofAdd 1. This is the inverse of Mathlib's zmodMulEquivOfGenerator, applied to the generator finRotate n.

Equations

• TauCeti.referenceSubgroupIndexZeroMulEquivZMod h = (zmodMulEquivOfGenerator ⋯ ⋯).symm

@[simp]

theorem TauCeti.coe_referenceSubgroupIndexZeroMulEquivZMod_symm_apply_ofAdd_intCast {n : ℕ} (h : 0 < numTransitiveGroups n) (k : ℤ) : ↑((referenceSubgroupIndexZeroMulEquivZMod h).symm (Multiplicative.ofAdd ↑k)) = finRotate n ^ k

The inverse of referenceSubgroupIndexZeroMulEquivZMod sends Multiplicative.ofAdd k to the k-th power finRotate n ^ k of the rotation.

@[simp]

theorem TauCeti.referenceSubgroupIndexZeroMulEquivZMod_apply_finRotate {n : ℕ} (h : 0 < numTransitiveGroups n) : (referenceSubgroupIndexZeroMulEquivZMod h) ⟨finRotate n, ⋯⟩ = Multiplicative.ofAdd 1

The isomorphism referenceSubgroupIndexZeroMulEquivZMod sends the rotation to Multiplicative.ofAdd 1.

theorem TauCeti.TransitiveGroupLabel.nonempty_mulEquiv_zmod_index_zero {n : ℕ} {h : 0 < numTransitiveGroups n} {G : Subgroup (Equiv.Perm (Fin n))} (hG : TransitiveGroupLabel ⟨0, h⟩ G) : Nonempty (↥G ≃* Multiplicative (ZMod n))

Every permutation group with label nT1 is abstractly the cyclic group of order n. The isomorphism depends on the conjugating permutation used to read the label.