Trivial-intersection subgroups and Frobenius complements

A subgroup H of G is a trivial-intersection subgroup when it meets each of its distinct conjugates trivially: H ⊓ g H g⁻¹ = ⊥ whenever g ∉ H. Equivalently H is malnormal: a nonidentity element of H is conjugated out of H by every g ∉ H. A Frobenius complement is such a subgroup that is in addition proper and nontrivial, and G is then called a Frobenius group with complement H.

The elementwise form is the definition taken here, because it is what every proof uses; the lattice form is TauCeti.isTISubgroup_iff_inf_conj_smul_eq_bot.

Alongside the subgroup notion there is a set-level one. A trivial-intersection set for H is a subset S ⊆ H normalized by H whose distinct G-conjugates are pairwise disjoint. The example that matters is the nonidentity part H# = (H : Set G) \ {1} of a Frobenius complement (TauCeti.IsFrobeniusComplement.isTISet_diff_one). Because the conjugates of such an S depend only on the coset of the conjugator and distinct cosets give disjoint conjugates, the elements they cover between them are indexed bijectively by the pairs (a coset of H, an element of S). That bijection is the Set.ncard identity (Group.conjugatesOfSet S).ncard = |G : H| · |S| (TauCeti.IsTISet.ncard_conjugatesOfSet), which counts the covered elements when the parametrizing sets are finite — H of finite index and S finite — and reads 0 on an infinite side otherwise; that count is what makes the Frobenius kernel of TauCeti/GroupTheory/FrobeniusKernel.lean come out with |G : H| elements.

A class function on H supported on such an S induces to G without changing its norm, as long as the order of G is invertible in the coefficient field k (IsUnit (Nat.card G : k), as everywhere in this theory, because induction divides by that order). That is the input to the exceptional-character argument for Frobenius's theorem. That induction statement is TauCeti.characterPairing_ind_ind_of_isTISet, in TauCeti/RepresentationTheory/Induction/TrivialIntersection.lean.

A concrete Frobenius group is normally presented the other way round, as a semidirect product G = N ⋊ H with H acting on N without nonidentity fixed points, and that presentation is enough: TauCeti.isTISubgroup_of_isComplement'_of_fixedPointFree reads the trivial-intersection condition off it. Conjugation by an element g = n · t outside H is conjugation by its H-part t, which stays inside H, followed by conjugation by its N-part n; so an element of H conjugated back into H commutes with n, and the fixed-point hypothesis leaves only the identity. That is the recognition criterion a concrete Frobenius group is checked with, and TauCeti.IsTISubgroup.coe_eq_frobeniusKernel_of_isComplement' completes it by identifying N with the Frobenius kernel.

Main definitions

• TauCeti.IsTISubgroup: H meets each of its distinct conjugates trivially.
• TauCeti.IsTISet: S is a trivial-intersection set relative to H.
• TauCeti.IsFrobeniusComplement: H is a proper nontrivial trivial-intersection subgroup.

Main results

• TauCeti.isTISubgroup_iff_inf_conj_smul_eq_bot: the lattice form of the definition.
• TauCeti.IsTISubgroup.normalizer_eq_self: a nontrivial trivial-intersection subgroup is self-normalizing.
• TauCeti.IsTISubgroup.mem_of_conj_eq_self and TauCeti.IsTISubgroup.centralizer_singleton_le: the centralizer of a nonidentity element of a trivial-intersection subgroup is contained in that subgroup.
• TauCeti.IsTISubgroup.isTISet: an H-invariant subset of H avoiding the identity is a trivial-intersection set, and in particular so is the nonidentity part of H.
• TauCeti.IsTISet.one_notMem: conversely, a trivial-intersection set for a proper subgroup avoids the identity.
• TauCeti.IsTISet.ncard_conjugatesOfSet: the Set.ncard identity (Group.conjugatesOfSet S).ncard = |G : H| · |S|, an actual count of the elements the conjugates of a trivial-intersection set cover when H has finite index and S is finite.
• 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.

Implementation notes

The count TauCeti.IsTISet.ncard_conjugatesOfSet is proved through a map into G out of (G ⧸ H) × S, rather than through an Equiv onto Group.conjugatesOfSet S, because the two facts it is used through are cleaner apart than bundled: that its range is the set of conjugates uses only that S is normalized by H, while its injectivity is exactly the disjointness of the distinct conjugates. The coset representatives are Quotient.out, so the map is noncomputable and needs no well-definedness argument; the price is that hitting a conjugate has to move a witness x to (x H).out by QuotientGroup.mk_out_eq_mul, conjugating the element of S along the way.

References

• I. M. Isaacs, Character Theory of Finite Groups, Chapter 7.
• Character theory roadmap, Layer 8 (IsTISet, IsFrobeniusComplement).

Trivial-intersection subgroups

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

