ProCGroups/Completion/FiniteQuotientSystems.lean

1import ProCGroups.Completion.FiniteQuotientLifts

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/ProCGroups/Completion/FiniteQuotientSystems.lean

7translation_root: data/translation

8purpose: identifies the local data snapshot used to build pages/

9placement: after imports, never before imports

10-/

11/-!

12# Pro-C completion and finite quotient systems

14Organizes finite quotient systems, completion maps, finite-target factorization, and the universal property of pro-C completion.

15-/

17namespace ProCGroups.Completion

19universe u

21variable {C : ProCGroups.FiniteGroupClass.{u}}

22variable {G : Type u} [Group G]

24/-- Normal subgroups whose corresponding quotient belongs to the chosen class `C`. -/

25structure NormalSubgroupInClass (C : ProCGroups.FiniteGroupClass.{u}) (G : Type u) [Group G] where

26 toSubgroup : Subgroup G

27 normal' : toSubgroup.Normal

28 quotient_mem' : C (G ⧸ toSubgroup)

30namespace NormalSubgroupInClass

32variable {C : ProCGroups.FiniteGroupClass.{u}}

33variable {G : Type u} [Group G]

35/-- Coerce a finite-quotient index to its underlying normal subgroup. -/

36instance instCoeOutNormalSubgroupInClass : CoeOut (NormalSubgroupInClass C G) (Subgroup G) where

37 coe N := N.toSubgroup

39/-- The subgroup underlying a finite-quotient index is normal. -/

40instance instNormalCoeNormalSubgroupInClass (N : NormalSubgroupInClass C G) :

41 (N : Subgroup G).Normal :=

42 N.normal'

44/-- Order finite-quotient indices by reverse inclusion of their subgroups. -/

45instance instLENormalSubgroupInClass : LE (NormalSubgroupInClass C G) where

46 le N M := (M : Subgroup G) ≤ (N : Subgroup G)

48/-- Finite-quotient indices form a preorder under reverse inclusion. -/

49instance instPreorderNormalSubgroupInClass : Preorder (NormalSubgroupInClass C G) where

50 le := fun N M => (M : Subgroup G) ≤ (N : Subgroup G)

51 le_refl N := show (N : Subgroup G) ≤ (N : Subgroup G) from le_rfl

52 le_trans N M K hNM hMK := show (K : Subgroup G) ≤ (N : Subgroup G) from hMK.trans hNM

54/-- The quotient attached to a normal subgroup in the finite-quotient index family lies in `C`. -/

55theorem quotient_mem (N : NormalSubgroupInClass C G) :

56 C (G ⧸ (N : Subgroup G)) :=

57 N.quotient_mem'

59/-- The canonical transition map between two quotients in the finite-quotient system. -/

60def map {N M : NormalSubgroupInClass C G}

61 (hNM : (M : Subgroup G) ≤ (N : Subgroup G)) :

62 G ⧸ (M : Subgroup G) →* G ⧸ (N : Subgroup G) :=

63 QuotientGroup.map _ _ (MonoidHom.id G) hNM

65/-- These transition maps are the natural quotient epimorphisms. -/

66theorem map_surjective {N M : NormalSubgroupInClass C G}

67 (hNM : (M : Subgroup G) ≤ (N : Subgroup G)) :

68 Function.Surjective (map (C := C) (G := G) hNM) := by

69 intro x

70 rcases QuotientGroup.mk'_surjective (N : Subgroup G) x with ⟨g, rfl⟩

71 exact ⟨QuotientGroup.mk' (M : Subgroup G) g, rfl⟩

73/-- The transition map attached to a normal subgroup in class is the identity at the same level. -/

74theorem map_id (N : NormalSubgroupInClass C G) :

75 map (C := C) (G := G)

76 (le_rfl : (N : Subgroup G) ≤ (N : Subgroup G)) = MonoidHom.id _ := by

77 simp only [map, QuotientGroup.map_id]

79/-- Transition maps between normal-subgroup-in-class quotients compose along inclusions. -/

80theorem map_comp {N M K : NormalSubgroupInClass C G}

81 (hNM : (M : Subgroup G) ≤ (N : Subgroup G))

82 (hMK : (K : Subgroup G) ≤ (M : Subgroup G)) :

83 (map (C := C) (G := G) hNM).comp (map (C := C) (G := G) hMK) =

84 map (C := C) (G := G) (hMK.trans hNM) := by

85 simpa [map] using QuotientGroup.map_comp_map

86 (N := (K : Subgroup G)) (M := (M : Subgroup G)) (O := (N : Subgroup G))

87 (f := MonoidHom.id G) (g := MonoidHom.id G) hMK hNM

89end NormalSubgroupInClass

