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

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

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

theorem Subgroup.smul_diff_smul' {G : Type u_1} [Group G] (H : Subgroup G) [Subgroup.IsCommutative H] [Subgroup.FiniteIndex H] (α : ↑(Subgroup.leftTransversals ↑H)) (β : ↑(Subgroup.leftTransversals ↑H)) [hH : Subgroup.Normal H] (g : Gᵐᵒᵖ) : Subgroup.leftTransversals.diff (MonoidHom.id { x // x ∈ H }) (g • α) (g • β) = { val := (MulOpposite.unop g)⁻¹ * ↑(Subgroup.leftTransversals.diff (MonoidHom.id { x // x ∈ H }) α β) * MulOpposite.unop g, property := (_ : (MulOpposite.unop g)⁻¹ * ↑(Subgroup.leftTransversals.diff (MonoidHom.id { x // x ∈ H }) α β) * MulOpposite.unop g ∈ H) }

noncomputable instance Subgroup.instMulActionQuotientDiffToMonoidToDivInvMonoid {G : Type u_1} [Group G] {H : Subgroup G} [Subgroup.IsCommutative H] [Subgroup.FiniteIndex H] [Subgroup.Normal H] : MulAction G (Subgroup.QuotientDiff H)

theorem Subgroup.smul_diff' {G : Type u_1} [Group G] {H : Subgroup G} [Subgroup.IsCommutative H] [Subgroup.FiniteIndex H] (α : ↑(Subgroup.leftTransversals ↑H)) (β : ↑(Subgroup.leftTransversals ↑H)) [Subgroup.Normal H] (h : { x // x ∈ H }) : Subgroup.leftTransversals.diff (MonoidHom.id { x // x ∈ H }) α (MulOpposite.op ↑h • β) = Subgroup.leftTransversals.diff (MonoidHom.id { x // x ∈ H }) α β * h ^ Subgroup.index H

theorem Subgroup.eq_one_of_smul_eq_one {G : Type u_1} [Group G] {H : Subgroup G} [Subgroup.IsCommutative H] [Subgroup.FiniteIndex H] [Subgroup.Normal H] (hH : Nat.Coprime (Nat.card { x // x ∈ H }) (Subgroup.index H)) (α : Subgroup.QuotientDiff H) (h : { x // x ∈ H }) : h • α = α → h = 1

theorem Subgroup.exists_smul_eq {G : Type u_1} [Group G] {H : Subgroup G} [Subgroup.IsCommutative H] [Subgroup.FiniteIndex H] [Subgroup.Normal H] (hH : Nat.Coprime (Nat.card { x // x ∈ H }) (Subgroup.index H)) (α : Subgroup.QuotientDiff H) (β : Subgroup.QuotientDiff H) : ∃ h, h • α = β

theorem Subgroup.isComplement'_stabilizer_of_coprime {G : Type u_1} [Group G] {H : Subgroup G} [Subgroup.IsCommutative H] [Subgroup.FiniteIndex H] [Subgroup.Normal H] {α : Subgroup.QuotientDiff H} (hH : Nat.Coprime (Nat.card { x // x ∈ H }) (Subgroup.index H)) : Subgroup.IsComplement' H (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:

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

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} [Subgroup.Normal N] (hN : Nat.Coprime (Fintype.card { x // x ∈ N }) (Subgroup.index N)) : ∃ H, Subgroup.IsComplement' N 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} [Subgroup.Normal N] (hN : Nat.Coprime (Nat.card { x // x ∈ N }) (Subgroup.index N)) : ∃ H, Subgroup.IsComplement' N 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} [Subgroup.Normal N] (hN : Nat.Coprime (Fintype.card { x // x ∈ N }) (Subgroup.index N)) : ∃ H, Subgroup.IsComplement' H 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} [Subgroup.Normal N] (hN : Nat.Coprime (Nat.card { x // x ∈ N }) (Subgroup.index N)) : ∃ H, Subgroup.IsComplement' H 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.