A trivial-intersection subgroup: H meets each of its distinct conjugates trivially. Stated elementwise, as the malnormality condition that only the identity of H can be conjugated back into H by an element outside H; TauCeti.isTISubgroup_iff_inf_conj_smul_eq_bot is the equivalent statement H ⊓ g H g⁻¹ = ⊥ about the subgroup lattice.

Equations

• TauCeti.IsTISubgroup H = ∀ ⦃g x : G⦄, g ∉ H → x ∈ H → g * x * g⁻¹ ∈ H → x = 1

theorem TauCeti.IsTISubgroup.eq_one {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsTISubgroup H) {g x : G} (hg : g ∉ H) (hx : x ∈ H) (hgx : g * x * g⁻¹ ∈ H) : x = 1

The defining property of a trivial-intersection subgroup, as a named lemma.

theorem TauCeti.IsTISubgroup.conj_notMem {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsTISubgroup H) {g x : G} (hg : g ∉ H) (hx : x ∈ H) (hx1 : x ≠ 1) : g * x * g⁻¹ ∉ H

A nonidentity element of a trivial-intersection subgroup is conjugated out of it by every element outside it.

theorem TauCeti.IsTISubgroup.normalizer_eq_self {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsTISubgroup H) (hne : H ≠ ⊥) : Subgroup.normalizer ↑H = H

A nontrivial trivial-intersection subgroup is self-normalizing. An element of the normalizer conjugates a chosen nonidentity element of H back into H, so it cannot lie outside H.

theorem TauCeti.IsTISubgroup.mem_of_conj_eq_self {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsTISubgroup H) {g x : G} (hx : x ∈ H) (hx1 : x ≠ 1) (hgx : g * x * g⁻¹ = x) : g ∈ H

An element commuting with a nonidentity element of a trivial-intersection subgroup lies in that subgroup, in conjugation form; the inclusion form is TauCeti.IsTISubgroup.centralizer_singleton_le.

theorem TauCeti.IsTISubgroup.centralizer_singleton_le {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsTISubgroup H) {x : G} (hx : x ∈ H) (hx1 : x ≠ 1) : Subgroup.centralizer {x} ≤ H

The centralizer of a nonidentity element of a trivial-intersection subgroup is contained in it, the inclusion form of TauCeti.IsTISubgroup.mem_of_conj_eq_self. So the centralizers of the nonidentity elements of H are as small as H itself allows, which is what makes the conjugation action of H on the nonidentity part of its Frobenius kernel free.

theorem TauCeti.isTISubgroup_iff_inf_conj_smul_eq_bot {G : Type u_1} [Group G] {H : Subgroup G} : IsTISubgroup H ↔ ∀ g ∉ H, H ⊓ MulAut.conj g • H = ⊥

The lattice form of the trivial-intersection condition: H meets each conjugate g H g⁻¹ with g ∉ H in the trivial subgroup. This is how the condition is usually written; the elementwise TauCeti.IsTISubgroup is the form the proofs use.

Trivial-intersection sets

structure TauCeti.IsTISet {G : Type u_1} [Group G] (S : Set G) (H : Subgroup G) : Prop

A trivial-intersection set for H: a subset of H, normalized by H, whose G-conjugates by elements outside H are disjoint from it. Since conjugation by an element of H fixes S, the conjugates of S are indexed by the cosets of H, and the condition says that the distinct ones are pairwise disjoint.

The motivating example is the nonidentity part (H : Set G) \ {1} of a trivial-intersection subgroup (TauCeti.IsTISubgroup.isTISet_diff_one).

• subset : S ⊆ ↑H

  A trivial-intersection set is contained in its subgroup.

• conj_mem (h : G) : h ∈ H → ∀ x ∈ S, h * x * h⁻¹ ∈ S

  A trivial-intersection set is normalized by its subgroup.

• disjoint_conj (g : G) : g ∉ H → ∀ x ∈ S, g * x * g⁻¹ ∉ S

  Conjugating a trivial-intersection set by an element outside its subgroup moves it off itself.

theorem TauCeti.IsTISet.conj_image_eq {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsTISet S H) {h : G} (hh : h ∈ H) : (fun (x : G) => h * x * h⁻¹) '' S = S

The image of a trivial-intersection set under conjugation by an element of its subgroup is the set itself; the two inclusions come from TauCeti.IsTISet.conj_mem at h and at h⁻¹.

theorem TauCeti.IsTISet.disjoint_conj_image {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsTISet S H) {g : G} (hg : g ∉ H) : Disjoint ((fun (x : G) => g * x * g⁻¹) '' S) S

Distinct conjugates of a trivial-intersection set are disjoint, in the form the name of the notion refers to.

theorem TauCeti.IsTISet.one_notMem {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsTISet S H) (hH : H ≠ ⊤) : 1 ∉ S

