The Frobenius kernel, its size, and the free action of the complement on it

The Frobenius kernel of a subgroup H of G is the identity together with the elements of G lying in no conjugate of H,

frobeniusKernel H = {1} ∪ (G ∖ ⋃_g g H g⁻¹).

That union of conjugates is Mathlib's Group.conjugatesOfSet (H : Set G), the set of elements conjugate to an element of H.

Frobenius's theorem says that when G is finite and H is a Frobenius complement — proper, nontrivial, and meeting each of its distinct conjugates trivially (TauCeti.IsFrobeniusComplement) — this set is a normal subgroup, and that is not elementary: the known proofs go through the character theory of G. What is elementary, and is what this file proves, is everything about the kernel except its closure under multiplication: it contains the identity, it is closed under inversion and under conjugation, it meets every conjugate of H only in the identity, and — the counting statement the divisibility results below rest on — for a finite G it has exactly |G : H| elements.

The count is the inclusion-exclusion that gives Frobenius's theorem its shape, and it is really a statement about a trivial-intersection set S for H (TauCeti.IsTISet): the conjugates g S g⁻¹ are pairwise disjoint for distinct cosets g H and depend only on the coset, so the elements they cover are indexed bijectively by the pairs (a coset of H, an element of S) and number |G : H| · |S|. That is TauCeti.IsTISet.ncard_conjugatesOfSet, proved alongside TauCeti.IsTISet itself in TauCeti/GroupTheory/TrivialIntersection.lean. The complement of the kernel is the set of conjugates of the nonidentity elements of H, which for a trivial-intersection subgroup is such a set (TauCeti.IsTISubgroup.isTISet_diff_one), and the count specializes to TauCeti.IsTISubgroup.ncard_compl_frobeniusKernel, the Set.ncard identity ((frobeniusKernel H)ᶜ).ncard = |G : H| · (|H| - 1). That identity holds for any G, finite or not, but for an infinite G it does not in general represent a count of elements: an infinite side reads as the junk value 0 that Set.ncard and Subgroup.index take on infinite arguments. A degenerate case can of course still be a genuine count — for H = ⊥ the kernel is everything and its complement is honestly empty — but nothing outside the finite case says so. For a finite G there are indeed |G : H| · (|H| - 1) elements outside the kernel, and the remaining |G| - |G : H| · (|H| - 1) = |G : H| elements are the kernel, and the rest is arithmetic.

Together with normality the count is exactly what makes the kernel a complement: TauCeti.IsTISubgroup.isComplement'_of_coe_eq_frobeniusKernel says that, for a finite G, a subgroup whose carrier is the Frobenius kernel is automatically a complement to H, so once Frobenius's theorem supplies the subgroup, the semidirect decomposition G = N ⋊ H is free. Nothing here asserts that a subgroup with that carrier exists.

The count has an arithmetic refinement, proved here as well: the conjugation action of H on the nonidentity part of the kernel is free (TauCeti.IsTISubgroup.stabilizer_eq_bot, with TauCeti.IsTISubgroup.isCancelSMul its typeclass form), and freeness against the |G : H| - 1 nonidentity kernel elements gives

|H| ∣ |G : H| - 1

(TauCeti.IsTISubgroup.card_dvd_index_sub_one), whence also |H| and |G : H| are coprime (TauCeti.IsTISubgroup.coprime_card_index) and, for a proper H, |H| < |G : H| (TauCeti.IsTISubgroup.card_lt_index). When Frobenius's theorem supplies the kernel as a subgroup N of order |G : H|, these are the classical statements that |H| divides |N| - 1 and that a Frobenius complement and a Frobenius kernel have coprime orders. Freeness has a second reading, bounding the centralizers the other way round: the centralizer of a nonidentity element of the kernel is contained in the kernel (TauCeti.IsTISubgroup.centralizer_singleton_subset_frobeniusKernel).

The last section runs the recognition in the other direction. A semidirect decomposition G = N ⋊ H in which H acts on N with no nonidentity fixed points forces H to be a trivial-intersection subgroup (TauCeti.isTISubgroup_of_isComplement'_of_fixedPointFree), and then the given N is already the Frobenius kernel (TauCeti.IsTISubgroup.coe_eq_frobeniusKernel_of_isComplement') -- the inclusion N ⊆ frobeniusKernel H needs only normality and disjointness, and the count above turns it into an equality. Nothing there is character theory: it is what a concrete Frobenius group is checked against once Frobenius's theorem has produced its kernel abstractly.

