Skip to content

Commit 050bf14

Browse files
tb65536tb65536
committed
feat: port GroupTheory.SchurZassenhaus (#4752)
1 parent 2d45c79 commit 050bf14

File tree

2 files changed

+334
-0
lines changed

2 files changed

+334
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1729,6 +1729,7 @@ import Mathlib.GroupTheory.Perm.ViaEmbedding
17291729
import Mathlib.GroupTheory.PresentedGroup
17301730
import Mathlib.GroupTheory.QuotientGroup
17311731
import Mathlib.GroupTheory.Schreier
1732+
import Mathlib.GroupTheory.SchurZassenhaus
17321733
import Mathlib.GroupTheory.SemidirectProduct
17331734
import Mathlib.GroupTheory.Solvable
17341735
import Mathlib.GroupTheory.SpecificGroups.Alternating

‎Mathlib/GroupTheory/SchurZassenhaus.lean‎

Lines changed: 333 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,333 @@
1+
/-
2+
Copyright (c) 2021 Thomas Browning. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Thomas Browning
5+
6+
! This file was ported from Lean 3 source module group_theory.schur_zassenhaus
7+
! leanprover-community/mathlib commit d57133e49cf06508700ef69030cd099917e0f0de
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.GroupTheory.Sylow
12+
import Mathlib.GroupTheory.Transfer
13+
14+
/-!
15+
# The Schur-Zassenhaus Theorem
16+
17+
In this file we prove the Schur-Zassenhaus theorem.
18+
19+
## Main results
20+
21+
- `exists_right_complement'_of_coprime` : The **Schur-Zassenhaus** theorem:
22+
If `H : Subgroup G` is normal and has order coprime to its index,
23+
then there exists a subgroup `K` which is a (right) complement of `H`.
24+
- `exists_left_complement'_of_coprime` The **Schur-Zassenhaus** theorem:
25+
If `H : Subgroup G` is normal and has order coprime to its index,
26+
then there exists a subgroup `K` which is a (left) complement of `H`.
27+
-/
28+
29+
30+
open scoped BigOperators
31+
32+
namespace Subgroup
33+
34+
section SchurZassenhausAbelian
35+
36+
open MulOpposite MulAction Subgroup.leftTransversals MemLeftTransversals
37+
38+
variable {G : Type _} [Group G] (H : Subgroup G) [IsCommutative H] [FiniteIndex H]
39+
(α β : leftTransversals (H : Set G))
40+
41+
/-- The quotient of the transversals of an abelian normal `N` by the `diff` relation. -/
42+
def QuotientDiff :=
43+
Quotient
44+
(Setoid.mk (fun α β => diff (MonoidHom.id H) α β = 1)
45+
⟨fun α => diff_self (MonoidHom.id H) α, fun h => by rw [← diff_inv, h, inv_one],
46+
fun h h' => by rw [← diff_mul_diff, h, h', one_mul]⟩)
47+
#align subgroup.quotient_diff Subgroup.QuotientDiff
48+
49+
instance : Inhabited H.QuotientDiff := by
50+
dsimp [QuotientDiff] -- porting note: Added `dsimp`
51+
infer_instance
52+
53+
theorem smul_diff_smul' [hH : Normal H] (g : Gᵐᵒᵖ) :
54+
diff (MonoidHom.id H) (g • α) (g • β) =
55+
⟨g.unop⁻¹ * (diff (MonoidHom.id H) α β : H) * g.unop,
56+
hH.mem_comm ((congr_arg (· ∈ H) (mul_inv_cancel_left _ _)).mpr (SetLike.coe_mem _))⟩ := by
57+
letI := H.fintypeQuotientOfFiniteIndex
58+
let ϕ : H →* H :=
59+
{ toFun := fun h =>
60+
⟨g.unop⁻¹ * h * g.unop,
61+
hH.mem_comm ((congr_arg (· ∈ H) (mul_inv_cancel_left _ _)).mpr (SetLike.coe_mem _))⟩
62+
map_one' := by rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_self]
63+
map_mul' := fun h₁ h₂ => by
64+
simp only [Subtype.ext_iff, coe_mk, coe_mul, mul_assoc, mul_inv_cancel_left] }
65+
refine'
66+
Eq.trans
67+
(Finset.prod_bij' (fun q _ => g⁻¹ • q) (fun q _ => Finset.mem_univ _)
68+
(fun q _ => Subtype.ext _) (fun q _ => g • q) (fun q _ => Finset.mem_univ _)
69+
(fun q _ => smul_inv_smul g q) fun q _ => inv_smul_smul g q)
70+
(map_prod ϕ _ _).symm
71+
simp only [MonoidHom.id_apply, MonoidHom.coe_mk, OneHom.coe_mk,
72+
smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, mul_inv_rev, mul_assoc]
73+
#align subgroup.smul_diff_smul' Subgroup.smul_diff_smul'
74+
75+
variable {H} [Normal H]
76+
77+
noncomputable instance : MulAction G H.QuotientDiff where
78+
smul g :=
79+
Quotient.map' (fun α => op g⁻¹ • α) fun α β h =>
80+
Subtype.ext
81+
(by
82+
rwa [smul_diff_smul', coe_mk, coe_one, mul_eq_one_iff_eq_inv, mul_right_eq_self, ←
83+
coe_one, ← Subtype.ext_iff])
84+
mul_smul g₁ g₂ q :=
85+
Quotient.inductionOn' q fun T =>
86+
congr_arg Quotient.mk'' (by rw [mul_inv_rev]; exact mul_smul (op g₁⁻¹) (op g₂⁻¹) T)
87+
one_smul q :=
88+
Quotient.inductionOn' q fun T =>
89+
congr_arg Quotient.mk'' (by rw [inv_one]; apply one_smul Gᵐᵒᵖ T)
90+
91+
theorem smul_diff' (h : H) :
92+
diff (MonoidHom.id H) α (op (h : G) • β) = diff (MonoidHom.id H) α β * h ^ H.index := by
93+
letI := H.fintypeQuotientOfFiniteIndex
94+
rw [diff, diff, index_eq_card, ←Finset.card_univ, ←Finset.prod_const, ←Finset.prod_mul_distrib]
95+
refine' Finset.prod_congr rfl fun q _ => _
96+
simp_rw [Subtype.ext_iff, MonoidHom.id_apply, coe_mul, coe_mk, mul_assoc, mul_right_inj]
97+
rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, unop_op, mul_left_inj, ←Subtype.ext_iff,
98+
Equiv.apply_eq_iff_eq, inv_smul_eq_iff]
99+
exact self_eq_mul_right.mpr ((QuotientGroup.eq_one_iff _).mpr h.2)
100+
#align subgroup.smul_diff' Subgroup.smul_diff'
101+
102+
theorem eq_one_of_smul_eq_one (hH : Nat.coprime (Nat.card H) H.index) (α : H.QuotientDiff)
103+
(h : H) : h • α = α → h = 1 :=
104+
Quotient.inductionOn' α fun α hα =>
105+
(powCoprime hH).injective <|
106+
calc
107+
h ^ H.index = diff (MonoidHom.id H) (op ((h⁻¹ : H) : G) • α) α := by
108+
rw [← diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]
109+
_ = 1 ^ H.index := (Quotient.exact' hα).trans (one_pow H.index).symm
110+
111+
#align subgroup.eq_one_of_smul_eq_one Subgroup.eq_one_of_smul_eq_one
112+
113+
theorem exists_smul_eq (hH : Nat.coprime (Nat.card H) H.index) (α β : H.QuotientDiff) :
114+
∃ h : H, h • α = β :=
115+
Quotient.inductionOn' α
116+
(Quotient.inductionOn' β fun β α =>
117+
Exists.imp (fun n => Quotient.sound')
118+
⟨(powCoprime hH).symm (diff (MonoidHom.id H) β α),
119+
(diff_inv _ _ _).symm.trans
120+
(inv_eq_one.mpr
121+
((smul_diff' β α ((powCoprime hH).symm (diff (MonoidHom.id H) β α))⁻¹).trans
122+
(by rw [inv_pow, ← powCoprime_apply hH, Equiv.apply_symm_apply, mul_inv_self])))⟩)
123+
#align subgroup.exists_smul_eq Subgroup.exists_smul_eq
124+
125+
theorem isComplement'_stabilizer_of_coprime {α : H.QuotientDiff}
126+
(hH : Nat.coprime (Nat.card H) H.index) : IsComplement' H (stabilizer G α) :=
127+
IsComplement'_stabilizer α (eq_one_of_smul_eq_one hH α) fun g => exists_smul_eq hH (g • α) α
128+
#align subgroup.is_complement'_stabilizer_of_coprime Subgroup.isComplement'_stabilizer_of_coprime
129+
130+
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
131+
private theorem exists_right_complement'_of_coprime_aux (hH : Nat.coprime (Nat.card H) H.index) :
132+
∃ K : Subgroup G, IsComplement' H K :=
133+
instNonempty.elim fun α => ⟨stabilizer G α, isComplement'_stabilizer_of_coprime hH⟩
134+
135+
end SchurZassenhausAbelian
136+
137+
open scoped Classical
138+
139+
universe u
140+
141+
namespace SchurZassenhausInduction
142+
143+
/-! ## Proof of the Schur-Zassenhaus theorem
144+
145+
In this section, we prove the Schur-Zassenhaus theorem.
146+
The proof is by contradiction. We assume that `G` is a minimal counterexample to the theorem.
147+
-/
148+
149+
150+
variable {G : Type u} [Group G] [Fintype G] {N : Subgroup G} [Normal N]
151+
(h1 : Nat.coprime (Fintype.card N) N.index)
152+
(h2 :
153+
∀ (G' : Type u) [Group G'] [Fintype G'],
154+
∀ (_ : Fintype.card G' < Fintype.card G) {N' : Subgroup G'} [N'.Normal]
155+
(_ : Nat.coprime (Fintype.card N') N'.index), ∃ H' : Subgroup G', IsComplement' N' H')
156+
(h3 : ∀ H : Subgroup G, ¬IsComplement' N H)
157+
158+
/-! We will arrive at a contradiction via the following steps:
159+
* step 0: `N` (the normal Hall subgroup) is nontrivial.
160+
* step 1: If `K` is a subgroup of `G` with `K ⊔ N = ⊤`, then `K = ⊤`.
161+
* step 2: `N` is a minimal normal subgroup, phrased in terms of subgroups of `G`.
162+
* step 3: `N` is a minimal normal subgroup, phrased in terms of subgroups of `N`.
163+
* step 4: `p` (`min_fact (Fintype.card N)`) is prime (follows from step0).
164+
* step 5: `P` (a Sylow `p`-subgroup of `N`) is nontrivial.
165+
* step 6: `N` is a `p`-group (applies step 1 to the normalizer of `P` in `G`).
166+
* step 7: `N` is abelian (applies step 3 to the center of `N`).
167+
-/
168+
169+
170+
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
171+
private theorem step0 : N ≠ ⊥ := by
172+
rintro rfl
173+
exact h3 ⊤ IsComplement'_bot_top
174+
175+
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
176+
private theorem step1 (K : Subgroup G) (hK : K ⊔ N = ⊤) : K = ⊤ := by
177+
contrapose! h3
178+
have h4 : (N.comap K.subtype).index = N.index := by
179+
rw [← N.relindex_top_right, ← hK]
180+
exact (relindex_sup_right K N).symm
181+
have h5 : Fintype.card K < Fintype.card G := by
182+
rw [← K.index_mul_card]
183+
exact lt_mul_of_one_lt_left Fintype.card_pos (one_lt_index_of_ne_top h3)
184+
have h6 : Nat.coprime (Fintype.card (N.comap K.subtype)) (N.comap K.subtype).index := by
185+
rw [h4]
186+
exact h1.coprime_dvd_left (card_comap_dvd_of_injective N K.subtype Subtype.coe_injective)
187+
obtain ⟨H, hH⟩ := h2 K h5 h6
188+
replace hH : Fintype.card (H.map K.subtype) = N.index := by
189+
rw [←relindex_bot_left_eq_card, ←relindex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
190+
relindex_bot_left, ←IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
191+
subtype_range, ←relindex_sup_right, hK, relindex_top_right]
192+
have h7 : Fintype.card N * Fintype.card (H.map K.subtype) = Fintype.card G := by
193+
rw [hH, ← N.index_mul_card, mul_comm]
194+
have h8 : (Fintype.card N).coprime (Fintype.card (H.map K.subtype)) := by
195+
rwa [hH]
196+
exact ⟨H.map K.subtype, IsComplement'_of_coprime h7 h8⟩
197+
198+
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
199+
private theorem step2 (K : Subgroup G) [K.Normal] (hK : K ≤ N) : K = ⊥ ∨ K = N := by
200+
have : Function.Surjective (QuotientGroup.mk' K) := Quotient.surjective_Quotient_mk''
201+
have h4 := step1 h1 h2 h3
202+
contrapose! h4
203+
rw [not_or] at h4 -- porting note: had to add `rw [not_or] at h4`
204+
have h5 : Fintype.card (G ⧸ K) < Fintype.card G := by
205+
rw [← index_eq_card, ← K.index_mul_card]
206+
refine'
207+
lt_mul_of_one_lt_right (Nat.pos_of_ne_zero index_ne_zero_of_finite)
208+
(K.one_lt_card_iff_ne_bot.mpr h4.1)
209+
have h6 :
210+
(Fintype.card (N.map (QuotientGroup.mk' K))).coprime (N.map (QuotientGroup.mk' K)).index := by
211+
have index_map := N.index_map_eq this (by rwa [QuotientGroup.ker_mk'])
212+
have index_pos : 0 < N.index := Nat.pos_of_ne_zero index_ne_zero_of_finite
213+
rw [index_map]
214+
refine' h1.coprime_dvd_left _
215+
rw [← Nat.mul_dvd_mul_iff_left index_pos, index_mul_card, ← index_map, index_mul_card]
216+
exact K.card_quotient_dvd_card
217+
obtain ⟨H, hH⟩ := h2 (G ⧸ K) h5 h6
218+
refine' ⟨H.comap (QuotientGroup.mk' K), _, _⟩
219+
· have key : (N.map (QuotientGroup.mk' K)).comap (QuotientGroup.mk' K) = N := by
220+
refine' comap_map_eq_self _
221+
rwa [QuotientGroup.ker_mk']
222+
rwa [← key, comap_sup_eq, hH.symm.sup_eq_top, comap_top]
223+
· rw [← comap_top (QuotientGroup.mk' K)]
224+
intro hH'
225+
rw [comap_injective this hH', IsComplement'_top_right, map_eq_bot_iff,
226+
QuotientGroup.ker_mk'] at hH
227+
· exact h4.2 (le_antisymm hK hH)
228+
229+
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
230+
private theorem step3 (K : Subgroup N) [(K.map N.subtype).Normal] : K = ⊥ ∨ K = ⊤ := by
231+
have key := step2 h1 h2 h3 (K.map N.subtype) (map_subtype_le K)
232+
rw [← map_bot N.subtype] at key
233+
conv at key =>
234+
rhs
235+
rhs
236+
rw [← N.subtype_range, N.subtype.range_eq_map]
237+
have inj := map_injective N.subtype_injective
238+
rwa [inj.eq_iff, inj.eq_iff] at key
239+
240+
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
241+
private theorem step4 : (Fintype.card N).minFac.Prime :=
242+
Nat.minFac_prime (N.one_lt_card_iff_ne_bot.mpr (step0 h1 h3)).ne'
243+
244+
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
245+
private theorem step5 {P : Sylow (Fintype.card N).minFac N} : P.1 ≠ ⊥ :=
246+
haveI : Fact (Fintype.card N).minFac.Prime := ⟨step4 h1 h3⟩
247+
P.ne_bot_of_dvd_card (Fintype.card N).minFac_dvd
248+
249+
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
250+
private theorem step6 : IsPGroup (Fintype.card N).minFac N := by
251+
haveI : Fact (Fintype.card N).minFac.Prime := ⟨step4 h1 h3⟩
252+
refine' Sylow.nonempty.elim fun P => P.2.of_surjective P.1.subtype _
253+
rw [← MonoidHom.range_top_iff_surjective, subtype_range]
254+
haveI : (P.1.map N.subtype).Normal :=
255+
normalizer_eq_top.mp (step1 h1 h2 h3 (P.1.map N.subtype).normalizer P.normalizer_sup_eq_top)
256+
exact (step3 h1 h2 h3 P.1).resolve_left (step5 h1 h3)
257+
258+
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
259+
theorem step7 : IsCommutative N := by
260+
haveI := N.bot_or_nontrivial.resolve_left (step0 h1 h3)
261+
haveI : Fact (Fintype.card N).minFac.Prime := ⟨step4 h1 h3⟩
262+
exact
263+
⟨⟨fun g h =>
264+
eq_top_iff.mp ((step3 h1 h2 h3 (center N)).resolve_left (step6 h1 h2 h3).bot_lt_center.ne')
265+
(mem_top h) g⟩⟩
266+
#align subgroup.schur_zassenhaus_induction.step7 Subgroup.SchurZassenhausInduction.step7
267+
268+
end SchurZassenhausInduction
269+
270+
variable {n : ℕ} {G : Type u} [Group G]
271+
272+
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
273+
private theorem exists_right_complement'_of_coprime_aux' [Fintype G] (hG : Fintype.card G = n)
274+
{N : Subgroup G} [N.Normal] (hN : Nat.coprime (Fintype.card N) N.index) :
275+
∃ H : Subgroup G, IsComplement' N H := by
276+
revert G
277+
apply Nat.strongInductionOn n
278+
rintro n ih G _ _ rfl N _ hN
279+
refine' not_forall_not.mp fun h3 => _
280+
haveI := SchurZassenhausInduction.step7 hN (fun G' _ _ hG' => by apply ih _ hG'; rfl) h3
281+
rw [← Nat.card_eq_fintype_card] at hN
282+
exact not_exists_of_forall_not h3 (exists_right_complement'_of_coprime_aux hN)
283+
284+
/-- **Schur-Zassenhaus** for normal subgroups:
285+
If `H : Subgroup G` is normal, and has order coprime to its index, then there exists a
286+
subgroup `K` which is a (right) complement of `H`. -/
287+
theorem exists_right_complement'_of_coprime_of_fintype [Fintype G] {N : Subgroup G} [N.Normal]
288+
(hN : Nat.coprime (Fintype.card N) N.index) : ∃ H : Subgroup G, IsComplement' N H :=
289+
exists_right_complement'_of_coprime_aux' rfl hN
290+
#align subgroup.exists_right_complement'_of_coprime_of_fintype
291+
Subgroup.exists_right_complement'_of_coprime_of_fintype
292+
293+
/-- **Schur-Zassenhaus** for normal subgroups:
294+
If `H : Subgroup G` is normal, and has order coprime to its index, then there exists a
295+
subgroup `K` which is a (right) complement of `H`. -/
296+
theorem exists_right_complement'_of_coprime {N : Subgroup G} [N.Normal]
297+
(hN : Nat.coprime (Nat.card N) N.index) : ∃ H : Subgroup G, IsComplement' N H := by
298+
by_cases hN1 : Nat.card N = 0
299+
· rw [hN1, Nat.coprime_zero_left, index_eq_one] at hN
300+
rw [hN]
301+
exact ⟨⊥, IsComplement'_top_bot⟩
302+
by_cases hN2 : N.index = 0
303+
· rw [hN2, Nat.coprime_zero_right] at hN
304+
haveI := (Cardinal.toNat_eq_one_iff_unique.mp hN).1
305+
rw [N.eq_bot_of_subsingleton]
306+
exact ⟨⊤, IsComplement'_bot_top⟩
307+
have hN3 : Nat.card G ≠ 0 := by
308+
rw [← N.card_mul_index]
309+
exact mul_ne_zero hN1 hN2
310+
haveI := (Cardinal.lt_aleph0_iff_fintype.mp
311+
(lt_of_not_ge (mt Cardinal.toNat_apply_of_aleph0_le hN3))).some
312+
apply exists_right_complement'_of_coprime_of_fintype
313+
rwa [←Nat.card_eq_fintype_card]
314+
#align subgroup.exists_right_complement'_of_coprime Subgroup.exists_right_complement'_of_coprime
315+
316+
/-- **Schur-Zassenhaus** for normal subgroups:
317+
If `H : Subgroup G` is normal, and has order coprime to its index, then there exists a
318+
subgroup `K` which is a (left) complement of `H`. -/
319+
theorem exists_left_complement'_of_coprime_of_fintype [Fintype G] {N : Subgroup G} [N.Normal]
320+
(hN : Nat.coprime (Fintype.card N) N.index) : ∃ H : Subgroup G, IsComplement' H N :=
321+
Exists.imp (fun _ => IsComplement'.symm) (exists_right_complement'_of_coprime_of_fintype hN)
322+
#align subgroup.exists_left_complement'_of_coprime_of_fintype
323+
Subgroup.exists_left_complement'_of_coprime_of_fintype
324+
325+
/-- **Schur-Zassenhaus** for normal subgroups:
326+
If `H : Subgroup G` is normal, and has order coprime to its index, then there exists a
327+
subgroup `K` which is a (left) complement of `H`. -/
328+
theorem exists_left_complement'_of_coprime {N : Subgroup G} [N.Normal]
329+
(hN : Nat.coprime (Nat.card N) N.index) : ∃ H : Subgroup G, IsComplement' H N :=
330+
Exists.imp (fun _ => IsComplement'.symm) (exists_right_complement'_of_coprime hN)
331+
#align subgroup.exists_left_complement'_of_coprime Subgroup.exists_left_complement'_of_coprime
332+
333+
end Subgroup

0 commit comments

Comments
 (0)