Source: ProCGroups.Completion.ProCIntegerPrimePower
1import ProCGroups.Completion.ProCInteger
3/-!
4# Pro C Groups / Completion / Prime-Power pro-C Integer
6This module specializes the pro-C integer construction to prime-power moduli and proves the
7pro-p density, generation, and procyclicity results.
8-/
10namespace ProCGroups.Completion
12noncomputable section
14universe u
16namespace ProCIntegerIndex
18/-- The \(p^k\)-modulus coefficient index for the pro-\(p\) integer limit. -/
19def pGroupPower (p k : ℕ) [Fact (Nat.Prime p)] :
20 ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}) where
21 modulus := p ^ k
22 positive := by
23 exact Nat.pow_pos (show 0 < p from (Fact.out : Nat.Prime p).pos)
24 cyclic_mem := by
25 refine (FiniteGroupClass.memAcrossUniverses_ulift_iff
26 (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})
27 (Multiplicative (ZMod (p ^ k)))).1 ?_
28 apply FiniteGroupClass.memAcrossUniverses_of_mem
29 letI : NeZero (p ^ k) := ⟨Nat.ne_of_gt (Nat.pow_pos
30 (show 0 < p from (Fact.out : Nat.Prime p).pos))⟩
31 letI : Fintype (ZMod (p ^ k)) := ZMod.fintype (p ^ k)
32 constructor
33 · have hfinZ : Finite (ZMod (p ^ k)) := Finite.of_fintype _
34 have hfinMul : Finite (Multiplicative (ZMod (p ^ k))) :=
35 @Finite.of_equiv _ _ hfinZ Multiplicative.toAdd
36 exact @Finite.of_equiv _ _ hfinMul Equiv.ulift.symm
37 · intro g
38 refine ⟨k, ?_⟩
39 cases g with
40 | up g' =>
41 apply ULift.ext
42 change g' ^ p ^ k = 1
43 cases g' with
44 | ofAdd z =>
45 change Multiplicative.ofAdd ((p ^ k) • z) = Multiplicative.ofAdd 0
46 simp only [nsmul_eq_mul, CharP.cast_eq_zero, zero_mul, ofAdd_zero]
48/-- The prime-power coefficient index has modulus \(p ^ n\). -/
49@[simp]
50theorem modulus_pGroupPower (p k : ℕ) [Fact (Nat.Prime p)] :
51 (pGroupPower p k :
52 ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})).modulus = p ^ k :=
53 rfl
55/-- Any coefficient index for the finite \(p\)-group class is dominated by a prime-power modulus. -/
56theorem modulus_dvd_pow_of_mem_pGroup (p : ℕ) [Fact (Nat.Prime p)]
57 (i : ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})) :
58 ∃ k, i.modulus ∣ p ^ k := by
59 rcases i.cyclic_mem with ⟨H, hH, ⟨e⟩⟩
60 rcases hH with ⟨_hfin, hp⟩
61 rcases hp (e.symm (Multiplicative.ofAdd (1 : ZMod i.modulus))) with ⟨k, hk⟩
62 refine ⟨k, ?_⟩
63 letI : NeZero i.modulus := ⟨Nat.ne_of_gt i.positive⟩
64 have hk' : ((p ^ k : ℕ) : ZMod i.modulus) = 0 := by
65 have hpow :
66 (Multiplicative.ofAdd (1 : ZMod i.modulus)) ^ (p ^ k) = 1 := by
67 simpa using congrArg e hk
68 have h := congrArg Multiplicative.toAdd hpow
69 simpa using h
70 exact (ZMod.natCast_eq_zero_iff (p ^ k) i.modulus).mp hk'
72/-- The finite \(p\)-group coefficient indices for pro-\(C\) integers are directed. -/
73theorem directed_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
74 Directed (· ≤ ·)
75 (id : ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}) →
76 ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})) := by
77 intro i j
78 rcases modulus_dvd_pow_of_mem_pGroup (p := p) i with ⟨ki, hki⟩
79 rcases modulus_dvd_pow_of_mem_pGroup (p := p) j with ⟨kj, hkj⟩
80 refine ⟨pGroupPower p (ki + kj), ?_, ?_⟩
81 · exact dvd_trans hki (pow_dvd_pow p (Nat.le_add_right ki kj))
82 · exact dvd_trans hkj (pow_dvd_pow p (Nat.le_add_left kj ki))
84end ProCIntegerIndex
86/-- The distinguished element \(1\) projects to \(1\) on every prime-power coordinate. -/
87@[simp]
88theorem proCIntegerProj_pGroupPower_one (p k : ℕ) [Fact (Nat.Prime p)] :
89 proCIntegerProj
90 (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))
91 (ProCIntegerIndex.pGroupPower p k)
92 (proCIntegerOne
93 (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))).toAdd =
94 (1 : ZMod (p ^ k)) :=
95 rfl
97/-- The ordinary integers are dense in the pro-\(p\) integer coefficient ring. -/
98theorem denseRange_intToProCInteger_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
99 DenseRange (intToProCInteger
100 (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))) := by
101 let C : FiniteGroupClass.{u} := FiniteGroupClass.pGroup p
102 let S := proCIntegerSystem C
103 let φ : ∀ i : ProCIntegerIndex C, ℤ → S.X i := fun i n => (n : ZMod i.modulus)
104 have hφ : S.CompatibleMaps φ := by
105 intro i j hij
106 funext n
107 exact map_intCast (ZMod.castHom hij (ZMod i.modulus)) n
108 have hsurj : ∀ i, Function.Surjective (φ i) := by
109 intro i
110 exact ZMod.intCast_surjective
111 letI : Nonempty (ProCIntegerIndex C) := ⟨ProCIntegerIndex.pGroupPower p 0⟩
112 have hdense : DenseRange (S.inverseLimitLift φ hφ) :=
114 (S := S) φ hφ hsurj (ProCIntegerIndex.directed_pGroup (p := p))
115 have hfun :
116 (intToProCInteger (C := C) : ℤ → ProCIntegerLimitCarrier C) =
117 S.inverseLimitLift φ hφ := by
118 funext n
119 apply Subtype.ext
120 rfl
121 rw [hfun]
122 exact hdense
124/-- The multiplicative infinite-cyclic map is dense in the pro-\(p\) integers. -/
125theorem denseRange_multiplicativeIntToProCInteger_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
126 DenseRange
127 (multiplicativeIntToProCInteger
128 (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))) := by
129 let C : FiniteGroupClass.{u} := FiniteGroupClass.pGroup p
130 have hdense :
131 Dense (Set.range fun n : ℤ =>
132 (n : ProCIntegerLimitCarrier C)) :=
133 denseRange_intToProCInteger_pGroup (p := p)
134 have hdense' :
135 Dense (Set.range fun n : ℤ =>
136 Multiplicative.ofAdd (n : ProCIntegerLimitCarrier C)) := by
137 change Dense (Set.range fun n : ℤ => (n : ProCIntegerLimitCarrier C))
138 exact hdense
139 change Dense (Set.range fun z : Multiplicative ℤ =>
140 Multiplicative.ofAdd (z.toAdd : ProCIntegerLimitCarrier C))
141 have hrange :
142 Set.range (fun z : Multiplicative ℤ =>
143 Multiplicative.ofAdd (z.toAdd : ProCIntegerLimitCarrier C)) =
144 Set.range (fun n : ℤ =>
145 Multiplicative.ofAdd (n : ProCIntegerLimitCarrier C)) := by
146 ext x
147 constructor
148 · rintro ⟨z, rfl⟩
149 exact ⟨z.toAdd, rfl⟩
150 · rintro ⟨n, rfl⟩
151 exact ⟨Multiplicative.ofAdd n, rfl⟩
152 rw [hrange]
153 exact hdense'
155/-- The distinguished element 1 topologically generates the pro-\(p\) integers. -/
156theorem topologicallyGenerates_singleton_proCIntegerOne_pGroup
157 (p : ℕ) [Fact (Nat.Prime p)] :
159 (G := Multiplicative
160 (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0})))
161 ({proCIntegerOne
162 (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{0}))} : Set _) := by
163 let C : FiniteGroupClass.{0} := FiniteGroupClass.pGroup p
164 simpa [C, proCIntegerOne] using
166 (f := multiplicativeIntToProCInteger (C := C))
167 (denseRange_multiplicativeIntToProCInteger_pGroup (p := p)))
169/-- The pro-\(p\) integers have an open-normal basis of finite \(p\)-group quotients. -/
170theorem hasPGroupOpenNormalBasis_multiplicative_proCInteger_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
172 (Multiplicative
173 (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0}))) := by
174 let C : FiniteGroupClass.{0} := FiniteGroupClass.pGroup p
175 letI : Nonempty (ProCIntegerIndex C) := ⟨ProCIntegerIndex.pGroupPower p 0⟩
176 simpa [ProCGroups.ProC.HasPGroupOpenNormalBasis, C] using
177 hasOpenNormalBasisInClass_multiplicative_proCInteger
178 (C := C)
179 (FiniteGroupClass.pGroup_formation p).isomClosed
180 (FiniteGroupClass.pGroup_formation p).quotientClosed
181 (ProCIntegerIndex.directed_pGroup (p := p))
183/-- The pro-\(p\) integers have a cyclic open-normal quotient basis. -/
184theorem hasCyclicOpenNormalBasis_multiplicative_proCInteger_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
186 (Multiplicative
187 (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0}))) := by
188 letI : T2Space
189 (Multiplicative
190 (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0}))) := by
191 change T2Space
192 (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0}))
193 exact instT2SpaceProCInteger
194 (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{0}))
195 letI : TotallyDisconnectedSpace
196 (Multiplicative
197 (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0}))) := by
198 change TotallyDisconnectedSpace
199 (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0}))
200 infer_instance
202 (G := Multiplicative
203 (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0})))
204 (topologicallyGenerates_singleton_proCIntegerOne_pGroup (p := p))
206end
208end ProCGroups.Completion