Source: ProCGroups.FiniteGroups.StandardClasses
1import Mathlib.GroupTheory.Nilpotent
2import Mathlib.NumberTheory.Padics.PadicVal.Basic
3import ProCGroups.FiniteGroups.AllFinite
5/-!
6# Standard classes of finite groups
8This module constructs the cyclic, abelian, solvable, nilpotent, finite \(p\)-group,
9\(\sigma\)-group, and bounded-exponent abelian classes. It proves the subgroup, quotient,
10product, extension, formation, and full-formation properties needed later, together with the
11finite-order arithmetic and cyclic witnesses supporting those proofs.
12-/
14namespace ProCGroups
16universe u v
18namespace FiniteGroupClass
20/-- If \(a \nmid b\), then some prime factor has a larger exponent in \(a\) than in \(b\). -/
21theorem exists_factorization_lt_of_not_dvd
22 {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (hndvd : ¬ a ∣ b) :
23 ∃ p, b.factorization p < a.factorization p := by
24 by_contra h
25 push Not at h
26 have hle : a.factorization ≤ b.factorization := by
27 intro p
28 exact h p
29 exact hndvd ((Nat.factorization_le_iff_dvd ha hb).1 hle)
31/-- The p-adic exponent of a positive integer is at most the integer itself. -/
32theorem nat_factorization_le_self_of_prime
33 {A p : ℕ} (hp : Nat.Prime p) :
34 A.factorization p ≤ A :=
35 Nat.factorization_le_of_le_pow (le_of_lt (Nat.lt_pow_self (n := A) (a := p) hp.one_lt))
37/-- The depth \((K*d)^(A+1)\) is large enough for the GCD-conditioned cyclic reduction. -/
38theorem gcd_mul_dvd_pow_depth
39 {K d A : ℕ} (hK : 0 < K) (hd : 0 < d) (hA : 0 < A) :
40 Nat.gcd (d * A) (K * (K * d) ^ (A + 1)) ∣ (K * d) ^ (A + 1) := by
41 let B : ℕ := K * d
42 let M : ℕ := B ^ (A + 1)
43 have hB : 0 < B := Nat.mul_pos hK hd
44 have hM : 0 < M := pow_pos hB (A + 1)
45 have hleft_ne : d * A ≠ 0 := Nat.ne_of_gt (Nat.mul_pos hd hA)
46 have hright_ne : K * M ≠ 0 := Nat.ne_of_gt (Nat.mul_pos hK hM)
47 have hgcd_ne : Nat.gcd (d * A) (K * M) ≠ 0 :=
48 Nat.ne_of_gt (Nat.gcd_pos_of_pos_left (K * M) (Nat.mul_pos hd hA))
49 rw [← Nat.factorization_le_iff_dvd hgcd_ne (Nat.ne_of_gt hM)]
50 intro p
51 by_cases hp : Nat.Prime p
52 · by_cases hpB : p ∣ B
53 · have hdvdB : d ∣ B := by
54 exact Nat.dvd_mul_left d K
55 have hdfacB : d.factorization p ≤ B.factorization p :=
56 (Nat.factorization_le_iff_dvd (Nat.ne_of_gt hd) (Nat.ne_of_gt hB)).2 hdvdB p
57 have hAfacle : A.factorization p ≤ A :=
58 nat_factorization_le_self_of_prime hp
59 have hBfacpos : 0 < B.factorization p := by
60 exact lt_of_lt_of_le Nat.zero_lt_one
61 ((hp.dvd_iff_one_le_factorization (Nat.ne_of_gt hB)).1 hpB)
62 have hleft_fac_le :
63 (d * A).factorization p ≤ M.factorization p := by
64 calc
65 (d * A).factorization p
66 = d.factorization p + A.factorization p := by
67 rw [Nat.factorization_mul (Nat.ne_of_gt hd) (Nat.ne_of_gt hA)]
68 rfl
69 _ ≤ B.factorization p + A := Nat.add_le_add hdfacB hAfacle
70 _ ≤ B.factorization p + A * B.factorization p := by
71 exact Nat.add_le_add_left
72 (Nat.le_mul_of_pos_right A hBfacpos) (B.factorization p)
73 _ = (A + 1) * B.factorization p := by
74 rw [Nat.add_mul, one_mul, add_comm]
75 _ = M.factorization p := by
76 simp only [Nat.factorization_pow, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, M]
77 have hgcd_fac :
78 (Nat.gcd (d * A) (K * M)).factorization p =
79 min ((d * A).factorization p) ((K * M).factorization p) := by
80 rw [Nat.factorization_gcd hleft_ne hright_ne]
81 rfl
82 rw [hgcd_fac]
83 exact (min_le_left _ _).trans hleft_fac_le
84 · have hnotK : ¬ p ∣ K := by
85 intro hpK
86 exact hpB (dvd_mul_of_dvd_left hpK d)
87 have hnotM : ¬ p ∣ M := by
88 intro hpM
89 exact hpB (hp.dvd_of_dvd_pow hpM)
90 have hnotKM : ¬ p ∣ K * M := by
91 exact hp.not_dvd_mul hnotK hnotM
92 have hright_fac : (K * M).factorization p = 0 :=
93 Nat.factorization_eq_zero_of_not_dvd hnotKM
94 have hgcd_fac :
95 (Nat.gcd (d * A) (K * M)).factorization p =
96 min ((d * A).factorization p) ((K * M).factorization p) := by
97 rw [Nat.factorization_gcd hleft_ne hright_ne]
98 rfl
99 rw [hgcd_fac, hright_fac]
100 simp only [zero_le, inf_of_le_right]
101 · simp only [Nat.factorization_eq_zero_of_not_prime _ hp, le_refl]
103/-- The class of finite cyclic groups. -/
104def cyclic : FiniteGroupClass.{u} where
105 pred := fun G [_] => Finite G ∧ IsCyclic G
106 finite_of_mem := fun hG => hG.1
107 mem_of_mulEquiv := by
108 intro G H _ _ e hG
109 letI : Finite G := hG.1
110 exact ⟨Finite.of_equiv G e.toEquiv, e.isCyclic.mp hG.2⟩
112/-- The class of finite abelian groups. -/
113def abelian : FiniteGroupClass.{u} where
114 pred := fun G [_] => Finite G ∧ ∀ a b : G, a * b = b * a
115 finite_of_mem := fun hG => hG.1
116 mem_of_mulEquiv := by
117 intro G H _ _ e hG
118 letI : Finite G := hG.1
119 refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
120 intro a b
121 apply e.symm.injective
122 simpa using hG.2 (e.symm a) (e.symm b)
124/-- The class of finite solvable groups. -/
125def solvable : FiniteGroupClass.{u} where
126 pred := fun G [_] => Finite G ∧ IsSolvable G
127 finite_of_mem := fun hG => hG.1
128 mem_of_mulEquiv := by
129 intro G H _ _ e hG
130 letI : Finite G := hG.1
131 letI : IsSolvable G := hG.2
132 exact ⟨Finite.of_equiv G e.toEquiv,
133 solvable_of_surjective (f := e.toMonoidHom) e.surjective⟩
135/-- The finite group class consisting of finite nilpotent groups. -/
136def nilpotent : FiniteGroupClass.{u} where
137 pred := fun G [_] => Finite G ∧ Group.IsNilpotent G
138 finite_of_mem := fun hG => hG.1
139 mem_of_mulEquiv := by
140 intro G H _ _ e hG
141 letI : Finite G := hG.1
142 exact ⟨Finite.of_equiv G e.toEquiv,
143 (Group.isNilpotent_congr e).mp hG.2⟩
145/-- The class of finite \(p\)-groups. -/
146def pGroup (p : ℕ) [Fact (Nat.Prime p)] : FiniteGroupClass.{u} where
147 pred := fun G [_] => Finite G ∧ IsPGroup p G
148 finite_of_mem := fun hG => hG.1
149 mem_of_mulEquiv := by
150 intro G H _ _ e hG
151 letI : Finite G := hG.1
152 exact ⟨Finite.of_equiv G e.toEquiv,
153 hG.2.of_surjective e.toMonoidHom e.surjective⟩
155/--
156A natural number whose prime divisors all lie in \(\Sigma\). This is the finite-level condition
157underlying finite \(\Sigma\)-groups and pro-\(\Sigma\) groups.
158-/
159def IsSigmaNumber (sigma : Set ℕ) (n : ℕ) : Prop :=
160 ∀ p, Nat.Prime p → p ∉ sigma → ¬ p ∣ n
162namespace IsSigmaNumber
164/-- Every divisor of a \(\Sigma\)-number is again a \(\Sigma\)-number. -/
165theorem of_dvd {sigma : Set ℕ} {m n : ℕ} (hn : IsSigmaNumber sigma n) (hmn : m ∣ n) :
166 IsSigmaNumber sigma m := by
167 intro p hp hpsigma hpm
168 exact hn p hp hpsigma (dvd_trans hpm hmn)
170/-- The product of two \(\Sigma\)-numbers is a \(\Sigma\)-number. -/
171theorem mul {sigma : Set ℕ} {m n : ℕ} (hm : IsSigmaNumber sigma m)
172 (hn : IsSigmaNumber sigma n) :
173 IsSigmaNumber sigma (m * n) := by
174 intro p hp hpsigma hpmn
175 exact (hp.not_dvd_mul (hm p hp hpsigma) (hn p hp hpsigma)) hpmn
177/-- A finite product of \(\Sigma\)-numbers is a \(\Sigma\)-number. -/
178theorem prod {sigma : Set ℕ} {ι : Type*} (s : Finset ι) (f : ι → ℕ)
179 (hf : ∀ i ∈ s, IsSigmaNumber sigma (f i)) :
180 IsSigmaNumber sigma (s.prod f) := by
181 classical
182 induction s using Finset.induction with
183 | empty =>
184 intro p hp _ hpdvd
185 exact hp.ne_one (Nat.dvd_one.mp hpdvd)
186 | insert a s ha hs =>
187 have hfa : IsSigmaNumber sigma (f a) := hf a (Finset.mem_insert_self a s)
188 have hfs : ∀ i ∈ s, IsSigmaNumber sigma (f i) :=
189 fun i hi => hf i (Finset.mem_insert_of_mem hi)
190 simpa [Finset.prod_insert ha] using mul (sigma := sigma) hfa (hs hfs)
192/-- A natural-number power of a \(\Sigma\)-number is a \(\Sigma\)-number. -/
193theorem pow {sigma : Set ℕ} {n k : ℕ} (hn : IsSigmaNumber sigma n) :
194 IsSigmaNumber sigma (n ^ k) := by
195 induction k with
196 | zero =>
197 intro p hp _ hpdvd
198 exact hp.ne_one (Nat.dvd_one.mp hpdvd)
199 | succ k ih =>
200 rw [pow_succ]
201 exact mul ih hn
203/-- A prime power whose prime lies in \(\Sigma\) is a \(\Sigma\)-number. -/
204theorem prime_pow_of_mem {sigma : Set ℕ} {p k : ℕ}
205 (hpsigma : p ∈ sigma) (hp : Nat.Prime p) :
206 IsSigmaNumber sigma (p ^ k) := by
207 intro q hq hqsigma hqdiv
208 by_cases hk : k = 0
209 · simp only [hk, pow_zero, Nat.dvd_one] at hqdiv
210 exact hq.ne_one hqdiv
211 · have hq_dvd_p : q ∣ p := hq.dvd_of_dvd_pow hqdiv
212 have hp_eq_q : p = q := (hp.dvd_iff_eq hq.ne_one).1 hq_dvd_p
213 exact hqsigma (hp_eq_q ▸ hpsigma)
215end IsSigmaNumber
217/--
218The class of finite \(\Sigma\)-groups: finite groups whose order has no prime divisors outside
219\(\Sigma\).
220-/
221def sigmaGroup (sigma : Set ℕ) : FiniteGroupClass.{u} where
222 pred := fun G [_] => Finite G ∧ IsSigmaNumber sigma (Nat.card G)
223 finite_of_mem := fun hG => hG.1
224 mem_of_mulEquiv := by
225 intro G H _ _ e hG
226 letI : Finite G := hG.1
227 refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
228 simpa [Nat.card_congr e.toEquiv] using hG.2
230/-- The class of finite abelian groups of exponent dividing \(n\). -/
231def abelianExponent (n : ℕ) : FiniteGroupClass.{u} where
232 pred := fun G [_] =>
233 Finite G ∧ (∀ a b : G, a * b = b * a) ∧ ∀ g : G, g ^ n = 1
234 finite_of_mem := fun hG => hG.1
235 mem_of_mulEquiv := by
236 intro G H _ _ e hG
237 letI : Finite G := hG.1
238 refine ⟨Finite.of_equiv G e.toEquiv, ?_, ?_⟩
239 · intro a b
240 apply e.symm.injective
241 simpa using hG.2.1 (e.symm a) (e.symm b)
242 · intro g
243 apply e.symm.injective
244 simpa using hG.2.2 (e.symm g)
246section
248variable {p : ℕ}
250/-- Finite products of abstract \(p\)-groups are \(p\)-groups. -/
251theorem isPGroup_pi {ι : Type u} [Finite ι] {G : ι → Type v}
252 [∀ i, Group (G i)] (hG : ∀ i, IsPGroup p (G i)) :
253 IsPGroup p ((i : ι) → G i) := by
254 classical
255 letI := Fintype.ofFinite ι
256 intro g
257 choose k hk using fun i => hG i (g i)
258 let N : ℕ := Finset.univ.sup k
259 refine ⟨N, ?_⟩
260 funext i
261 have hki : k i ≤ N := Finset.le_sup (Finset.mem_univ i)
262 calc
263 (g ^ p ^ N) i = (g i) ^ (p ^ N) := by simp only [Pi.pow_apply]
264 _ = (g i) ^ (p ^ (k i) * p ^ (N - k i)) := by
265 rw [← Nat.pow_add, Nat.add_sub_of_le hki]
266 _ = ((g i) ^ (p ^ k i)) ^ (p ^ (N - k i)) := by
267 rw [pow_mul]
268 _ = 1 := by simp only [hk i, one_pow]
270/-- The class of finite \(p\)-groups is a formation. -/
271theorem pGroup_formation (p : ℕ) [Fact (Nat.Prime p)] :
272 FiniteGroupClass.Formation (FiniteGroupClass.pGroup p) := by
273 refine ⟨?_, ?_⟩
274 · intro G _ N _ hG
275 rcases hG with ⟨hfin, hpG⟩
276 refine ⟨?_, hpG.to_quotient N⟩
277 letI : Finite G := hfin
278 infer_instance
279 · intro ι _ G _ H _ f hf _hsurj hH
280 letI : ∀ i, Finite (H i) := fun i => (hH i).1
281 have hPi : IsPGroup p ((i : ι) → H i) := isPGroup_pi (p := p) fun i => (hH i).2
282 exact ⟨Finite.of_injective f hf, hPi.of_injective f hf⟩
284/-- Finite \(p\)-groups contain the trivial quotients. -/
285instance pGroup_containsTrivialQuotients (p : ℕ) [Fact (Nat.Prime p)] :
286 ContainsTrivialQuotients (pGroup p : FiniteGroupClass.{u}) :=
287 (pGroup_formation p).containsTrivialQuotients
289/-- Subgroups of finite \(p\)-groups are finite \(p\)-groups. -/
290theorem pGroup_subgroupClosed (p : ℕ) [Fact (Nat.Prime p)] : SubgroupClosed (pGroup p) := by
291 intro G _ H hG
292 rcases hG with ⟨hfin, hpG⟩
293 exact ⟨Finite.of_injective ((↑) : H → G) Subtype.coe_injective, hpG.to_subgroup H⟩
295/-- A group is finite when a normal subgroup and the corresponding quotient are finite. -/
296theorem finite_of_finite_normalSubgroup_and_quotient
297 {E : Type u} [Group E] (N : Subgroup E) [N.Normal]
298 [Finite N] [Finite (E ⧸ N)] :
299 Finite E := by
300 classical
301 let s : E ⧸ N → E := Quotient.out
302 let f : N × (E ⧸ N) → E := fun z => z.1.1 * s z.2
303 have hsurj : Function.Surjective f := by
304 intro e
305 let q : E ⧸ N := QuotientGroup.mk' N e
306 have hsq : QuotientGroup.mk' N (s q) = q := Quotient.out_eq' q
307 have hmem : e * (s q)⁻¹ ∈ N := by
308 apply (QuotientGroup.eq_one_iff (N := N) (e * (s q)⁻¹)).1
309 change QuotientGroup.mk' N e * (QuotientGroup.mk' N (s q))⁻¹ = 1
310 rw [hsq]
311 simp only [QuotientGroup.mk'_apply, mul_inv_cancel, q]
312 refine ⟨(⟨e * (s q)⁻¹, hmem⟩, q), ?_⟩
313 simp only [QuotientGroup.mk'_apply, mul_assoc, inv_mul_cancel, mul_one, f, q]
314 exact Finite.of_surjective f hsurj
316/-- Extensions of finite \(p\)-groups are finite \(p\)-groups. -/
317theorem pGroup_extensionClosed (p : ℕ) [Fact (Nat.Prime p)] :
318 ExtensionClosed (pGroup p) := by
319 intro E _ N _ hN hQ
320 rcases hN with ⟨hNfin, hpN⟩
321 rcases hQ with ⟨hQfin, hpQ⟩
322 letI : Finite N := hNfin
323 letI : Finite (E ⧸ N) := hQfin
324 have hEfin : Finite E := finite_of_finite_normalSubgroup_and_quotient (N := N)
325 letI : Finite E := hEfin
326 have hker :
327 IsPGroup p ((QuotientGroup.mk' N).ker : Subgroup E) := by
328 exact hpN.of_equiv (MulEquiv.subgroupCongr (QuotientGroup.ker_mk' N).symm)
329 have hTopQ : IsPGroup p (⊤ : Subgroup (E ⧸ N)) := hpQ.to_subgroup ⊤
330 have hTopE :
331 IsPGroup p ((⊤ : Subgroup (E ⧸ N)).comap (QuotientGroup.mk' N)) :=
332 hTopQ.comap_of_ker_isPGroup (QuotientGroup.mk' N) hker
333 have hTop' : IsPGroup p (⊤ : Subgroup E) := by
334 rw [Subgroup.comap_top] at hTopE
335 exact hTopE
336 have hEp : IsPGroup p E :=
337 hTop'.of_surjective (⊤ : Subgroup E).subtype <| by
338 intro x
339 exact ⟨⟨x, by simp only [Subgroup.mem_top]⟩, rfl⟩
340 exact ⟨hEfin, hEp⟩
342/-- The class of finite \(p\)-groups is hereditary under subgroups. -/
343theorem pGroup_hereditary (p : ℕ) [Fact (Nat.Prime p)] : Hereditary (pGroup p) :=
344 Hereditary.of_subgroupClosed_isomClosed
345 (pGroup_subgroupClosed p)
346 (pGroup_formation p).isomClosed
348end
350section
352variable {sigma : Set ℕ}
354/-- `sigmaGroup` is closed under group isomorphism. -/
355theorem sigmaGroup_isomClosed (sigma : Set ℕ) : IsomClosed (sigmaGroup sigma) := by
356 intro G H _ _ hGH hG
357 rcases hGH with ⟨e⟩
358 rcases hG with ⟨hfin, hsigma⟩
359 refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
360 simpa [Nat.card_congr e.toEquiv] using hsigma
362/-- `sigmaGroup` is closed under subgroups. -/
363theorem sigmaGroup_subgroupClosed (sigma : Set ℕ) : SubgroupClosed (sigmaGroup sigma) := by
364 intro G _ H hG
365 rcases hG with ⟨hfin, hsigma⟩
366 refine ⟨Finite.of_injective ((↑) : H → G) Subtype.coe_injective, ?_⟩
367 exact IsSigmaNumber.of_dvd (sigma := sigma) hsigma (Subgroup.card_subgroup_dvd_card H)
369/-- `sigmaGroup` is closed under quotients. -/
370theorem sigmaGroup_quotientClosed (sigma : Set ℕ) : QuotientClosed (sigmaGroup sigma) := by
371 intro G _ N _ hG
372 rcases hG with ⟨hfin, hsigma⟩
373 refine ⟨?_, ?_⟩
374 · letI : Finite G := hfin
375 infer_instance
376 · exact IsSigmaNumber.of_dvd (sigma := sigma) hsigma (Subgroup.card_quotient_dvd_card N)
378/-- `sigmaGroup` is closed under finite products. -/
379theorem sigmaGroup_finiteProductClosed (sigma : Set ℕ) : FiniteProductClosed (sigmaGroup sigma)
380 := by
381 intro ι _ A _ hA
382 refine ⟨?_, ?_⟩
383 · letI : ∀ i, Finite (A i) := fun i => (hA i).1
384 infer_instance
385 · simpa [Nat.card_pi] using
386 IsSigmaNumber.prod (sigma := sigma) Finset.univ (fun i => Nat.card (A i))
387 (fun i _ => (hA i).2)
389/-- `sigmaGroup` is a finite-group variety. -/
390theorem sigmaGroup_variety (sigma : Set ℕ) : Variety (sigmaGroup sigma) := by
391 refine ⟨sigmaGroup_subgroupClosed sigma, sigmaGroup_quotientClosed sigma,
392 sigmaGroup_finiteProductClosed sigma⟩
394/-- `sigmaGroup` is a formation of finite groups. -/
395theorem sigmaGroup_formation (sigma : Set ℕ) : Formation (sigmaGroup sigma) :=
396 variety_formation (sigmaGroup_variety sigma) (sigmaGroup_isomClosed sigma)
398/-- Finite `Σ`-groups are closed under extensions. -/
399theorem sigmaGroup_extensionClosed (sigma : Set ℕ) :
400 ExtensionClosed (sigmaGroup sigma) := by
401 intro E _ N _ hN hQ
402 rcases hN with ⟨hNfin, hsigmaN⟩
403 rcases hQ with ⟨hQfin, hsigmaQ⟩
404 letI : Finite N := hNfin
405 letI : Finite (E ⧸ N) := hQfin
406 have hEfin : Finite E := finite_of_finite_normalSubgroup_and_quotient (N := N)
407 letI : Finite E := hEfin
408 refine ⟨hEfin, ?_⟩
409 have hcard :
410 Nat.card E = Nat.card (E ⧸ N) * Nat.card N := by
411 exact Subgroup.card_eq_card_quotient_mul_card_subgroup (α := E) N
412 rw [hcard]
413 exact IsSigmaNumber.mul hsigmaQ hsigmaN
415/-- Finite `Σ`-groups form a Melnikov formation. -/
416theorem sigmaGroup_melnikovFormation (sigma : Set ℕ) :
417 MelnikovFormation (sigmaGroup sigma) where
418 formation := sigmaGroup_formation sigma
419 normalSubgroupClosed := fun N _ hG => sigmaGroup_subgroupClosed sigma N hG
420 extensionClosed := sigmaGroup_extensionClosed sigma
422/-- Finite `Σ`-groups form a full formation. -/
423theorem sigmaGroup_fullFormation (sigma : Set ℕ) :
424 FullFormation (sigmaGroup sigma) where
425 melnikovFormation := sigmaGroup_melnikovFormation sigma
426 subgroupClosed := sigmaGroup_subgroupClosed sigma
428/-- A positive `Σ`-number gives an allowed finite cyclic `Σ`-group. -/
429theorem sigmaGroup_cyclicZMod
430 {sigma : Set ℕ} {n : ℕ} (hn : 0 < n)
431 (hsigma : IsSigmaNumber sigma n) :
432 sigmaGroup sigma (ULift.{u} (Multiplicative (ZMod n))) := by
433 letI : NeZero n := ⟨Nat.ne_of_gt hn⟩
434 let A := ULift.{u} (Multiplicative (ZMod n))
435 let e : A ≃* Multiplicative (ZMod n) := MulEquiv.ulift
436 letI : Finite A := Finite.of_equiv (Multiplicative (ZMod n)) e.symm.toEquiv
437 refine ⟨inferInstance, ?_⟩
438 have hcard : Nat.card A = n := by
439 calc
440 Nat.card A = Nat.card (Multiplicative (ZMod n)) := Nat.card_congr e.toEquiv
441 _ = n := by simp only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, ZMod.card]
442 simpa [hcard] using hsigma
444/-- A nonempty set of primes supplies a nontrivial finite cyclic `Σ`-group. -/
445theorem sigmaGroup_nontrivialCyclic
446 {sigma : Set ℕ} (hsigma : ∃ p, p ∈ sigma ∧ Nat.Prime p) :
447 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
448 sigmaGroup sigma A ∧ IsCyclic A ∧ Nontrivial A := by
449 rcases hsigma with ⟨p, hpsigma, hp⟩
450 letI : Fact (1 < p) := ⟨hp.one_lt⟩
451 let A := ULift.{u} (Multiplicative (ZMod p))
452 let e : A ≃* Multiplicative (ZMod p) := MulEquiv.ulift
453 letI : Finite A := Finite.of_equiv (Multiplicative (ZMod p)) e.symm.toEquiv
454 have hcyc : IsCyclic A :=
455 isCyclic_of_surjective e.symm.toMonoidHom e.symm.surjective
456 have hnon : Nontrivial A := e.toEquiv.nontrivial
457 refine ⟨A, inferInstance, inferInstance, ?_, hcyc, hnon⟩
458 exact sigmaGroup_cyclicZMod (sigma := sigma) hp.pos <| by
459 simpa using
460 (IsSigmaNumber.prime_pow_of_mem (sigma := sigma) (p := p) (k := 1) hpsigma hp)
462/-- Product of a finite `Σ`-group with the concrete cyclic group `ZMod N`. -/
463theorem sigmaGroup_prod_multiplicativeZMod
464 {sigma : Set ℕ} {Q : Type u} [Group Q]
465 (hQ : sigmaGroup sigma Q)
466 {N : ℕ} (hNpos : 0 < N)
467 (hNsigma : IsSigmaNumber sigma N) :
468 sigmaGroup sigma (Q × Multiplicative (ZMod N)) := by
469 rcases hQ with ⟨hQfin, hQsigma⟩
470 letI : Finite Q := hQfin
471 letI : NeZero N := ⟨Nat.ne_of_gt hNpos⟩
472 letI : Finite (Multiplicative (ZMod N)) :=
473 @Finite.of_equiv _ _ (show Finite (ZMod N) by infer_instance) Multiplicative.toAdd
474 refine ⟨inferInstance, ?_⟩
475 have hcard : Nat.card (Multiplicative (ZMod N)) = N := by
476 simp only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, ZMod.card]
477 rw [Nat.card_prod, hcard]
478 exact IsSigmaNumber.mul hQsigma hNsigma
480/-- A nontrivial finite `Σ`-group power supplies a coefficient prime and depth. -/
481theorem exists_prime_power_orderOf_gt_padicValNat_of_zpow_ne_one
482 {sigma : Set ℕ} {G : Type u} [Group G] [Finite G]
483 (hG : sigmaGroup sigma G) {g : G} {n : ℤ} (hgn : g ^ n ≠ 1) :
484 ∃ ℓ σ : ℕ,
485 Nat.Prime ℓ ∧ 0 < σ ∧ ℓ ∈ sigma ∧
486 padicValNat ℓ n.natAbs < σ ∧ ℓ ^ σ ∣ orderOf g := by
487 have hnZ : g ^ ((n.natAbs : ℕ) : ℤ) ≠ 1 := by
488 intro h
489 apply hgn
490 rcases Int.natAbs_eq n with hn | hn
491 · rw [hn]
492 simpa using h
493 · rw [hn]
494 have hinv : (g ^ ((n.natAbs : ℕ) : ℤ))⁻¹ = (1 : G) := by
495 rw [h, inv_one]
496 simpa [zpow_neg] using hinv
497 have hnat : g ^ n.natAbs ≠ 1 := by
498 intro hpow
499 exact hnZ (by simpa using hpow)
500 have hgfin : IsOfFinOrder g := isOfFinOrder_of_finite g
501 have horder_pos : 0 < orderOf g := (orderOf_pos_iff).2 hgfin
502 have horder_ne : orderOf g ≠ 0 := Nat.ne_of_gt horder_pos
503 have hnabs_ne : n.natAbs ≠ 0 := by
504 intro hnabs
505 apply hnat
506 simp only [hnabs, pow_zero]
507 have hnotdvd : ¬ orderOf g ∣ n.natAbs := by
508 intro hdiv
509 exact hnat ((orderOf_dvd_iff_pow_eq_one (x := g) (n := n.natAbs)).1 hdiv)
510 rcases exists_factorization_lt_of_not_dvd horder_ne hnabs_ne hnotdvd with
511 ⟨ℓ, hℓlt⟩
512 have hℓ_fac_ne : (orderOf g).factorization ℓ ≠ 0 :=
513 ne_of_gt (lt_of_le_of_lt (Nat.zero_le _) hℓlt)
514 have hℓ_mem_support : ℓ ∈ (orderOf g).factorization.support :=
515 Finsupp.mem_support_iff.mpr hℓ_fac_ne
516 have hℓ_mem_primeFactors : ℓ ∈ (orderOf g).primeFactors := by
517 simpa [Nat.support_factorization] using hℓ_mem_support
518 have hℓprime : Nat.Prime ℓ :=
519 Nat.prime_of_mem_primeFactors hℓ_mem_primeFactors
520 have hℓdiv_order : ℓ ∣ orderOf g :=
521 Nat.dvd_of_factorization_pos hℓ_fac_ne
522 have hℓsigma : ℓ ∈ sigma := by
523 by_contra hℓnot
524 exact hG.2 ℓ hℓprime hℓnot
525 (hℓdiv_order.trans (orderOf_dvd_natCard g))
526 let σ : ℕ := padicValNat ℓ (orderOf g)
527 have hltpadic : padicValNat ℓ n.natAbs < σ := by
528 simpa [σ, Nat.factorization_def _ hℓprime] using hℓlt
529 have hσpos : 0 < σ := lt_of_le_of_lt (Nat.zero_le _) hltpadic
530 have hσdvd : ℓ ^ σ ∣ orderOf g := by
531 simpa [σ] using (pow_padicValNat_dvd (p := ℓ) (n := orderOf g))
532 exact ⟨ℓ, σ, hℓprime, hσpos, hℓsigma, hltpadic, hσdvd⟩
534end
536/-- Finite abelian groups are closed under subgroups. -/
537theorem abelian_subgroupClosed : SubgroupClosed abelian := by
538 intro G _ H hG
539 rcases hG with ⟨hfin, hcomm⟩
540 refine ⟨Finite.of_injective ((↑) : H → G) Subtype.coe_injective, ?_⟩
541 letI : CommGroup G := { toGroup := inferInstance, mul_comm := hcomm }
542 intro a b
543 exact mul_comm a b
545/-- Finite abelian groups are closed under quotients. -/
546theorem abelian_quotientClosed : QuotientClosed abelian := by
547 intro G _ N _ hG
548 rcases hG with ⟨hfin, hcomm⟩
549 refine ⟨?_, ?_⟩
550 · letI : Finite G := hfin
551 infer_instance
552 · letI : CommGroup G := { toGroup := inferInstance, mul_comm := hcomm }
553 intro a b
554 exact mul_comm a b
556/-- Finite abelian groups are closed under finite direct products. -/
557theorem abelian_finiteProductClosed : FiniteProductClosed abelian := by
558 intro ι _ G _ hG
559 change Finite ((i : ι) → G i) ∧ ∀ a b : ((i : ι) → G i), a * b = b * a
560 constructor
561 · letI : ∀ i, Finite (G i) := fun i => (hG i).1
562 infer_instance
563 · intro a b
564 funext i
565 exact (hG i).2 (a i) (b i)
567/-- Finite abelian groups form a variety. -/
568theorem abelian_variety : Variety abelian := by
569 refine ⟨abelian_subgroupClosed, abelian_quotientClosed,
570 abelian_finiteProductClosed⟩
572/-- Finite abelian groups are closed under isomorphism. -/
573theorem abelian_isomClosed : IsomClosed abelian := by
574 intro G H _ _ hGH hG
575 rcases hGH with ⟨e⟩
576 rcases hG with ⟨hfin, hcomm⟩
577 refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
578 intro a b
579 have h := hcomm (e.symm a) (e.symm b)
580 simpa using congrArg e h
582/-- Finite abelian groups form a formation. -/
583theorem abelian_formation : Formation abelian :=
584 variety_formation abelian_variety abelian_isomClosed
586/-- Subgroups of finite abelian groups of bounded exponent again have bounded exponent. -/
587theorem abelianExponent_subgroupClosed (n : ℕ) : SubgroupClosed (abelianExponent n) := by
588 intro G _ H hG
589 rcases hG with ⟨hfin, hcomm, hexp⟩
590 refine ⟨Finite.of_injective ((↑) : H → G) Subtype.coe_injective, ?_, ?_⟩
591 · intro a b
592 ext
593 exact hcomm a.1 b.1
594 · intro g
595 ext
596 exact hexp g.1
598/-- Quotients of finite abelian groups of bounded exponent again have bounded exponent. -/
599theorem abelianExponent_quotientClosed (n : ℕ) : QuotientClosed (abelianExponent n) := by
600 intro G _ N _ hG
601 rcases hG with ⟨hfin, hcomm, hexp⟩
602 refine ⟨?_, ?_, ?_⟩
603 · letI : Finite G := hfin
604 infer_instance
605 · letI : CommGroup G := { toGroup := inferInstance, mul_comm := hcomm }
606 intro a b
607 exact mul_comm a b
608 · intro g
609 refine Quotient.inductionOn' g ?_
610 intro x
611 change QuotientGroup.mk' N (x ^ n) = 1
612 rw [hexp x]
613 rfl
615/-- Finite products of finite abelian groups of bounded exponent again have bounded exponent. -/
616theorem abelianExponent_finiteProductClosed (n : ℕ) :
617 FiniteProductClosed (abelianExponent n) := by
618 intro ι _ G _ hG
619 refine ⟨?_, ?_, ?_⟩
620 · letI : ∀ i, Finite (G i) := fun i => (hG i).1
621 infer_instance
622 · intro a b
623 funext i
624 exact (hG i).2.1 (a i) (b i)
625 · intro g
626 funext i
627 exact (hG i).2.2 (g i)
629/-- abelianExponent is a finite-group variety. -/
630theorem abelianExponent_variety (n : ℕ) : Variety (abelianExponent n) := by
631 refine ⟨abelianExponent_subgroupClosed n,
632 abelianExponent_quotientClosed n, abelianExponent_finiteProductClosed n⟩
634/-- Finite abelian groups of exponent dividing \(n\) are closed under isomorphism. -/
635theorem abelianExponent_isomClosed (n : ℕ) : IsomClosed (abelianExponent n) := by
636 intro G H _ _ hGH hG
637 rcases hGH with ⟨e⟩
638 rcases hG with ⟨hfin, hcomm, hexp⟩
639 refine ⟨Finite.of_equiv G e.toEquiv, ?_, ?_⟩
640 · intro a b
641 have h := hcomm (e.symm a) (e.symm b)
642 simpa using congrArg e h
643 · intro a
644 have h := hexp (e.symm a)
645 simpa using congrArg e h
647/-- Finite abelian groups of exponent dividing \(n\) form a formation. -/
648theorem abelianExponent_formation (n : ℕ) : Formation (abelianExponent n) :=
649 variety_formation (abelianExponent_variety n) (abelianExponent_isomClosed n)
651/-- Finite cyclic groups are closed under isomorphism. -/
652theorem cyclic_isomClosed : IsomClosed cyclic := by
653 intro G H _ _ hGH hG
654 rcases hGH with ⟨e⟩
655 rcases hG with ⟨hfin, hcyc⟩
656 refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
657 letI : IsCyclic G := hcyc
658 exact isCyclic_of_surjective e e.surjective
660/-- Finite cyclic groups are closed under quotients. -/
661theorem cyclic_quotientClosed : QuotientClosed cyclic := by
662 intro G _ N _ hG
663 rcases hG with ⟨hfin, hcyc⟩
664 refine ⟨?_, ?_⟩
665 · letI : Finite G := hfin
666 infer_instance
667 · letI : IsCyclic G := hcyc
668 exact isCyclic_of_surjective (QuotientGroup.mk' N) (QuotientGroup.mk'_surjective N)
670/-- Finite solvable groups are closed under isomorphism. -/
671theorem solvable_isomClosed : IsomClosed solvable := by
672 intro G H _ _ hGH hG
673 rcases hGH with ⟨e⟩
674 rcases hG with ⟨hfin, hsolv⟩
675 refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
676 letI : IsSolvable G := hsolv
677 exact solvable_of_surjective (f := e.toMonoidHom) e.surjective
679/-- Finite solvable groups are closed under quotients. -/
680theorem solvable_quotientClosed : QuotientClosed solvable := by
681 intro G _ N _ hG
682 rcases hG with ⟨hfin, hsolv⟩
683 refine ⟨?_, ?_⟩
684 · letI : Finite G := hfin
685 infer_instance
686 · letI : IsSolvable G := hsolv
687 infer_instance
689/-- Finite nilpotent groups are closed under isomorphism. -/
690theorem nilpotent_isomClosed : IsomClosed nilpotent := by
691 intro G H _ _ hGH hG
692 rcases hGH with ⟨e⟩
693 rcases hG with ⟨hfin, hnil⟩
694 refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
695 letI : Group.IsNilpotent G := hnil
696 exact Group.nilpotent_of_mulEquiv e
698/-- Finite nilpotent groups are closed under quotients. -/
699theorem nilpotent_quotientClosed : QuotientClosed nilpotent := by
700 intro G _ N _ hG
701 rcases hG with ⟨hfin, hnil⟩
702 refine ⟨?_, ?_⟩
703 · letI : Finite G := hfin
704 infer_instance
705 · letI : Group.IsNilpotent G := hnil
706 infer_instance
708/-- Every finite cyclic group is finite nilpotent. -/
709theorem cyclic_to_nilpotent {G : Type u} [Group G] :
710 cyclic G → nilpotent G := by
711 rintro ⟨hfin, hcyc⟩
712 refine ⟨hfin, ?_⟩
713 letI : IsCyclic G := hcyc
714 letI : CommGroup G := IsCyclic.commGroup
715 infer_instance
717/-- Every finite cyclic group belongs to the finite solvable class. -/
718theorem cyclic_to_solvable {G : Type u} [Group G] :
719 cyclic G → solvable G := by
720 rintro ⟨hfin, hcyc⟩
721 refine ⟨hfin, ?_⟩
722 letI : IsCyclic G := hcyc
723 letI : CommGroup G := IsCyclic.commGroup
724 infer_instance
726/-- Every finite \(p\)-group belongs to the finite nilpotent class. -/
727theorem pGroup_to_nilpotent {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] :
728 pGroup p G → nilpotent G := by
729 rintro ⟨hfin, hpG⟩
730 letI : Finite G := hfin
731 exact ⟨hfin, hpG.isNilpotent⟩
733/-- Every finite \(p\)-group belongs to the finite solvable class. -/
734theorem pGroup_to_solvable {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] :
735 pGroup p G → solvable G := by
736 rintro ⟨hfin, hpG⟩
737 refine ⟨hfin, ?_⟩
738 letI : Group.IsNilpotent G := hpG.isNilpotent
739 infer_instance
741end FiniteGroupClass
743end ProCGroups