Focal Subgroup Theorem

This file defines the focal subgroup and proves the Focal Subgroup Theorem.

Main definitions

• focalSubgroup H : The focal subgroup H* of a subgroup H, generated by elements of the form ⁅x, u⁆ where x ∈ H and ⁅x, u⁆ ∈ H.
• focalSubgroupOf H : The focal subgroup of H considered as a subgroup of H, i.e., (focalSubgroup H).subgroupOf H.
• transferFocal H : The transfer homomorphism V : G →* H ⧸ H*, defined using the abelian quotient H / H*.

Main Theorems

• transferFocal_eq_pow: The restriction of the transfer map to H acts like the power map x ↦ x ^ [G : H] mod H*.
• commutator_inf_eq_focalSubgroup: The Focal Subgroup Theorem. For a Sylow p-subgroup P of a finite group G, G' ⊓ P = P*, where P* is the focal subgroup of P.

References

• [D. Gorenstein, Finite Groups][gorenstein1968]

def Subgroup.focalSubgroup {G : Type u_1} [Group G] (H : Subgroup G) : Subgroup G

The Focal Subgroup of a subgroup H (denoted H* or foc(H)). It is generated by elements of the form x⁻¹ * (u * x * u⁻¹) where both x and x^u are in H.

def AddSubgroup.focalAddSubgroup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : AddSubgroup G

The Focal Subgroup of a subgroup H (denoted H* or foc(H)). It is generated by elements of the form x⁻¹ * (u * x * u⁻¹) where both x and x^u are in H.

def Subgroup.focalSubgroupOf {G : Type u_1} [Group G] (H : Subgroup G) : Subgroup ↥H

The focal subgroup considered as a subgroup of H. Note that focalSubgroup H is always contained in H.

def AddSubgroup.focalAddSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : AddSubgroup ↥H

The focal subgroup considered as a subgroup of H. Note that focalSubgroup H is always contained in H.

theorem Subgroup.focalSubgroup_def {G : Type u_1} [Group G] (H : Subgroup G) : H.focalSubgroup = closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}

theorem AddSubgroup.focalAddSubgroup_def {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.focalAddSubgroup = closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}

theorem Subgroup.focalSubgroupOf_def {G : Type u_1} [Group G] (H : Subgroup G) : H.focalSubgroupOf = H.focalSubgroup.subgroupOf H