No subgroup hypothesis beyond TauCeti.IsTISubgroup is needed for the count once G is finite, and the two degenerate cases are honest instances rather than exclusions: frobeniusKernel ⊤ = {1} has one element and ⊤ has index 1, while frobeniusKernel ⊥ is everything and ⊥ has index |G|.

Main definitions

• TauCeti.frobeniusKernel: the identity together with the elements in no conjugate of H.

Main results

• TauCeti.mem_frobeniusKernel: membership, elementwise.
• TauCeti.inv_mem_frobeniusKernel_iff and TauCeti.conj_mem_frobeniusKernel_iff: the kernel is closed under inversion and invariant under conjugation, for every subgroup H.
• TauCeti.frobeniusKernel_inter_conj_smul_eq_singleton and TauCeti.frobeniusKernel_inter_eq_singleton: the kernel meets every conjugate of H, and in particular H itself, exactly in the identity.
• TauCeti.IsTISubgroup.ncard_compl_frobeniusKernel: the Set.ncard identity ((frobeniusKernel H)ᶜ).ncard = |G : H| · (|H| - 1), which for a finite G counts the elements outside the kernel — the nonidentity elements of the conjugates of H, each counted once — and for an infinite G reads 0 = 0.
• TauCeti.IsTISubgroup.ncard_frobeniusKernel and TauCeti.IsTISubgroup.natCard_frobeniusKernel: for a finite G the kernel has |G : H| elements.
• TauCeti.IsTISubgroup.isComplement'_of_coe_eq_frobeniusKernel: for a finite G, a subgroup whose carrier is the kernel is a complement to H.
• TauCeti.IsTISubgroup.conj_ne_self_of_mem_frobeniusKernel, TauCeti.IsTISubgroup.stabilizer_eq_bot and TauCeti.IsTISubgroup.isCancelSMul: a nonidentity element of H commutes with no nonidentity element of the kernel, so the conjugation action of H on the nonidentity part of the kernel is free.
• TauCeti.IsTISubgroup.mem_frobeniusKernel_of_conj_eq_self and TauCeti.IsTISubgroup.centralizer_singleton_subset_frobeniusKernel: the centralizer of a nonidentity element of the kernel is contained in the kernel.
• TauCeti.IsTISubgroup.card_dvd_index_sub_one: |H| ∣ |G : H| - 1 for a finite G, with TauCeti.IsTISubgroup.coprime_card_index the coprimality and TauCeti.IsTISubgroup.card_lt_index the strict inequality |H| < |G : H| it implies.
• TauCeti.isTISubgroup_of_isComplement'_of_fixedPointFree: a complement to a normal subgroup on which it acts without nonidentity fixed points is a trivial-intersection subgroup, with TauCeti.isFrobeniusComplement_of_isComplement'_of_fixedPointFree its bundled form for a proper nontrivial H.
• TauCeti.coe_subset_frobeniusKernel and TauCeti.IsTISubgroup.coe_eq_frobeniusKernel_of_isComplement': a normal complement meeting H trivially lies in the Frobenius kernel, and for a finite G it is the Frobenius kernel when H is a trivial-intersection subgroup.

References

