Source: ProCGroups.FreeConstructions.FiniteSubgroupBounds
1import ProCGroups.FreeConstructions.Framework
3/-!
4# Generator bounds from finite subgroup families
6Independent generating tuples for finitely many subgroups can be concatenated.
7The two theorems below turn that elementary construction into explicit
8ambient-group rank bounds.
9-/
11namespace ProCGroups.FreeConstructions
13universe u v
15/-- If two subgroups generate `G` and each has an `r`-element generating
16family, concatenating those families gives a `2r`-element generating family
17for `G`. -/
18theorem generatorRankLE_add_of_two_subgroups
19 (G : Type u) [Group G] (r : Nat) (A B : Subgroup G)
20 (hABtop : Subgroup.closure ((A : Set G) ∪ (B : Set G)) = ⊤)
21 (hA : AbstractGeneratorRankLE A r)
22 (hB : AbstractGeneratorRankLE B r) :
23 AbstractGeneratorRankLE G (r + r) := by
24 rcases hA with ⟨genA, hgenA⟩
25 rcases hB with ⟨genB, hgenB⟩
26 let gen : Fin (r + r) → G :=
27 Fin.append (fun i => (genA i : G)) (fun i => (genB i : G))
28 let S : Set G := Set.range gen
29 refine ⟨gen, ?_⟩
30 have hA_le : (A : Set G) ⊆ Subgroup.closure S := by
31 intro a ha
32 let aA : A := ⟨a, ha⟩
33 have haA : aA ∈ Subgroup.closure (Set.range genA) := by
34 rw [hgenA]
35 trivial
36 exact Subgroup.closure_induction
37 (p := fun (x : A) _ => (x : G) ∈ Subgroup.closure S)
38 (fun x hx => by
39 rcases hx with ⟨i, rfl⟩
40 exact Subgroup.subset_closure (by
41 refine ⟨Fin.castAdd r i, ?_⟩
42 simp only [Fin.append_left, gen]))
43 (by simp only [OneMemClass.coe_one, one_mem])
44 (fun x y _ _ hx hy => by
45 simpa using (Subgroup.mul_mem (Subgroup.closure S) hx hy))
46 (fun x _ hx => by
47 simpa using (Subgroup.inv_mem (Subgroup.closure S) hx))
48 haA
49 have hB_le : (B : Set G) ⊆ Subgroup.closure S := by
50 intro b hb
51 let bB : B := ⟨b, hb⟩
52 have hbB : bB ∈ Subgroup.closure (Set.range genB) := by
53 rw [hgenB]
54 trivial
55 exact Subgroup.closure_induction
56 (p := fun (x : B) _ => (x : G) ∈ Subgroup.closure S)
57 (fun x hx => by
58 rcases hx with ⟨i, rfl⟩
59 exact Subgroup.subset_closure (by
60 refine ⟨Fin.natAdd r i, ?_⟩
61 simpa [gen] using
62 (Fin.append_right (fun i => (genA i : G)) (fun i => (genB i : G)) i)))
63 (by simp only [OneMemClass.coe_one, one_mem])
64 (fun x y _ _ hx hy => by
65 simpa using (Subgroup.mul_mem (Subgroup.closure S) hx hy))
66 (fun x _ hx => by
67 simpa using (Subgroup.inv_mem (Subgroup.closure S) hx))
68 hbB
69 apply le_antisymm
70 · exact le_top
71 · rw [← hABtop]
72 exact (Subgroup.closure_le (K := Subgroup.closure S)).2 (by
73 intro x hx
74 exact hx.elim (fun hxA => hA_le hxA) (fun hxB => hB_le hxB))
76/-- If an `s`-element family of subgroups generates `G` and every member has
77an `r`-element generating family, concatenating all families gives an
78`s * r`-element generating family for `G`. -/
79theorem finite_subgroup_family_generator_bound
80 {ι : Type v} [Finite ι] (G : Type u) [Group G]
81 (subgroups : ι → Subgroup G) (r s : Nat)
82 (hcard : Nat.card ι = s)
83 (hgenerates : Subgroup.closure (Set.iUnion fun i => (subgroups i : Set G)) = ⊤)
84 (hEach : ∀ i, AbstractGeneratorRankLE (subgroups i) r) :
85 AbstractGeneratorRankLE G (s * r) := by
86 classical
87 letI : Fintype ι := Fintype.ofFinite ι
88 have hcard' : Fintype.card ι = s := by
89 simpa [Nat.card_eq_fintype_card] using hcard
90 have hprod : Fintype.card (ι × Fin r) = s * r := by
91 simp only [Fintype.card_prod, hcard', Fintype.card_fin]
92 let e : Fin (s * r) ≃ ι × Fin r :=
93 (Fin.castOrderIso hprod.symm).toEquiv.trans (Fintype.equivFin (ι × Fin r)).symm
94 let genSub : (i : ι) → Fin r → subgroups i :=
95 fun i => Classical.choose (hEach i)
96 have hgenSub : ∀ i, Subgroup.closure (Set.range (genSub i)) = ⊤ :=
97 fun i => Classical.choose_spec (hEach i)
98 let gen : Fin (s * r) → G := fun a => (genSub (e a).1 (e a).2 : G)
99 let S : Set G := Set.range gen
100 refine ⟨gen, ?_⟩
101 let K : Subgroup G := Subgroup.closure S
102 have hsub_le : ∀ i, (subgroups i : Set G) ⊆ K := by
103 intro i x hx
104 let xi : subgroups i := ⟨x, hx⟩
105 have hxi : xi ∈ Subgroup.closure (Set.range (genSub i)) := by
106 rw [hgenSub i]
107 trivial
108 exact Subgroup.closure_induction
109 (p := fun (y : subgroups i) _ => (y : G) ∈ K)
110 (fun y hy => by
111 rcases hy with ⟨j, rfl⟩
112 exact Subgroup.subset_closure (by
113 refine ⟨e.symm (i, j), ?_⟩
114 simpa [gen] using
115 congrArg (fun p : ι × Fin r => (genSub p.1 p.2 : G))
116 (e.apply_symm_apply (i, j))))
117 (by simp only [OneMemClass.coe_one, one_mem, K])
118 (fun y z _ _ hy hz => by
119 simpa [K] using Subgroup.mul_mem K hy hz)
120 (fun y _ hy => by
121 simpa [K] using Subgroup.inv_mem K hy)
122 hxi
123 apply le_antisymm
124 · exact le_top
125 · rw [← hgenerates]
126 exact (Subgroup.closure_le (K := K)).2 (by
127 intro x hx
128 rcases Set.mem_iUnion.mp hx with ⟨i, hxi⟩
129 exact hsub_le i hxi)
131end ProCGroups.FreeConstructions