ProCGroups/FreeConstructions/FiniteSubgroupBounds.lean
1import ProCGroups.FreeConstructions.Framework
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/FreeConstructions/FiniteSubgroupBounds.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Abstract free construction framework
14Provides reusable universal-property infrastructure for free constructions, comparison maps, and uniqueness principles in topological group settings.
15-/
17namespace ProCGroups.FreeConstructions
19universe u v
21/-- Data recording that a finite subgroup is conjugate into one of the two factor images. -/
22structure FiniteSubgroupConjugacyData
23 (C : ProCGroups.FiniteGroupClass.{u})
24 {G A B : Type u} [Group G] [Group A] [Group B]
25 [TopologicalSpace G] [TopologicalSpace A] [TopologicalSpace B]
26 [IsTopologicalGroup G] [IsTopologicalGroup A] [IsTopologicalGroup B]
27 (ιA : A →ₜ* G) (ιB : B →ₜ* G)
28 (H : Subgroup G) : Prop where
29 isFreeProduct :
30 ProCGroups.FreeProducts.IsFreeProCProduct
31 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ιA ιB
32 finite : IsFiniteSubgroup H
33 conjugate_into_factor :
37/-- Finite groups generated by two subgroups each generated by at most `r` elements are
38generated by the concatenated list of `r + r` generators.
40The stronger bound `r` is not forced by two independently supplied rank-`r` generating data: the
41definition gives two independent length-`r` generating tuples, so the direct formal
42consequence is the concatenated bound. -/
44 (G : Type u) [Group G] (r : Nat) :
46 AbstractGeneratorRankLE G (r + r) := by
47 intro hG
48 rcases hG with ⟨A, B, _hAfinite, _hBfinite, _hcoprime, hABtop, ⟨genA, hgenA⟩,
49 ⟨genB, hgenB⟩⟩
50 let gen : Fin (r + r) → G :=
51 Fin.append (fun i => (genA i : G)) (fun i => (genB i : G))
52 let S : Set G := Set.range gen
53 refine ⟨gen, ?_⟩
54 have hA_le : (A : Set G) ⊆ Subgroup.closure S := by
55 intro a ha
56 let aA : A := ⟨a, ha⟩
57 have haA : aA ∈ Subgroup.closure (Set.range genA) := by
58 rw [hgenA]
59 trivial
60 exact Subgroup.closure_induction
61 (p := fun (x : A) _ => (x : G) ∈ Subgroup.closure S)
62 (fun x hx => by
63 rcases hx with ⟨i, rfl⟩
64 exact Subgroup.subset_closure (by
65 refine ⟨Fin.castAdd r i, ?_⟩
66 simp only [Fin.append_left, gen]))
67 (by simp only [OneMemClass.coe_one, one_mem])
68 (fun x y _ _ hx hy => by
69 simpa using (Subgroup.mul_mem (Subgroup.closure S) hx hy))
70 (fun x _ hx => by
71 simpa using (Subgroup.inv_mem (Subgroup.closure S) hx))
72 haA
73 have hB_le : (B : Set G) ⊆ Subgroup.closure S := by
74 intro b hb
75 let bB : B := ⟨b, hb⟩
76 have hbB : bB ∈ Subgroup.closure (Set.range genB) := by
77 rw [hgenB]
78 trivial
79 exact Subgroup.closure_induction
80 (p := fun (x : B) _ => (x : G) ∈ Subgroup.closure S)
81 (fun x hx => by
82 rcases hx with ⟨i, rfl⟩
83 exact Subgroup.subset_closure (by
84 refine ⟨Fin.natAdd r i, ?_⟩
85 simpa [gen] using
86 (Fin.append_right (fun i => (genA i : G)) (fun i => (genB i : G)) i)))
87 (by simp only [OneMemClass.coe_one, one_mem])
88 (fun x y _ _ hx hy => by
89 simpa using (Subgroup.mul_mem (Subgroup.closure S) hx hy))
90 (fun x _ hx => by
91 simpa using (Subgroup.inv_mem (Subgroup.closure S) hx))
92 hbB
93 apply le_antisymm
94 · exact le_top
95 · rw [← hABtop]
96 exact (Subgroup.closure_le (K := Subgroup.closure S)).2 (by
97 intro x hx
98 exact hx.elim (fun hxA => hA_le hxA) (fun hxB => hB_le hxB))
100/-- If a finite family has cardinality `s`, generates the ambient group, and each member is
101generated by at most `r` elements, then the ambient group is generated by the concatenated family
102of `s * r` generators.
104Sharper bounds require additional group-theoretic input beyond the concatenation data alone. -/
106 {ι : Type v} [Finite ι] (G : Type u) [Group G] (subgroups : ι → Subgroup G) (r s : Nat) :
107 SubgroupFamilyCardinality (ι := ι) s →
108 SubgroupFamilyGenerates subgroups →
109 SubgroupFamilyEachGeneratedByAtMost subgroups r →
110 AbstractGeneratorRankLE G (s * r) := by
111 classical
112 intro hcard hgenerates hEach
113 letI : Fintype ι := Fintype.ofFinite ι
114 have hcard' : Fintype.card ι = s := by
115 simpa [SubgroupFamilyCardinality, Nat.card_eq_fintype_card] using hcard
116 have hprod : Fintype.card (ι × Fin r) = s * r := by
117 simp only [Fintype.card_prod, hcard', Fintype.card_fin]
118 let e : Fin (s * r) ≃ ι × Fin r :=
119 (Fin.castOrderIso hprod.symm).toEquiv.trans (Fintype.equivFin (ι × Fin r)).symm
120 let genSub : (i : ι) → Fin r → subgroups i :=
121 fun i => Classical.choose (hEach i)
122 have hgenSub : ∀ i, Subgroup.closure (Set.range (genSub i)) = ⊤ :=
123 fun i => Classical.choose_spec (hEach i)
124 let gen : Fin (s * r) → G := fun a => (genSub (e a).1 (e a).2 : G)
125 let S : Set G := Set.range gen
126 refine ⟨gen, ?_⟩
127 let K : Subgroup G := Subgroup.closure S
128 have hsub_le : ∀ i, (subgroups i : Set G) ⊆ K := by
129 intro i x hx
130 let xi : subgroups i := ⟨x, hx⟩
131 have hxi : xi ∈ Subgroup.closure (Set.range (genSub i)) := by
132 rw [hgenSub i]
133 trivial
134 exact Subgroup.closure_induction
135 (p := fun (y : subgroups i) _ => (y : G) ∈ K)
136 (fun y hy => by
137 rcases hy with ⟨j, rfl⟩
138 exact Subgroup.subset_closure (by
139 refine ⟨e.symm (i, j), ?_⟩
140 simpa [gen] using
141 congrArg (fun p : ι × Fin r => (genSub p.1 p.2 : G))
142 (e.apply_symm_apply (i, j))))
143 (by simp only [OneMemClass.coe_one, one_mem, K])
144 (fun y z _ _ hy hz => by
145 simpa [K] using Subgroup.mul_mem K hy hz)
146 (fun y _ hy => by
147 simpa [K] using Subgroup.inv_mem K hy)
148 hxi
149 apply le_antisymm
150 · exact le_top
151 · rw [← hgenerates]
152 exact (Subgroup.closure_le (K := K)).2 (by
153 intro x hx
154 rcases Set.mem_iUnion.mp hx with ⟨i, hxi⟩
155 exact hsub_le i hxi)
157end ProCGroups.FreeConstructions