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