Frobenius's theorem: the Frobenius kernel is a normal subgroup

Let H be a trivial-intersection subgroup of a finite group G (TauCeti.IsTISubgroup), as a Frobenius complement is. The Frobenius kernel TauCeti.frobeniusKernel H — the identity together with the elements of G lying in no conjugate of H — is available as a set for any H, and for a trivial-intersection H it is already known to have |G : H| elements (TauCeti.IsTISubgroup.ncard_frobeniusKernel) and to meet each conjugate of H only in the identity. What is not elementary, and is proved here, is that it is a subgroup: closure under multiplication is Frobenius's theorem, and no proof avoiding character theory is known.

This file supplies the character theory. Over ℂ, induction from a trivial-intersection subgroup is an isometry on the class functions vanishing at the identity, and the correction φ* = Ind_H^G (φ - φ(1) · 1_H) + φ(1) · 1_G turns an irreducible character of H into an irreducible character of G restricting back to φ (TauCeti.ClassFunction.indExtend_mem_irreducibleCharacters, the exceptional-character correspondence). Choosing a representation σ_φ affording each φ*, the common kernel N = ⨅_φ ker σ_φ is a normal subgroup, and it is the Frobenius kernel:

• a nonidentity element g of the Frobenius kernel lies in no conjugate of H, so every summand of the induced class function vanishes at g and φ*(g) = φ(1) = φ*(1) — that is, g ∈ N; the identity, the one other element of the kernel, lies in N outright;
• conversely N is normal and N ∩ H = 1, because Res_H φ* = φ means an element of N ∩ H has the same value as the identity under every irreducible character of H, and the irreducible characters of a finite group detect the identity; so a nonidentity element of N can lie in no conjugate of H.

Both inclusions are equalities of sets, so the Frobenius kernel inherits the subgroup structure of N. The bundled subgroup is TauCeti.frobeniusKernelSubgroup, and with the counting already available it is a complement to H, so G is the semidirect product of the kernel by the complement.

Main statements

• TauCeti.frobeniusKernelSubgroup: Frobenius's theorem — the Frobenius kernel, bundled as a subgroup, with TauCeti.coe_frobeniusKernelSubgroup and TauCeti.mem_frobeniusKernelSubgroup its carrier and membership, and TauCeti.frobeniusKernelSubgroup_normal its normality.
• TauCeti.frobeniusKernel_isComplement': the kernel is a complement to H, so G = N ⋊ H.
• TauCeti.frobeniusKernelSubgroup_ne_bot and TauCeti.frobeniusKernelSubgroup_ne_top: when H is proper the kernel is nontrivial, and when H is nontrivial the kernel is proper — so for a Frobenius complement (TauCeti.IsFrobeniusComplement, which is both) the kernel is a proper nontrivial normal subgroup.
• TauCeti.card_frobeniusKernelSubgroup: the kernel has |G : H| elements.
• TauCeti.card_dvd_card_frobeniusKernelSubgroup_sub_one: |H| ∣ |N| - 1, with TauCeti.coprime_card_card_frobeniusKernelSubgroup and TauCeti.card_lt_card_frobeniusKernelSubgroup its two immediate consequences — a Frobenius complement and a Frobenius kernel have coprime orders, and a proper H is strictly smaller than its kernel.
• TauCeti.frobeniusKernelSubgroup_eq_of_isComplement': the kernel constructed here is the normal complement one started from, whenever G = N ⋊ H with N normal.

A concrete Frobenius group is presented the other way round, as a semidirect product G = N ⋊ H whose complement acts on the kernel without nonidentity fixed points. That presentation already forces the trivial-intersection condition and already exhibits the kernel (TauCeti.isTISubgroup_of_isComplement'_of_fixedPointFree and TauCeti.IsTISubgroup.coe_eq_frobeniusKernel_of_isComplement', both elementary), so TauCeti.frobeniusKernelSubgroup_eq_of_isComplement' is the statement that the character-theoretic construction above agrees with it.

