# The Schur-Zassenhaus Theorem #

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.
def Subgroup.QuotientDiff {G : Type u_1} [] (H : ) [H.IsCommutative] [H.FiniteIndex] :
Type u_1

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

Equations
• H.QuotientDiff = Quotient { r := fun (α β : ) => = 1, iseqv := }
Instances For
instance Subgroup.instInhabitedQuotientDiff {G : Type u_1} [] (H : ) [H.IsCommutative] [H.FiniteIndex] :
Inhabited H.QuotientDiff
Equations
• H.instInhabitedQuotientDiff = id inferInstance
theorem Subgroup.smul_diff_smul' {G : Type u_1} [] (H : ) [H.IsCommutative] [H.FiniteIndex] (α : ) (β : ) [hH : H.Normal] (g : Gᵐᵒᵖ) :
Subgroup.leftTransversals.diff () (g α) (g β) = g.unop⁻¹ * () * g.unop,
noncomputable instance Subgroup.instMulActionQuotientDiff {G : Type u_1} [] {H : } [H.IsCommutative] [H.FiniteIndex] [H.Normal] :
MulAction G H.QuotientDiff
Equations
• Subgroup.instMulActionQuotientDiff =
theorem Subgroup.smul_diff' {G : Type u_1} [] {H : } [H.IsCommutative] [H.FiniteIndex] (α : ) (β : ) [H.Normal] (h : H) :
= * h ^ H.index
theorem Subgroup.eq_one_of_smul_eq_one {G : Type u_1} [] {H : } [H.IsCommutative] [H.FiniteIndex] [H.Normal] (hH : (Nat.card H).Coprime H.index) (α : H.QuotientDiff) (h : H) :
h α = αh = 1
theorem Subgroup.exists_smul_eq {G : Type u_1} [] {H : } [H.IsCommutative] [H.FiniteIndex] [H.Normal] (hH : (Nat.card H).Coprime H.index) (α : H.QuotientDiff) (β : H.QuotientDiff) :
∃ (h : H), h α = β
theorem Subgroup.isComplement'_stabilizer_of_coprime {G : Type u_1} [] {H : } [H.IsCommutative] [H.FiniteIndex] [H.Normal] {α : H.QuotientDiff} (hH : (Nat.card H).Coprime H.index) :
H.IsComplement' ()

## 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).
theorem Subgroup.SchurZassenhausInduction.step7 {G : Type u} [] [] {N : } [N.Normal] (h1 : ().Coprime N.index) (h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'], ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Fintype.card N').Coprime N'.index∃ (H' : Subgroup G'), N'.IsComplement' H') (h3 : ∀ (H : ), ¬N.IsComplement' H) :
N.IsCommutative

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

theorem Subgroup.exists_right_complement'_of_coprime_of_fintype {G : Type u} [] [] {N : } [N.Normal] (hN : ().Coprime N.index) :
∃ (H : ), N.IsComplement' 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.

theorem Subgroup.exists_right_complement'_of_coprime {G : Type u} [] {N : } [N.Normal] (hN : (Nat.card N).Coprime N.index) :
∃ (H : ), N.IsComplement' 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.

theorem Subgroup.exists_left_complement'_of_coprime_of_fintype {G : Type u} [] [] {N : } [N.Normal] (hN : ().Coprime N.index) :
∃ (H : ), H.IsComplement' 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.

theorem Subgroup.exists_left_complement'_of_coprime {G : Type u} [] {N : } [N.Normal] (hN : (Nat.card N).Coprime N.index) :
∃ (H : ), H.IsComplement' 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.