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

Source: ProCGroups.Completion.ProCInteger

1import Mathlib.Topology.Instances.ZMod
2import ProCGroups.ProC.InverseLimits.Limits
3import ProCGroups.ProC.InverseLimits.Predicates
5/-!
6# `ProCGroups.Completion.ProCInteger`
8This module constructs the inverse limit of cyclic integer quotients indexed by the moduli
9admitted by a finite group class, equips it with its topological ring structure, and proves its
10profinite multiplicative and density properties.
11-/
13open scoped Topology
15namespace ProCGroups.Completion
17noncomputable section
19universe u v
21/-- A coefficient level: a positive modulus whose additive cyclic group belongs to \(C\),
22independently of the universe used to represent that finite group. -/
23structure ProCIntegerIndex (C : FiniteGroupClass.{u}) where
24 /-- The positive integer defining the coefficient ring `ZMod modulus` at this level. -/
25 modulus : ℕ
26 /-- The modulus is nonzero, as required for the finite cyclic coefficient group. -/
27 positive : 0 < modulus
28 /--
29 The multiplicative presentation of the additive cyclic group `ZMod modulus` belongs to `C`,
30 using universe-independent membership.
31 -/
32 cyclic_mem : C.MemAcrossUniverses (Multiplicative (ZMod modulus))
34namespace ProCIntegerIndex
36/-- Internal bridge from native membership of a universe lift to the universe-independent
37public membership predicate. -/
38private theorem memAcrossUniverses_of_ulift_mem
39 {C : FiniteGroupClass.{u}} {G : Type} [Group G]
40 (hG : C (ULift.{u} G)) : C.MemAcrossUniverses G :=
41 (C.memAcrossUniverses_ulift_iff G).1 (C.memAcrossUniverses_of_mem hG)
43/-- Internal bridge used when a universe-specific formation theorem needs a native carrier. -/
44private theorem ulift_mem_of_memAcrossUniverses
45 {C : FiniteGroupClass.{u}} {G : Type} [Group G]
46 (hG : C.MemAcrossUniverses G) : C (ULift.{u} G) :=
47 C.mem_of_memAcrossUniverses ((C.memAcrossUniverses_ulift_iff G).2 hG)
49/-- The order relation is the refinement relation on the corresponding data. -/
50instance instLEProCIntegerIndex (C : FiniteGroupClass.{u}) : LE (ProCIntegerIndex C) where
51 le i j := i.modulus ∣ j.modulus
53/-- The preorder is induced by refinement of the corresponding data. -/
54instance instPreorderProCIntegerIndex (C : FiniteGroupClass.{u}) : Preorder (ProCIntegerIndex C)
55 where
56 le := (· ≤ ·)
57 le_refl i := dvd_rfl
58 le_trans _ _ _ hij hjk := dvd_trans hij hjk
60/-- A coefficient index built from an allowed positive modulus. -/
61def ofModulus {C : FiniteGroupClass.{u}} (n : ℕ) (hn : 0 < n)
62 (hC : C.MemAcrossUniverses (Multiplicative (ZMod n))) : ProCIntegerIndex C where
63 modulus := n
64 positive := hn
65 cyclic_mem := hC
67/--
68The positivity certificate carried by a coefficient index, packaged for formulations requiring
69Fact.
70-/
71theorem positiveFact {C : FiniteGroupClass.{u}} (i : ProCIntegerIndex C) :
72 Fact (0 < i.modulus) :=
73 ⟨i.positive⟩
75/--
76The terminal coefficient index \(\mathbb{Z}/1\mathbb{Z}\), available when \(C\) contains trivial
77quotients.
78-/
79def terminal {C : FiniteGroupClass.{u}} (htriv : FiniteGroupClass.ContainsTrivialQuotients C) :
80 ProCIntegerIndex C where
81 modulus := 1
82 positive := Nat.zero_lt_one
83 cyclic_mem := memAcrossUniverses_of_ulift_mem (htriv.of_subsingleton inferInstance)
85/-- Every positive modulus is allowed for the all-finite class. -/
86def ofAllFiniteModulus (n : ℕ) (hn : 0 < n) :
87 ProCIntegerIndex (FiniteGroupClass.allFinite : FiniteGroupClass.{u}) where
88 modulus := n
89 positive := hn
90 cyclic_mem := memAcrossUniverses_of_ulift_mem (by
91 letI : NeZero n := ⟨Nat.ne_of_gt hn⟩
92 letI : Fintype (ZMod n) := ZMod.fintype n
93 have hfinZ : Finite (ZMod n) := Finite.of_fintype _
94 have hfinMul : Finite (Multiplicative (ZMod n)) :=
95 @Finite.of_equiv _ _ hfinZ Multiplicative.toAdd
96 exact @Finite.of_equiv _ _ hfinMul Equiv.ulift.symm)
98/-- The all-finite coefficient index has the prescribed modulus. -/
99@[simp]
100theorem modulus_ofAllFiniteModulus (n : ℕ) (hn : 0 < n) :
101 (ofAllFiniteModulus n hn).modulus = n :=
102 rfl
104/--
105The order of an element of a finite \(C\)-group is an allowed coefficient modulus for hereditary
106classes.
107-/
108def ofElementOrder {C : FiniteGroupClass.{u}}
109 (hHer : FiniteGroupClass.Hereditary C)
110 {K : Type u} [Group K] [Finite K] (hK : C K) (k : K) :
111 ProCIntegerIndex C := by
112 letI : NeZero (orderOf k) := ⟨Nat.ne_of_gt (orderOf_pos k)⟩
113 refine ofModulus (orderOf k) (orderOf_pos k) ?_
114 let fInt : ℤ →+ Additive (Subgroup.zpowers k) :=
115 { toFun := fun z => Additive.ofMul ⟨k ^ z, z, rfl⟩
116 map_zero' := by
117 apply Additive.ext
118 ext
119 simp only [zpow_zero, toMul_ofMul, toMul_zero, OneMemClass.coe_one]
120 map_add' a b := by
121 apply Additive.ext
122 ext
123 simp only [zpow_add, toMul_ofMul, toMul_add, Subgroup.coe_mul]}
124 have hfInt_order : fInt (orderOf k) = 0 := by
125 apply Additive.ext
126 ext
127 change k ^ ((orderOf k : ℕ) : ℤ) = 1
128 simp only [zpow_natCast, pow_orderOf_eq_one]
129 let fZ : ZMod (orderOf k) →+ Additive (Subgroup.zpowers k) :=
130 (ZMod.lift (orderOf k)) ⟨fInt, hfInt_order⟩
131 have hfZ_inj : Function.Injective fZ := by
132 rw [ZMod.lift_injective]
133 intro m hm
134 have hpow : k ^ m = 1 := by
135 have hm' : (⟨k ^ m, m, rfl⟩ : Subgroup.zpowers k) = 1 := by
136 change (fInt m).toMul = (0 : Additive (Subgroup.zpowers k)).toMul
137 exact congrArg Additive.toMul hm
138 simpa using congrArg Subtype.val hm'
139 exact (ZMod.intCast_zmod_eq_zero_iff_dvd m (orderOf k)).2
140 ((orderOf_dvd_iff_zpow_eq_one (x := k) (i := m)).2 hpow)
141 let φ0 : Multiplicative (ZMod (orderOf k)) →* Subgroup.zpowers k :=
142 AddMonoidHom.toMultiplicativeLeft fZ
143 let uliftDown :
144 ULift (Multiplicative (ZMod (orderOf k))) →*
145 Multiplicative (ZMod (orderOf k)) :=
146 { toFun := fun x => x.down
147 map_one' := rfl
148 map_mul' := by
149 intro x y
150 cases x
151 cases y
152 rfl }
153 let φ : ULift (Multiplicative (ZMod (orderOf k))) →* K :=
154 (Subgroup.zpowers k).subtype.comp (φ0.comp uliftDown)
155 have hφ_inj : Function.Injective φ := by
156 intro a b hab
157 have hval :
158 ((φ0 a.down : Subgroup.zpowers k) : K) =
159 ((φ0 b.down : Subgroup.zpowers k) : K) := by
160 simpa [φ, uliftDown] using hab
161 have hsub : φ0 a.down = φ0 b.down := Subtype.ext hval
162 have hadd : fZ a.down.toAdd = fZ b.down.toAdd := by
163 apply Additive.ext
164 simpa [φ0] using hsub
165 have hz : a.down.toAdd = b.down.toAdd := hfZ_inj hadd
166 apply ULift.ext
167 exact Multiplicative.ext hz
168 exact memAcrossUniverses_of_ulift_mem (hHer.of_injective hK φ hφ_inj)
170/-- Formation closure makes the allowed coefficient moduli directed by common multiples. -/
171theorem directed_of_formation {C : FiniteGroupClass.{u}} (hForm : FiniteGroupClass.Formation C) :
172 Directed (· ≤ ·) (id : ProCIntegerIndex C → ProCIntegerIndex C) := by
173 classical
174 intro i j
175 let n := Nat.lcm i.modulus j.modulus
176 have hn : 0 < n := Nat.lcm_pos i.positive j.positive
177 have hi : i.modulus ∣ n := Nat.dvd_lcm_left i.modulus j.modulus
178 have hj : j.modulus ∣ n := Nat.dvd_lcm_right i.modulus j.modulus
179 let A : Type u := ULift.{u} (Multiplicative (ZMod n))
180 let K : ULift Bool → Type u
181 | ⟨false⟩ => ULift.{u} (Multiplicative (ZMod i.modulus))
182 | ⟨true⟩ => ULift.{u} (Multiplicative (ZMod j.modulus))
183 letI : ∀ b : ULift Bool, Group (K b) := by
184 intro b
185 cases b with
186 | up b =>
187 cases b <;> infer_instance
188 let f : A →* (∀ b : ULift Bool, K b) := {
189 toFun := fun x b => by
190 cases b with
191 | up b =>
192 cases b
193 · exact ULift.up
194 (Multiplicative.ofAdd (ZMod.castHom hi (ZMod i.modulus) x.down.toAdd))
195 · exact ULift.up
196 (Multiplicative.ofAdd (ZMod.castHom hj (ZMod j.modulus) x.down.toAdd))
197 map_one' := by
198 funext b
199 cases b with
200 | up b =>
201 cases b
202 · change
203 ULift.up
204 (Multiplicative.ofAdd
205 (ZMod.castHom hi (ZMod i.modulus) (0 : ZMod n))) =
206 (1 : ULift (Multiplicative (ZMod i.modulus)))
207 ext
208 simp only [ZMod.castHom_apply, ZMod.cast_zero, ofAdd_zero, toAdd_one, ULift.one_down]
209 · change
210 ULift.up
211 (Multiplicative.ofAdd
212 (ZMod.castHom hj (ZMod j.modulus) (0 : ZMod n))) =
213 (1 : ULift (Multiplicative (ZMod j.modulus)))
214 ext
215 simp only [ZMod.castHom_apply, ZMod.cast_zero, ofAdd_zero, toAdd_one, ULift.one_down]
216 map_mul' := by
217 intro x y
218 funext b
219 cases b with
220 | up b =>
221 cases b
222 · cases x with
223 | up x =>
224 cases y with
225 | up y =>
226 change
227 ULift.up
228 (Multiplicative.ofAdd
229 (ZMod.castHom hi (ZMod i.modulus) (x.toAdd + y.toAdd))) =
230 ULift.up
231 (Multiplicative.ofAdd
232 (ZMod.castHom hi (ZMod i.modulus) x.toAdd +
233 ZMod.castHom hi (ZMod i.modulus) y.toAdd))
234 ext
235 exact (ZMod.castHom hi (ZMod i.modulus)).map_add x.toAdd y.toAdd
236 · cases x with
237 | up x =>
238 cases y with
239 | up y =>
240 change
241 ULift.up
242 (Multiplicative.ofAdd
243 (ZMod.castHom hj (ZMod j.modulus) (x.toAdd + y.toAdd))) =
244 ULift.up
245 (Multiplicative.ofAdd
246 (ZMod.castHom hj (ZMod j.modulus) x.toAdd +
247 ZMod.castHom hj (ZMod j.modulus) y.toAdd))
248 ext
249 exact (ZMod.castHom hj (ZMod j.modulus)).map_add x.toAdd y.toAdd
250 }
251 have hf : Function.Injective f := by
252 intro x y hxy
253 have hfalse :
254 ZMod.castHom hi (ZMod i.modulus) x.down.toAdd =
255 ZMod.castHom hi (ZMod i.modulus) y.down.toAdd := by
256 simpa [f, K] using congrFun hxy ⟨false⟩
257 have htrue :
258 ZMod.castHom hj (ZMod j.modulus) x.down.toAdd =
259 ZMod.castHom hj (ZMod j.modulus) y.down.toAdd := by
260 simpa [f, K] using congrFun hxy ⟨true⟩
261 rcases ZMod.intCast_surjective x.down.toAdd with ⟨a, ha⟩
262 rcases ZMod.intCast_surjective y.down.toAdd with ⟨b, hb⟩
263 have hiab : (i.modulus : ℤ) ∣ a - b := by
264 rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]
265 rw [Int.cast_sub, sub_eq_zero]
266 have ha_i :
267 ZMod.castHom hi (ZMod i.modulus) x.down.toAdd = (a : ZMod i.modulus) := by
268 simp only [← ha, map_intCast]
269 have hb_i :
270 ZMod.castHom hi (ZMod i.modulus) y.down.toAdd = (b : ZMod i.modulus) := by
271 simp only [← hb, map_intCast]
272 exact ha_i.symm.trans (hfalse.trans hb_i)
273 have hjab : (j.modulus : ℤ) ∣ a - b := by
274 rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]
275 rw [Int.cast_sub, sub_eq_zero]
276 have ha_j :
277 ZMod.castHom hj (ZMod j.modulus) x.down.toAdd = (a : ZMod j.modulus) := by
278 simp only [← ha, map_intCast]
279 have hb_j :
280 ZMod.castHom hj (ZMod j.modulus) y.down.toAdd = (b : ZMod j.modulus) := by
281 simp only [← hb, map_intCast]
282 exact ha_j.symm.trans (htrue.trans hb_j)
283 have hnab_nat : n ∣ (a - b).natAbs := by
284 exact Nat.lcm_dvd ((Int.natCast_dvd).1 hiab) ((Int.natCast_dvd).1 hjab)
285 have hnab : (n : ℤ) ∣ a - b := (Int.natCast_dvd).2 hnab_nat
286 have hab : (a : ZMod n) = (b : ZMod n) := by
287 rw [← sub_eq_zero, ← Int.cast_sub, ZMod.intCast_zmod_eq_zero_iff_dvd]
288 exact hnab
289 have hxy_add : x.down.toAdd = y.down.toAdd := by
290 calc
291 x.down.toAdd = (a : ZMod n) := ha.symm
292 _ = (b : ZMod n) := hab
293 _ = y.down.toAdd := hb
294 apply ULift.ext
295 exact Multiplicative.ext hxy_add
296 have hsurj : ∀ b : ULift Bool,
297 Function.Surjective fun g : A => f g b := by
298 intro b
299 cases b with
300 | up b =>
301 cases b
302 · intro y
303 rcases ZMod.castHom_surjective hi y.down.toAdd with ⟨x, hx⟩
304 refine ⟨ULift.up (Multiplicative.ofAdd x), ?_⟩
305 cases y
306 apply ULift.ext
307 apply Multiplicative.ext
308 exact hx
309 · intro y
310 rcases ZMod.castHom_surjective hj y.down.toAdd with ⟨x, hx⟩
311 refine ⟨ULift.up (Multiplicative.ofAdd x), ?_⟩
312 cases y
313 apply ULift.ext
314 apply Multiplicative.ext
315 exact hx
316 have hCK : ∀ b : ULift Bool, C (K b) := by
317 intro b
318 cases b with
319 | up b =>
320 cases b
321 · simpa [K] using ulift_mem_of_memAcrossUniverses i.cyclic_mem
322 · simpa [K] using ulift_mem_of_memAcrossUniverses j.cyclic_mem
323 have hCn : C A :=
324 hForm.finiteSubdirectProductClosed f hf hsurj hCK
325 refine ⟨ofModulus n hn ?_, ?_, ?_⟩
326 · exact memAcrossUniverses_of_ulift_mem (by simpa [A] using hCn)
327 · exact hi
328 · exact hj
330/--
331In a finite \(C\)-group, a single allowed coefficient modulus is divisible by every element
332order.
333-/
334theorem exists_index_orderOf_dvd_of_finite_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, orderOf k ∣ i.modulus := by
339 classical
340 letI : Fintype K := Fintype.ofFinite K
341 have hfinset :
342 ∀ s : Finset K, ∃ i : ProCIntegerIndex C, ∀ k ∈ s, orderOf k ∣ i.modulus := by
343 intro s
344 induction s using Finset.induction with
345 | empty =>
346 exact ⟨ofElementOrder hHer hK (1 : K), by simp only [Finset.notMem_empty,
347 IsEmpty.forall_iff, implies_true]⟩
348 | insert a s has ih =>
349 rcases ih with ⟨i, hi⟩
350 let j := ofElementOrder hHer hK a
351 rcases ProCIntegerIndex.directed_of_formation (C := C) hForm i j with ⟨m, hmi, hmj⟩
352 refine ⟨m, ?_⟩
353 intro k hk
354 rw [Finset.mem_insert] at hk
355 rcases hk with hk_eq | hk
356 · subst k
357 exact dvd_trans (by rfl : orderOf a ∣ j.modulus) hmj
358 · exact dvd_trans (hi k hk) hmi
359 rcases hfinset (Finset.univ : Finset K) with ⟨i, hi⟩
360 exact ⟨i, fun k => hi k (Finset.mem_univ k)⟩
362/-- In a finite \(C\)-group, some allowed coefficient modulus kills every element. -/
363theorem exists_index_kills_finite_group_of_mem {C : FiniteGroupClass.{u}}
364 (hForm : FiniteGroupClass.Formation C)
365 (hHer : FiniteGroupClass.Hereditary C)
366 {K : Type u} [Group K] [Finite K] (hK : C K) :
367 ∃ i : ProCIntegerIndex C, ∀ k : K, k ^ i.modulus = 1 := by
368 rcases exists_index_orderOf_dvd_of_finite_mem
369 (C := C) hForm hHer hK with ⟨i, hi⟩
370 exact ⟨i, fun k =>
371 (orderOf_dvd_iff_pow_eq_one (x := k) (n := i.modulus)).1 (hi k)⟩
373end ProCIntegerIndex
375variable (C : FiniteGroupClass.{u})
377/-- The finite cyclic stage \(\mathbb{Z}/n\mathbb{Z}\) of the pro-\(C\) integers. -/
378abbrev ProCIntegerStage (i : ProCIntegerIndex C) : Type :=
379 ZMod i.modulus
381/-- The transition map between finite stages is induced by the corresponding quotient map. -/
382def proCIntegerTransition {i j : ProCIntegerIndex C} (hij : i ≤ j) :
383 ProCIntegerStage C j →+* ProCIntegerStage C i :=
384 ZMod.castHom hij (ZMod i.modulus)
386/-- The finite cyclic stages defining the pro-\(C\) integers as an inverse system. -/
387def proCIntegerSystem : ProCGroups.InverseSystems.InverseSystem (I := ProCIntegerIndex C) where
388 X := ProCIntegerStage C
389 topologicalSpace := fun _ => inferInstance
390 map := fun {i j} hij => proCIntegerTransition (C := C) hij
391 continuous_map := by
392 intro i j hij
393 exact continuous_of_discreteTopology
394 map_id := by
395 intro i
396 ext x
397 simp only [proCIntegerTransition, ZMod.castHom_self, RingHom.id_apply, id_eq]
398 map_comp := by
399 intro i j k hij hjk
400 ext x
401 exact congrArg (fun f : ZMod k.modulus →+* ZMod i.modulus => f x)
402 (ZMod.castHom_comp hij hjk)
404/-- The compatibility condition for a point of the inverse limit defining the pro-\(C\) integers. -/
405def ProCIntegerCompatible
406 (x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) : Prop :=
407 ∀ i j, ∀ hij : i ≤ j, proCIntegerTransition (C := C) hij (x j) = x i
409/--
410Explicit carrier-level name for the current inverse-limit implementation of pro-\(C\) integers.
411-/
412abbrev ProCIntegerLimitCarrier : Type _ :=
413 {x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i // ProCIntegerCompatible C x}
415/-- The projection from the pro-\(C\) integers to a finite cyclic stage. -/
416def proCIntegerProj (i : ProCIntegerIndex C) : ProCIntegerLimitCarrier C → ProCIntegerStage C i :=
417 fun x => x.1 i
419/-- Extensionality for pro-\(C\) integers through their finite cyclic projections. -/
420@[ext]
421theorem ProCIntegerLimitCarrier.ext {x y : ProCIntegerLimitCarrier C}
422 (h : ∀ i : ProCIntegerIndex C,
423 proCIntegerProj (C := C) i x = proCIntegerProj (C := C) i y) :
424 x = y :=
425 Subtype.ext (funext h)
427/--
428The zero element is defined coordinatewise as the compatible family of zero elements at all
429finite stages.
430-/
431instance instZeroProCInteger : Zero (ProCIntegerLimitCarrier C) where
432 zero := ⟨fun _ => 0, by
433 intro i j hij
434 exact map_zero (proCIntegerTransition (C := C) hij)⟩
436/--
437Addition on the pro-\(C\) integer completion is defined coordinatewise through finite quotient
438stages.
439-/
440instance instAddProCInteger : Add (ProCIntegerLimitCarrier C) where
441 add x y := ⟨fun i => x.1 i + y.1 i, by
442 intro i j hij
443 rw [map_add]
444 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
446/--
447Negation on the pro-\(C\) completed integers is defined coordinatewise through finite quotients.
448-/
449instance instNegProCInteger : Neg (ProCIntegerLimitCarrier C) where
450 neg x := ⟨fun i => -x.1 i, by
451 intro i j hij
452 rw [map_neg]
453 exact congrArg Neg.neg (x.2 i j hij)⟩
455/--
456Subtraction on the completed group algebra is defined coordinatewise through the finite-stage
457group-algebra subtractions.
458-/
459instance instSubProCInteger : Sub (ProCIntegerLimitCarrier C) where
460 sub x y := ⟨fun i => x.1 i - y.1 i, by
461 intro i j hij
462 rw [map_sub]
463 exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
465/-- The pro-\(C\) completed integers carry natural-number scalar multiplication coordinatewise. -/
466instance instSMulNatProCInteger : SMul ℕ (ProCIntegerLimitCarrier C) where
467 smul n x := ⟨fun i => n • x.1 i, by
468 intro i j hij
469 rw [map_nsmul]
470 exact congrArg (n • ·) (x.2 i j hij)⟩
472/--
473The completed group algebra carries integer scalar multiplication by applying the scalar action
474at every finite quotient stage.
475-/
476instance instSMulIntProCInteger : SMul ℤ (ProCIntegerLimitCarrier C) where
477 smul n x := ⟨fun i => n • x.1 i, by
478 intro i j hij
479 rw [map_zsmul]
480 exact congrArg (n • ·) (x.2 i j hij)⟩
482/-- The unit pro-\(C\) integer is defined coordinatewise. -/
483instance instOneProCInteger : One (ProCIntegerLimitCarrier C) where
484 one := ⟨fun _ => 1, by
485 intro i j hij
486 exact map_one (proCIntegerTransition (C := C) hij)⟩
488/--
489Multiplication on the pro-\(C\) completed integers is defined coordinatewise through finite
490quotients.
491-/
492instance instMulProCInteger : Mul (ProCIntegerLimitCarrier C) where
493 mul x y := ⟨fun i => x.1 i * y.1 i, by
494 intro i j hij
495 rw [map_mul]
496 exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩
498/--
499Natural number casts in the pro-\(C\) integer completion are computed coordinatewise from
500finite-stage natural number casts.
501-/
502instance instNatCastProCInteger : NatCast (ProCIntegerLimitCarrier C) where
503 natCast n := ⟨fun _ => n, by
504 intro i j hij
505 exact map_natCast (proCIntegerTransition (C := C) hij) n⟩
507/--
508Integer casts in the pro-\(C\) integer completion are computed coordinatewise from finite-stage
509integer casts.
510-/
511instance instIntCastProCInteger : IntCast (ProCIntegerLimitCarrier C) where
512 intCast n := ⟨fun _ => n, by
513 intro i j hij
514 exact map_intCast (proCIntegerTransition (C := C) hij) n⟩
516/-- The profinite or pro-\(C\) group object has powers computed at every finite-stage coordinate. -/
517instance instPowProCInteger : Pow (ProCIntegerLimitCarrier C) ℕ where
518 pow x n := ⟨fun i => x.1 i ^ n, by
519 intro i j hij
520 rw [map_pow]
521 exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩
523/-- The underlying compatible family of pro-\(C\) integers computes zero coordinatewise. -/
524@[simp]
525theorem coe_zero_proCInteger :
526 ((0 : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = 0 := by
527 funext i
528 rfl
530/-- The underlying compatible family of pro-\(C\) integers computes \(1\) coordinatewise. -/
531@[simp]
532theorem coe_one_proCInteger :
533 ((1 : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = 1 := by
534 funext i
535 rfl
537/-- The underlying compatible family of pro-\(C\) integers computes addition coordinatewise. -/
538@[simp]
539theorem coe_add_proCInteger (x y : ProCIntegerLimitCarrier C) :
540 ((x + y : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = x +
541 y := by
542 funext i
543 rfl
545/--
546The underlying compatible family of pro-\(C\) integers computes multiplication coordinatewise.
547-/
548@[simp]
549theorem coe_mul_proCInteger (x y : ProCIntegerLimitCarrier C) :
550 ((x * y : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = x *
551 y := by
552 funext i
553 rfl
555/-- The underlying compatible family of pro-\(C\) integers computes negation coordinatewise. -/
556@[simp]
557theorem coe_neg_proCInteger (x : ProCIntegerLimitCarrier C) :
558 ((-x : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = -x := by
559 funext i
560 rfl
562/-- The underlying compatible family of pro-\(C\) integers computes subtraction coordinatewise. -/
563@[simp]
564theorem coe_sub_proCInteger (x y : ProCIntegerLimitCarrier C) :
565 ((x - y : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = x -
566 y := by
567 funext i
568 rfl
570/--
571The underlying compatible family of pro-\(C\) integers computes natural number casts
572coordinatewise.
573-/
574@[simp]
575theorem coe_natCast_proCInteger (n : ℕ) :
576 ((n : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = n := by
577 funext i
578 rfl
580/-- The underlying compatible family of pro-\(C\) integers computes integer casts coordinatewise. -/
581@[simp]
582theorem coe_intCast_proCInteger (n : ℤ) :
583 ((n : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) =
584 fun i => (n : ProCIntegerStage C i) := by
585 funext i
586 rfl
588/-- The underlying compatible family of pro-\(C\) integers computes powers coordinatewise. -/
589@[simp]
590theorem coe_pow_proCInteger (x : ProCIntegerLimitCarrier C) (n : ℕ) :
591 ((x ^ n : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = x ^
592 n := by
593 funext i
594 rfl
596/--
597The pro-\(C\) integer completion inherits a ring structure from the compatible finite-stage
598rings.
599-/
600instance instCommRingProCInteger : CommRing (ProCIntegerLimitCarrier C) :=
601 Function.Injective.commRing
602 (fun x : ProCIntegerLimitCarrier C => (x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i))
603 Subtype.val_injective
604 (coe_zero_proCInteger (C := C))
605 (coe_one_proCInteger (C := C))
606 (coe_add_proCInteger (C := C))
607 (coe_mul_proCInteger (C := C))
608 (coe_neg_proCInteger (C := C))
609 (coe_sub_proCInteger (C := C))
610 (by intro n x; funext i; change (n • x).1 i = n • x.1 i; rfl)
611 (by intro n x; funext i; change (n • x).1 i = n • x.1 i; rfl)
612 (coe_pow_proCInteger (C := C))
613 (coe_natCast_proCInteger (C := C))
614 (coe_intCast_proCInteger (C := C))
616/-- Finite projections of pro-\(C\) integers commute with 0. -/
617@[simp]
618theorem proCIntegerProj_zero (i : ProCIntegerIndex C) :
619 proCIntegerProj (C := C) i (0 : ProCIntegerLimitCarrier C) = 0 :=
620 by rfl
622/-- Finite projections of pro-\(C\) integers commute with 1. -/
623@[simp]
624theorem proCIntegerProj_one (i : ProCIntegerIndex C) :
625 proCIntegerProj (C := C) i (1 : ProCIntegerLimitCarrier C) = 1 :=
626 by rfl
628/-- Finite projections of pro-\(C\) integers commute with addition. -/
629@[simp]
630theorem proCIntegerProj_add (i : ProCIntegerIndex C) (x y : ProCIntegerLimitCarrier C) :
631 proCIntegerProj (C := C) i (x + y) =
632 proCIntegerProj (C := C) i x + proCIntegerProj (C := C) i y :=
633 by
634 change (x + y).1 i = x.1 i + y.1 i
635 rfl
637/-- Finite projections of pro-\(C\) integers commute with multiplication. -/
638@[simp]
639theorem proCIntegerProj_mul (i : ProCIntegerIndex C) (x y : ProCIntegerLimitCarrier C) :
640 proCIntegerProj (C := C) i (x * y) =
641 proCIntegerProj (C := C) i x * proCIntegerProj (C := C) i y :=
642 by
643 change (x * y).1 i = x.1 i * y.1 i
644 rfl
646/-- Finite projections of pro-\(C\) integers commute with negation. -/
647@[simp]
648theorem proCIntegerProj_neg (i : ProCIntegerIndex C) (x : ProCIntegerLimitCarrier C) :
649 proCIntegerProj (C := C) i (-x) = -proCIntegerProj (C := C) i x :=
650 by
651 change (-x).1 i = -x.1 i
652 rfl
654/-- Finite projections of pro-\(C\) integers commute with subtraction. -/
655@[simp]
656theorem proCIntegerProj_sub (i : ProCIntegerIndex C) (x y : ProCIntegerLimitCarrier C) :
657 proCIntegerProj (C := C) i (x - y) =
658 proCIntegerProj (C := C) i x - proCIntegerProj (C := C) i y :=
659 by
660 change (x - y).1 i = x.1 i - y.1 i
661 rfl
663/-- Finite projections of pro-\(C\) integers commute with natural number casts. -/
664@[simp]
665theorem proCIntegerProj_natCast (i : ProCIntegerIndex C) (n : ℕ) :
666 proCIntegerProj (C := C) i (n : ProCIntegerLimitCarrier C) = n :=
667 by rfl
669/-- Finite projections of pro-\(C\) integers commute with integer casts. -/
670@[simp]
671theorem proCIntegerProj_intCast (i : ProCIntegerIndex C) (n : ℤ) :
672 proCIntegerProj (C := C) i (n : ProCIntegerLimitCarrier C) = n :=
673 by rfl
675/--
676The projection from the pro-\(C\) integers to a finite cyclic stage is bundled as a ring
677homomorphism.
678-/
679def proCIntegerProjRingHom (i : ProCIntegerIndex C) :
680 ProCIntegerLimitCarrier C →+* ProCIntegerStage C i where
681 toFun := proCIntegerProj (C := C) i
682 map_zero' := by simp only [proCIntegerProj_zero]
683 map_one' := by simp only [proCIntegerProj_one]
684 map_add' := by intro x y; simp only [proCIntegerProj_add]
685 map_mul' := by intro x y; simp only [proCIntegerProj_mul]
687/--
688The bundled ring homomorphism has the same underlying function as the coordinatewise
689construction.
690-/
691@[simp]
692theorem proCIntegerProjRingHom_apply (i : ProCIntegerIndex C) (x : ProCIntegerLimitCarrier C) :
693 proCIntegerProjRingHom (C := C) i x = proCIntegerProj (C := C) i x :=
694 by rfl
696/-- Each finite projection from the pro-\(C\) integer ring is continuous. -/
697theorem continuous_proCIntegerProj (i : ProCIntegerIndex C) :
698 Continuous (proCIntegerProj (C := C) i) :=
699 (continuous_apply i).comp continuous_subtype_val
701/-- Compatibility of the finite projections with reduction maps. -/
702theorem proCIntegerProj_transition {i j : ProCIntegerIndex C} (hij : i ≤ j)
703 (x : ProCIntegerLimitCarrier C) :
704 proCIntegerTransition (C := C) hij (proCIntegerProj (C := C) j x) =
705 proCIntegerProj (C := C) i x :=
706 x.2 i j hij
708/-- A finite cyclic stage belongs to `C` across universes. This is the public stage-membership API;
709it avoids exposing a Type-0 specialization or requiring a separately supplied isomorphism-closure
710hypothesis. -/
711theorem multiplicative_proCIntegerStage_mem
712 {C : FiniteGroupClass.{u}} (i : ProCIntegerIndex C) :
713 C.MemAcrossUniverses (Multiplicative (ProCIntegerStage C i)) := by
714 simpa [ProCIntegerStage] using i.cyclic_mem
716/-- Each finite multiplicative cyclic stage has an open-normal \(C\)-basis when \(C\) is
717quotient-closed. -/
718theorem hasOpenNormalBasisInClass_multiplicative_proCIntegerStage
719 {C : FiniteGroupClass.{0}}
720 (hQuot : FiniteGroupClass.QuotientClosed C)
721 (i : ProCIntegerIndex C) :
722 ProCGroups.ProC.HasOpenNormalBasisInClass C (Multiplicative (ProCIntegerStage C i)) := by
723 haveI : NeZero i.modulus := ⟨Nat.ne_of_gt i.positive⟩
724 haveI : Fintype (ZMod i.modulus) := ZMod.fintype i.modulus
725 haveI : Finite (Multiplicative (ProCIntegerStage C i)) := by
726 have hfinZ : Finite (ZMod i.modulus) := Finite.of_fintype _
727 dsimp [ProCIntegerStage]
728 exact @Finite.of_equiv _ _ hfinZ Multiplicative.toAdd
729 haveI : DiscreteTopology (Multiplicative (ProCIntegerStage C i)) := by
730 dsimp [ProCIntegerStage]
731 infer_instance
733 (G := Multiplicative (ProCIntegerStage C i)) hQuot
734 ((C.memAcrossUniverses_iff).1
735 (multiplicative_proCIntegerStage_mem (C := C) i))
737/-- The group-valued inverse system obtained from the finite cyclic coefficient stages. -/
738def proCIntegerMultiplicativeSystem (C : FiniteGroupClass.{u}) :
739 ProCGroups.InverseSystems.InverseSystem (I := ProCIntegerIndex C) where
740 X := fun i => Multiplicative (ProCIntegerStage C i)
741 topologicalSpace := fun _ => inferInstance
742 map := fun {i j} hij =>
743 (proCIntegerTransition (C := C) hij).toAddMonoidHom.toMultiplicative
744 continuous_map := by
745 intro i j hij
746 exact continuous_of_discreteTopology
747 map_id := by
748 intro i
749 ext x
750 apply Multiplicative.ext
751 change proCIntegerTransition (C := C) (le_rfl : i ≤ i) x.toAdd = x.toAdd
752 simp only [proCIntegerTransition, ZMod.castHom_self, RingHom.id_apply]
753 map_comp := by
754 intro i j k hij hjk
755 ext x
756 apply Multiplicative.ext
757 change
758 proCIntegerTransition (C := C) hij
759 (proCIntegerTransition (C := C) hjk x.toAdd) =
760 proCIntegerTransition (C := C) (hij.trans hjk) x.toAdd
761 exact congrArg (fun f : ZMod k.modulus →+* ZMod i.modulus => f x.toAdd)
762 (ZMod.castHom_comp hij hjk)
764/--
765The constructed carrier inherits its group structure from the coordinatewise group structure of
766the construction.
767-/
768instance instGroupProCIntegerMultiplicativeSystemStage
769 (C : FiniteGroupClass.{u}) (i : ProCIntegerIndex C) :
770 Group ((proCIntegerMultiplicativeSystem C).X i) := by
771 dsimp [proCIntegerMultiplicativeSystem, ProCIntegerStage]
772 infer_instance
774/-- The object is a topological group with the induced group operations and topology. -/
775instance instIsTopologicalGroupProCIntegerMultiplicativeSystemStage
776 (C : FiniteGroupClass.{u}) (i : ProCIntegerIndex C) :
777 IsTopologicalGroup ((proCIntegerMultiplicativeSystem C).X i) := by
778 haveI : NeZero i.modulus := ⟨Nat.ne_of_gt i.positive⟩
779 letI : DiscreteTopology ((proCIntegerMultiplicativeSystem C).X i) := by
780 dsimp [proCIntegerMultiplicativeSystem, ProCIntegerStage]
781 exact ⟨rfl⟩
782 exact topologicalGroup_of_discreteTopology
784/-- The pro-\(C\) integer multiplicative system carries the induced group-system structure. -/
785instance instIsGroupSystemProCIntegerMultiplicativeSystem
786 (C : FiniteGroupClass.{u}) :
788 (proCIntegerMultiplicativeSystem C) where
789 map_one := by
790 intro i j hij
791 dsimp [proCIntegerMultiplicativeSystem, ProCIntegerStage]
792 apply Multiplicative.ext
793 exact map_zero (proCIntegerTransition (C := C) hij)
794 map_mul := by
795 intro i j hij x y
796 dsimp [proCIntegerMultiplicativeSystem, ProCIntegerStage] at x y ⊢
797 apply Multiplicative.ext
798 exact map_add (proCIntegerTransition (C := C) hij) x.toAdd y.toAdd
799 map_inv := by
800 intro i j hij x
801 dsimp [proCIntegerMultiplicativeSystem, ProCIntegerStage] at x ⊢
802 apply Multiplicative.ext
803 exact map_neg (proCIntegerTransition (C := C) hij) x.toAdd
805/--
806The inverse limit of the multiplicative finite stages is the multiplicative group underlying the
807pro-\(C\) integers.
808-/
809def proCIntegerMultiplicativeLimitEquiv
810 (C : FiniteGroupClass.{u}) :
811 (proCIntegerMultiplicativeSystem C).inverseLimit ≃ₜ*
812 Multiplicative (ProCIntegerLimitCarrier C) := by
813 let S := proCIntegerMultiplicativeSystem C
814 refine
815 { toMulEquiv := ?_
816 continuous_toFun := ?_
817 continuous_invFun := ?_ }
818 · refine
819 { toFun := fun x =>
820 Multiplicative.ofAdd
821 (⟨fun i => (S.projection i x).toAdd, by
822 intro i j hij
823 exact congrArg Multiplicative.toAdd (S.projection_compatible x i j hij)⟩ :
824 ProCIntegerLimitCarrier C)
825 invFun := fun x =>
826 (⟨fun i => Multiplicative.ofAdd (proCIntegerProj (C := C) i x.toAdd), by
827 intro i j hij
828 apply Multiplicative.ext
829 exact proCIntegerProj_transition (C := C) hij x.toAdd⟩ :
830 S.inverseLimit)
831 left_inv := by
832 intro x
833 apply S.ext
834 intro i
835 rfl
836 right_inv := by
837 intro x
838 apply Multiplicative.ext
839 ext i
840 rfl
841 map_mul' := by
842 intro x y
843 apply Multiplicative.ext
844 ext i
845 rfl }
846 · refine continuous_ofAdd.comp ?_
847 have hambient : Continuous fun x : S.inverseLimit =>
848 (fun i : ProCIntegerIndex C => (S.projection i x).toAdd :
849 ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) := by
850 exact continuous_pi fun i => continuous_toAdd.comp (S.continuous_projection i)
851 exact Continuous.subtype_mk hambient (fun x => by
852 intro i j hij
853 exact congrArg Multiplicative.toAdd (S.projection_compatible x i j hij))
854 · have hambient : Continuous fun x : Multiplicative (ProCIntegerLimitCarrier C) =>
855 (fun i : ProCIntegerIndex C =>
856 Multiplicative.ofAdd (proCIntegerProj (C := C) i x.toAdd) :
857 ∀ i : ProCIntegerIndex C, S.X i) := by
858 exact continuous_pi fun i =>
859 continuous_ofAdd.comp
860 ((continuous_proCIntegerProj (C := C) i).comp continuous_toAdd)
861 exact Continuous.subtype_mk hambient (fun x => by
862 intro i j hij
863 apply Multiplicative.ext
864 exact proCIntegerProj_transition (C := C) hij x.toAdd)
866/-- A directed pro-\(C\) integer coefficient system has an open-normal \(C\)-basis on its
867multiplicative inverse limit. -/
868theorem hasOpenNormalBasisInClass_proCIntegerMultiplicativeSystem_inverseLimit
869 {C : FiniteGroupClass.{0}}
870 [Nonempty (ProCIntegerIndex C)]
871 (hIso : FiniteGroupClass.IsomClosed C)
872 (hQuot : FiniteGroupClass.QuotientClosed C)
873 (hdir : Directed (· ≤ ·) (id : ProCIntegerIndex C → ProCIntegerIndex C)) :
874 ProCGroups.ProC.HasOpenNormalBasisInClass C (proCIntegerMultiplicativeSystem C).inverseLimit
875 := by
876 let S := proCIntegerMultiplicativeSystem C
877 letI : ∀ i : ProCIntegerIndex C, IsTopologicalGroup (S.X i) := fun i => by
878 haveI : NeZero i.modulus := ⟨Nat.ne_of_gt i.positive⟩
879 letI : DiscreteTopology (S.X i) := by
880 dsimp [S, proCIntegerMultiplicativeSystem, ProCIntegerStage]
881 exact ⟨rfl⟩
882 exact topologicalGroup_of_discreteTopology
883 letI : ∀ i : ProCIntegerIndex C, CompactSpace (S.X i) := fun i => by
884 haveI : NeZero i.modulus := ⟨Nat.ne_of_gt i.positive⟩
885 dsimp [S, proCIntegerMultiplicativeSystem, ProCIntegerStage]
886 infer_instance
887 letI : ∀ i : ProCIntegerIndex C, T2Space (S.X i) := fun i => by
888 haveI : NeZero i.modulus := ⟨Nat.ne_of_gt i.positive⟩
889 letI : DiscreteTopology (S.X i) := by
890 dsimp [S, proCIntegerMultiplicativeSystem, ProCIntegerStage]
891 exact ⟨rfl⟩
892 exact DiscreteTopology.toT2Space
893 letI : ∀ i : ProCIntegerIndex C, TotallyDisconnectedSpace (S.X i) := fun i => by
894 haveI : NeZero i.modulus := ⟨Nat.ne_of_gt i.positive⟩
895 letI : DiscreteTopology (S.X i) := by
896 dsimp [S, proCIntegerMultiplicativeSystem, ProCIntegerStage]
897 exact ⟨rfl⟩
898 letI : TotallySeparatedSpace (S.X i) :=
899 TotallySeparatedSpace.of_discrete (S.X i)
900 exact TotallySeparatedSpace.totallyDisconnectedSpace (S.X i)
901 exact ProCGroups.ProC.inverseLimit (S := S) hIso hQuot hdir
902 (fun i => hasOpenNormalBasisInClass_multiplicative_proCIntegerStage
903 (C := C) hQuot i)
905/--
906The compatibility condition defining pro-\(C\) integers is closed in the product of the finite
907cyclic stages.
908-/
909theorem isClosed_setOf_proCIntegerCompatible :
910 IsClosed {x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i |
911 ProCIntegerCompatible C x} := by
912 simp only [ProCIntegerCompatible, Set.setOf_forall]
913 refine isClosed_iInter fun i => isClosed_iInter fun j => isClosed_iInter fun hij => ?_
914 have hleft :
915 Continuous fun x : (∀ k : ProCIntegerIndex C, ProCIntegerStage C k) =>
916 proCIntegerTransition (C := C) hij (x j) := by
917 exact (continuous_of_discreteTopology :
918 Continuous (proCIntegerTransition (C := C) hij)).comp (continuous_apply j)
919 exact isClosed_eq hleft (continuous_apply i)
921/--
922The constructed object carries the compact space structure inherited from its profinite
923construction.
924-/
925instance instCompactSpaceProCInteger : CompactSpace (ProCIntegerLimitCarrier C) := by
926 letI : ∀ i : ProCIntegerIndex C, CompactSpace (ProCIntegerStage C i) := fun i => by
927 haveI : NeZero i.modulus := ⟨Nat.ne_of_gt i.positive⟩
928 dsimp [ProCIntegerStage]
929 infer_instance
930 let hs : IsClosed {x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i |
931 ProCIntegerCompatible C x} :=
932 isClosed_setOf_proCIntegerCompatible (C := C)
933 change CompactSpace {x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i //
934 ProCIntegerCompatible C x}
935 exact hs.isClosedEmbedding_subtypeVal.compactSpace
937/--
938The constructed object is Hausdorff, with its \(T_2\) structure inherited from the profinite
939construction.
940-/
941instance instT2SpaceProCInteger : T2Space (ProCIntegerLimitCarrier C) := by
942 change T2Space {x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i //
943 ProCIntegerCompatible C x}
944 infer_instance
946/-- Addition on the pro-\(C\) integer completion is continuous for the inverse-limit topology. -/
947instance instContinuousAddProCInteger : ContinuousAdd (ProCIntegerLimitCarrier C) where
948 continuous_add := by
949 refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun p => (p.1 + p.2).2)
950 change Continuous fun p : ProCIntegerLimitCarrier C × ProCIntegerLimitCarrier C =>
951 proCIntegerProj (C := C) i p.1 + proCIntegerProj (C := C) i p.2
952 exact ((continuous_proCIntegerProj (C := C) i).comp continuous_fst).add
953 ((continuous_proCIntegerProj (C := C) i).comp continuous_snd)
955/--
956Multiplication on the pro-\(C\) integer completion is continuous for the inverse-limit topology.
957-/
958instance instContinuousMulProCInteger : ContinuousMul (ProCIntegerLimitCarrier C) where
959 continuous_mul := by
960 refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun p => (p.1 * p.2).2)
961 change Continuous fun p : ProCIntegerLimitCarrier C × ProCIntegerLimitCarrier C =>
962 proCIntegerProj (C := C) i p.1 * proCIntegerProj (C := C) i p.2
963 exact ((continuous_proCIntegerProj (C := C) i).comp continuous_fst).mul
964 ((continuous_proCIntegerProj (C := C) i).comp continuous_snd)
966/-- Negation on the pro-\(C\) integer completion is continuous for the inverse-limit topology. -/
967instance instContinuousNegProCInteger : ContinuousNeg (ProCIntegerLimitCarrier C) where
968 continuous_neg := by
969 refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun x => (-x).2)
970 change Continuous fun x : ProCIntegerLimitCarrier C => -proCIntegerProj (C := C) i x
971 exact (continuous_proCIntegerProj (C := C) i).neg
973/--
974The coordinatewise ring operations make the pro-\(C\) integer completion a topological ring.
975-/
976instance instIsTopologicalRingProCInteger : IsTopologicalRing (ProCIntegerLimitCarrier C) := by
977 letI : ContinuousAdd (ProCIntegerLimitCarrier C) := instContinuousAddProCInteger (C := C)
978 letI : ContinuousMul (ProCIntegerLimitCarrier C) := instContinuousMulProCInteger (C := C)
979 letI : ContinuousNeg (ProCIntegerLimitCarrier C) := instContinuousNegProCInteger (C := C)
980 letI : IsTopologicalSemiring (ProCIntegerLimitCarrier C) := IsTopologicalSemiring.mk
981 exact IsTopologicalRing.mk
983/-- The additive group underlying the pro-\(C\) integers, written multiplicatively, has an
984open-normal \(C\)-basis whenever the coefficient indices are directed and \(C\) is isomorphism- and
985quotient-closed. -/
986theorem hasOpenNormalBasisInClass_multiplicative_proCInteger
987 {C : FiniteGroupClass.{0}}
988 [Nonempty (ProCIntegerIndex C)]
989 (hIso : FiniteGroupClass.IsomClosed C)
990 (hQuot : FiniteGroupClass.QuotientClosed C)
991 (hdir : Directed (· ≤ ·) (id : ProCIntegerIndex C → ProCIntegerIndex C)) :
992 ProCGroups.ProC.HasOpenNormalBasisInClass C (Multiplicative (ProCIntegerLimitCarrier C)) := by
993 let S := proCIntegerMultiplicativeSystem C
994 have hS : ProCGroups.ProC.HasOpenNormalBasisInClass C S.inverseLimit :=
995 hasOpenNormalBasisInClass_proCIntegerMultiplicativeSystem_inverseLimit
996 (C := C) hIso hQuot hdir
998 (proCIntegerMultiplicativeLimitEquiv C)
1000/-- Integer constants in the pro-\(C\) integers. -/
1001def intToProCInteger : ℤ →+* ProCIntegerLimitCarrier C where
1002 toFun n := (n : ProCIntegerLimitCarrier C)
1003 map_zero' := by ext i; exact Int.cast_zero
1004 map_one' := by ext i; exact Int.cast_one
1005 map_add' := by intro m n; ext i; exact Int.cast_add m n
1006 map_mul' := by intro m n; ext i; exact Int.cast_mul m n
1008/-- The bundled integer embedding evaluates to the coordinatewise integer cast in the limit. -/
1009@[simp]
1010theorem intToProCInteger_apply (n : ℤ) :
1011 intToProCInteger (C := C) n = (n : ProCIntegerLimitCarrier C) :=
1012 by rfl
1014/--
1015Projecting an integer embedded in the pro-\(C\) integers gives its residue class at that
1016modulus.
1018@[simp]
1019theorem proCIntegerProj_intToProCInteger (i : ProCIntegerIndex C) (n : ℤ) :
1020 proCIntegerProj (C := C) i (intToProCInteger (C := C) n) = (n : ZMod i.modulus) :=
1021 by rfl
1023/--
1024The ordinary integers are dense in the pro-\(C\) integer completion when the coefficient indices
1025are directed.
1027theorem denseRange_intToProCInteger_of_directed
1028 [Nonempty (ProCIntegerIndex C)]
1029 (hdir : Directed (· ≤ ·) (id : ProCIntegerIndex C → ProCIntegerIndex C)) :
1030 DenseRange (intToProCInteger (C := C)) := by
1031 let S := proCIntegerSystem C
1032 let ρ : ∀ i : ProCIntegerIndex C, ℤ → S.X i := fun i n => (n : ZMod i.modulus)
1033 have hρ : S.CompatibleMaps ρ := by
1034 intro i j hij
1035 funext n
1036 exact map_intCast (ZMod.castHom hij (ZMod i.modulus)) n
1037 have hsurj : ∀ i, Function.Surjective (ρ i) := by
1038 intro i
1039 exact ZMod.intCast_surjective
1040 have hdense : DenseRange (S.inverseLimitLift ρ hρ) :=
1042 (S := S) ρ hρ hsurj hdir
1043 have hfun :
1044 (intToProCInteger (C := C) : ℤ → ProCIntegerLimitCarrier C) =
1045 S.inverseLimitLift ρ hρ := by
1046 funext n
1047 apply Subtype.ext
1048 rfl
1049 rw [hfun]
1050 exact hdense
1052/-- All-finite pro-integer coefficient indices are directed by common multiples. -/
1053theorem directed_proCIntegerIndex_allFinite :
1054 Directed (· ≤ ·)
1055 (id : ProCIntegerIndex (FiniteGroupClass.allFinite : FiniteGroupClass.{u}) →
1056 ProCIntegerIndex (FiniteGroupClass.allFinite : FiniteGroupClass.{u})) := by
1057 intro i j
1058 let n := Nat.lcm i.modulus j.modulus
1059 have hn : 0 < n := Nat.lcm_pos i.positive j.positive
1060 refine ⟨ProCIntegerIndex.ofAllFiniteModulus n hn, ?_, ?_⟩
1061 · change i.modulus ∣ n
1062 exact Nat.dvd_lcm_left i.modulus j.modulus
1063 · change j.modulus ∣ n
1064 exact Nat.dvd_lcm_right i.modulus j.modulus
1066/-- The multiplicative group of ordinary profinite integers has an open-normal basis for the
1067all-finite quotient class. -/
1068theorem hasOpenNormalBasisInClass_multiplicative_proCInteger_allFinite :
1070 (FiniteGroupClass.allFinite : FiniteGroupClass.{0})
1071 (Multiplicative
1072 (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))) := by
1073 let C : FiniteGroupClass.{0} := FiniteGroupClass.allFinite
1074 letI : Nonempty (ProCIntegerIndex C) :=
1075 ⟨ProCIntegerIndex.ofAllFiniteModulus 1 Nat.zero_lt_one⟩
1076 simpa [C] using
1077 hasOpenNormalBasisInClass_multiplicative_proCInteger
1078 (C := C)
1079 FiniteGroupClass.allFinite_isomClosed
1080 FiniteGroupClass.allFinite_quotientClosed
1081 directed_proCIntegerIndex_allFinite
1083/--
1084The ordinary integers are dense in the profinite completion with all finite cyclic coefficient
1085stages.
1087theorem denseRange_intToProCInteger_allFinite :
1088 DenseRange (intToProCInteger
1089 (C := (FiniteGroupClass.allFinite : FiniteGroupClass.{u}))) := by
1090 let C : FiniteGroupClass.{u} := FiniteGroupClass.allFinite
1091 let S := proCIntegerSystem C
1092 let ρ : ∀ i : ProCIntegerIndex C, ℤ → S.X i := fun i n => (n : ZMod i.modulus)
1093 have hρ : S.CompatibleMaps ρ := by
1094 intro i j hij
1095 funext n
1096 exact map_intCast (ZMod.castHom hij (ZMod i.modulus)) n
1097 have hsurj : ∀ i, Function.Surjective (ρ i) := by
1098 intro i
1099 exact ZMod.intCast_surjective
1100 letI : Nonempty (ProCIntegerIndex C) :=
1101 ⟨ProCIntegerIndex.ofAllFiniteModulus 1 Nat.zero_lt_one⟩
1102 have hdense : DenseRange (S.inverseLimitLift ρ hρ) :=
1104 (S := S) ρ hρ hsurj directed_proCIntegerIndex_allFinite
1105 have hfun :
1106 (intToProCInteger (C := C) : ℤ → ProCIntegerLimitCarrier C) =
1107 S.inverseLimitLift ρ hρ := by
1108 funext n
1109 apply Subtype.ext
1110 rfl
1111 rw [hfun]
1112 exact hdense
1114/--
1115The distinguished multiplicative element corresponding to \(1\) in the additive pro-\(C\)
1116integers. It is a topological generator only for suitable finite-group classes.
1118def proCIntegerOne : Multiplicative (ProCIntegerLimitCarrier C) :=
1119 Multiplicative.ofAdd (1 : ProCIntegerLimitCarrier C)
1121/--
1122The canonical homomorphism from the infinite cyclic group to multiplicative pro-\(C\) integers.
1124def multiplicativeIntToProCInteger :
1125 Multiplicative ℤ →* Multiplicative (ProCIntegerLimitCarrier C) where
1126 toFun z := Multiplicative.ofAdd ((z.toAdd : ℤ) : ProCIntegerLimitCarrier C)
1127 map_one' := by
1128 apply Multiplicative.ext
1129 simp only [toAdd_one, Int.cast_zero, ofAdd_zero]
1130 map_mul' z w := by
1131 apply Multiplicative.ext
1132 ext i
1133 change (((z * w).toAdd : ℤ) : ProCIntegerStage C i) =
1134 ((z.toAdd : ℤ) : ProCIntegerStage C i) + ((w.toAdd : ℤ) : ProCIntegerStage C i)
1135 exact Int.cast_add z.toAdd w.toAdd
1137/--
1138On the multiplicative copy of an integer `n`, the canonical cyclic homomorphism returns the
1139multiplicative form of the coordinatewise cast of `n` into the pro-\(C\) integers.
1141@[simp]
1142theorem multiplicativeIntToProCInteger_apply (n : ℤ) :
1143 multiplicativeIntToProCInteger (C := C) (Multiplicative.ofAdd n) =
1144 Multiplicative.ofAdd ((n : ℤ) : ProCIntegerLimitCarrier C) :=
1145 rfl
1147/-- The dense infinite-cyclic map sends n to the n-th power of the canonical generator. -/
1148theorem multiplicativeIntToProCInteger_zpow_one (n : ℤ) :
1149 multiplicativeIntToProCInteger (C := C) (Multiplicative.ofAdd n) =
1150 (proCIntegerOne (C := C)) ^ n := by
1151 apply Multiplicative.ext
1152 ext i
1153 simp only [multiplicativeIntToProCInteger, MonoidHom.coe_mk, OneHom.coe_mk, toAdd_ofAdd,
1154 proCIntegerProj_intCast, proCIntegerOne, toAdd_zpow, zsmul_eq_mul, mul_one]
1156/-- The multiplicative infinite-cyclic map is dense in the ordinary profinite integers. -/
1157theorem denseRange_multiplicativeIntToProCInteger_allFinite :
1158 DenseRange
1159 (multiplicativeIntToProCInteger
1160 (C := (FiniteGroupClass.allFinite : FiniteGroupClass.{u}))) := by
1161 let C : FiniteGroupClass.{u} := FiniteGroupClass.allFinite
1162 have hdense :
1163 Dense (Set.range fun n : ℤ =>
1164 (n : ProCIntegerLimitCarrier C)) :=
1165 denseRange_intToProCInteger_allFinite
1166 have hdense' :
1167 Dense (Set.range fun n : ℤ =>
1168 Multiplicative.ofAdd (n : ProCIntegerLimitCarrier C)) := by
1169 change Dense (Set.range fun n : ℤ => (n : ProCIntegerLimitCarrier C))
1170 exact hdense
1171 change Dense (Set.range fun z : Multiplicative ℤ =>
1172 Multiplicative.ofAdd (z.toAdd : ProCIntegerLimitCarrier C))
1173 have hrange :
1174 Set.range (fun z : Multiplicative ℤ =>
1175 Multiplicative.ofAdd (z.toAdd : ProCIntegerLimitCarrier C)) =
1176 Set.range (fun n : ℤ =>
1177 Multiplicative.ofAdd (n : ProCIntegerLimitCarrier C)) := by
1178 ext x
1179 constructor
1180 · rintro ⟨z, rfl⟩
1181 exact ⟨z.toAdd, rfl⟩
1182 · rintro ⟨n, rfl⟩
1183 exact ⟨Multiplicative.ofAdd n, rfl⟩
1184 rw [hrange]
1185 exact hdense'
1187/-- The distinguished element 1 topologically generates the ordinary profinite integers. -/
1188theorem topologicallyGenerates_singleton_proCIntegerOne_allFinite :
1190 (G := Multiplicative
1191 (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0})))
1192 ({proCIntegerOne
1193 (C := (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))} : Set _) := by
1194 let C : FiniteGroupClass.{0} := FiniteGroupClass.allFinite
1195 simpa [C, proCIntegerOne] using
1197 (f := multiplicativeIntToProCInteger (C := C))
1198 denseRange_multiplicativeIntToProCInteger_allFinite)
1200/-- The ordinary profinite integers have a cyclic open-normal quotient basis. -/
1201theorem hasCyclicOpenNormalBasis_multiplicative_proCInteger_allFinite :
1203 (Multiplicative
1204 (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))) := by
1205 letI : T2Space
1206 (Multiplicative
1207 (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))) := by
1208 change T2Space
1209 (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))
1210 exact instT2SpaceProCInteger
1211 (C := (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))
1212 letI : TotallyDisconnectedSpace
1213 (Multiplicative
1214 (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))) := by
1215 change TotallyDisconnectedSpace
1216 (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0}))
1217 infer_instance
1219 (G := Multiplicative
1220 (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0})))
1221 topologicallyGenerates_singleton_proCIntegerOne_allFinite
1223end
1225end ProCGroups.Completion