The affine group AGL(1, F) as a primitive permutation group

The one-dimensional affine group TauCeti.AffineGroup F of a division ring F acts on F by x ↦ b + a x. This action is 2-transitive: any two distinct points can be sent to any two distinct points by an affine map. In particular it is primitive.

For a finite division ring with q elements the image of AGL(1, F) in the permutations of F therefore has order q (q - 1), which is smaller than the order q! / 2 of the alternating group as soon as q ≥ 5. It nevertheless contains long cycles, in two ways.

• For a finite field, multiplication by a generator of the cyclic group Fˣ is a single cycle of length q - 1 fixing 0.
• When q is prime, transitivity forces a cycle of length q.

These are the classical witnesses that the bound p + 3 ≤ n in Jordan's theorem TauCeti.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem cannot be weakened to p ≤ n or to p + 1 ≤ n: AGL(1, 5) is primitive of degree 5 and contains a 5-cycle, and AGL(1, 8) is primitive of degree 8 and contains a 7-cycle, yet neither contains the alternating group. The two counterexamples are stated in TauCeti.GroupTheory.Perm.Jordan.Counterexamples.

Main results

• TauCeti.AffineGroup.isPreprimitive: AGL(1, F) acts primitively on F, being 2-transitive.
• TauCeti.AffineGroup.natCard_range_toPermHom: the permutation image of AGL(1, F) has order q (q - 1).
• TauCeti.AffineGroup.not_alternatingGroup_le_range_toPermHom: for q ≥ 5 the image does not contain the alternating group.
• TauCeti.AffineGroup.exists_isCycle_mem_range_toPermHom_support_eq_compl_zero: over a finite field with at least three elements the image contains a cycle with support {0}ᶜ.
• TauCeti.AffineGroup.exists_isCycle_mem_range_toPermHom_support_eq_univ: in prime degree the image contains a full cycle.

References

• H. Wielandt, Finite Permutation Groups, §13.
• J. D. Dixon and B. Mortimer, Permutation Groups, §3.3 and §7.7.

instance TauCeti.AffineGroup.isMultiplyPretransitive_two {F : Type u_1} [DivisionRing F] : MulAction.IsMultiplyPretransitive (AffineGroup F) F 2

The affine group of a division ring acts 2-transitively on it: two distinct points can be sent to any two distinct points by an affine map.

instance TauCeti.AffineGroup.isPreprimitive {F : Type u_1} [DivisionRing F] : MulAction.IsPreprimitive (AffineGroup F) F

The affine group of a division ring acts primitively on it.

theorem TauCeti.AffineGroup.natCard_range_toPermHom {F : Type u_1} [DivisionRing F] : Nat.card ↥(MulAction.toPermHom (AffineGroup F) F).range = Nat.card F * (Nat.card F - 1)

The image of the affine group in the permutations of the division ring has order |F| (|F| - 1).

theorem TauCeti.AffineGroup.not_alternatingGroup_le_range_toPermHom {F : Type u_1} [DivisionRing F] [Fintype F] [DecidableEq F] (hF : 5 ≤ Nat.card F) : ¬alternatingGroup F ≤ (MulAction.toPermHom (AffineGroup F) F).range

AGL(1, F) does not contain the alternating group once F has at least five elements: its order q (q - 1) is smaller than q! / 2.

theorem TauCeti.AffineGroup.exists_isCycle_mem_range_toPermHom_support_eq_univ {F : Type u_1} [DivisionRing F] [Fintype F] [DecidableEq F] (hp : Nat.Prime (Nat.card F)) : ∃ g ∈ (MulAction.toPermHom (AffineGroup F) F).range, g.IsCycle ∧ g.support = Finset.univ

AGL(1, F) contains a full cycle in prime degree. When the number of elements of F is prime, the transitive group AGL(1, F) contains a cycle moving every point.

theorem TauCeti.AffineGroup.exists_isCycle_mem_range_toPermHom_support_eq_compl_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : 2 < Nat.card F) : ∃ g ∈ (MulAction.toPermHom (AffineGroup F) F).range, g.IsCycle ∧ g.support = {0}ᶜ

AGL(1, F) contains a cycle of length q - 1. Over a finite field with at least three elements, multiplication by a generator of the cyclic group Fˣ is a single cycle moving every nonzero element and fixing 0.