# mathlibdocumentation

group_theory.schur_zassenhaus

# 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.
@[protected, instance]
Equations
@[protected, instance]
def subgroup.left_transversals.mul_action {G : Type u_1} [group G] {H : subgroup G} :
Equations
theorem subgroup.smul_symm_apply_eq_mul_symm_apply_inv_smul {G : Type u_1} [group G] {H : subgroup G} (g : G) (α : ) (q : quotient_group.quotient H) :
(((equiv.of_bijective (g α).val) _).symm) q) = g * (.symm) (g⁻¹ q))
noncomputable def add_subgroup.diff {G : Type u_1} [add_group G] {H : add_subgroup G} [H.is_commutative] (α β : ) [hH : H.normal] :

The difference of two left transversals

Equations
noncomputable def subgroup.diff {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] (α β : ) [hH : H.normal] :

The difference of two left transversals

Equations
=
theorem subgroup.diff_mul_diff {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] (α β γ : ) [H.normal] :
β) * =
theorem subgroup.diff_self {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] (α : ) [H.normal] :
= 1
theorem add_subgroup.diff_self {G : Type u_1} [add_group G] {H : add_subgroup G} [H.is_commutative] (α : ) [H.normal] :
= 0
theorem add_subgroup.diff_neg {G : Type u_1} [add_group G] {H : add_subgroup G} [H.is_commutative] (α β : ) [H.normal] :
theorem subgroup.diff_inv {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] (α β : ) [H.normal] :
β)⁻¹ =
theorem subgroup.smul_diff_smul {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] (α β : ) [hH : H.normal] (g : G) :
subgroup.diff (g α) (g β) = (g * β)) * g⁻¹, _⟩
theorem subgroup.smul_diff {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] (α β : ) [H.normal] (h : H) :
subgroup.diff (h α) β = (h ^ H.index) *
@[protected, instance]
def subgroup.setoid_diff {G : Type u_1} [group G] (H : subgroup G) [H.is_commutative] [H.normal] :
Equations
def subgroup.quotient_diff {G : Type u_1} [group G] (H : subgroup G) [H.is_commutative] [H.normal] :
Type u_1

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

Equations
@[protected, instance]
def subgroup.quotient_diff.inhabited {G : Type u_1} [group G] (H : subgroup G) [H.is_commutative] [H.normal] :
Equations
@[protected, instance]
def subgroup.quotient_diff.mul_action {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [H.normal] :
Equations
theorem subgroup.exists_smul_eq {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [fintype H] [H.normal] (α β : H.quotient_diff) (hH : .coprime H.index) :
∃ (h : H), h α = β
theorem subgroup.smul_left_injective {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [fintype H] [H.normal] (α : H.quotient_diff) (hH : .coprime H.index) :
function.injective (λ (h : H), h α)
theorem subgroup.is_complement'_stabilizer_of_coprime {G : Type u_1} [group G] {H : subgroup G} [H.is_commutative] [fintype H] [fintype G] [H.normal] {α : H.quotient_diff} (hH : .coprime H.index) :

## 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.schur_zassenhaus_induction.step7 {G : Type u} [group G] [fintype G] {N : subgroup G} [N.normal] (h1 : .coprime N.index) (h2 : ∀ (G' : Type u) [_inst_4 : group G'] [_inst_5 : fintype 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), ¬) :

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} [group G] [fintype G] {N : subgroup G} [N.normal] (hN : .coprime N.index) :
∃ (H : subgroup G),

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} [group G] {N : subgroup G} [N.normal] (hN : (nat.card N).coprime N.index) :
∃ (H : subgroup G),

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} [group G] [fintype G] {N : subgroup G} [N.normal] (hN : .coprime N.index) :
∃ (H : subgroup G),

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} [group G] {N : subgroup G} [N.normal] (hN : (nat.card N).coprime N.index) :
∃ (H : subgroup G),

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.