Implementation notes

Everything here needs only TauCeti.IsTISubgroup H, not the full TauCeti.IsFrobeniusComplement H: properness and nontriviality of H play no part in the character argument, and the degenerate cases are true as stated (frobeniusKernel ⊤ = {1} is the carrier of ⊥, and frobeniusKernel ⊥ = Set.univ that of ⊤). They are exactly what makes the kernel itself nontrivial and proper, so the statements that need them take H ≠ ⊤ and H ≠ ⊥ as plain hypotheses.

The arithmetic of the last three statements is not character theory: it is the freeness of the conjugation action of H on the nonidentity part of the kernel, proved for a trivial-intersection subgroup in TauCeti/GroupTheory/FrobeniusKernel.lean as TauCeti.IsTISubgroup.card_dvd_index_sub_one. What Frobenius's theorem adds here is only that the kernel is a subgroup N, so that |G : H| may be read as |N|.

The bundled subgroup is read off a private existence statement with Exists.choose. That keeps the choice of affording representations — which is genuinely arbitrary — inside a single proof, rather than spread over an auxiliary definition whose Invertible (Nat.card G : ℂ) instance would then have to be produced identically at every use site. Nothing downstream depends on which subgroup the choice returns: TauCeti.coe_frobeniusKernelSubgroup pins its carrier, and a subgroup is determined by its carrier.

The separation input — that a nonidentity element of a finite group is moved by some irreducible character — is the private TauCeti.eq_one_of_forall_irreducibleCharacter_eq below. It is the completeness theorem TauCeti.ClassFunction.le_span_irreducibleCharacters applied to the indicator class function of the identity class, which is 1 at the identity and 0 elsewhere.

References

• I. M. Isaacs, Character Theory of Finite Groups (1976), Chapter 7, Theorem 7.2.
• J.-P. Serre, Linear Representations of Finite Groups, Section 7.2.

The irreducible characters detect the identity

Frobenius's theorem

noncomputable def TauCeti.frobeniusKernelSubgroup {G : Type u} [Group G] [Finite G] {H : Subgroup G} (hH : IsTISubgroup H) : Subgroup G

The Frobenius kernel of a trivial-intersection subgroup, as a subgroup.

Its carrier is the Frobenius kernel (TauCeti.coe_frobeniusKernelSubgroup) and it is normal (TauCeti.frobeniusKernelSubgroup_normal), which is Frobenius's theorem. A subgroup is determined by its carrier, so nothing depends on the choice made inside that proof.

Equations

• TauCeti.frobeniusKernelSubgroup hH = ⋯.choose

@[simp]

theorem TauCeti.coe_frobeniusKernelSubgroup {G : Type u} [Group G] [Finite G] {H : Subgroup G} (hH : IsTISubgroup H) : ↑(frobeniusKernelSubgroup hH) = frobeniusKernel H

The carrier of TauCeti.frobeniusKernelSubgroup is the Frobenius kernel.

theorem TauCeti.frobeniusKernelSubgroup_normal {G : Type u} [Group G] [Finite G] {H : Subgroup G} (hH : IsTISubgroup H) : (frobeniusKernelSubgroup hH).Normal

Frobenius's theorem: the Frobenius kernel is normal.

@[simp]

theorem TauCeti.mem_frobeniusKernelSubgroup {G : Type u} [Group G] [Finite G] {H : Subgroup G} (hH : IsTISubgroup H) {g : G} : g ∈ frobeniusKernelSubgroup hH ↔ g = 1 ∨ ∀ (x : G), x⁻¹ * g * x ∉ H

Membership in the Frobenius kernel subgroup is membership in the Frobenius kernel.

theorem TauCeti.frobeniusKernel_isComplement' {G : Type u} [Group G] [Finite G] {H : Subgroup G} (hH : IsTISubgroup H) : (frobeniusKernelSubgroup hH).IsComplement' H