• I. M. Isaacs, Character Theory of Finite Groups, Chapter 7, Section 7B.
• Character theory roadmap, Layer 8 (frobeniusKernel, "a set of size |G : H|", and frobeniusKernel_isComplement').

def TauCeti.frobeniusKernel {G : Type u_1} [Group G] (H : Subgroup G) : Set G

The Frobenius kernel of a subgroup: the identity together with the elements of G lying in no conjugate of H, the conjugates being collected by Group.conjugatesOfSet. For a Frobenius complement H of a finite group this set is a normal subgroup of G, but that is Frobenius's theorem and needs character theory; as a set it is available for any H, and TauCeti.mem_frobeniusKernel is the elementwise description everything below uses.

Equations

• TauCeti.frobeniusKernel H = {1} ∪ (Group.conjugatesOfSet ↑H)ᶜ

theorem TauCeti.frobeniusKernel_def {G : Type u_1} [Group G] (H : Subgroup G) : frobeniusKernel H = {1} ∪ (Group.conjugatesOfSet ↑H)ᶜ

The Frobenius kernel is the identity together with the complement of the set of conjugates of elements of H, by definition.

theorem TauCeti.mem_frobeniusKernel {G : Type u_1} [Group G] {H : Subgroup G} {y : G} : y ∈ frobeniusKernel H ↔ y = 1 ∨ ∀ (x : G), x⁻¹ * y * x ∉ H

Membership in the Frobenius kernel: an element is the identity, or no conjugate of it lands in H.

@[simp]

theorem TauCeti.notMem_frobeniusKernel_iff {G : Type u_1} [Group G] {H : Subgroup G} {y : G} : y ∉ frobeniusKernel H ↔ y ≠ 1 ∧ ∃ (x : G), x⁻¹ * y * x ∈ H

Being outside the Frobenius kernel means being a nonidentity element of some conjugate of H.

@[simp]

theorem TauCeti.one_mem_frobeniusKernel {G : Type u_1} [Group G] {H : Subgroup G} : 1 ∈ frobeniusKernel H

@[simp]

theorem TauCeti.inv_mem_frobeniusKernel_iff {G : Type u_1} [Group G] {H : Subgroup G} {y : G} : y⁻¹ ∈ frobeniusKernel H ↔ y ∈ frobeniusKernel H

The Frobenius kernel is closed under inversion: x⁻¹ y⁻¹ x is the inverse of x⁻¹ y x, and a subgroup contains an element exactly when it contains its inverse.

@[simp]

theorem TauCeti.conj_mem_frobeniusKernel_iff {G : Type u_1} [Group G] {H : Subgroup G} {y g : G} : g * y * g⁻¹ ∈ frobeniusKernel H ↔ y ∈ frobeniusKernel H

The Frobenius kernel is invariant under conjugation: it is the identity together with the complement of a conjugation-closed set, and Group.conj_mem_conjugatesOfSet is that closure. This is the half of normality that costs nothing; closure under multiplication is Frobenius's theorem.

@[simp]

theorem TauCeti.frobeniusKernel_inter_conj_smul_eq_singleton {G : Type u_1} [Group G] {H : Subgroup G} (g : G) : frobeniusKernel H ∩ MulAut.conj g • ↑H = {1}

The Frobenius kernel meets each conjugate of H exactly in the identity. A nonidentity element of g H g⁻¹ lies in a conjugate of H, so it is outside the kernel.

@[simp]

theorem TauCeti.frobeniusKernel_inter_eq_singleton {G : Type u_1} [Group G] {H : Subgroup G} : frobeniusKernel H ∩ ↑H = {1}

The Frobenius kernel meets H exactly in the identity, the case g = 1 of TauCeti.frobeniusKernel_inter_conj_smul_eq_singleton.

@[simp]

theorem TauCeti.frobeniusKernel_top {G : Type u_1} [Group G] : frobeniusKernel ⊤ = {1}

The Frobenius kernel of the whole group is trivial: every element lies in ⊤.

@[simp]

theorem TauCeti.frobeniusKernel_bot {G : Type u_1} [Group G] : frobeniusKernel ⊥ = Set.univ

The Frobenius kernel of the trivial subgroup is everything: no conjugate of a nonidentity element is the identity.

Counting the kernel

theorem TauCeti.IsTISubgroup.ncard_compl_frobeniusKernel {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsTISubgroup H) : (frobeniusKernel H)ᶜ.ncard = H.index * (Nat.card ↥H - 1)

The complement of the Frobenius kernel has Set.ncard equal to |G : H| · (|H| - 1). For a trivial-intersection subgroup the elements outside the kernel are exactly the conjugates of the nonidentity elements of H, which TauCeti.IsTISet.ncard_conjugatesOfSet counts as |G : H| times the |H| - 1 elements of H that are conjugated. No finiteness is assumed — but this is an ncard identity, which for an infinite G need not be an element count: an infinite side reads as the junk value 0 that Set.ncard and Subgroup.index take on infinite arguments, even though a degenerate case may still be a genuine count (for H = ⊥ the complement of the kernel is honestly empty). The count that is guaranteed to be one is TauCeti.IsTISubgroup.ncard_frobeniusKernel, stated for a finite G.

theorem TauCeti.IsTISubgroup.ncard_frobeniusKernel {G : Type u_1} [Group G] {H : Subgroup G} [Finite G] (hH : IsTISubgroup H) : (frobeniusKernel H).ncard = H.index

The Frobenius kernel of a trivial-intersection subgroup of a finite group has |G : H| elements. The conjugates of H cover |G : H| · (|H| - 1) nonidentity elements between them, and |G| = |G : H| · |H|, so |G : H| elements are left over.

theorem TauCeti.IsTISubgroup.natCard_frobeniusKernel {G : Type u_1} [Group G] {H : Subgroup G} [Finite G] (hH : IsTISubgroup H) : Nat.card ↑(frobeniusKernel H) = H.index

The Frobenius kernel of a trivial-intersection subgroup of a finite group has |G : H| elements, read as the cardinality of its coercion to a type.

theorem TauCeti.IsTISubgroup.isComplement'_of_coe_eq_frobeniusKernel {G : Type u_1} [Group G] {H : Subgroup G} [Finite G] (hH : IsTISubgroup H) {N : Subgroup G} (hN : ↑N = frobeniusKernel H) : N.IsComplement' H

A subgroup of a finite group carried by the Frobenius kernel is a complement to H. Frobenius's theorem provides such a subgroup for a Frobenius complement; that it is a complement is then pure counting, the kernel having |G : H| elements and meeting H only in the identity. Nothing here asserts that such a subgroup exists.

The free conjugation action on the nonidentity part of the kernel

theorem TauCeti.conj_mem_frobeniusKernel_sdiff_singleton {G : Type u_1} [Group G] {H : Subgroup G} (g : G) {y : G} (hy : y ∈ frobeniusKernel H \ {1}) : g * y * g⁻¹ ∈ frobeniusKernel H \ {1}

Conjugation carries a nonidentity element of the Frobenius kernel to another one: the kernel is conjugation-invariant, and only the identity is conjugate to the identity.

@[instance_reducible]

instance TauCeti.instSMulSubtypeMemSubgroupElemSdiffSetFrobeniusKernelSingletonOfNat {G : Type u_1} [Group G] {H : Subgroup G} : SMul ↥H ↑(frobeniusKernel H \ {1})

Conjugation by an element of H, as a scalar action on the nonidentity part of the Frobenius kernel. This instance records only the underlying map; that it is an action is the MulAction instance below.

Equations

• TauCeti.instSMulSubtypeMemSubgroupElemSdiffSetFrobeniusKernelSingletonOfNat = { smul := fun (h : ↥H) (y : ↑(TauCeti.frobeniusKernel H \ {1})) => ⟨↑h * ↑y * (↑h)⁻¹, ⋯⟩ }

@[simp]

theorem TauCeti.coe_smul_frobeniusKernel_sdiff_singleton {G : Type u_1} [Group G] {H : Subgroup G} (h : ↥H) (y : ↑(frobeniusKernel H \ {1})) : ↑(h • y) = ↑h * ↑y * (↑h)⁻¹

@[instance_reducible]

instance TauCeti.instMulActionSubtypeMemSubgroupElemSdiffSetFrobeniusKernelSingletonOfNat {G : Type u_1} [Group G] {H : Subgroup G} : MulAction ↥H ↑(frobeniusKernel H \ {1})

H acts on the nonidentity part of its Frobenius kernel by conjugation. Freeness of this action is TauCeti.IsTISubgroup.stabilizer_eq_bot, and it is what forces |H| to divide |G : H| - 1.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.IsTISubgroup.conj_ne_self_of_mem_frobeniusKernel {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsTISubgroup H) {h y : G} (hh : h ∈ H) (hh1 : h ≠ 1) (hy : y ∈ frobeniusKernel H) (hy1 : y ≠ 1) : h * y * h⁻¹ ≠ y

A nonidentity element of a trivial-intersection subgroup commutes with no nonidentity element of its Frobenius kernel, in conjugation form. Both the freeness of the conjugation action (TauCeti.IsTISubgroup.stabilizer_eq_bot) and the centralizer bound on the kernel side (TauCeti.IsTISubgroup.centralizer_singleton_subset_frobeniusKernel) are readings of it.

theorem TauCeti.IsTISubgroup.stabilizer_eq_bot {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsTISubgroup H) (y : ↑(frobeniusKernel H \ {1})) : MulAction.stabilizer (↥H) y = ⊥

The conjugation action of a trivial-intersection subgroup on the nonidentity part of its Frobenius kernel is free: every stabilizer is trivial. This is the hypothesis the orbit counting in TauCeti.IsTISubgroup.card_dvd_index_sub_one consumes.

theorem TauCeti.IsTISubgroup.isCancelSMul {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsTISubgroup H) : IsCancelSMul ↥H ↑(frobeniusKernel H \ {1})

The conjugation action of a trivial-intersection subgroup on the nonidentity part of its Frobenius kernel is cancellative, the typeclass form of TauCeti.IsTISubgroup.stabilizer_eq_bot, for the generic results that take freeness as an instance. It cannot itself be an instance, since freeness holds only under the hypothesis hH.

theorem TauCeti.IsTISubgroup.mem_frobeniusKernel_of_conj_eq_self {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsTISubgroup H) {g y : G} (hy : y ∈ frobeniusKernel H) (hy1 : y ≠ 1) (hgy : g * y * g⁻¹ = y) : g ∈ frobeniusKernel H

An element commuting with a nonidentity element of the Frobenius kernel lies in the kernel, the mirror on the kernel side of TauCeti.IsTISubgroup.mem_of_conj_eq_self. Its inclusion form is TauCeti.IsTISubgroup.centralizer_singleton_subset_frobeniusKernel.

theorem TauCeti.IsTISubgroup.centralizer_singleton_subset_frobeniusKernel {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsTISubgroup H) {y : G} (hy : y ∈ frobeniusKernel H) (hy1 : y ≠ 1) : ↑(Subgroup.centralizer {y}) ⊆ frobeniusKernel H

The centralizer of a nonidentity element of the Frobenius kernel is contained in the kernel, the inclusion form of TauCeti.IsTISubgroup.mem_frobeniusKernel_of_conj_eq_self.

The order of the complement divides the size of the kernel minus one

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

The order of a trivial-intersection subgroup of a finite group divides |G : H| - 1. For a Frobenius complement H, Frobenius's theorem makes the kernel a subgroup N of order |G : H|, so this is the classical |H| ∣ |N| - 1 (TauCeti.card_dvd_card_frobeniusKernelSubgroup_sub_one).

theorem TauCeti.IsTISubgroup.coprime_card_index {G : Type u_1} [Group G] {H : Subgroup G} [Finite G] (hH : IsTISubgroup H) : (Nat.card ↥H).Coprime H.index

The order of a trivial-intersection subgroup of a finite group is coprime to its index, an immediate consequence of TauCeti.IsTISubgroup.card_dvd_index_sub_one. For a Frobenius group it says that the complement and the kernel have coprime orders (TauCeti.coprime_card_card_frobeniusKernelSubgroup).

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

A proper trivial-intersection subgroup of a finite group is smaller than its index, |H| < |G : H|, another immediate consequence of TauCeti.IsTISubgroup.card_dvd_index_sub_one. Properness is needed: for H = ⊤ the index is 1 and the inequality reverses. For a Frobenius group it says that the complement is smaller than the kernel (TauCeti.card_lt_card_frobeniusKernelSubgroup).

Recognizing the kernel from a semidirect decomposition

theorem TauCeti.coe_subset_frobeniusKernel {G : Type u_1} [Group G] {H N : Subgroup G} [N.Normal] (hdisj : Disjoint N H) : ↑N ⊆ frobeniusKernel H

A normal subgroup meeting H trivially lies in the Frobenius kernel of H. Neither finiteness nor a complement hypothesis is needed; this inclusion is the easy half of TauCeti.IsTISubgroup.coe_eq_frobeniusKernel_of_isComplement'.

theorem TauCeti.IsTISubgroup.coe_eq_frobeniusKernel_of_isComplement' {G : Type u_1} [Group G] {H N : Subgroup G} [Finite G] [N.Normal] (hH : IsTISubgroup H) (hNH : N.IsComplement' H) : ↑N = frobeniusKernel H

The Frobenius kernel of a normal complement to a trivial-intersection subgroup is that complement itself. This identifies the kernel that Frobenius's theorem constructs from the character theory of G with the normal complement a semidirect decomposition G = N ⋊ H hands over directly; a fixed-point-free action of H on N supplies the trivial-intersection hypothesis through TauCeti.isTISubgroup_of_isComplement'_of_fixedPointFree, and the subgroup-level statement is TauCeti.frobeniusKernelSubgroup_eq_of_isComplement'.