ProCGroups/Completion/ProCIntegerPrimePower.lean
1import ProCGroups.Completion.ProCInteger
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/Completion/ProCIntegerPrimePower.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14Constructs pro-C integers as inverse limits of allowed finite cyclic rings and records coordinate formulas at each finite modulus.
15-/
17namespace ProCGroups.Completion
19noncomputable section
21universe u
23namespace ProCIntegerIndex
25/-- The `p^k` coefficient coordinate for `ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p)`. -/
26def pGroupPower (p k : ℕ) [Fact (Nat.Prime p)] :
27 ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}) where
28 modulus := p ^ k
29 positive := by
30 exact Nat.pow_pos (show 0 < p from (Fact.out : Nat.Prime p).pos)
31 cyclic_mem := by
32 letI : NeZero (p ^ k) := ⟨Nat.ne_of_gt (Nat.pow_pos
33 (show 0 < p from (Fact.out : Nat.Prime p).pos))⟩
34 letI : Fintype (ZMod (p ^ k)) := ZMod.fintype (p ^ k)
35 constructor
36 · have hfinZ : Finite (ZMod (p ^ k)) := Finite.of_fintype _
37 have hfinMul : Finite (Multiplicative (ZMod (p ^ k))) :=
38 @Finite.of_equiv _ _ hfinZ Multiplicative.toAdd
39 exact @Finite.of_equiv _ _ hfinMul Equiv.ulift.symm
40 · intro g
41 refine ⟨k, ?_⟩
42 cases g with
43 | up g' =>
44 apply ULift.ext
45 change g' ^ p ^ k = 1
46 cases g' with
47 | ofAdd z =>
48 change Multiplicative.ofAdd ((p ^ k) • z) = Multiplicative.ofAdd 0
49 simp only [nsmul_eq_mul, CharP.cast_eq_zero, zero_mul, ofAdd_zero]
51/-- The prime-power coefficient index has modulus `p ^ n`. -/
52@[simp]
53theorem modulus_pGroupPower (p k : ℕ) [Fact (Nat.Prime p)] :
54 (pGroupPower p k :
55 ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})).modulus = p ^ k :=
56 rfl
58/-- Any coefficient index for the finite `p`-group class is dominated by a prime-power modulus. -/
59theorem modulus_dvd_pow_of_mem_pGroup (p : ℕ)
60 (i : ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})) :
61 ∃ k, i.modulus ∣ p ^ k := by
62 rcases i.cyclic_mem with ⟨_hfin, hp⟩
63 rcases hp (ULift.up (Multiplicative.ofAdd (1 : ZMod i.modulus))) with ⟨k, hk⟩
64 refine ⟨k, ?_⟩
65 letI : NeZero i.modulus := ⟨Nat.ne_of_gt i.positive⟩
66 have hk' : ((p ^ k : ℕ) : ZMod i.modulus) = 0 := by
67 have hdown := congrArg ULift.down hk
68 change (Multiplicative.ofAdd (1 : ZMod i.modulus)) ^ (p ^ k) = 1 at hdown
69 have h := congrArg Multiplicative.toAdd hdown
70 simpa using h
71 exact (ZMod.natCast_eq_zero_iff (p ^ k) i.modulus).mp hk'
73/-- The finite `p`-group coefficient indices for pro-`C` integers are directed. -/
74theorem directed_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
75 Directed (· ≤ ·)
76 (id : ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}) →
77 ProCIntegerIndex (FiniteGroupClass.pGroup p : FiniteGroupClass.{u})) := by
78 intro i j
79 rcases modulus_dvd_pow_of_mem_pGroup (p := p) i with ⟨ki, hki⟩
80 rcases modulus_dvd_pow_of_mem_pGroup (p := p) j with ⟨kj, hkj⟩
81 refine ⟨pGroupPower p (ki + kj), ?_, ?_⟩
82 · exact dvd_trans hki (pow_dvd_pow p (Nat.le_add_right ki kj))
83 · exact dvd_trans hkj (pow_dvd_pow p (Nat.le_add_left kj ki))
87/-- The distinguished element `1` projects to `1` on every prime-power coordinate. -/
88@[simp]
89theorem proCIntegerProj_pGroupPower_one (p k : ℕ) [Fact (Nat.Prime p)] :
91 (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))
92 (ProCIntegerIndex.pGroupPower p k)
94 (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))).toAdd =
95 (1 : ZMod (p ^ k)) :=
96 rfl
98/-- The ordinary integers are dense in the pro-`p` integer coefficient ring. -/
99theorem denseRange_intToProCInteger_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
100 DenseRange (intToProCInteger
101 (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))) := by
102 let C : FiniteGroupClass.{u} := FiniteGroupClass.pGroup p
103 let S := proCIntegerSystem C
104 let φ : ∀ i : ProCIntegerIndex C, ℤ → S.X i := fun i n => (n : ZMod i.modulus)
105 have hφ : S.CompatibleMaps φ := by
106 intro i j hij
107 funext n
108 exact map_intCast (ZMod.castHom hij (ZMod i.modulus)) n
109 have hsurj : ∀ i, Function.Surjective (φ i) := by
110 intro i
111 exact ZMod.intCast_surjective
112 letI : Nonempty (ProCIntegerIndex C) := ⟨ProCIntegerIndex.pGroupPower p 0⟩
113 have hdense : DenseRange (S.inverseLimitLift φ hφ) :=
115 (S := S) φ hφ hsurj (ProCIntegerIndex.directed_pGroup (p := p))
116 simpa [C, S, φ, proCIntegerSystem, ProCIntegerLimitCarrier, ProCIntegerCompatible, intToProCInteger,
117 ProCGroups.InverseSystems.InverseSystem.inverseLimitLift] using hdense
119/-- The multiplicative infinite-cyclic map is dense in the pro-`p` integers. -/
120theorem denseRange_multiplicativeIntToProCInteger_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
121 DenseRange
123 (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))) := by
124 simpa [multiplicativeIntToProCInteger, intToProCInteger, DenseRange, Function.comp_def] using
125 (denseRange_intToProCInteger_pGroup (p := p) :
126 DenseRange (intToProCInteger
127 (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{u}))))
129/-- The distinguished element `1` topologically generates the pro-`p` integers. -/
131 (p : ℕ) [Fact (Nat.Prime p)] :
133 (G := Multiplicative
134 (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0})))
136 (C := (FiniteGroupClass.pGroup p : FiniteGroupClass.{0}))} : Set _) := by
137 let C : FiniteGroupClass.{0} := FiniteGroupClass.pGroup p
138 simpa [C, proCIntegerOne] using
140 (f := multiplicativeIntToProCInteger (C := C))
141 (denseRange_multiplicativeIntToProCInteger_pGroup (p := p)))
143/-- The pro-`p` integers are a pro-`p` group. -/
144theorem isProPGroup_multiplicative_proCInteger_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
146 (Multiplicative
147 (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0}))) := by
148 let C : FiniteGroupClass.{0} := FiniteGroupClass.pGroup p
149 letI : Nonempty (ProCIntegerIndex C) := ⟨ProCIntegerIndex.pGroupPower p 0⟩
150 simpa [ProCGroups.ProC.IsProPGroup, C] using
152 (C := C)
153 (FiniteGroupClass.pGroup_formation p).isomClosed
154 (FiniteGroupClass.pGroup_formation p).quotientClosed
155 (ProCIntegerIndex.directed_pGroup (p := p))
157/-- The pro-`p` integers are procyclic. -/
158theorem isProcyclicGroup_multiplicative_proCInteger_pGroup (p : ℕ) [Fact (Nat.Prime p)] :
160 (Multiplicative
161 (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0}))) := by
163 (G := Multiplicative
164 (ProCIntegerLimitCarrier (FiniteGroupClass.pGroup p : FiniteGroupClass.{0})))
165 ((isProPGroup_multiplicative_proCInteger_pGroup (p := p)).1)
168end
170end ProCGroups.Completion