Yamaguchi Lean 4 Library
ProCGroups/Completion/ProCInteger.lean
ProCGroups/Completion/ProCInteger/Source

ProCGroups/Completion/ProCInteger.lean

1import Mathlib.Topology.Instances.ZMod
2import ProCGroups.ProC.InverseLimits.Limits
3import ProCGroups.ProC.InverseLimits.Predicates
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/Completion/ProCInteger.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Pro-C integers and finite cyclic stages
16Constructs pro-C integers as inverse limits of allowed finite cyclic rings and records coordinate formulas at each finite modulus.
17-/
19open scoped Topology
21namespace ProCGroups.Completion
23noncomputable section
25universe u v
27/-- A coefficient level: a positive modulus whose additive cyclic group is in `C`. -/
28structure ProCIntegerIndex (C : FiniteGroupClass.{u}) where
29 modulus : ℕ
30 positive : 0 < modulus
31 cyclic_mem : C (ULift (Multiplicative (ZMod modulus)))
35/-- Order pro-`C` integer coefficient indices by divisibility of moduli. -/
36instance instLEProCIntegerIndex (C : FiniteGroupClass.{u}) : LE (ProCIntegerIndex C) where
37 le i j := i.modulus ∣ j.modulus
39/-- Pro-`C` integer coefficient indices form a preorder under divisibility. -/
40instance instPreorderProCIntegerIndex (C : FiniteGroupClass.{u}) : Preorder (ProCIntegerIndex C) where
41 le := (· ≤ ·)
42 le_refl i := dvd_rfl
43 le_trans _ _ _ hij hjk := dvd_trans hij hjk
45/-- Build a coefficient index from an allowed positive modulus. -/
46def ofModulus {C : FiniteGroupClass.{u}} (n : ℕ) (hn : 0 < n)
47 (hC : C (ULift (Multiplicative (ZMod n)))) : ProCIntegerIndex C where
48 modulus := n
49 positive := hn
50 cyclic_mem := hC
52/-- The positivity proof carried by a coefficient index, packaged for APIs requiring `Fact`. -/
53def positiveFact {C : FiniteGroupClass.{u}} (i : ProCIntegerIndex C) :
54 Fact (0 < i.modulus) :=
55 ⟨i.positive⟩
57/-- The terminal coefficient index `ZMod 1`, available when `C` contains trivial quotients. -/
58def terminal {C : FiniteGroupClass.{u}} (htriv : FiniteGroupClass.ContainsTrivialQuotients C) :
60 modulus := 1
61 positive := Nat.zero_lt_one
62 cyclic_mem := htriv.of_subsingleton inferInstance
64/-- Every positive modulus is allowed for the all-finite class. -/
65def ofAllFiniteModulus (n : ℕ) (hn : 0 < n) :
66 ProCIntegerIndex (FiniteGroupClass.allFinite : FiniteGroupClass.{u}) where
67 modulus := n
68 positive := hn
69 cyclic_mem := by
70 letI : NeZero n := ⟨Nat.ne_of_gt hn⟩
71 letI : Fintype (ZMod n) := ZMod.fintype n
72 have hfinZ : Finite (ZMod n) := Finite.of_fintype _
73 have hfinMul : Finite (Multiplicative (ZMod n)) :=
74 @Finite.of_equiv _ _ hfinZ Multiplicative.toAdd
75 exact @Finite.of_equiv _ _ hfinMul Equiv.ulift.symm
77/-- The all-finite coefficient index has the prescribed modulus. -/
78@[simp]
79theorem modulus_ofAllFiniteModulus (n : ℕ) (hn : 0 < n) :
80 (ofAllFiniteModulus n hn).modulus = n :=
81 rfl
83/-- The order of an element of a finite `C`-group is an allowed coefficient modulus for
84hereditary classes. -/
85def ofElementOrder {C : FiniteGroupClass.{u}}
86 (hHer : FiniteGroupClass.Hereditary C)
87 {K : Type u} [Group K] [Finite K] (hK : C K) (k : K) :
89 letI : NeZero (orderOf k) := ⟨Nat.ne_of_gt (orderOf_pos k)⟩
90 refine ofModulus (orderOf k) (orderOf_pos k) ?_
91 let fInt : ℤ →+ Additive (Subgroup.zpowers k) :=
92 { toFun := fun z => Additive.ofMul ⟨k ^ z, z, rfl⟩
93 map_zero' := by
94 apply Additive.ext
95 ext
96 simp only [zpow_zero, toMul_ofMul, toMul_zero, OneMemClass.coe_one]
97 map_add' a b := by
98 apply Additive.ext
99 ext
100 simp only [zpow_add, toMul_ofMul, toMul_add, Subgroup.coe_mul]}
101 have hfInt_order : fInt (orderOf k) = 0 := by
102 apply Additive.ext
103 ext
104 change k ^ ((orderOf k : ℕ) : ℤ) = 1
105 simp only [zpow_natCast, pow_orderOf_eq_one]
106 let fZ : ZMod (orderOf k) →+ Additive (Subgroup.zpowers k) :=
107 (ZMod.lift (orderOf k)) ⟨fInt, hfInt_order⟩
108 have hfZ_inj : Function.Injective fZ := by
109 rw [ZMod.lift_injective]
110 intro m hm
111 have hpow : k ^ m = 1 := by
112 have hm' : (⟨k ^ m, m, rfl⟩ : Subgroup.zpowers k) = 1 := by
113 change (fInt m).toMul = (0 : Additive (Subgroup.zpowers k)).toMul
114 exact congrArg Additive.toMul hm
115 simpa using congrArg Subtype.val hm'
116 exact (ZMod.intCast_zmod_eq_zero_iff_dvd m (orderOf k)).2
117 ((orderOf_dvd_iff_zpow_eq_one (x := k) (i := m)).2 hpow)
118 let φ0 : Multiplicative (ZMod (orderOf k)) →* Subgroup.zpowers k :=
119 AddMonoidHom.toMultiplicativeLeft fZ
120 let uliftDown :
121 ULift (Multiplicative (ZMod (orderOf k))) →*
122 Multiplicative (ZMod (orderOf k)) :=
123 { toFun := fun x => x.down
124 map_one' := rfl
125 map_mul' := by
126 intro x y
127 cases x
128 cases y
129 rfl }
130 let φ : ULift (Multiplicative (ZMod (orderOf k))) →* K :=
131 (Subgroup.zpowers k).subtype.comp (φ0.comp uliftDown)
132 have hφ_inj : Function.Injective φ := by
133 intro a b hab
134 have hval :
135 ((φ0 a.down : Subgroup.zpowers k) : K) =
136 ((φ0 b.down : Subgroup.zpowers k) : K) := by
137 simpa [φ, uliftDown] using hab
138 have hsub : φ0 a.down = φ0 b.down := Subtype.ext hval
139 have hadd : fZ a.down.toAdd = fZ b.down.toAdd := by
140 apply Additive.ext
141 change (fZ a.down.toAdd).toMul = (fZ b.down.toAdd).toMul
142 simpa [φ0] using hsub
143 have hz : a.down.toAdd = b.down.toAdd := hfZ_inj hadd
144 apply ULift.ext
145 exact Multiplicative.ext hz
146 exact hHer.of_injective hK φ hφ_inj
148/-- Formation closure makes the allowed coefficient moduli directed by common multiples. -/
149theorem directed_of_formation {C : FiniteGroupClass.{u}} (hForm : FiniteGroupClass.Formation C) :
150 Directed (· ≤ ·) (id : ProCIntegerIndex C → ProCIntegerIndex C) := by
151 classical
152 intro i j
153 let n := Nat.lcm i.modulus j.modulus
154 have hn : 0 < n := Nat.lcm_pos i.positive j.positive
155 have hi : i.modulus ∣ n := Nat.dvd_lcm_left i.modulus j.modulus
156 have hj : j.modulus ∣ n := Nat.dvd_lcm_right i.modulus j.modulus
157 let A : Type u := ULift.{u} (Multiplicative (ZMod n))
158 let K : ULift Bool → Type u
159 | ⟨false⟩ => ULift.{u} (Multiplicative (ZMod i.modulus))
160 | ⟨true⟩ => ULift.{u} (Multiplicative (ZMod j.modulus))
161 letI : ∀ b : ULift Bool, Group (K b) := by
162 intro b
163 cases b with
164 | up b =>
165 cases b <;> infer_instance
166 let f : A →* (∀ b : ULift Bool, K b) := {
167 toFun := fun x b => by
168 cases b with
169 | up b =>
170 cases b
171 · exact ULift.up
172 (Multiplicative.ofAdd (ZMod.castHom hi (ZMod i.modulus) x.down.toAdd))
173 · exact ULift.up
174 (Multiplicative.ofAdd (ZMod.castHom hj (ZMod j.modulus) x.down.toAdd))
175 map_one' := by
176 funext b
177 cases b with
178 | up b =>
179 cases b
180 · change
181 ULift.up
182 (Multiplicative.ofAdd
183 (ZMod.castHom hi (ZMod i.modulus) (0 : ZMod n))) =
184 (1 : ULift (Multiplicative (ZMod i.modulus)))
185 ext
186 simp only [ZMod.castHom_apply, ZMod.cast_zero, ofAdd_zero, toAdd_one, ULift.one_down]
187 · change
188 ULift.up
189 (Multiplicative.ofAdd
190 (ZMod.castHom hj (ZMod j.modulus) (0 : ZMod n))) =
191 (1 : ULift (Multiplicative (ZMod j.modulus)))
192 ext
193 simp only [ZMod.castHom_apply, ZMod.cast_zero, ofAdd_zero, toAdd_one, ULift.one_down]
194 map_mul' := by
195 intro x y
196 funext b
197 cases b with
198 | up b =>
199 cases b
200 · cases x with
201 | up x =>
202 cases y with
203 | up y =>
204 change
205 ULift.up
206 (Multiplicative.ofAdd
207 (ZMod.castHom hi (ZMod i.modulus) (x.toAdd + y.toAdd))) =
208 ULift.up
209 (Multiplicative.ofAdd
210 (ZMod.castHom hi (ZMod i.modulus) x.toAdd +
211 ZMod.castHom hi (ZMod i.modulus) y.toAdd))
212 ext
213 exact (ZMod.castHom hi (ZMod i.modulus)).map_add x.toAdd y.toAdd
214 · cases x with
215 | up x =>
216 cases y with
217 | up y =>
218 change
219 ULift.up
220 (Multiplicative.ofAdd
221 (ZMod.castHom hj (ZMod j.modulus) (x.toAdd + y.toAdd))) =
222 ULift.up
223 (Multiplicative.ofAdd
224 (ZMod.castHom hj (ZMod j.modulus) x.toAdd +
225 ZMod.castHom hj (ZMod j.modulus) y.toAdd))
226 ext
227 exact (ZMod.castHom hj (ZMod j.modulus)).map_add x.toAdd y.toAdd
228 }
229 have hf : Function.Injective f := by
230 intro x y hxy
231 have hfalse :
232 ZMod.castHom hi (ZMod i.modulus) x.down.toAdd =
233 ZMod.castHom hi (ZMod i.modulus) y.down.toAdd := by
234 simpa [f, K] using congrFun hxy ⟨false⟩
235 have htrue :
236 ZMod.castHom hj (ZMod j.modulus) x.down.toAdd =
237 ZMod.castHom hj (ZMod j.modulus) y.down.toAdd := by
238 simpa [f, K] using congrFun hxy ⟨true⟩
239 rcases ZMod.intCast_surjective x.down.toAdd with ⟨a, ha⟩
240 rcases ZMod.intCast_surjective y.down.toAdd with ⟨b, hb⟩
241 have hiab : (i.modulus : ℤ) ∣ a - b := by
242 rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]
243 rw [Int.cast_sub, sub_eq_zero]
244 have ha_i :
245 ZMod.castHom hi (ZMod i.modulus) x.down.toAdd = (a : ZMod i.modulus) := by
246 simp only [← ha, map_intCast]
247 have hb_i :
248 ZMod.castHom hi (ZMod i.modulus) y.down.toAdd = (b : ZMod i.modulus) := by
249 simp only [← hb, map_intCast]
250 exact ha_i.symm.trans (hfalse.trans hb_i)
251 have hjab : (j.modulus : ℤ) ∣ a - b := by
252 rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]
253 rw [Int.cast_sub, sub_eq_zero]
254 have ha_j :
255 ZMod.castHom hj (ZMod j.modulus) x.down.toAdd = (a : ZMod j.modulus) := by
256 simp only [← ha, map_intCast]
257 have hb_j :
258 ZMod.castHom hj (ZMod j.modulus) y.down.toAdd = (b : ZMod j.modulus) := by
259 simp only [← hb, map_intCast]
260 exact ha_j.symm.trans (htrue.trans hb_j)
261 have hnab_nat : n ∣ (a - b).natAbs := by
262 exact Nat.lcm_dvd ((Int.natCast_dvd).1 hiab) ((Int.natCast_dvd).1 hjab)
263 have hnab : (n : ℤ) ∣ a - b := (Int.natCast_dvd).2 hnab_nat
264 have hab : (a : ZMod n) = (b : ZMod n) := by
265 rw [← sub_eq_zero, ← Int.cast_sub, ZMod.intCast_zmod_eq_zero_iff_dvd]
266 exact hnab
267 have hxy_add : x.down.toAdd = y.down.toAdd := by
268 calc
269 x.down.toAdd = (a : ZMod n) := ha.symm
270 _ = (b : ZMod n) := hab
271 _ = y.down.toAdd := hb
272 apply ULift.ext
273 exact Multiplicative.ext hxy_add
274 have hsurj : ∀ b : ULift Bool,
275 Function.Surjective fun g : A => f g b := by
276 intro b
277 cases b with
278 | up b =>
279 cases b
280 · intro y
281 rcases ZMod.castHom_surjective hi y.down.toAdd with ⟨x, hx⟩
282 refine ⟨ULift.up (Multiplicative.ofAdd x), ?_⟩
283 cases y
284 exact congrArg ULift.up (congrArg Multiplicative.ofAdd (by simpa [f, K] using hx))
285 · intro y
286 rcases ZMod.castHom_surjective hj y.down.toAdd with ⟨x, hx⟩
287 refine ⟨ULift.up (Multiplicative.ofAdd x), ?_⟩
288 cases y
289 exact congrArg ULift.up (congrArg Multiplicative.ofAdd (by simpa [f, K] using hx))
290 have hCK : ∀ b : ULift Bool, C (K b) := by
291 intro b
292 cases b with
293 | up b =>
294 cases b
295 · simpa [K] using i.cyclic_mem
296 · simpa [K] using j.cyclic_mem
297 have hCn : C A :=
298 hForm.finiteSubdirectProductClosed f hf hsurj hCK
299 refine ⟨ofModulus n hn ?_, ?_, ?_⟩
300 · simpa [A] using hCn
301 · exact hi
302 · exact hj
304/-- In a finite `C`-group, a single allowed coefficient modulus is divisible by every element
305order. -/
306theorem exists_index_orderOf_dvd_of_finite_mem {C : FiniteGroupClass.{u}}
307 (hForm : FiniteGroupClass.Formation C)
308 (hHer : FiniteGroupClass.Hereditary C)
309 {K : Type u} [Group K] [Finite K] (hK : C K) :
310 ∃ i : ProCIntegerIndex C, ∀ k : K, orderOf k ∣ i.modulus := by
311 classical
312 letI : Fintype K := Fintype.ofFinite K
313 have hfinset :
314 ∀ s : Finset K, ∃ i : ProCIntegerIndex C, ∀ k ∈ s, orderOf k ∣ i.modulus := by
315 intro s
316 induction s using Finset.induction with
317 | empty =>
318 exact ⟨ofElementOrder hHer hK (1 : K), by simp only [Finset.notMem_empty, IsEmpty.forall_iff, implies_true]⟩
319 | insert a s has ih =>
320 rcases ih with ⟨i, hi⟩
321 let j := ofElementOrder hHer hK a
322 rcases ProCIntegerIndex.directed_of_formation (C := C) hForm i j with ⟨m, hmi, hmj⟩
323 refine ⟨m, ?_⟩
324 intro k hk
325 rw [Finset.mem_insert] at hk
326 rcases hk with hk_eq | hk
327 · subst k
328 exact dvd_trans (by rfl : orderOf a ∣ j.modulus) hmj
329 · exact dvd_trans (hi k hk) hmi
330 rcases hfinset (Finset.univ : Finset K) with ⟨i, hi⟩
331 exact ⟨i, fun k => hi k (Finset.mem_univ k)⟩
333/-- In a finite `C`-group, some allowed coefficient modulus kills every element. -/
334theorem exists_index_kills_finite_group_of_mem {C : FiniteGroupClass.{u}}
335 (hForm : FiniteGroupClass.Formation C)
336 (hHer : FiniteGroupClass.Hereditary C)
337 {K : Type u} [Group K] [Finite K] (hK : C K) :
338 ∃ i : ProCIntegerIndex C, ∀ k : K, k ^ i.modulus = 1 := by
340 (C := C) hForm hHer hK with ⟨i, hi⟩
341 exact ⟨i, fun k =>
342 (orderOf_dvd_iff_pow_eq_one (x := k) (n := i.modulus)).1 (hi k)⟩
346variable (C : FiniteGroupClass.{u})
348/-- The finite cyclic stage `Z/nZ` of the pro-`C` integers. -/
349abbrev ProCIntegerStage (i : ProCIntegerIndex C) : Type :=
350 ZMod i.modulus
352/-- Reduction between finite cyclic stages. -/
353def proCIntegerTransition {i j : ProCIntegerIndex C} (hij : i ≤ j) :
355 ZMod.castHom hij (ZMod i.modulus)
357/-- The finite cyclic stages defining the pro-`C` integers as an inverse system. -/
360 topologicalSpace := fun _ => inferInstance
361 map := fun {i j} hij => proCIntegerTransition (C := C) hij
362 continuous_map := by
363 intro i j hij
364 exact continuous_of_discreteTopology
365 map_id := by
366 intro i
367 ext x
368 simp only [proCIntegerTransition, ZMod.castHom_self, RingHom.id_apply, id_eq]
369 map_comp := by
370 intro i j k hij hjk
371 ext x
372 exact congrArg (fun f : ZMod k.modulus →+* ZMod i.modulus => f x)
373 (ZMod.castHom_comp hij hjk)
375/-- Compatibility condition for a point of the inverse limit defining the pro-`C` integers. -/
377 (x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) : Prop :=
378 ∀ i j, ∀ hij : i ≤ j, proCIntegerTransition (C := C) hij (x j) = x i
380/-- Explicit carrier-level name for the current inverse-limit implementation of pro-`C`
381integers. -/
382abbrev ProCIntegerLimitCarrier : Type _ :=
385/-- The all-finite profinite integers. Kept as a public type synonym because downstream
386HLF files use this as their interface for `\hat{\mathbb Z}`. -/
387abbrev ProfiniteInteger : Type _ :=
388 ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{u})
390/-- Projection from the pro-`C` integers to a finite cyclic stage. -/
392 fun x => x.1 i
394/-- Extensionality for pro-`C` integers through their finite cyclic projections. -/
395@[ext]
396theorem ProCIntegerLimitCarrier.ext {x y : ProCIntegerLimitCarrier C}
397 (h : ∀ i : ProCIntegerIndex C,
398 proCIntegerProj (C := C) i x = proCIntegerProj (C := C) i y) :
399 x = y :=
400 Subtype.ext (funext h)
402/-- The zero pro-`C` integer is defined coordinatewise. -/
404 zero := ⟨fun _ => 0, by
405 intro i j hij
406 exact map_zero (proCIntegerTransition (C := C) hij)⟩
408/-- Addition of pro-`C` integers is defined coordinatewise. -/
410 add x y := ⟨fun i => x.1 i + y.1 i, by
411 intro i j hij
413 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
415/-- Negation of pro-`C` integers is defined coordinatewise. -/
417 neg x := ⟨fun i => -x.1 i, by
418 intro i j hij
419 rw [map_neg]
420 exact congrArg Neg.neg (x.2 i j hij)⟩
422/-- Subtraction of pro-`C` integers is defined coordinatewise. -/
424 sub x y := ⟨fun i => x.1 i - y.1 i, by
425 intro i j hij
426 rw [map_sub]
427 exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
429/-- Natural-number scalar multiplication of pro-`C` integers is defined coordinatewise. -/
431 smul n x := ⟨fun i => n • x.1 i, by
432 intro i j hij
433 rw [map_nsmul]
434 exact congrArg (n • ·) (x.2 i j hij)⟩
436/-- Integer scalar multiplication of pro-`C` integers is defined coordinatewise. -/
438 smul n x := ⟨fun i => n • x.1 i, by
439 intro i j hij
440 rw [map_zsmul]
441 exact congrArg (n • ·) (x.2 i j hij)⟩
443/-- The unit pro-`C` integer is defined coordinatewise. -/
445 one := ⟨fun _ => 1, by
446 intro i j hij
447 exact map_one (proCIntegerTransition (C := C) hij)⟩
449/-- Multiplication of pro-`C` integers is defined coordinatewise. -/
451 mul x y := ⟨fun i => x.1 i * y.1 i, by
452 intro i j hij
454 exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩
456/-- Natural-number casts into pro-`C` integers are defined coordinatewise. -/
458 natCast n := ⟨fun _ => n, by
459 intro i j hij
460 exact map_natCast (proCIntegerTransition (C := C) hij) n⟩
462/-- Integer casts into pro-`C` integers are defined coordinatewise. -/
464 intCast n := ⟨fun _ => n, by
465 intro i j hij
466 exact map_intCast (proCIntegerTransition (C := C) hij) n⟩
468/-- Powers of pro-`C` integers are defined coordinatewise. -/
469instance instPowProCInteger : Pow (ProCIntegerLimitCarrier C) ℕ where
470 pow x n := ⟨fun i => x.1 i ^ n, by
471 intro i j hij
472 rw [map_pow]
473 exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩
475/-- The underlying compatible family of pro-`C` integers computes zero coordinatewise. -/
476@[simp]
478 ((0 : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = 0 := by
479 funext i
480 rfl
482/-- The underlying compatible family of pro-`C` integers computes one coordinatewise. -/
483@[simp]
485 ((1 : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = 1 := by
486 funext i
487 rfl
489/-- The underlying compatible family of pro-`C` integers computes addition coordinatewise. -/
490@[simp]
492 ((x + y : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = x + y := by
493 funext i
494 rfl
496/-- The underlying compatible family of pro-`C` integers computes multiplication coordinatewise. -/
497@[simp]
499 ((x * y : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = x * y := by
500 funext i
501 rfl
503/-- The underlying compatible family of pro-`C` integers computes negation coordinatewise. -/
504@[simp]
506 ((-x : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = -x := by
507 funext i
508 rfl
510/-- The underlying compatible family of pro-`C` integers computes subtraction coordinatewise. -/
511@[simp]
513 ((x - y : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = x - y := by
514 funext i
515 rfl
517/-- The underlying compatible family of pro-`C` integers computes natural-number casts coordinatewise. -/
518@[simp]
519theorem coe_natCast_proCInteger (n : ℕ) :
520 ((n : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = n := by
521 funext i
522 rfl
524/-- The underlying compatible family of pro-`C` integers computes integer casts coordinatewise. -/
525@[simp]
526theorem coe_intCast_proCInteger (n : ℤ) :
528 fun i => (n : ProCIntegerStage C i) := by
529 funext i
530 rfl
532/-- The underlying compatible family of pro-`C` integers computes powers coordinatewise. -/
533@[simp]
535 ((x ^ n : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = x ^ n := by
536 funext i
537 rfl
539/-- The pro-`C` integers are a ring by coordinatewise operations. -/
541 Function.Injective.ring
542 (fun x : ProCIntegerLimitCarrier C => (x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i))
543 Subtype.val_injective
550 (by intro n x; funext i; change (n • x).1 i = n • x.1 i; rfl)
551 (by intro n x; funext i; change (n • x).1 i = n • x.1 i; rfl)
556/-- The pro-`C` integers are a commutative ring by coordinatewise operations. -/
558 Function.Injective.commRing
559 (fun x : ProCIntegerLimitCarrier C => (x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i))
560 Subtype.val_injective
567 (by intro n x; funext i; change (n • x).1 i = n • x.1 i; rfl)
568 (by intro n x; funext i; change (n • x).1 i = n • x.1 i; rfl)
573/-- Finite projections of pro-`C` integers commute with `0`. -/
574@[simp]
576 proCIntegerProj (C := C) i (0 : ProCIntegerLimitCarrier C) = 0 :=
577 by rfl
579/-- Finite projections of pro-`C` integers commute with `1`. -/
580@[simp]
582 proCIntegerProj (C := C) i (1 : ProCIntegerLimitCarrier C) = 1 :=
583 by rfl
585/-- Finite projections of pro-`C` integers commute with addition. -/
586@[simp]
588 proCIntegerProj (C := C) i (x + y) =
589 proCIntegerProj (C := C) i x + proCIntegerProj (C := C) i y :=
590 by
591 change (x + y).1 i = x.1 i + y.1 i
592 rfl
594/-- Finite projections of pro-`C` integers commute with multiplication. -/
595@[simp]
597 proCIntegerProj (C := C) i (x * y) =
598 proCIntegerProj (C := C) i x * proCIntegerProj (C := C) i y :=
599 by
600 change (x * y).1 i = x.1 i * y.1 i
601 rfl
603/-- Finite projections of pro-`C` integers commute with negation. -/
604@[simp]
606 proCIntegerProj (C := C) i (-x) = -proCIntegerProj (C := C) i x :=
607 by
608 change (-x).1 i = -x.1 i
609 rfl
611/-- Finite projections of pro-`C` integers commute with subtraction. -/
612@[simp]
614 proCIntegerProj (C := C) i (x - y) =
615 proCIntegerProj (C := C) i x - proCIntegerProj (C := C) i y :=
616 by
617 change (x - y).1 i = x.1 i - y.1 i
618 rfl
620/-- Finite projections of pro-`C` integers commute with natural-number casts. -/
621@[simp]
622theorem proCIntegerProj_natCast (i : ProCIntegerIndex C) (n : ℕ) :
623 proCIntegerProj (C := C) i (n : ProCIntegerLimitCarrier C) = n :=
624 by rfl
626/-- Finite projections of pro-`C` integers commute with integer casts. -/
627@[simp]
628theorem proCIntegerProj_intCast (i : ProCIntegerIndex C) (n : ℤ) :
629 proCIntegerProj (C := C) i (n : ProCIntegerLimitCarrier C) = n :=
630 by rfl
632/-- Projection from the pro-`C` integers to a finite cyclic stage as a ring homomorphism. -/
635 toFun := proCIntegerProj (C := C) i
636 map_zero' := by simp only [proCIntegerProj_zero]
637 map_one' := by simp only [proCIntegerProj_one]
638 map_add' := by intro x y; simp only [proCIntegerProj_add]
639 map_mul' := by intro x y; simp only [proCIntegerProj_mul]
641/-- The ring-hom version of a finite pro-`C` integer projection evaluates to the projection map. -/
642@[simp]
644 proCIntegerProjRingHom (C := C) i x = proCIntegerProj (C := C) i x :=
645 by rfl
647/-- Each finite projection from the pro-`C` integer ring is continuous. -/
649 Continuous (proCIntegerProj (C := C) i) :=
650 (continuous_apply i).comp continuous_subtype_val
652/-- Compatibility of the finite projections with reduction maps. -/
653theorem proCIntegerProj_transition {i j : ProCIntegerIndex C} (hij : i ≤ j)
655 proCIntegerTransition (C := C) hij (proCIntegerProj (C := C) j x) =
656 proCIntegerProj (C := C) i x :=
657 x.2 i j hij
659/-- The `ULift`ed multiplicative finite cyclic stage belongs to the indexing class. -/
661 {C : FiniteGroupClass.{u}} (i : ProCIntegerIndex C) :
662 C (ULift (Multiplicative (ProCIntegerStage C i))) := by
663 simpa [ProCIntegerStage] using i.cyclic_mem
665/-- Type-0 descent of `ulift_multiplicative_proCIntegerStage_mem`. -/
667 {C : FiniteGroupClass.{0}}
668 (hIso : FiniteGroupClass.IsomClosed C) (i : ProCIntegerIndex C) :
669 C (Multiplicative (ProCIntegerStage C i)) := by
670 let e : ULift (Multiplicative (ProCIntegerStage C i)) ≃*
671 Multiplicative (ProCIntegerStage C i) := {
672 toFun x := x.down
673 invFun x := ULift.up x
674 left_inv := by
675 intro x
676 cases x
677 rfl
678 right_inv := by
679 intro x
680 rfl
681 map_mul' := by
682 intro x y
683 rfl }
684 exact hIso ⟨e⟩ i.cyclic_mem
686/-- Each finite multiplicative cyclic stage is a finite discrete pro-`C` group when `C` is
687quotient-closed. -/
689 {C : FiniteGroupClass.{0}}
690 (hIso : FiniteGroupClass.IsomClosed C)
691 (hQuot : FiniteGroupClass.QuotientClosed C)
693 ProCGroups.ProC.IsProCGroup C (Multiplicative (ProCIntegerStage C i)) := by
694 haveI : NeZero i.modulus := ⟨Nat.ne_of_gt i.positive⟩
695 haveI : Fintype (ZMod i.modulus) := ZMod.fintype i.modulus
696 haveI : Finite (Multiplicative (ProCIntegerStage C i)) := by
697 have hfinZ : Finite (ZMod i.modulus) := Finite.of_fintype _
699 exact @Finite.of_equiv _ _ hfinZ Multiplicative.toAdd
700 haveI : DiscreteTopology (Multiplicative (ProCIntegerStage C i)) := by
702 infer_instance
704 (G := Multiplicative (ProCIntegerStage C i)) hQuot
707/-- The group-valued inverse system obtained from the finite cyclic coefficient stages. -/
708def proCIntegerMultiplicativeSystem (C : FiniteGroupClass.{0}) :
710 X := fun i => Multiplicative (ProCIntegerStage C i)
711 topologicalSpace := fun _ => inferInstance
712 map := fun {i j} hij =>
713 (proCIntegerTransition (C := C) hij).toAddMonoidHom.toMultiplicative
714 continuous_map := by
715 intro i j hij
716 exact continuous_of_discreteTopology
717 map_id := by
718 intro i
719 ext x
720 apply Multiplicative.ext
721 change proCIntegerTransition (C := C) (le_rfl : i ≤ i) x.toAdd = x.toAdd
722 simp only [proCIntegerTransition, ZMod.castHom_self, RingHom.id_apply]
723 map_comp := by
724 intro i j k hij hjk
725 ext x
726 apply Multiplicative.ext
727 change
729 (proCIntegerTransition (C := C) hjk x.toAdd) =
730 proCIntegerTransition (C := C) (hij.trans hjk) x.toAdd
731 exact congrArg (fun f : ZMod k.modulus →+* ZMod i.modulus => f x.toAdd)
732 (ZMod.castHom_comp hij hjk)
735 (C : FiniteGroupClass.{0}) (i : ProCIntegerIndex C) :
736 Group ((proCIntegerMultiplicativeSystem C).X i) := by
738 infer_instance
741 (C : FiniteGroupClass.{0}) (i : ProCIntegerIndex C) :
742 IsTopologicalGroup ((proCIntegerMultiplicativeSystem C).X i) := by
744 infer_instance
746/-- The multiplicative pro-`C` integer stages form a group-valued inverse system. -/
748 (C : FiniteGroupClass.{0}) :
751 map_one := by
752 intro i j hij
754 apply Multiplicative.ext
755 exact map_zero (proCIntegerTransition (C := C) hij)
756 map_mul := by
757 intro i j hij x y
759 apply Multiplicative.ext
760 exact map_add (proCIntegerTransition (C := C) hij) x.toAdd y.toAdd
761 map_inv := by
762 intro i j hij x
764 apply Multiplicative.ext
765 exact map_neg (proCIntegerTransition (C := C) hij) x.toAdd
767/-- The inverse limit of the multiplicative finite stages is the multiplicative group underlying
768the pro-`C` integers. -/
770 (C : FiniteGroupClass.{0}) :
771 (proCIntegerMultiplicativeSystem C).inverseLimit ≃ₜ*
772 Multiplicative (ProCIntegerLimitCarrier C) := by
774 refine
775 { toMulEquiv := ?_
776 continuous_toFun := ?_
777 continuous_invFun := ?_ }
778 · refine
779 { toFun := fun x =>
780 Multiplicative.ofAdd
781 (⟨fun i => (S.projection i x).toAdd, by
782 intro i j hij
783 exact congrArg Multiplicative.toAdd (S.projection_compatible x i j hij)⟩ :
785 invFun := fun x =>
786 (⟨fun i => Multiplicative.ofAdd (proCIntegerProj (C := C) i x.toAdd), by
787 intro i j hij
788 apply Multiplicative.ext
789 exact proCIntegerProj_transition (C := C) hij x.toAdd⟩ :
790 S.inverseLimit)
791 left_inv := by
792 intro x
793 apply S.ext
794 intro i
795 rfl
796 right_inv := by
797 intro x
798 apply Multiplicative.ext
799 ext i
800 rfl
801 map_mul' := by
802 intro x y
803 apply Multiplicative.ext
804 ext i
805 rfl }
806 · refine continuous_ofAdd.comp ?_
807 have hambient : Continuous fun x : S.inverseLimit =>
808 (fun i : ProCIntegerIndex C => (S.projection i x).toAdd :
809 ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) := by
810 exact continuous_pi fun i => continuous_toAdd.comp (S.continuous_projection i)
811 exact Continuous.subtype_mk hambient (fun x => by
812 intro i j hij
813 exact congrArg Multiplicative.toAdd (S.projection_compatible x i j hij))
814 · have hambient : Continuous fun x : Multiplicative (ProCIntegerLimitCarrier C) =>
815 (fun i : ProCIntegerIndex C =>
816 Multiplicative.ofAdd (proCIntegerProj (C := C) i x.toAdd) :
817 ∀ i : ProCIntegerIndex C, S.X i) := by
818 exact continuous_pi fun i =>
819 continuous_ofAdd.comp
820 ((continuous_proCIntegerProj (C := C) i).comp continuous_toAdd)
821 exact Continuous.subtype_mk hambient (fun x => by
822 intro i j hij
823 apply Multiplicative.ext
824 exact proCIntegerProj_transition (C := C) hij x.toAdd)
826/-- A directed pro-`C` integer coefficient system has a pro-`C` multiplicative inverse limit. -/
828 {C : FiniteGroupClass.{0}}
829 [Nonempty (ProCIntegerIndex C)]
830 (hIso : FiniteGroupClass.IsomClosed C)
831 (hQuot : FiniteGroupClass.QuotientClosed C)
832 (hdir : Directed (· ≤ ·) (id : ProCIntegerIndex C → ProCIntegerIndex C)) :
833 ProCGroups.ProC.IsProCGroup C (proCIntegerMultiplicativeSystem C).inverseLimit := by
835 letI : ∀ i : ProCIntegerIndex C, IsTopologicalGroup (S.X i) := fun i => by
837 infer_instance
838 exact ProCGroups.ProC.inverseLimit (S := S) hIso hQuot hdir
840 (C := C) hIso hQuot i)
842/-- The compatibility condition defining pro-`C` integers is closed in the product of the finite
843cyclic stages. -/
845 IsClosed {x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i |
847 simp only [ProCIntegerCompatible, Set.setOf_forall]
848 refine isClosed_iInter fun i => isClosed_iInter fun j => isClosed_iInter fun hij => ?_
849 have hleft :
850 Continuous fun x : (∀ k : ProCIntegerIndex C, ProCIntegerStage C k) =>
851 proCIntegerTransition (C := C) hij (x j) := by
852 exact (continuous_of_discreteTopology :
853 Continuous (proCIntegerTransition (C := C) hij)).comp (continuous_apply j)
854 exact isClosed_eq hleft (continuous_apply i)
856/-- The pro-`C` integers are compact as a closed subspace of the product of finite cyclic stages. -/
858 letI : ∀ i : ProCIntegerIndex C, CompactSpace (ProCIntegerStage C i) := fun i => by
859 haveI : NeZero i.modulus := ⟨Nat.ne_of_gt i.positive⟩
861 infer_instance
862 let hs : IsClosed {x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i |
865 simpa [ProCIntegerLimitCarrier] using hs.isClosedEmbedding_subtypeVal.compactSpace
867/-- The pro-`C` integers are Hausdorff as a subtype of the product of finite discrete stages. -/
869 change T2Space {x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i //
871 infer_instance
873/-- Addition on pro-`C` integers is continuous because all finite projections are continuous. -/
874instance instContinuousAddProCInteger : ContinuousAdd (ProCIntegerLimitCarrier C) where
875 continuous_add := by
876 refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun p => (p.1 + p.2).2)
877 change Continuous fun p : ProCIntegerLimitCarrier C × ProCIntegerLimitCarrier C =>
878 proCIntegerProj (C := C) i p.1 + proCIntegerProj (C := C) i p.2
879 exact ((continuous_proCIntegerProj (C := C) i).comp continuous_fst).add
880 ((continuous_proCIntegerProj (C := C) i).comp continuous_snd)
882/-- Multiplication on pro-`C` integers is continuous because all finite projections are
883continuous. -/
884instance instContinuousMulProCInteger : ContinuousMul (ProCIntegerLimitCarrier C) where
885 continuous_mul := by
886 refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun p => (p.1 * p.2).2)
887 change Continuous fun p : ProCIntegerLimitCarrier C × ProCIntegerLimitCarrier C =>
888 proCIntegerProj (C := C) i p.1 * proCIntegerProj (C := C) i p.2
889 exact ((continuous_proCIntegerProj (C := C) i).comp continuous_fst).mul
890 ((continuous_proCIntegerProj (C := C) i).comp continuous_snd)
892/-- Negation on pro-`C` integers is continuous because all finite projections are continuous. -/
893instance instContinuousNegProCInteger : ContinuousNeg (ProCIntegerLimitCarrier C) where
894 continuous_neg := by
895 refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun x => (-x).2)
896 change Continuous fun x : ProCIntegerLimitCarrier C => -proCIntegerProj (C := C) i x
899/-- The pro-`C` integer ring is a topological ring. -/
900instance instIsTopologicalRingProCInteger : IsTopologicalRing (ProCIntegerLimitCarrier C) := by
901 letI : ContinuousAdd (ProCIntegerLimitCarrier C) := instContinuousAddProCInteger (C := C)
902 letI : ContinuousMul (ProCIntegerLimitCarrier C) := instContinuousMulProCInteger (C := C)
903 letI : ContinuousNeg (ProCIntegerLimitCarrier C) := instContinuousNegProCInteger (C := C)
904 letI : IsTopologicalSemiring (ProCIntegerLimitCarrier C) := IsTopologicalSemiring.mk
905 exact IsTopologicalRing.mk
907/-- The additive group underlying the pro-`C` integers, written multiplicatively, is a pro-`C`
908group whenever the coefficient indices are directed and `C` is isomorphism- and quotient-closed. -/
910 {C : FiniteGroupClass.{0}}
911 [Nonempty (ProCIntegerIndex C)]
912 (hIso : FiniteGroupClass.IsomClosed C)
913 (hQuot : FiniteGroupClass.QuotientClosed C)
914 (hdir : Directed (· ≤ ·) (id : ProCIntegerIndex C → ProCIntegerIndex C)) :
915 ProCGroups.ProC.IsProCGroup C (Multiplicative (ProCIntegerLimitCarrier C)) := by
917 have hS : ProCGroups.ProC.IsProCGroup C S.inverseLimit :=
919 (C := C) hIso hQuot hdir
923/-- Integer constants in the pro-`C` integers. -/
925 toFun n := (n : ProCIntegerLimitCarrier C)
926 map_zero' := by ext i; exact Int.cast_zero
927 map_one' := by ext i; exact Int.cast_one
928 map_add' := by intro m n; ext i; exact Int.cast_add m n
929 map_mul' := by intro m n; ext i; exact Int.cast_mul m n
931/-- Embedding an integer in the pro-`C` integers is the same as using the integer cast. -/
932@[simp]
933theorem intToProCInteger_apply (n : ℤ) :
935 by rfl
937/-- Projecting an integer embedded in the pro-`C` integers gives its residue class at that modulus. -/
938@[simp]
940 proCIntegerProj (C := C) i (intToProCInteger (C := C) n) = (n : ZMod i.modulus) :=
941 by rfl
943/-- The ordinary integers are dense in a directed pro-`C` integer carrier. -/
945 [Nonempty (ProCIntegerIndex C)]
946 (hdir : Directed (· ≤ ·) (id : ProCIntegerIndex C → ProCIntegerIndex C)) :
947 DenseRange (intToProCInteger (C := C)) := by
949 let ρ : ∀ i : ProCIntegerIndex C, ℤ → S.X i := fun i n => (n : ZMod i.modulus)
950 have hρ : S.CompatibleMaps ρ := by
951 intro i j hij
952 funext n
953 exact map_intCast (ZMod.castHom hij (ZMod i.modulus)) n
954 have hsurj : ∀ i, Function.Surjective (ρ i) := by
955 intro i
956 exact ZMod.intCast_surjective
957 have hdense : DenseRange (S.inverseLimitLift ρ hρ) :=
959 (S := S) ρ hρ hsurj hdir
963/-- All-finite pro-integer coefficient indices are directed by common multiples. -/
965 Directed (· ≤ ·)
966 (id : ProCIntegerIndex (FiniteGroupClass.allFinite : FiniteGroupClass.{u}) →
967 ProCIntegerIndex (FiniteGroupClass.allFinite : FiniteGroupClass.{u})) := by
968 intro i j
969 let n := Nat.lcm i.modulus j.modulus
970 have hn : 0 < n := Nat.lcm_pos i.positive j.positive
971 refine ⟨ProCIntegerIndex.ofAllFiniteModulus n hn, ?_, ?_⟩
972 · simpa [n] using Nat.dvd_lcm_left i.modulus j.modulus
973 · simpa [n] using Nat.dvd_lcm_right i.modulus j.modulus
975/-- The usual profinite integer coefficient group is a pro-finite group. -/
977 ProCGroups.ProC.IsProCGroup
978 (FiniteGroupClass.allFinite : FiniteGroupClass.{0})
979 (Multiplicative
980 (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))) := by
981 let C : FiniteGroupClass.{0} := FiniteGroupClass.allFinite
982 letI : Nonempty (ProCIntegerIndex C) :=
983 ⟨ProCIntegerIndex.ofAllFiniteModulus 1 Nat.zero_lt_one⟩
984 simpa [C] using
986 (C := C)
987 FiniteGroupClass.allFinite_isomClosed
988 FiniteGroupClass.allFinite_quotientClosed
991/-- The ordinary integers are dense in the profinite completion with all finite cyclic
992coefficient stages. -/
994 DenseRange (intToProCInteger
995 (C := (FiniteGroupClass.allFinite : FiniteGroupClass.{u}))) := by
996 let C : FiniteGroupClass.{u} := FiniteGroupClass.allFinite
998 let ρ : ∀ i : ProCIntegerIndex C, ℤ → S.X i := fun i n => (n : ZMod i.modulus)
999 have hρ : S.CompatibleMaps ρ := by
1000 intro i j hij
1001 funext n
1002 exact map_intCast (ZMod.castHom hij (ZMod i.modulus)) n
1003 have hsurj : ∀ i, Function.Surjective (ρ i) := by
1004 intro i
1005 exact ZMod.intCast_surjective
1006 letI : Nonempty (ProCIntegerIndex C) :=
1007 ⟨ProCIntegerIndex.ofAllFiniteModulus 1 Nat.zero_lt_one⟩
1008 have hdense : DenseRange (S.inverseLimitLift ρ hρ) :=
1014/-- The distinguished multiplicative element corresponding to `1` in the additive pro-`C`
1015integers. It is a topological generator only for suitable finite-group classes. -/
1016def proCIntegerOne : Multiplicative (ProCIntegerLimitCarrier C) :=
1017 Multiplicative.ofAdd (1 : ProCIntegerLimitCarrier C)
1019/-- The canonical homomorphism from the infinite cyclic group to multiplicative pro-`C` integers. -/
1021 Multiplicative ℤ →* Multiplicative (ProCIntegerLimitCarrier C) where
1022 toFun z := Multiplicative.ofAdd ((z.toAdd : ℤ) : ProCIntegerLimitCarrier C)
1023 map_one' := by
1024 apply Multiplicative.ext
1025 simp only [toAdd_one, Int.cast_zero, ofAdd_zero]
1026 map_mul' z w := by
1027 apply Multiplicative.ext
1028 ext i
1029 change (((z * w).toAdd : ℤ) : ProCIntegerStage C i) =
1030 ((z.toAdd : ℤ) : ProCIntegerStage C i) + ((w.toAdd : ℤ) : ProCIntegerStage C i)
1031 exact Int.cast_add z.toAdd w.toAdd
1033/-- The multiplicative integer map sends an additive integer to the corresponding multiplicative pro-`C` integer. -/
1034@[simp]
1036 multiplicativeIntToProCInteger (C := C) (Multiplicative.ofAdd n) =
1037 Multiplicative.ofAdd ((n : ℤ) : ProCIntegerLimitCarrier C) :=
1038 rfl
1040/-- The dense infinite-cyclic map sends `n` to the `n`-th power of the canonical generator. -/
1042 multiplicativeIntToProCInteger (C := C) (Multiplicative.ofAdd n) =
1043 (proCIntegerOne (C := C)) ^ n := by
1044 apply Multiplicative.ext
1045 ext i
1046 simp only [multiplicativeIntToProCInteger, MonoidHom.coe_mk, OneHom.coe_mk, toAdd_ofAdd,
1047 proCIntegerProj_intCast, proCIntegerOne, toAdd_zpow, zsmul_eq_mul, mul_one]
1049/-- The multiplicative infinite-cyclic map is dense in the ordinary profinite integers. -/
1051 DenseRange
1053 (C := (FiniteGroupClass.allFinite : FiniteGroupClass.{u}))) := by
1054 simpa [multiplicativeIntToProCInteger, intToProCInteger, DenseRange, Function.comp_def] using
1057 (C := (FiniteGroupClass.allFinite : FiniteGroupClass.{u}))))
1059/-- The distinguished element `1` topologically generates the ordinary profinite integers. -/
1062 (G := Multiplicative
1063 (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0})))
1065 (C := (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))} : Set _) := by
1066 let C : FiniteGroupClass.{0} := FiniteGroupClass.allFinite
1067 simpa [C, proCIntegerOne] using
1072/-- The ordinary profinite integers are procyclic. -/
1075 (Multiplicative
1076 (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))) := by
1078 (G := Multiplicative
1079 (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0})))
1080 (isProCGroup_multiplicative_proCInteger_allFinite.1)
1083end
1085end ProCGroups.Completion