The Frobenius kernel is a complement to the complement: G = N ⋊ H. The kernel has |G : H| elements and meets H only in the identity, which is all that TauCeti.IsTISubgroup.isComplement'_of_coe_eq_frobeniusKernel needs.

theorem TauCeti.frobeniusKernelSubgroup_ne_top {G : Type u} [Group G] [Finite G] {H : Subgroup G} (hH : IsTISubgroup H) (hne : H ≠ ⊥) : frobeniusKernelSubgroup hH ≠ ⊤

The Frobenius kernel of a nontrivial trivial-intersection subgroup is proper: it is disjoint from H, which is not ⊥.

theorem TauCeti.frobeniusKernelSubgroup_ne_bot {G : Type u} [Group G] [Finite G] {H : Subgroup G} (hH : IsTISubgroup H) (hne : H ≠ ⊤) : frobeniusKernelSubgroup hH ≠ ⊥

The Frobenius kernel of a proper trivial-intersection subgroup is nontrivial: it has |G : H| elements, and H ≠ ⊤ says that index is not 1.

The order of the complement against the order of the kernel

theorem TauCeti.card_frobeniusKernelSubgroup {G : Type u} [Group G] [Finite G] {H : Subgroup G} (hH : IsTISubgroup H) : Nat.card ↥(frobeniusKernelSubgroup hH) = H.index

The Frobenius kernel has |G : H| elements, the counting half of TauCeti.frobeniusKernel_isComplement' read on the bundled subgroup.

theorem TauCeti.card_dvd_card_frobeniusKernelSubgroup_sub_one {G : Type u} [Group G] [Finite G] {H : Subgroup G} (hH : IsTISubgroup H) : Nat.card ↥H ∣ Nat.card ↥(frobeniusKernelSubgroup hH) - 1

The order of a Frobenius complement divides the order of the Frobenius kernel minus one, |H| ∣ |N| - 1. This is TauCeti.IsTISubgroup.card_dvd_index_sub_one read on the bundled kernel, whose order is |G : H|.

theorem TauCeti.coprime_card_card_frobeniusKernelSubgroup {G : Type u} [Group G] [Finite G] {H : Subgroup G} (hH : IsTISubgroup H) : (Nat.card ↥H).Coprime (Nat.card ↥(frobeniusKernelSubgroup hH))

A Frobenius complement and the Frobenius kernel have coprime orders, the bundled form of TauCeti.IsTISubgroup.coprime_card_index.

theorem TauCeti.card_lt_card_frobeniusKernelSubgroup {G : Type u} [Group G] [Finite G] {H : Subgroup G} (hH : IsTISubgroup H) (hne : H ≠ ⊤) : Nat.card ↥H < Nat.card ↥(frobeniusKernelSubgroup hH)

A proper trivial-intersection subgroup is smaller than its Frobenius kernel, |H| < |N|, the bundled form of TauCeti.IsTISubgroup.card_lt_index. Properness is needed: for H = ⊤ the kernel is trivial and the inequality reverses.

The kernel of a normal complement

theorem TauCeti.frobeniusKernelSubgroup_eq_of_isComplement' {G : Type u} [Group G] [Finite G] {H N : Subgroup G} [N.Normal] (hH : IsTISubgroup H) (hNH : N.IsComplement' H) : frobeniusKernelSubgroup hH = N

Frobenius's theorem returns the normal complement it was handed. If G = N ⋊ H with N normal and H a trivial-intersection subgroup, then the subgroup that the exceptional-character argument above constructs -- out of the irreducible characters of H, with no reference to N -- is N itself.

This is what makes the abstract construction checkable on a concrete Frobenius group, which comes presented as such a decomposition with H acting on N without nonidentity fixed points (TauCeti.isTISubgroup_of_isComplement'_of_fixedPointFree).