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.

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.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.

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_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.