Finite affine groups as Frobenius groups

For a finite ring F without zero divisors, the translations form the Frobenius kernel associated to the linear factor. When F is a division ring with at least three elements, its linear factor is a Frobenius complement, so the affine group F ⋊ Fˣ is a Frobenius group. The general Frobenius theorem constructs the kernel from the complement alone; the main result here identifies that abstractly constructed subgroup with the visible translation factor.

The specialization to ZMod 5 gives the affine group of order twenty, with kernel of order five and complement of order four.

Main results

• TauCeti.frobeniusKernelSubgroup_affineLinearSubgroup: the Frobenius kernel is the translation subgroup.
• TauCeti.card_frobeniusKernelSubgroup_affineLinearSubgroup: the kernel has |F| elements.
• TauCeti.card_affineLinearSubgroup: the complement has |F| - 1 elements.
• TauCeti.card_affineGroup: the affine group has |F| (|F| - 1) elements.
• TauCeti.card_affineGroup_zmod_five: the F₅ example has order twenty.

The construction follows Isaacs, Character Theory of Finite Groups, Chapter 7.

theorem TauCeti.frobeniusKernelSubgroup_affineLinearSubgroup (F : Type u_1) [Ring F] [NoZeroDivisors F] [Finite F] : frobeniusKernelSubgroup ⋯ = affineTranslationSubgroup F

The Frobenius kernel constructed from the linear factor of a finite affine group is exactly its translation subgroup.

theorem TauCeti.card_frobeniusKernelSubgroup_affineLinearSubgroup (F : Type u_1) [Ring F] [NoZeroDivisors F] [Finite F] : Nat.card ↥(frobeniusKernelSubgroup ⋯) = Nat.card F

The Frobenius kernel of a finite affine group has |F| elements.

theorem TauCeti.instFactPrimeFiveAffine : Fact (Nat.Prime 5)

theorem TauCeti.isFrobeniusComplement_affineLinearSubgroup_zmod_five : IsFrobeniusComplement (affineLinearSubgroup (ZMod 5))

The linear factor of the affine group over F₅ is a Frobenius complement.

theorem TauCeti.card_affineGroup_zmod_five : Nat.card (AffineGroup (ZMod 5)) = 20

The affine group over F₅ has order twenty.

theorem TauCeti.card_affineLinearSubgroup_zmod_five : Nat.card ↥(affineLinearSubgroup (ZMod 5)) = 4

The linear Frobenius complement in the affine group over F₅ has order four.

theorem TauCeti.card_frobeniusKernelSubgroup_affineLinearSubgroup_zmod_five : Nat.card ↥(frobeniusKernelSubgroup ⋯) = 5

The Frobenius kernel constructed from the linear complement in the affine group over F₅ has order five.