91/-- The inverse system of quotients `G/N`, indexed by reverse inclusion.

93The coordinates carry the discrete topology, matching the finite-quotient setting. -/

94def normalSubgroupInClassSystem (C : ProCGroups.FiniteGroupClass.{u}) (G : Type u) [Group G] :

95 ProCGroups.InverseSystems.InverseSystem (I := NormalSubgroupInClass C G) where

96 X := fun N => G ⧸ (N : Subgroup G)

97 topologicalSpace := fun _ => ⊥

98 map := fun {N M} hNM =>

99 NormalSubgroupInClass.map (C := C) (G := G) (N := N) (M := M)

100 (show (M : Subgroup G) ≤ (N : Subgroup G) from hNM)

101 continuous_map := by

102 intro N M hNM

103 letI : TopologicalSpace (G ⧸ (M : Subgroup G)) := ⊥

104 letI : TopologicalSpace (G ⧸ (N : Subgroup G)) := ⊥

105 letI : DiscreteTopology (G ⧸ (M : Subgroup G)) := ⟨rfl⟩

106 exact continuous_of_discreteTopology

107 map_id := by

108 intro N

109 ext g

110 rcases QuotientGroup.mk'_surjective (N : Subgroup G) g with ⟨x, rfl⟩

111 rfl

112 map_comp := by

113 intro N M K hNM hMK

114 ext g

115 rcases QuotientGroup.mk'_surjective (K : Subgroup G) g with ⟨x, rfl⟩

116 rfl

117

118/-- Every coordinate of `normalSubgroupInClassSystem` is a quotient group. -/

119instance instGroupNormalSubgroupInClassSystemX

120 (N : NormalSubgroupInClass C G) :

121 Group ((normalSubgroupInClassSystem C G).X N) := by

122 dsimp [normalSubgroupInClassSystem]

123 infer_instance

124

125/-- The quotient system is group-valued. -/

126instance instIsGroupSystemNormalSubgroupInClassSystem :

127 ProCGroups.InverseSystems.IsGroupSystem (normalSubgroupInClassSystem C G) where

128 map_one := by

129 intro i j hij

130 change

131 NormalSubgroupInClass.map

132 (C := C) (G := G) (N := i) (M := j)

133 (show (j : Subgroup G) ≤ (i : Subgroup G) from hij) 1 = 1

134 exact

135 (NormalSubgroupInClass.map

136 (C := C) (G := G) (N := i) (M := j)

137 (show (j : Subgroup G) ≤ (i : Subgroup G) from hij)).map_one

138 map_mul := by

139 intro i j hij x y

140 change

141 NormalSubgroupInClass.map

142 (C := C) (G := G) (N := i) (M := j)

143 (show (j : Subgroup G) ≤ (i : Subgroup G) from hij) (x * y) =

144 NormalSubgroupInClass.map

145 (C := C) (G := G) (N := i) (M := j)

146 (show (j : Subgroup G) ≤ (i : Subgroup G) from hij) x *

147 NormalSubgroupInClass.map

148 (C := C) (G := G) (N := i) (M := j)

149 (show (j : Subgroup G) ≤ (i : Subgroup G) from hij) y

150 exact

151 (NormalSubgroupInClass.map

152 (C := C) (G := G) (N := i) (M := j)

153 (show (j : Subgroup G) ≤ (i : Subgroup G) from hij)).map_mul x y

154 map_inv := by

155 intro i j hij x

156 change

157 NormalSubgroupInClass.map

158 (C := C) (G := G) (N := i) (M := j)

159 (show (j : Subgroup G) ≤ (i : Subgroup G) from hij) x⁻¹ =

160 (NormalSubgroupInClass.map

161 (C := C) (G := G) (N := i) (M := j)

162 (show (j : Subgroup G) ≤ (i : Subgroup G) from hij) x)⁻¹

163 exact

164 (NormalSubgroupInClass.map

165 (C := C) (G := G) (N := i) (M := j)

166 (show (j : Subgroup G) ≤ (i : Subgroup G) from hij)).map_inv x

167

168/-- Under the formation hypothesis, the finite-quotient indexing family is directed by reverse

169inclusion. -/

170theorem directed_normalSubgroupInClass (hForm : ProCGroups.FiniteGroupClass.Formation C) :

171 Directed (α := NormalSubgroupInClass C G) (· ≤ ·) fun N => N := by

172 intro N M

173 letI : (N : Subgroup G).Normal := N.normal'

174 letI : (M : Subgroup G).Normal := M.normal'

175 let K : NormalSubgroupInClass C G :=

176 ⟨(N : Subgroup G) ⊓ (M : Subgroup G), inferInstance,

177 ProCGroups.FiniteGroupClass.Formation.quotient_inf_mem

