The Schur-Zassenhaus Theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove the Schur-Zassenhaus theorem.

Main results #

exists_right_complement'_of_coprime : The Schur-Zassenhaus theorem: If H : subgroup G is normal and has order coprime to its index, then there exists a subgroup K which is a (right) complement of H.
exists_left_complement'_of_coprime The Schur-Zassenhaus theorem: If H : subgroup G is normal and has order coprime to its index, then there exists a subgroup K which is a (left) complement of H.

source

def subgroup.quotient_diff {G : Type u_1} [group G] (H : subgroup G) [H.is_commutative] [H.finite_index] :

Type u_1

The quotient of the transversals of an abelian normal N by the diff relation.

Equations

H.quotient_diff = quotient {r := λ (α β : ↥(subgroup.left_transversals ↑H)), subgroup.left_transversals.diff (monoid_hom.id ↥H) α β = 1, iseqv := _}

Instances for subgroup.quotient_diff

source

@[protected, instance]

def subgroup.quotient_diff.inhabited {G : Type u_1} [group G] (H : subgroup G) [H.is_commutative] [H.finite_index] :

inhabited H.quotient_diff

Equations

subgroup.quotient_diff.inhabited H = quotient.inhabited {r := λ (α β : ↥(subgroup.left_transversals ↑H)), subgroup.left_transversals.diff (monoid_hom.id ↥H) α β = 1, iseqv := _}

source

theorem subgroup.smul_diff_smul' {G : Type u_1} [group G] (H : subgroup G) [H.is_commutative] [H.finite_index] (α β : ↥(subgroup.left_transversals ↑H)) [hH : H.normal] (g : Gᵐᵒᵖ) :

subgroup.left_transversals.diff (monoid_hom.id ↥H) (g • α) (g • β) = ⟨(mul_opposite.unop g)⁻¹ * ↑(subgroup.left_transversals.diff (monoid_hom.id ↥H) α β) * mul_opposite.unop g, _⟩

source

@[protected, instance]

def subgroup.quotient_diff.mul_action {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [H.finite_index] [H.normal] :

mul_action G H.quotient_diff

Equations

subgroup.quotient_diff.mul_action = {to_has_smul := {smul := λ (g : G), quotient.map' (λ (α : ↥(subgroup.left_transversals ↑H)), mul_opposite.op g⁻¹ • α) _}, one_smul := _, mul_smul := _}

source

theorem subgroup.smul_diff' {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [H.finite_index] (α β : ↥(subgroup.left_transversals ↑H)) [H.normal] (h : ↥H) :

subgroup.left_transversals.diff (monoid_hom.id ↥H) α (mul_opposite.op ↑h • β) = subgroup.left_transversals.diff (monoid_hom.id ↥H) α β * h ^ H.index

source

theorem subgroup.eq_one_of_smul_eq_one {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [H.finite_index] [H.normal] (hH : (nat.card ↥H).coprime H.index) (α : H.quotient_diff) (h : ↥H) :

h • α = α → h = 1

source

theorem subgroup.exists_smul_eq {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [H.finite_index] [H.normal] (hH : (nat.card ↥H).coprime H.index) (α β : H.quotient_diff) :

∃ (h : ↥H), h • α = β

source

theorem subgroup.is_complement'_stabilizer_of_coprime {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [H.finite_index] [H.normal] {α : H.quotient_diff} (hH : (nat.card ↥H).coprime H.index) :

H.is_complement' (mul_action.stabilizer G α)

Proof of the Schur-Zassenhaus theorem #

In this section, we prove the Schur-Zassenhaus theorem. The proof is by contradiction. We assume that G is a minimal counterexample to the theorem.

We will arrive at a contradiction via the following steps:

step 0: N (the normal Hall subgroup) is nontrivial.
step 1: If K is a subgroup of G with K ⊔ N = ⊤, then K = ⊤.
step 2: N is a minimal normal subgroup, phrased in terms of subgroups of G.
step 3: N is a minimal normal subgroup, phrased in terms of subgroups of N.
step 4: p (min_fact (fintype.card N)) is prime (follows from step0).
step 5: P (a Sylow p-subgroup of N) is nontrivial.
step 6: N is a p-group (applies step 1 to the normalizer of P in G).
step 7: N is abelian (applies step 3 to the center of N).

source

theorem subgroup.schur_zassenhaus_induction.step7 {G : Type u} [group G] [fintype G] {N : subgroup G} [N.normal] (h1 : (fintype.card ↥N).coprime N.index) (h2 : ∀ (G' : Type u) [_inst_4 : group G'] [_inst_5 : fintype G'], fintype.card G' < fintype.card G → ∀ {N' : subgroup G'} [_inst_6 : N'.normal], (fintype.card ↥N').coprime N'.index → (∃ (H' : subgroup G'), N'.is_complement' H')) (h3 : ∀ (H : subgroup G), ¬N.is_complement' H) :

N.is_commutative

Do not use this lemma: It is made obsolete by exists_right_complement'_of_coprime

source

theorem subgroup.exists_right_complement'_of_coprime_of_fintype {G : Type u} [group G] [fintype G] {N : subgroup G} [N.normal] (hN : (fintype.card ↥N).coprime N.index) :

∃ (H : subgroup G), N.is_complement' H

Schur-Zassenhaus for normal subgroups: If H : subgroup G is normal, and has order coprime to its index, then there exists a subgroup K which is a (right) complement of H.

source

theorem subgroup.exists_right_complement'_of_coprime {G : Type u} [group G] {N : subgroup G} [N.normal] (hN : (nat.card ↥N).coprime N.index) :

∃ (H : subgroup G), N.is_complement' H

Schur-Zassenhaus for normal subgroups: If H : subgroup G is normal, and has order coprime to its index, then there exists a subgroup K which is a (right) complement of H.

source

theorem subgroup.exists_left_complement'_of_coprime_of_fintype {G : Type u} [group G] [fintype G] {N : subgroup G} [N.normal] (hN : (fintype.card ↥N).coprime N.index) :

∃ (H : subgroup G), H.is_complement' N

Schur-Zassenhaus for normal subgroups: If H : subgroup G is normal, and has order coprime to its index, then there exists a subgroup K which is a (left) complement of H.

source

theorem subgroup.exists_left_complement'_of_coprime {G : Type u} [group G] {N : subgroup G} [N.normal] (hN : (nat.card ↥N).coprime N.index) :

∃ (H : subgroup G), H.is_complement' N

Schur-Zassenhaus for normal subgroups: If H : subgroup G is normal, and has order coprime to its index, then there exists a subgroup K which is a (left) complement of H.