ProCGroups.FiniteGroups.StandardClasses
This module studies standard classes for pro cgroups. If \(a \nmid b\), then some prime factor has a larger exponent in \(a\) than in \(b\). The p-adic exponent of a positive integer is at most the integer itself.
import
- Mathlib.GroupTheory.Nilpotent
- Mathlib.NumberTheory.Padics.PadicVal.Basic
- ProCGroups.FiniteGroups.AllFinite
theorem exists_factorization_lt_of_not_dvd
{a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (hndvd : ¬ a ∣ b) :
∃ p, b.factorization p < a.factorization pIf \(a \nmid b\), then some prime factor has a larger exponent in \(a\) than in \(b\).
Show proof
by
by_contra h
push_neg at h
have hle : a.factorization ≤ b.factorization := by
intro p
exact h p
exact hndvd ((Nat.factorization_le_iff_dvd ha hb).1 hle)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem nat_factorization_le_self_of_prime
{A p : ℕ} (hp : Nat.Prime p) :
A.factorization p ≤ AThe p-adic exponent of a positive integer is at most the integer itself.
Show proof
Nat.factorization_le_of_le_pow (le_of_lt (Nat.lt_pow_self (n := A) (a := p) hp.one_lt))Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem gcd_mul_dvd_pow_depth
{K d A : ℕ} (hK : 0 < K) (hd : 0 < d) (hA : 0 < A) :
Nat.gcd (d * A) (K * (K * d) ^ (A + 1)) ∣ (K * d) ^ (A + 1)The depth \((K*d)^(A+1)\) is large enough for the GCD-conditioned cyclic reduction.
Show proof
by
let B : ℕ := K * d
let M : ℕ := B ^ (A + 1)
have hB : 0 < B := Nat.mul_pos hK hd
have hM : 0 < M := pow_pos hB (A + 1)
have hleft_ne : d * A ≠ 0 := Nat.ne_of_gt (Nat.mul_pos hd hA)
have hright_ne : K * M ≠ 0 := Nat.ne_of_gt (Nat.mul_pos hK hM)
have hgcd_ne : Nat.gcd (d * A) (K * M) ≠ 0 :=
Nat.ne_of_gt (Nat.gcd_pos_of_pos_left (K * M) (Nat.mul_pos hd hA))
rw [← Nat.factorization_le_iff_dvd hgcd_ne (Nat.ne_of_gt hM)]
intro p
by_cases hp : Nat.Prime p
· by_cases hpB : p ∣ B
· have hdvdB : d ∣ B := by
exact Nat.dvd_mul_left d K
have hdfacB : d.factorization p ≤ B.factorization p :=
(Nat.factorization_le_iff_dvd (Nat.ne_of_gt hd) (Nat.ne_of_gt hB)).2 hdvdB p
have hAfacle : A.factorization p ≤ A :=
nat_factorization_le_self_of_prime hp
have hBfacpos : 0 < B.factorization p := by
exact lt_of_lt_of_le Nat.zero_lt_one
((hp.dvd_iff_one_le_factorization (Nat.ne_of_gt hB)).1 hpB)
have hleft_fac_le :
(d * A).factorization p ≤ M.factorization p := by
calc
(d * A).factorization p
= d.factorization p + A.factorization p := by
rw [Nat.factorization_mul (Nat.ne_of_gt hd) (Nat.ne_of_gt hA)]
rfl
_ ≤ B.factorization p + A := Nat.add_le_add hdfacB hAfacle
_ ≤ B.factorization p + A * B.factorization p := by
exact Nat.add_le_add_left
(Nat.le_mul_of_pos_right A hBfacpos) (B.factorization p)
_ = (A + 1) * B.factorization p := by
rw [Nat.add_mul, one_mul, add_comm]
_ = M.factorization p := by
simp only [Nat.factorization_pow, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, M]
have hgcd_fac :
(Nat.gcd (d * A) (K * M)).factorization p =
min ((d * A).factorization p) ((K * M).factorization p) := by
rw [Nat.factorization_gcd hleft_ne hright_ne]
rfl
rw [hgcd_fac]
exact (min_le_left _ _).trans hleft_fac_le
· have hnotK : ¬ p ∣ K := by
intro hpK
exact hpB (dvd_mul_of_dvd_left hpK d)
have hnotM : ¬ p ∣ M := by
intro hpM
exact hpB (hp.dvd_of_dvd_pow hpM)
have hnotKM : ¬ p ∣ K * M := by
exact hp.not_dvd_mul hnotK hnotM
have hright_fac : (K * M).factorization p = 0 :=
Nat.factorization_eq_zero_of_not_dvd hnotKM
have hgcd_fac :
(Nat.gcd (d * A) (K * M)).factorization p =
min ((d * A).factorization p) ((K * M).factorization p) := by
rw [Nat.factorization_gcd hleft_ne hright_ne]
rfl
rw [hgcd_fac, hright_fac]
simp only [zero_le, inf_of_le_right]
· simp only [Nat.factorization_eq_zero_of_not_prime _ hp, le_refl]Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□def cyclic : FiniteGroupClass.{u} where
pred := fun G [_] => Finite G ∧ IsCyclic G
finite_of_mem := fun hG => hG.1The class of finite cyclic groups.
def abelian : FiniteGroupClass.{u} where
pred := fun G [_] => Finite G ∧ ∀ a b : G, a * b = b * a
finite_of_mem := fun hG => hG.1The class of finite abelian groups.
def solvable : FiniteGroupClass.{u} where
pred := fun G [_] => Finite G ∧ IsSolvable G
finite_of_mem := fun hG => hG.1The class of finite solvable groups.
def nilpotent : FiniteGroupClass.{u} where
pred := fun G [_] => Finite G ∧ Group.IsNilpotent G
finite_of_mem := fun hG => hG.1The finite group class consisting of finite nilpotent groups.
def pGroup (p : ℕ) : FiniteGroupClass.{u} where
pred := fun G [_] => Finite G ∧ IsPGroup p G
finite_of_mem := fun hG => hG.1The class of finite \(p\)-groups.
theorem of_dvd {sigma : Set ℕ} {m n : ℕ} (hn : IsSigmaNumber sigma n) (hmn : m ∣ n) :
IsSigmaNumber sigma mEvery divisor of a \(\Sigma\)-number is again a \(\Sigma\)-number.
Show proof
by
intro p hp hpsigma hpm
exact hn p hp hpsigma (dvd_trans hpm hmn)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem mul {sigma : Set ℕ} {m n : ℕ} (hm : IsSigmaNumber sigma m)
(hn : IsSigmaNumber sigma n) :
IsSigmaNumber sigma (m * n)The product of two \(\Sigma\)-numbers is a \(\Sigma\)-number.
Show proof
by
intro p hp hpsigma hpmn
exact (hp.not_dvd_mul (hm p hp hpsigma) (hn p hp hpsigma)) hpmnProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem prod {sigma : Set ℕ} {ι : Type*} (s : Finset ι) (f : ι → ℕ)
(hf : ∀ i ∈ s, IsSigmaNumber sigma (f i)) :
IsSigmaNumber sigma (s.prod f)A finite product of \(\Sigma\)-numbers is a \(\Sigma\)-number.
Show proof
by
classical
induction s using Finset.induction with
| empty =>
intro p hp _ hpdvd
exact hp.ne_one (Nat.dvd_one.mp hpdvd)
| insert a s ha hs =>
have hfa : IsSigmaNumber sigma (f a) := hf a (Finset.mem_insert_self a s)
have hfs : ∀ i ∈ s, IsSigmaNumber sigma (f i) :=
fun i hi => hf i (Finset.mem_insert_of_mem hi)
simpa [Finset.prod_insert ha] using mul (sigma := sigma) hfa (hs hfs)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem pow {sigma : Set ℕ} {n k : ℕ} (hn : IsSigmaNumber sigma n) :
IsSigmaNumber sigma (n ^ k)A natural-number power of a \(\Sigma\)-number is a \(\Sigma\)-number.
Show proof
by
induction k with
| zero =>
intro p hp _ hpdvd
exact hp.ne_one (Nat.dvd_one.mp hpdvd)
| succ k ih =>
rw [pow_succ]
exact mul ih hnProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem prime_pow_of_mem {sigma : Set ℕ} {p k : ℕ}
(hpsigma : p ∈ sigma) (hp : Nat.Prime p) :
IsSigmaNumber sigma (p ^ k)A prime power whose prime lies in \(\Sigma\) is a \(\Sigma\)-number.
Show proof
by
intro q hq hqsigma hqdiv
by_cases hk : k = 0
· simp only [hk, pow_zero, Nat.dvd_one] at hqdiv
exact hq.ne_one hqdiv
· have hq_dvd_p : q ∣ p := hq.dvd_of_dvd_pow hqdiv
have hp_eq_q : p = q := (hp.dvd_iff_eq hq.ne_one).1 hq_dvd_p
exact hqsigma (hp_eq_q ▸ hpsigma)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□def sigmaGroup (sigma : Set ℕ) : FiniteGroupClass.{u} where
pred := fun G [_] => Finite G ∧ IsSigmaNumber sigma (Nat.card G)
finite_of_mem := fun hG => hG.1theorem isPGroup_pi {ι : Type u} [Finite ι] {G : ι → Type v}
[∀ i, Group (G i)] (hG : ∀ i, IsPGroup p (G i)) :
IsPGroup p ((i : ι) → G i)Finite products of abstract \(p\)-groups are \(p\)-groups.
Show proof
by
classical
letI := Fintype.ofFinite ι
intro g
choose k hk using fun i => hG i (g i)
let N : ℕ := Finset.univ.sup k
refine ⟨N, ?_⟩
funext i
have hki : k i ≤ N := Finset.le_sup (Finset.mem_univ i)
calc
(g ^ p ^ N) i = (g i) ^ (p ^ N) := by simp only [Pi.pow_apply]
_ = (g i) ^ (p ^ (k i) * p ^ (N - k i)) := by
rw [← Nat.pow_add, Nat.add_sub_of_le hki]
_ = ((g i) ^ (p ^ k i)) ^ (p ^ (N - k i)) := by
rw [pow_mul]
_ = 1 := by simp only [hk i, one_pow]Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem pGroup_formation (p : ℕ) :
FiniteGroupClass.Formation (FiniteGroupClass.pGroup p)The class of finite \(p\)-groups is a formation.
Show proof
by
refine ⟨?_, ?_⟩
· intro G _ N _ hG
rcases hG with ⟨hfin, hpG⟩
refine ⟨?_, hpG.to_quotient N⟩
letI : Finite G := hfin
infer_instance
· intro ι _ G _ H _ f hf _hsurj hH
letI : ∀ i, Finite (H i) := fun i => (hH i).1
have hPi : IsPGroup p ((i : ι) → H i) := isPGroup_pi (p := p) fun i => (hH i).2
exact ⟨Finite.of_injective f hf, hPi.of_injective f hf⟩Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□instance pGroup_containsTrivialQuotients (p : ℕ) :
ContainsTrivialQuotients (pGroup p : FiniteGroupClass.{u}) :=
(pGroup_formation p).containsTrivialQuotientsFinite \(p\)-groups contain the trivial quotients.
theorem pGroup_subgroupClosed (p : ℕ) : SubgroupClosed (pGroup p)Show proof
by
intro G _ H hG
rcases hG with ⟨hfin, hpG⟩
exact ⟨Finite.of_injective ((↑) : H → G) Subtype.coe_injective, hpG.to_subgroup H⟩Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem finite_of_finite_normalSubgroup_and_quotient
{E : Type u} [Group E] (N : Subgroup E) [N.Normal]
[Finite N] [Finite (E ⧸ N)] :
Finite EA group is finite when a normal subgroup and the corresponding quotient are finite.
Show proof
by
classical
let s : E ⧸ N → E := Quotient.out
let f : N × (E ⧸ N) → E := fun z => z.1.1 * s z.2
have hsurj : Function.Surjective f := by
intro e
let q : E ⧸ N := QuotientGroup.mk' N e
have hsq : QuotientGroup.mk' N (s q) = q := Quotient.out_eq' q
have hmem : e * (s q)⁻¹ ∈ N := by
apply (QuotientGroup.eq_one_iff (N := N) (e * (s q)⁻¹)).1
change QuotientGroup.mk' N e * (QuotientGroup.mk' N (s q))⁻¹ = 1
rw [hsq]
simp only [QuotientGroup.mk'_apply, mul_inv_cancel, q]
refine ⟨(⟨e * (s q)⁻¹, hmem⟩, q), ?_⟩
simp only [QuotientGroup.mk'_apply, mul_assoc, inv_mul_cancel, mul_one, f, q]
exact Finite.of_surjective f hsurjProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem pGroup_extensionClosed (p : ℕ) :
ExtensionClosed (pGroup p)Show proof
by
intro E _ N _ hN hQ
rcases hN with ⟨hNfin, hpN⟩
rcases hQ with ⟨hQfin, hpQ⟩
letI : Finite N := hNfin
letI : Finite (E ⧸ N) := hQfin
have hEfin : Finite E := finite_of_finite_normalSubgroup_and_quotient (N := N)
letI : Finite E := hEfin
have hker :
IsPGroup p ((QuotientGroup.mk' N).ker : Subgroup E) := by
exact hpN.of_equiv (MulEquiv.subgroupCongr (QuotientGroup.ker_mk' N).symm)
have hTopQ : IsPGroup p (⊤ : Subgroup (E ⧸ N)) := hpQ.to_subgroup ⊤
have hTopE :
IsPGroup p ((⊤ : Subgroup (E ⧸ N)).comap (QuotientGroup.mk' N)) :=
hTopQ.comap_of_ker_isPGroup (QuotientGroup.mk' N) hker
have hTop' : IsPGroup p (⊤ : Subgroup E) := by
simpa using hTopE
have hEp : IsPGroup p E :=
hTop'.of_surjective (⊤ : Subgroup E).subtype <| by
intro x
exact ⟨⟨x, by simp only [Subgroup.mem_top]⟩, rfl⟩
exact ⟨hEfin, hEp⟩Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem pGroup_hereditary (p : ℕ) : Hereditary (pGroup p)The class of finite \(p\)-groups is hereditary under subgroups.
Show proof
Hereditary.of_subgroupClosed_isomClosed
(pGroup_subgroupClosed p)
(pGroup_formation p).isomClosedProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem sigmaGroup_isomClosed (sigma : Set ℕ) : IsomClosed (sigmaGroup sigma)The class of finite \(\Sigma\)-groups is closed under isomorphism.
Show proof
by
intro G H _ _ hGH hG
rcases hGH with ⟨e⟩
rcases hG with ⟨hfin, hsigma⟩
refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
simpa [Nat.card_congr e.toEquiv] using hsigmaProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem sigmaGroup_subgroupClosed (sigma : Set ℕ) : SubgroupClosed (sigmaGroup sigma)Show proof
by
intro G _ H hG
rcases hG with ⟨hfin, hsigma⟩
refine ⟨Finite.of_injective ((↑) : H → G) Subtype.coe_injective, ?_⟩
exact IsSigmaNumber.of_dvd (sigma := sigma) hsigma (Subgroup.card_subgroup_dvd_card H)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem sigmaGroup_quotientClosed (sigma : Set ℕ) : QuotientClosed (sigmaGroup sigma)Show proof
by
intro G _ N _ hG
rcases hG with ⟨hfin, hsigma⟩
refine ⟨?_, ?_⟩
· letI : Finite G := hfin
infer_instance
· exact IsSigmaNumber.of_dvd (sigma := sigma) hsigma (Subgroup.card_quotient_dvd_card N)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem sigmaGroup_finiteProductClosed (sigma : Set ℕ) : FiniteProductClosed (sigmaGroup sigma)Show proof
by
intro ι _ A _ hA
refine ⟨?_, ?_⟩
· letI : ∀ i, Finite (A i) := fun i => (hA i).1
infer_instance
· simpa [Nat.card_pi] using
IsSigmaNumber.prod (sigma := sigma) Finset.univ (fun i => Nat.card (A i))
(fun i _ => (hA i).2)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem sigmaGroup_variety (sigma : Set ℕ) : Variety (sigmaGroup sigma)sigmaGroup is a finite-group variety.
Show proof
by
refine ⟨sigmaGroup_subgroupClosed sigma, sigmaGroup_quotientClosed sigma,
sigmaGroup_finiteProductClosed sigma⟩Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem sigmaGroup_formation (sigma : Set ℕ) : Formation (sigmaGroup sigma)Show proof
variety_formation (sigmaGroup_variety sigma) (sigmaGroup_isomClosed sigma)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem sigmaGroup_extensionClosed (sigma : Set ℕ) :
ExtensionClosed (sigmaGroup sigma)Show proof
by
intro E _ N _ hN hQ
rcases hN with ⟨hNfin, hsigmaN⟩
rcases hQ with ⟨hQfin, hsigmaQ⟩
letI : Finite N := hNfin
letI : Finite (E ⧸ N) := hQfin
have hEfin : Finite E := finite_of_finite_normalSubgroup_and_quotient (N := N)
letI : Finite E := hEfin
refine ⟨hEfin, ?_⟩
have hcard :
Nat.card E = Nat.card (E ⧸ N) * Nat.card N := by
exact Subgroup.card_eq_card_quotient_mul_card_subgroup (α := E) N
rw [hcard]
exact IsSigmaNumber.mul hsigmaQ hsigmaNProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem sigmaGroup_melnikovFormation (sigma : Set ℕ) :
MelnikovFormation (sigmaGroup sigma) where
formationFinite \(\Sigma\)-groups form a Melnikov formation.
Show proof
sigmaGroup_formation sigma
normalSubgroupClosed := fun N _ hG => sigmaGroup_subgroupClosed sigma N hG
extensionClosed := sigmaGroup_extensionClosed sigmaProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem sigmaGroup_fullFormation (sigma : Set ℕ) :
FullFormation (sigmaGroup sigma) where
melnikovFormationFinite \(\Sigma\)-groups form a full formation.
Show proof
sigmaGroup_melnikovFormation sigma
subgroupClosed := sigmaGroup_subgroupClosed sigmaProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem sigmaGroup_cyclicZMod
{sigma : Set ℕ} {n : ℕ} (hn : 0 < n)
(hsigma : IsSigmaNumber sigma n) :
sigmaGroup sigma (ULift.{u} (Multiplicative (ZMod n)))Show proof
by
letI : NeZero n := ⟨Nat.ne_of_gt hn⟩
let A := ULift.{u} (Multiplicative (ZMod n))
let e : A ≃* Multiplicative (ZMod n) := MulEquiv.ulift
letI : Finite A := Finite.of_equiv (Multiplicative (ZMod n)) e.symm.toEquiv
refine ⟨inferInstance, ?_⟩
have hcard : Nat.card A = n := by
calc
Nat.card A = Nat.card (Multiplicative (ZMod n)) := Nat.card_congr e.toEquiv
_ = n := by simp only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, ZMod.card]
simpa [hcard] using hsigmaProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem sigmaGroup_nontrivialCyclic
{sigma : Set ℕ} (hsigma : ∃ p, p ∈ sigma ∧ Nat.Prime p) :
∃ (A : Type u) (_ : Group A) (_ : Finite A),
sigmaGroup sigma A ∧ IsCyclic A ∧ Nontrivial AShow proof
by
rcases hsigma with ⟨p, hpsigma, hp⟩
letI : Fact (1 < p) := ⟨hp.one_lt⟩
let A := ULift.{u} (Multiplicative (ZMod p))
let e : A ≃* Multiplicative (ZMod p) := MulEquiv.ulift
letI : Finite A := Finite.of_equiv (Multiplicative (ZMod p)) e.symm.toEquiv
have hcyc : IsCyclic A :=
isCyclic_of_surjective e.symm.toMonoidHom e.symm.surjective
have hnon : Nontrivial A := e.toEquiv.nontrivial
refine ⟨A, inferInstance, inferInstance, ?_, hcyc, hnon⟩
exact sigmaGroup_cyclicZMod (sigma := sigma) hp.pos <| by
simpa using
(IsSigmaNumber.prime_pow_of_mem (sigma := sigma) (p := p) (k := 1) hpsigma hp)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem sigmaGroup_prod_multiplicativeZMod
{sigma : Set ℕ} {Q : Type u} [Group Q]
(hQ : sigmaGroup sigma Q)
{N : ℕ} (hNpos : 0 < N)
(hNsigma : IsSigmaNumber sigma N) :
sigmaGroup sigma (Q × Multiplicative (ZMod N))Show proof
by
rcases hQ with ⟨hQfin, hQsigma⟩
letI : Finite Q := hQfin
letI : NeZero N := ⟨Nat.ne_of_gt hNpos⟩
letI : Finite (Multiplicative (ZMod N)) :=
@Finite.of_equiv _ _ (show Finite (ZMod N) by infer_instance) Multiplicative.toAdd
refine ⟨inferInstance, ?_⟩
have hcard : Nat.card (Multiplicative (ZMod N)) = N := by
simp only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, ZMod.card]
rw [Nat.card_prod, hcard]
exact IsSigmaNumber.mul hQsigma hNsigmaProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem exists_prime_power_orderOf_gt_padicValNat_of_zpow_ne_one
{sigma : Set ℕ} {G : Type u} [Group G] [Finite G]
(hG : sigmaGroup sigma G) {g : G} {n : ℤ} (hgn : g ^ n ≠ 1) :
∃ ℓ σ : ℕ,
Nat.Prime ℓ ∧ 0 < σ ∧ ℓ ∈ sigma ∧
padicValNat ℓ n.natAbs < σ ∧ ℓ ^ σ ∣ orderOf gA nontrivial finite \(\Sigma\)-group power supplies a coefficient prime and depth.
Show proof
by
have hnZ : g ^ ((n.natAbs : ℕ) : ℤ) ≠ 1 := by
intro h
apply hgn
rcases Int.natAbs_eq n with hn | hn
· rw [hn]
simpa using h
· rw [hn]
have hinv : (g ^ ((n.natAbs : ℕ) : ℤ))⁻¹ = (1 : G) := by
rw [h, inv_one]
simpa [zpow_neg] using hinv
have hnat : g ^ n.natAbs ≠ 1 := by
intro hpow
exact hnZ (by simpa using hpow)
have hgfin : IsOfFinOrder g := isOfFinOrder_of_finite g
have horder_pos : 0 < orderOf g := (orderOf_pos_iff).2 hgfin
have horder_ne : orderOf g ≠ 0 := Nat.ne_of_gt horder_pos
have hnabs_ne : n.natAbs ≠ 0 := by
intro hnabs
apply hnat
simp only [hnabs, pow_zero]
have hnotdvd : ¬ orderOf g ∣ n.natAbs := by
intro hdiv
exact hnat ((orderOf_dvd_iff_pow_eq_one (x := g) (n := n.natAbs)).1 hdiv)
rcases exists_factorization_lt_of_not_dvd horder_ne hnabs_ne hnotdvd with
⟨ℓ, hℓlt⟩
have hℓ_fac_ne : (orderOf g).factorization ℓ ≠ 0 :=
ne_of_gt (lt_of_le_of_lt (Nat.zero_le _) hℓlt)
have hℓ_mem_support : ℓ ∈ (orderOf g).factorization.support :=
Finsupp.mem_support_iff.mpr hℓ_fac_ne
have hℓ_mem_primeFactors : ℓ ∈ (orderOf g).primeFactors := by
simpa [Nat.support_factorization] using hℓ_mem_support
have hℓprime : Nat.Prime ℓ :=
Nat.prime_of_mem_primeFactors hℓ_mem_primeFactors
have hℓdiv_order : ℓ ∣ orderOf g :=
Nat.dvd_of_factorization_pos hℓ_fac_ne
have hℓsigma : ℓ ∈ sigma := by
by_contra hℓnot
exact hG.2 ℓ hℓprime hℓnot
(hℓdiv_order.trans (orderOf_dvd_natCard g))
let σ : ℕ := padicValNat ℓ (orderOf g)
have hltpadic : padicValNat ℓ n.natAbs < σ := by
simpa [σ, Nat.factorization_def _ hℓprime] using hℓlt
have hσpos : 0 < σ := lt_of_le_of_lt (Nat.zero_le _) hltpadic
have hσdvd : ℓ ^ σ ∣ orderOf g := by
simpa [σ] using (pow_padicValNat_dvd (p := ℓ) (n := orderOf g))
exact ⟨ℓ, σ, hℓprime, hσpos, hℓsigma, hltpadic, hσdvd⟩Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem abelian_subgroupClosed : SubgroupClosed abelianFinite abelian groups are closed under subgroups.
Show proof
by
intro G _ H hG
rcases hG with ⟨hfin, hcomm⟩
refine ⟨Finite.of_injective ((↑) : H → G) Subtype.coe_injective, ?_⟩
letI : CommGroup G := { toGroup := inferInstance, mul_comm := hcomm }
intro a b
exact mul_comm a bProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem abelian_quotientClosed : QuotientClosed abelianFinite abelian groups are closed under quotients.
Show proof
by
intro G _ N _ hG
rcases hG with ⟨hfin, hcomm⟩
refine ⟨?_, ?_⟩
· letI : Finite G := hfin
infer_instance
· letI : CommGroup G := { toGroup := inferInstance, mul_comm := hcomm }
intro a b
exact mul_comm a bProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem abelian_finiteProductClosed : FiniteProductClosed abelianShow proof
by
intro ι _ G _ hG
change Finite ((i : ι) → G i) ∧ ∀ a b : ((i : ι) → G i), a * b = b * a
constructor
· change Finite ((i : ι) → G i)
letI : ∀ i, Finite (G i) := fun i => (hG i).1
infer_instance
· intro a b
funext i
exact (hG i).2 (a i) (b i)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□Show proof
by
refine ⟨abelian_subgroupClosed, abelian_quotientClosed,
abelian_finiteProductClosed⟩Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem abelian_isomClosed : IsomClosed abelianFinite abelian groups are closed under isomorphism.
Show proof
by
intro G H _ _ hGH hG
rcases hGH with ⟨e⟩
rcases hG with ⟨hfin, hcomm⟩
refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
intro a b
have h := hcomm (e.symm a) (e.symm b)
simpa using congrArg e hProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□Show proof
variety_formation abelian_variety abelian_isomClosedProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem abelianExponent_subgroupClosed (n : ℕ) : SubgroupClosed (abelianExponent n)Show proof
by
intro G _ H hG
rcases hG with ⟨hfin, hcomm, hexp⟩
refine ⟨Finite.of_injective ((↑) : H → G) Subtype.coe_injective, ?_, ?_⟩
· intro a b
ext
exact hcomm a.1 b.1
· intro g
ext
exact hexp g.1Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem abelianExponent_quotientClosed (n : ℕ) : QuotientClosed (abelianExponent n)Show proof
by
intro G _ N _ hG
rcases hG with ⟨hfin, hcomm, hexp⟩
refine ⟨?_, ?_, ?_⟩
· letI : Finite G := hfin
infer_instance
· letI : CommGroup G := { toGroup := inferInstance, mul_comm := hcomm }
intro a b
exact mul_comm a b
· intro g
refine Quotient.inductionOn' g ?_
intro x
change QuotientGroup.mk' N (x ^ n) = 1
rw [hexp x]
rflProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem abelianExponent_finiteProductClosed (n : ℕ) :
FiniteProductClosed (abelianExponent n)Show proof
by
intro ι _ G _ hG
refine ⟨?_, ?_, ?_⟩
· letI : ∀ i, Finite (G i) := fun i => (hG i).1
infer_instance
· intro a b
funext i
exact (hG i).2.1 (a i) (b i)
· intro g
funext i
exact (hG i).2.2 (g i)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem abelianExponent_variety (n : ℕ) : Variety (abelianExponent n)abelianExponent is a finite-group variety.
Show proof
by
refine ⟨abelianExponent_subgroupClosed n,
abelianExponent_quotientClosed n, abelianExponent_finiteProductClosed n⟩Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem abelianExponent_isomClosed (n : ℕ) : IsomClosed (abelianExponent n)Finite abelian groups of exponent dividing \(n\) are closed under isomorphism.
Show proof
by
intro G H _ _ hGH hG
rcases hGH with ⟨e⟩
rcases hG with ⟨hfin, hcomm, hexp⟩
refine ⟨Finite.of_equiv G e.toEquiv, ?_, ?_⟩
· intro a b
have h := hcomm (e.symm a) (e.symm b)
simpa using congrArg e h
· intro a
have h := hexp (e.symm a)
simpa using congrArg e hProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem abelianExponent_formation (n : ℕ) : Formation (abelianExponent n)Finite abelian groups of exponent dividing \(n\) form a formation.
Show proof
variety_formation (abelianExponent_variety n) (abelianExponent_isomClosed n)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem cyclic_isomClosed : IsomClosed cyclicFinite cyclic groups are closed under isomorphism.
Show proof
by
intro G H _ _ hGH hG
rcases hGH with ⟨e⟩
rcases hG with ⟨hfin, hcyc⟩
refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
letI : IsCyclic G := hcyc
exact isCyclic_of_surjective e e.surjectiveProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem cyclic_quotientClosed : QuotientClosed cyclicFinite cyclic groups are closed under quotients.
Show proof
by
intro G _ N _ hG
rcases hG with ⟨hfin, hcyc⟩
refine ⟨?_, ?_⟩
· letI : Finite G := hfin
infer_instance
· letI : IsCyclic G := hcyc
exact isCyclic_of_surjective (QuotientGroup.mk' N) (QuotientGroup.mk'_surjective N)Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem solvable_isomClosed : IsomClosed solvableFinite solvable groups are closed under isomorphism.
Show proof
by
intro G H _ _ hGH hG
rcases hGH with ⟨e⟩
rcases hG with ⟨hfin, hsolv⟩
refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
letI : IsSolvable G := hsolv
exact solvable_of_surjective (f := e.toMonoidHom) e.surjectiveProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem solvable_quotientClosed : QuotientClosed solvableFinite solvable groups are closed under quotients.
Show proof
by
intro G _ N _ hG
rcases hG with ⟨hfin, hsolv⟩
refine ⟨?_, ?_⟩
· letI : Finite G := hfin
infer_instance
· letI : IsSolvable G := hsolv
infer_instanceProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem nilpotent_isomClosed : IsomClosed nilpotentFinite nilpotent groups are closed under isomorphism.
Show proof
by
intro G H _ _ hGH hG
rcases hGH with ⟨e⟩
rcases hG with ⟨hfin, hnil⟩
refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
letI : Group.IsNilpotent G := hnil
exact nilpotent_of_mulEquiv eProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem nilpotent_quotientClosed : QuotientClosed nilpotentFinite nilpotent groups are closed under quotients.
Show proof
by
intro G _ N _ hG
rcases hG with ⟨hfin, hnil⟩
refine ⟨?_, ?_⟩
· letI : Finite G := hfin
infer_instance
· letI : Group.IsNilpotent G := hnil
infer_instanceProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□Show proof
by
rintro ⟨hfin, hcyc⟩
refine ⟨hfin, ?_⟩
letI : IsCyclic G := hcyc
letI : CommGroup G := IsCyclic.commGroup
infer_instanceProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□Show proof
by
rintro ⟨hfin, hcyc⟩
refine ⟨hfin, ?_⟩
letI : IsCyclic G := hcyc
letI : CommGroup G := IsCyclic.commGroup
infer_instanceProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem pGroup_to_nilpotent {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] :
pGroup p G → nilpotent GShow proof
by
rintro ⟨hfin, hpG⟩
letI : Finite G := hfin
exact ⟨hfin, hpG.isNilpotent⟩Proof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□theorem pGroup_to_solvable {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] :
pGroup p G → solvable GShow proof
by
rintro ⟨hfin, hpG⟩
refine ⟨hfin, ?_⟩
letI : Group.IsNilpotent G := hpG.isNilpotent
infer_instanceProof. Unfold the finite-group class and the relevant closure property. The argument is purely finite group-theoretic: trivial groups, quotients, subgroups, normal subgroups, finite products, subdirect products, extensions, and isomorphism transport preserve the defining predicate by the bundled class hypotheses. For the cyclic, abelian, nilpotent, solvable, \(p\)-group, and \(\Sigma\)-group classes, the conclusion follows by checking the corresponding standard finite-group property and its permanence under the operation in question; no profinite inverse-limit argument is involved.
□