A trivial-intersection set for a proper subgroup avoids the identity. The identity is fixed by every conjugation, so it could not be moved off the set.

theorem TauCeti.IsTISubgroup.isTISet {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hH : IsTISubgroup H) (hS : S ⊆ ↑H) (h1 : 1 ∉ S) (hconj : ∀ h ∈ H, ∀ x ∈ S, h * x * h⁻¹ ∈ S) : IsTISet S H

An H-invariant subset of H avoiding the identity is a trivial-intersection set. This is where the trivial-intersection condition on the subgroup does the work: an element of S conjugated by some g ∉ H back into H would have to be the identity.

theorem TauCeti.IsTISubgroup.isTISet_diff_one {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsTISubgroup H) : IsTISet (↑H \ {1}) H

The nonidentity part of a trivial-intersection subgroup is a trivial-intersection set. This is the set H# the exceptional-character argument induces from.

Counting the conjugates of a trivial-intersection set

theorem TauCeti.IsTISet.ncard_conjugatesOfSet {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : IsTISet S H) : (Group.conjugatesOfSet S).ncard = H.index * S.ncard

The conjugates of a trivial-intersection set have Set.ncard equal to |G : H| · |S|. The conjugate g S g⁻¹ depends only on the coset g H, because S is normalized by H, and distinct cosets give disjoint conjugates, so the elements covered are indexed bijectively by the pairs (a coset of H, an element of S). The parametrization argument is uniform, so no finiteness is assumed — but this is an ncard identity, and it counts elements only when the parametrizing sets are finite, H of finite index and S finite: an infinite side otherwise reads as the junk value 0 that Set.ncard and Subgroup.index take on infinite arguments. The Frobenius kernel count TauCeti.IsTISubgroup.ncard_compl_frobeniusKernel is the case S = H \ {1}.

Frobenius complements

structure TauCeti.IsFrobeniusComplement {G : Type u_1} [Group G] (H : Subgroup G) : Prop

A Frobenius complement: a proper, nontrivial trivial-intersection subgroup. A group with such a subgroup is a Frobenius group with complement H; Frobenius's theorem says that the elements lying in no conjugate of H, together with the identity, form a normal complement to H.

• ne_bot : H ≠ ⊥

  A Frobenius complement is nontrivial.

• ne_top : H ≠ ⊤

  A Frobenius complement is proper.

• isTISubgroup : IsTISubgroup H

  A Frobenius complement meets each of its distinct conjugates trivially.

theorem TauCeti.IsFrobeniusComplement.normalizer_eq_self {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsFrobeniusComplement H) : Subgroup.normalizer ↑H = H

A Frobenius complement is self-normalizing.

theorem TauCeti.IsFrobeniusComplement.isTISet_diff_one {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsFrobeniusComplement H) : IsTISet (↑H \ {1}) H

The nonidentity part of a Frobenius complement is a trivial-intersection set.

theorem TauCeti.IsFrobeniusComplement.not_normal {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsFrobeniusComplement H) : ¬H.Normal

A Frobenius complement is not normal. It is self-normalizing and proper, so its normalizer is not the whole group.

Fixed-point-free complements

theorem TauCeti.isTISubgroup_of_isComplement'_of_fixedPointFree {G : Type u_1} [Group G] {H N : Subgroup G} [N.Normal] (hNH : N.IsComplement' H) (hfpf : ∀ (h : ↥H), h ≠ 1 → MonoidHom.FixedPointFree ⇑(MulAut.conjNormal ↑h)) : IsTISubgroup H

A complement to a normal subgroup that acts on it without nonidentity fixed points is a trivial-intersection subgroup. This is the elementary converse direction of Frobenius's theorem: where Frobenius's theorem produces a normal complement out of the trivial-intersection condition, here a normal complement is given and the trivial-intersection condition is read off its action. It is the criterion a concrete Frobenius group, presented as a semidirect product G = N ⋊ H, is recognized by; TauCeti.IsTISubgroup.coe_eq_frobeniusKernel_of_isComplement' then identifies N as the Frobenius kernel.

theorem TauCeti.isFrobeniusComplement_of_isComplement'_of_fixedPointFree {G : Type u_1} [Group G] {H N : Subgroup G} [N.Normal] (hNH : N.IsComplement' H) (hbot : H ≠ ⊥) (htop : H ≠ ⊤) (hfpf : ∀ (h : ↥H), h ≠ 1 → MonoidHom.FixedPointFree ⇑(MulAut.conjNormal ↑h)) : IsFrobeniusComplement H

A proper nontrivial fixed-point-free complement is a Frobenius complement. The trivial-intersection condition is TauCeti.isTISubgroup_of_isComplement'_of_fixedPointFree; properness and nontriviality are exactly what the bundled predicate adds.