The Schur-Zassenhaus Theorem #
In this file we prove the Schur-Zassenhaus theorem.
Main results #
exists_right_complement'_of_coprime: The Schur-Zassenhaus theorem: IfH : subgroup Gis normal and has order coprime to its index, then there exists a subgroupKwhich is a (right) complement ofH.exists_left_complement'_of_coprimeThe Schur-Zassenhaus theorem: IfH : subgroup Gis normal and has order coprime to its index, then there exists a subgroupKwhich is a (left) complement ofH.
@[protected, instance]
Equations
- add_subgroup.left_transversals.add_action = {to_has_vadd := {vadd := λ (g : G) (T : ↥(add_subgroup.left_transversals ↑H)), ⟨g +l ↑T, _⟩}, zero_vadd := _, add_vadd := _}
@[protected, instance]
Equations
- subgroup.left_transversals.mul_action = {to_has_scalar := {smul := λ (g : G) (T : ↥(subgroup.left_transversals ↑H)), ⟨g *l ↑T, _⟩}, one_smul := _, mul_smul := _}
theorem
subgroup.smul_symm_apply_eq_mul_symm_apply_inv_smul
{G : Type u_1}
[group G]
{H : subgroup G}
(g : G)
(α : ↥(subgroup.left_transversals ↑H))
(q : G ⧸ H) :
↑(⇑((equiv.of_bijective (set.restrict quotient.mk' (g • α).val) _).symm) q) = g * ↑(⇑((equiv.of_bijective (set.restrict quotient.mk' α.val) _).symm) (g⁻¹ • q))
noncomputable
def
add_subgroup.diff
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
(α β : ↥(add_subgroup.left_transversals ↑H))
[hH : H.normal] :
↥H
The difference of two left transversals
Equations
- add_subgroup.diff α β = let α' : quotient (quotient_add_group.left_rel H) ≃ ↥(α.val) := (equiv.of_bijective (set.restrict quotient.mk' α.val) _).symm, β' : quotient (quotient_add_group.left_rel H) ≃ ↥(β.val) := (equiv.of_bijective (set.restrict quotient.mk' β.val) _).symm in ∑ (q : G ⧸ H), ⟨↑(⇑α' q) + -↑(⇑β' q), _⟩
noncomputable
def
subgroup.diff
{G : Type u_1}
[group G]
{H : subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
(α β : ↥(subgroup.left_transversals ↑H))
[hH : H.normal] :
↥H
The difference of two left transversals
Equations
- subgroup.diff α β = let α' : quotient (quotient_group.left_rel H) ≃ ↥(α.val) := (equiv.of_bijective (set.restrict quotient.mk' α.val) _).symm, β' : quotient (quotient_group.left_rel H) ≃ ↥(β.val) := (equiv.of_bijective (set.restrict quotient.mk' β.val) _).symm in ∏ (q : G ⧸ H), ⟨(↑(⇑α' q)) * (↑(⇑β' q))⁻¹, _⟩
theorem
add_subgroup.diff_add_diff
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
(α β γ : ↥(add_subgroup.left_transversals ↑H))
[H.normal] :
add_subgroup.diff α β + add_subgroup.diff β γ = add_subgroup.diff α γ
theorem
subgroup.diff_mul_diff
{G : Type u_1}
[group G]
{H : subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
(α β γ : ↥(subgroup.left_transversals ↑H))
[H.normal] :
(subgroup.diff α β) * subgroup.diff β γ = subgroup.diff α γ
theorem
subgroup.diff_self
{G : Type u_1}
[group G]
{H : subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
(α : ↥(subgroup.left_transversals ↑H))
[H.normal] :
subgroup.diff α α = 1
theorem
add_subgroup.diff_self
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
(α : ↥(add_subgroup.left_transversals ↑H))
[H.normal] :
add_subgroup.diff α α = 0
theorem
add_subgroup.diff_neg
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
(α β : ↥(add_subgroup.left_transversals ↑H))
[H.normal] :
-add_subgroup.diff α β = add_subgroup.diff β α
theorem
subgroup.diff_inv
{G : Type u_1}
[group G]
{H : subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
(α β : ↥(subgroup.left_transversals ↑H))
[H.normal] :
(subgroup.diff α β)⁻¹ = subgroup.diff β α
theorem
subgroup.smul_diff_smul
{G : Type u_1}
[group G]
{H : subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
(α β : ↥(subgroup.left_transversals ↑H))
[hH : H.normal]
(g : G) :
subgroup.diff (g • α) (g • β) = ⟨(g * ↑(subgroup.diff α β)) * g⁻¹, _⟩
theorem
subgroup.smul_diff
{G : Type u_1}
[group G]
{H : subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
(α β : ↥(subgroup.left_transversals ↑H))
[H.normal]
(h : ↥H) :
subgroup.diff (h • α) β = (h ^ H.index) * subgroup.diff α β
@[protected, instance]
def
subgroup.setoid_diff
{G : Type u_1}
[group G]
(H : subgroup G)
[H.is_commutative]
[fintype (G ⧸ H)]
[H.normal] :
Equations
- H.setoid_diff = {r := λ (α β : ↥(subgroup.left_transversals ↑H)), subgroup.diff α β = 1, iseqv := _}
def
subgroup.quotient_diff
{G : Type u_1}
[group G]
(H : subgroup G)
[H.is_commutative]
[fintype (G ⧸ H)]
[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]
[fintype (G ⧸ H)]
[H.normal] :
Equations
@[protected, instance]
def
subgroup.quotient_diff.mul_action
{G : Type u_1}
[group G]
{H : subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
[H.normal] :
Equations
- subgroup.quotient_diff.mul_action = {to_has_scalar := {smul := λ (g : G), quotient.map (λ (α : ↥(subgroup.left_transversals ↑H)), g • α) _}, one_smul := _, mul_smul := _}
theorem
subgroup.exists_smul_eq
{G : Type u_1}
[group G]
{H : subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
[fintype ↥H]
[H.normal]
(α β : H.quotient_diff)
(hH : (fintype.card ↥H).coprime H.index) :
theorem
subgroup.smul_left_injective
{G : Type u_1}
[group G]
{H : subgroup G}
[H.is_commutative]
[fintype (G ⧸ H)]
[fintype ↥H]
[H.normal]
(α : H.quotient_diff)
(hH : (fintype.card ↥H).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 (G ⧸ H)]
[fintype ↥H]
[fintype G]
[H.normal]
{α : H.quotient_diff}
(hH : (fintype.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
Kis a subgroup ofGwithK ⊔ N = ⊤, thenK = ⊤. - step 2:
Nis a minimal normal subgroup, phrased in terms of subgroups ofG. - step 3:
Nis a minimal normal subgroup, phrased in terms of subgroups ofN. - step 4:
p(min_fact (fintype.card N)) is prime (follows from step0). - step 5:
P(a Sylowp-subgroup ofN) is nontrivial. - step 6:
Nis ap-group (applies step 1 to the normalizer ofPinG). - step 7:
Nis abelian (applies step 3 to the center ofN).
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
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.
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.
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.
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.