Documentation

Mathlib.GroupTheory.SchurZassenhaus

The Schur-Zassenhaus Theorem #

In this file we prove the Schur-Zassenhaus theorem.

Main results #

def Subgroup.QuotientDiff {G : Type u_1} [Group G] (H : Subgroup G) [H.IsCommutative] [H.FiniteIndex] :
Type u_1

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

Equations
Instances For
    instance Subgroup.instInhabitedQuotientDiff {G : Type u_1} [Group G] (H : Subgroup G) [H.IsCommutative] [H.FiniteIndex] :
    Inhabited H.QuotientDiff
    Equations
    • H.instInhabitedQuotientDiff = id inferInstance
    theorem Subgroup.smul_diff_smul' {G : Type u_1} [Group G] (H : Subgroup G) [H.IsCommutative] [H.FiniteIndex] (α : (Subgroup.leftTransversals H)) (β : (Subgroup.leftTransversals H)) [hH : H.Normal] (g : Gᵐᵒᵖ) :
    noncomputable instance Subgroup.instMulActionQuotientDiff {G : Type u_1} [Group G] {H : Subgroup G} [H.IsCommutative] [H.FiniteIndex] [H.Normal] :
    MulAction G H.QuotientDiff
    Equations
    theorem Subgroup.smul_diff' {G : Type u_1} [Group G] {H : Subgroup G} [H.IsCommutative] [H.FiniteIndex] (α : (Subgroup.leftTransversals H)) (β : (Subgroup.leftTransversals H)) [H.Normal] (h : H) :
    theorem Subgroup.eq_one_of_smul_eq_one {G : Type u_1} [Group G] {H : Subgroup G} [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} [Group G] {H : Subgroup G} [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} [Group G] {H : Subgroup G} [H.IsCommutative] [H.FiniteIndex] [H.Normal] {α : H.QuotientDiff} (hH : (Nat.card H).Coprime H.index) :
    H.IsComplement' (MulAction.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:

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