178 (C := C) (G := G) hForm (N : Subgroup G) (M : Subgroup G)

179 N.quotient_mem' M.quotient_mem'⟩

180 refine ⟨K, ?_, ?_⟩

181 · change ((K : Subgroup G) ≤ (N : Subgroup G))

182 exact inf_le_left

183 · change ((K : Subgroup G) ≤ (M : Subgroup G))

184 exact inf_le_right

185

186/-- The inverse-limit carrier built from the quotients `G/N` with `N ◁ G` and `G/N ∈ C`.

187

188This is the concrete carrier used in the finite-quotient construction, not the public completion

189object with its universal property. -/

190abbrev ProCCompletionLimitCarrier (C : ProCGroups.FiniteGroupClass.{u}) (G : Type u) [Group G] :=

191 (normalSubgroupInClassSystem C G).inverseLimit

192

193/-- A pro-`C` completion object: a target, its completion map, and the universal property. -/

194structure ProCCompletion

195 (T : ProCGroups.ProC.ProCTheory.{u})

196 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where

197 carrier : Type u

198 [group : Group carrier]

199 [topology : TopologicalSpace carrier]

200 [topologicalGroup : IsTopologicalGroup carrier]

201 map : G →ₜ* carrier

202 isCompletion : IsProCCompletion T.predicate G carrier map

203

204attribute [instance] ProCCompletion.group ProCCompletion.topology ProCCompletion.topologicalGroup

205

206/-- The canonical abstract homomorphism from `G` to its finite-quotient inverse-limit carrier. -/

207noncomputable def proCCompletionLimitCarrierHom

208 (C : ProCGroups.FiniteGroupClass.{u}) (G : Type u) [Group G] :

209 G →* ProCCompletionLimitCarrier C G where

210 toFun g :=

211 ⟨fun N => QuotientGroup.mk' (N : Subgroup G) g, by

212 intro N M hNM

213 rfl⟩

214 map_one' := by

215 apply (normalSubgroupInClassSystem C G).ext

216 intro N

217 rfl

218 map_mul' := by

219 intro x y

220 apply (normalSubgroupInClassSystem C G).ext

221 intro N

222 rfl

223

224/-- The canonical continuous map from a discrete group to its finite-quotient inverse-limit

225carrier. -/

226noncomputable def proCCompletionLimitCarrierMap

227 (C : ProCGroups.FiniteGroupClass.{u}) (G : Type u)

228 [Group G] [TopologicalSpace G] [DiscreteTopology G] :

229 G →ₜ* ProCCompletionLimitCarrier C G where

230 toMonoidHom := proCCompletionLimitCarrierHom C G

231 continuous_toFun := continuous_of_discreteTopology

232

233/-- Coordinatewise description of the canonical map to the pro-`C` completion. -/

234@[simp] theorem projection_proCCompletionLimitCarrierHom

235 (N : NormalSubgroupInClass C G) (g : G) :

236 (normalSubgroupInClassSystem C G).projection N (proCCompletionLimitCarrierHom C G g) =

237 QuotientGroup.mk' (N : Subgroup G) g :=

238 rfl

239

240/-- Coordinatewise description of the canonical continuous map from a discrete group. -/

241@[simp] theorem projection_proCCompletionLimitCarrierMap

242 [TopologicalSpace G] [DiscreteTopology G]

243 (N : NormalSubgroupInClass C G) (g : G) :

244 (normalSubgroupInClassSystem C G).projection N (proCCompletionLimitCarrierMap C G g) =

245 QuotientGroup.mk' (N : Subgroup G) g :=

246 rfl

247

248/-- The finite-quotient inverse-limit carrier is a pro-`C` completion once the required

249construction hypotheses are supplied explicitly. -/

250theorem proCCompletionLimitCarrier_isCompletion

251 (hForm : ProCGroups.FiniteGroupClass.Formation C)

252 [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G]

253 [IsTopologicalGroup (ProCCompletionLimitCarrier C G)]

254 (hCarrier :

255 ProCGroups.ProC.IsProCGroup C (ProCCompletionLimitCarrier C G))

256 (hdense : DenseRange (proCCompletionLimitCarrierMap C G))

257 (hlifts :

258 HasUniqueFiniteDiscreteQuotientLifts C (proCCompletionLimitCarrierMap C G)) :

259 IsProCCompletion (ProCGroups.ProC.finiteGroupClassProCPredicate C)

260 G (ProCCompletionLimitCarrier C G) (proCCompletionLimitCarrierMap C G) :=

261 isProCCompletion_of_finiteDiscreteQuotientLifts

262 (C := C) hForm hCarrier hdense hlifts

263

264end ProCGroups.Completion