mathlib3 documentation

group_theory.schur_zassenhaus

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 #

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
Instances for subgroup.quotient_diff
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
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 α = β

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:

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) :

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

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.

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.

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.

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.