ProCGroups/FreeProC/Criteria/AbstractResidual.lean
1import Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
2import ProCGroups.FiniteGroups.StandardClasses
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/FreeProC/Criteria/AbstractResidual.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Free pro-C groups
15Develops free pro-C groups on spaces and pointed spaces, their universal properties, finite quotient characterizations, and standard comparison isomorphisms.
16-/
18namespace ProCGroups.FreeProC
20universe u v
23/-- A finite group embedding into a finite direct power of `S`.
25This definition does not require `S` to be simple; the literature term "finite `S`-group" is the
28 (S : Type u) [Group S]
29 (G : Type u) [Group G] : Prop :=
30 Finite G ∧ ∃ ι : Type u, Finite ι ∧ ∃ f : G →* (ι → S), Function.Injective f
32/-- A finite-group class contains all finite `S`-groups. -/
34 (C : ProCGroups.FiniteGroupClass.{u})
35 (S : Type u) [Group S] : Prop :=
36 ∀ {G : Type u} [Group G], EmbedsInFinitePower S G → C G
38/-- An abstract group has generator rank at most `κ` if it is a quotient of a free group on a set
39of cardinality at most `κ`. -/
41 (G : Type u) [Group G] (κ : Cardinal) : Prop :=
42 ∃ X : Type u, Cardinal.mk X ≤ κ ∧ ∃ φ : FreeGroup X →* G, Function.Surjective φ
44/-- Residual `C`-ness for an abstract group, stated directly in terms of separating nontrivial
47 (C : ProCGroups.FiniteGroupClass.{u})
48 (G : Type u) [Group G] : Prop :=
49 ∀ g : G, g ≠ 1 →
50 ∃ Q : Type u, ∃ _ : Group Q, C Q ∧ ∃ φ : G →* Q, φ g ≠ 1
52/-- Residual separation when the only allowed finite targets are finite `S`-groups. -/
54 (S : Type u) [Group S]
55 (G : Type u) [Group G] : Prop :=
56 ∀ g : G, g ≠ 1 →
57 ∃ Q : Type u, ∃ _ : Group Q, EmbedsInFinitePower S Q ∧ ∃ φ : G →* Q, φ g ≠ 1
59/-- Finite direct powers of `S` embed into a finite direct power of `S`. -/
60theorem embedsInFinitePower_pi
61 (S : Type u) [Group S] [Finite S]
62 (ι : Type u) [Finite ι] :
63 EmbedsInFinitePower S (ι → S) := by
64 refine ⟨inferInstance, ι, inferInstance, MonoidHom.id (ι → S), ?_⟩
65 exact fun _ _ h => h
67/-- A finite group embeds into the rank-one direct power of itself. -/
68theorem embedsInFinitePower_self
69 (S : Type u) [Group S] [Finite S] :
70 EmbedsInFinitePower S S := by
71 let f : S →* (PUnit.{u + 1} → S) :=
72 { toFun := fun s _ => s
73 map_one' := by
74 funext _
75 rfl
76 map_mul' := by
77 intro _ _
78 funext _
79 rfl }
80 refine ⟨inferInstance, PUnit.{u + 1}, inferInstance, f, ?_⟩
81 intro a b h
82 exact congrFun h PUnit.unit
84/-- A finite group that injects into a finite `S`-group is a finite `S`-group. -/
85theorem EmbedsInFinitePower.of_injective
86 {S : Type u} [Group S] {G H : Type u} [Group G] [Group H]
87 [Finite G] (hH : EmbedsInFinitePower S H) (f : G →* H)
88 (hf : Function.Injective f) :
89 EmbedsInFinitePower S G := by
90 rcases hH with ⟨_, ι, hι, e, he⟩
91 exact ⟨inferInstance, ι, hι, e.comp f, he.comp hf⟩
93/-- Subgroups of finite `S`-groups are finite `S`-groups. -/
94theorem EmbedsInFinitePower.subgroup
95 {S : Type u} [Group S] {G : Type u} [Group G]
96 (hG : EmbedsInFinitePower S G) (H : Subgroup G) :
97 EmbedsInFinitePower S H := by
98 rcases hG with ⟨hfinite, ι, hι, f, hf⟩
99 haveI : Finite G := hfinite
100 haveI : Finite H := Finite.of_injective ((↑) : H → G) Subtype.coe_injective
101 exact ⟨inferInstance, ι, hι, f.comp H.subtype, hf.comp Subtype.coe_injective⟩
103/-- Binary products of finite `S`-groups are finite `S`-groups. -/
104theorem EmbedsInFinitePower.prod
105 {S : Type u} [Group S] {G H : Type u} [Group G] [Group H]
106 (hG : EmbedsInFinitePower S G) (hH : EmbedsInFinitePower S H) :
107 EmbedsInFinitePower S (G × H) := by
108 rcases hG with ⟨hfiniteG, ιG, hιG, fG, hfG⟩
109 rcases hH with ⟨hfiniteH, ιH, hιH, fH, hfH⟩
110 haveI : Finite G := hfiniteG
111 haveI : Finite H := hfiniteH
112 haveI : Finite ιG := hιG
113 haveI : Finite ιH := hιH
114 let f : G × H →* (Sum ιG ιH → S) :=
115 { toFun := fun gh i =>
116 match i with
117 | Sum.inl iG => fG gh.1 iG
118 | Sum.inr iH => fH gh.2 iH
119 map_one' := by
120 funext i
121 cases i
124 map_mul' := by
125 intro a b
126 funext i
127 cases i
130 refine ⟨inferInstance, Sum ιG ιH, inferInstance, f, ?_⟩
131 intro a b hab
132 apply Prod.ext
133 · apply hfG
134 funext i
135 exact congrFun hab (Sum.inl i)
136 · apply hfH
137 funext i
138 exact congrFun hab (Sum.inr i)
140/-- Every finite `S`-group is killed by the exponent of `S`. -/
141theorem EmbedsInFinitePower.pow_exponent_eq_one
142 {S : Type u} [Group S] {G : Type u} [Group G]
143 (hG : EmbedsInFinitePower S G) (g : G) :
144 g ^ Monoid.exponent S = 1 := by
145 rcases hG with ⟨_, ι, _, f, hf⟩
146 apply hf
147 funext i
149 exact Monoid.pow_exponent_eq_one (f g i)
151/-- Homomorphisms into finite `S`-groups kill every `S`-exponent power. -/
152theorem EmbedsInFinitePower.map_pow_exponent_eq_one
153 {S : Type u} [Group S] {G Q : Type u} [Group G] [Group Q]
154 (hQ : EmbedsInFinitePower S Q) (φ : G →* Q) (g : G) :
155 φ (g ^ Monoid.exponent S) = 1 := by
156 rw [map_pow]
157 exact hQ.pow_exponent_eq_one (φ g)
159/-- If some `S`-exponent power is nontrivial, finite `S`-groups cannot separate all nontrivial
160elements. -/
162 {S : Type u} [Group S] {G : Type u} [Group G] {g : G}
163 (hg : g ^ Monoid.exponent S ≠ 1) :
164 ¬ IsResiduallyFiniteSGroups S G := by
165 intro hres
166 rcases hres (g ^ Monoid.exponent S) hg with ⟨Q, hQGroup, hQ, φ, hφ⟩
167 letI : Group Q := hQGroup
168 exact hφ (hQ.map_pow_exponent_eq_one φ g)
170/-- A nonzero power of a free generator is nontrivial. -/
171theorem freeGroup_of_pow_ne_one
172 {X : Type u} (x : X) {n : ℕ} (hn : n ≠ 0) :
173 (FreeGroup.of x : FreeGroup X) ^ n ≠ 1 := by
174 intro hpow
175 have hx : (FreeGroup.of x : FreeGroup X) = 1 :=
176 (pow_eq_one_iff_left (M := FreeGroup X) hn).mp hpow
177 exact FreeGroup.of_ne_one x hx
179/-- Finite `S`-groups alone cannot make a nonempty free group residually `S`. -/
181 (S : Type u) [Group S] [Finite S] {X : Type u} (x : X) :
182 ¬ IsResiduallyFiniteSGroups S (FreeGroup X) :=
184 (S := S) (G := FreeGroup X) (g := FreeGroup.of x)
185 (freeGroup_of_pow_ne_one x (Monoid.exponent_ne_zero_of_finite (G := S)))
187/-- A class containing all finite `S`-groups contains every finite direct power of `S`. -/
188theorem ContainsAllFiniteSGroups.pi_mem
189 {C : ProCGroups.FiniteGroupClass.{u}} {S : Type u} [Group S] [Finite S]
190 (hcontains : ContainsAllFiniteSGroups C S)
191 (ι : Type u) [Finite ι] :
192 C (ι → S) :=
193 hcontains (embedsInFinitePower_pi S ι)
195/-- A class containing all finite `S`-groups contains `S` itself. -/
196theorem ContainsAllFiniteSGroups.self_mem
197 {C : ProCGroups.FiniteGroupClass.{u}} {S : Type u} [Group S] [Finite S]
198 (hcontains : ContainsAllFiniteSGroups C S) :
199 C S :=
200 hcontains (embedsInFinitePower_self S)
202end ProCGroups.FreeProC