theorem AddSubgroup.focalAddSubgroupOf_def {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.focalAddSubgroupOf = H.focalAddSubgroup.addSubgroupOf H

theorem Subgroup.focalSubgroup_le {G : Type u_1} [Group G] (H : Subgroup G) : H.focalSubgroup ≤ H

Lemma: The focal subgroup is indeed a subgroup of H.

theorem AddSubgroup.focalAddSubgroup_le {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.focalAddSubgroup ≤ H

Lemma: The focal subgroup is indeed a subgroup of H.

@[simp]

theorem Subgroup.map_focalSubgroupOf {G : Type u_1} [Group G] (H : Subgroup G) : map H.subtype H.focalSubgroupOf = H.focalSubgroup

@[simp]

theorem AddSubgroup.map_focalAddSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : map H.subtype H.focalAddSubgroupOf = H.focalAddSubgroup

instance Subgroup.instNormalSubtypeMemFocalSubgroupOf {G : Type u_1} [Group G] (H : Subgroup G) : H.focalSubgroupOf.Normal

Lemma: H* is a normal subgroup of H.

instance AddSubgroup.instNormalSubtypeMemFocalAddSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.focalAddSubgroupOf.Normal

Lemma: H* is a normal subgroup of H.

theorem Subgroup.focalSubgroup_le_commutator {G : Type u_1} [Group G] (H : Subgroup G) : H.focalSubgroup ≤ _root_.commutator G

Lemma: The focal subgroup is contained in the commutator subgroup G'.

theorem AddSubgroup.focalAddSubgroup_le_addCommutator {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.focalAddSubgroup ≤ _root_.addCommutator G

Lemma: The focal subgroup is contained in the commutator subgroup G'.

theorem Subgroup.focalSubgroupOf.mk'_conj_eq {G : Type u_1} [Group G] (H : Subgroup G) {h : G} (hh : h ∈ H) (g : G) (hconj : g⁻¹ * h * g ∈ H) : (QuotientGroup.mk' H.focalSubgroupOf) ⟨g⁻¹ * h * g, hconj⟩ = (QuotientGroup.mk' H.focalSubgroupOf) ⟨h, hh⟩

In the quotient H / H*, conjugation by any element of G preserves equivalence classes. If h ∈ H and g⁻¹ * h * g ∈ H, then g⁻¹hg ≡ h (mod H*).

theorem AddSubgroup.focalAddSubgroupOf.mk'_addConj_eq {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {h : G} (hh : h ∈ H) (g : G) (haddConj : -g + h + g ∈ H) : (QuotientAddGroup.mk' H.focalAddSubgroupOf) ⟨-g + h + g, haddConj⟩ = (QuotientAddGroup.mk' H.focalAddSubgroupOf) ⟨h, hh⟩

In the quotient H / H*, conjugation by any element of G preserves equivalence classes. If h ∈ H and g⁻¹ * h * g ∈ H, then g⁻¹hg ≡ h (mod H*).

theorem Subgroup.focalSubgroupOf_eq_closure {G : Type u_1} [Group G] (H : Subgroup G) : H.focalSubgroupOf = closure {g : ↥H | ∃ x ∈ H, ∃ (u : G), ↑g = ⁅x, u⁆}

theorem AddSubgroup.focalAddSubgroupOf_eq_closure {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.focalAddSubgroupOf = closure {g : ↥H | ∃ x ∈ H, ∃ (u : G), ↑g = ⁅x, u⁆}

theorem Subgroup.commutator_le_focalSubgroupOf {G : Type u_1} [Group G] (H : Subgroup G) : _root_.commutator ↥H ≤ H.focalSubgroupOf

theorem AddSubgroup.addCommutator_le_focalAddSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : _root_.addCommutator ↥H ≤ H.focalAddSubgroupOf

theorem Subgroup.commutator_le_focalSubgroup {G : Type u_1} [Group G] (H : Subgroup G) : ⁅H, H⁆ ≤ H.focalSubgroup

theorem AddSubgroup.addCommutator_le_focalAddSubgroup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⁅H, H⁆ ≤ H.focalAddSubgroup

instance Subgroup.instIsMulCommutativeQuotientSubtypeMemFocalSubgroupOf {G : Type u_1} [Group G] (H : Subgroup G) : IsMulCommutative (↥H ⧸ H.focalSubgroupOf)

instance AddSubgroup.instIsAddCommutativeQuotientSubtypeMemFocalAddSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : IsAddCommutative (↥H ⧸ H.focalAddSubgroupOf)

noncomputable def Subgroup.transferFocal {G : Type u_1} [Group G] (H : Subgroup G) [H.FiniteIndex] : G →* ↥H ⧸ H.focalSubgroupOf

The transfer homomorphism V : G → H/H* from G the abelian quotient H/H*.

noncomputable def AddSubgroup.transferFocal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.FiniteIndex] : G →+ ↥H ⧸ H.focalAddSubgroupOf

The transfer homomorphism V : G → H/H* from G the abelian quotient H/H*.

theorem Subgroup.transferFocal_eq_pow {G : Type u_1} [Group G] (H : Subgroup G) [H.FiniteIndex] (x : ↥H) : H.transferFocal ↑x = ↑x ^ H.index

The restriction of the transfer map to H acts like the power map x ↦ x^n mod H*, where n = [G:H].

theorem Subgroup.focalSubgroupOf.pow_index_surjective {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) [(↑P).FiniteIndex] : Function.Surjective fun (y : ↥↑P ⧸ (↑P).focalSubgroupOf) => y ^ (↑P).index

The power map y ↦ y^n is surjective on P/P* because gcd(n, p) = 1.

theorem Subgroup.transferFocal_surjective {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) [(↑P).FiniteIndex] : Function.Surjective ⇑(↑P).transferFocal

The Transfer homomorphism is surjective from G to P/P*.

noncomputable def Subgroup.transferFocal.quotientKerMulEquivQuotientFocalSubroupOf {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) [(↑P).FiniteIndex] : G ⧸ (↑P).transferFocal.ker ≃* ↥↑P ⧸ (↑P).focalSubgroupOf

Isomorphism theorem: G / ker(V) ≅ P / P*.

theorem Subgroup.ker_restrict_transferFocal_eq_focalSubgroupOf {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) [(↑P).FiniteIndex] : ((↑P).transferFocal.restrict P).ker = (↑P).focalSubgroupOf

theorem Subgroup.ker_transferFocal_inf_eq_focalSubgroup {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) [(↑P).FiniteIndex] : (↑P).transferFocal.ker ⊓ ↑P = (↑P).focalSubgroup

theorem Subgroup.commutator_inf_eq_focalSubgroup {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) [(↑P).FiniteIndex] : _root_.commutator G ⊓ ↑P = (↑P).focalSubgroup

The Focal Subgroup Theorem

For a Sylow p-subgroup P of a finite group G, P ∩ G' = P*, where P* is the focal subgroup of P.