Yamaguchi Lean 4 Library
CrowellExactSequence/Profinite/FreeProCSourceData.lean
CrowellExactSequence/Profinite/FreeProCSourceData/Source

CrowellExactSequence/Profinite/FreeProCSourceData.lean

1import ProCGroups.FreeProC.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CrowellExactSequence/Profinite/FreeProCSourceData.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Free pro-C data for the direct completed-partials route
14This file contains only the free pro-`C` source data and the chosen finite family attached to a
15finite basis. Coordinate packages, source-refined middles, and conditional exactness routes live
16elsewhere.
17-/
19namespace CrowellExactSequence
21noncomputable section
23open scoped Pointwise Topology
24open Filter
25open ProCGroups.ProC
27universe u
29/-- Packaged carrier for a free pro-`C` group on a set converging to `1`. -/
30structure FreeProCSourceData (ProC : ProCGroupPredicate.{u}) where
31 basis : Type u
32 carrier : Type u
33 instGroup : Group carrier
34 instTopologicalSpace : TopologicalSpace carrier
35 instIsTopologicalGroup : IsTopologicalGroup carrier
36 inclusion : basis → carrier
37 isFree :
38 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
39 (ProC := ProC) basis carrier inclusion
40 proCGroup : ProCGroup ProC carrier
42attribute [instance] FreeProCSourceData.instGroup
43attribute [instance] FreeProCSourceData.instTopologicalSpace
44attribute [instance] FreeProCSourceData.instIsTopologicalGroup
46/-- The carrier of packaged free pro-`C` data is a pro-`C` group by construction. -/
47instance FreeProCSourceData.instProCGroup
48 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC) :
49 ProCGroup ProC sourceData.carrier :=
50 sourceData.proCGroup
52/-- Choose an equivalence from a finite free pro-`C` basis to `Fin n`. -/
54 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
55 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
56 sourceData.basis ≃ Fin n :=
57 Classical.choice ((Cardinal.mk_eq_nat_iff).1 hbasis)
59/-- The concrete `Fin n`-indexed family obtained from the chosen free pro-`C` basis. -/
61 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
62 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
63 Fin n → sourceData.carrier :=
64 fun i =>
65 sourceData.inclusion
66 ((freeProCChosenBasisEquivOfBasisCard (ProC := ProC) sourceData hbasis).symm i)
68/-- The universe-lifted chosen finite family. ProGroups' free pro-`C` API keeps the generator
69space in the same universe as the carrier, while `Fin n` lives in universe `0`; this is the
70canonical lifted version used when invoking that API. -/
72 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
73 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
74 ULift.{u} (Fin n) → sourceData.carrier :=
75 fun i => freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis i.down
77/-- The lifted chosen family has the same range as the concrete `Fin n` family. -/
79 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
80 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
81 Set.range (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) =
82 Set.range (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) := by
83 ext g
84 constructor
85 · rintro ⟨i, rfl⟩
86 exact ⟨i.down, rfl⟩
87 · rintro ⟨i, rfl⟩
88 exact ⟨ULift.up i, rfl⟩
90/-- The concrete `Fin n`-indexed chosen family is the same free pro-`C` converging basis,
91reindexed. This is the finite-coordinate form used by the Crowell exactness assembly. -/
93 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
94 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
95 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
96 (ProC := ProC) (Fin n) sourceData.carrier
97 (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) := by
98 let e : Fin n ≃ sourceData.basis :=
99 (freeProCChosenBasisEquivOfBasisCard (ProC := ProC) sourceData hbasis).symm
101 sourceData.isFree.precompEquiv e
103/-- The lifted chosen `Fin n`-indexed family is the same free pro-`C` converging basis,
104reindexed. -/
106 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
107 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
108 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
109 (ProC := ProC) (ULift.{u} (Fin n)) sourceData.carrier
110 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) := by
111 let e : ULift.{u} (Fin n) ≃ sourceData.basis :=
112 { toFun := fun i =>
113 (freeProCChosenBasisEquivOfBasisCard (ProC := ProC) sourceData hbasis).symm i.down
114 invFun := fun b =>
115 ULift.up ((freeProCChosenBasisEquivOfBasisCard (ProC := ProC) sourceData hbasis) b)
116 left_inv := by
117 intro i
118 cases i
119 simp only [Equiv.apply_symm_apply]
120 right_inv := by
121 intro b
122 simp only [Equiv.symm_apply_apply]}
124 sourceData.isFree.precompEquiv e
126/-- Reindexing the chosen basis by `Fin n` preserves topological generation. -/
128 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
129 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
131 (G := sourceData.carrier)
132 (Set.range (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis)) := by
133 classical
134 have hRange :
135 Set.range (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) =
136 Set.range sourceData.inclusion := by
137 ext g
138 constructor
139 · rintro ⟨i, rfl⟩
140 exact
141 ⟨(freeProCChosenBasisEquivOfBasisCard (ProC := ProC) sourceData hbasis).symm i, rfl⟩
142 · rintro ⟨b, rfl⟩
143 exact
144 ⟨(freeProCChosenBasisEquivOfBasisCard (ProC := ProC) sourceData hbasis) b, by
145 simp only [freeProCChosenFamilyOfBasisCard, Equiv.symm_apply_apply]⟩
146 simpa [hRange] using sourceData.isFree.generates_range
148/-- The image of the concrete chosen finite free basis under any map converges to `1`,
149because the indexing type is finite. -/
151 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
152 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
153 {H : Type u} [Group H] [TopologicalSpace H] (ψ : sourceData.carrier → H) :
154 ProCGroups.FreeProC.FamilyConvergesToOne
155 (G := H)
156 (fun i : Fin n =>
157 ψ (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis i)) := by
158 exact ProCGroups.FreeProC.FamilyConvergesToOne.of_finite_domain
159 (G := H)
160 (fun i : Fin n =>
161 ψ (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))
163/-- A surjective continuous homomorphism carries the chosen finite free basis to a topological
164generating family of the target. -/
166 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
167 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
168 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
169 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi) :
171 (G := H)
172 (Set.range
173 (fun i : Fin n =>
174 psi (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))) := by
175 let family : Fin n → sourceData.carrier :=
176 freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis
177 have hsourceGen :
179 (G := sourceData.carrier) (Set.range family) := by
180 simpa [family] using
181 freeProCChosenFamilyOfBasisCard_generates (ProC := ProC) sourceData hbasis
182 have himage :=
184 (G := sourceData.carrier) (H := H) psi hpsi hsourceGen
185 have hrange :
186 psi '' Set.range family = Set.range (fun i : Fin n => psi (family i)) := by
187 ext h
188 constructor
189 · rintro ⟨g, ⟨i, rfl⟩, rfl⟩
190 exact ⟨i, rfl⟩
191 · rintro ⟨i, rfl⟩
192 exact ⟨family i, ⟨i, rfl⟩, rfl⟩
193 simpa [family, hrange] using himage
195/-- The universe-lifted chosen family also topologically generates the free pro-`C` source. -/
197 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
198 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n) :
200 (G := sourceData.carrier)
201 (Set.range (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)) := by
202 simpa [freeProCChosenULiftFamilyOfBasisCard_range (ProC := ProC) sourceData hbasis] using
203 freeProCChosenFamilyOfBasisCard_generates (ProC := ProC) sourceData hbasis
205/-- The image of the finite lifted basis under any target homomorphism converges to `1` in the
206converging-set sense used by the free pro-`C` API. -/
208 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
209 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
210 {H : Type u} [Group H] [TopologicalSpace H]
211 (ψ : sourceData.carrier →* H) :
212 ProCGroups.FreeProC.FamilyConvergesToOne
213 (G := H)
214 (fun i : ULift.{u} (Fin n) =>
215 ψ (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i)) := by
216 exact ProCGroups.FreeProC.FamilyConvergesToOne.of_finite_domain
217 (G := H)
218 (fun i : ULift.{u} (Fin n) =>
219 ψ (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))
221/-- A surjective continuous homomorphism carries the lifted chosen finite free basis to a
222topological generating family of the target. -/
224 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
225 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
226 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
227 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi) :
229 (G := H)
230 (Set.range
231 (fun i : ULift.{u} (Fin n) =>
232 psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))) := by
233 let family : Fin n → sourceData.carrier :=
234 freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis
235 let liftedFamily : ULift.{u} (Fin n) → sourceData.carrier :=
236 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
237 have hfin :
239 (G := H) (Set.range (fun i : Fin n => psi (family i))) := by
240 simpa [family] using
242 (ProC := ProC) sourceData hbasis psi hpsi
243 have hrange :
244 Set.range (fun i : ULift.{u} (Fin n) => psi (liftedFamily i)) =
245 Set.range (fun i : Fin n => psi (family i)) := by
246 ext h
247 constructor
248 · rintro ⟨i, rfl⟩
249 exact ⟨i.down, rfl⟩
250 · rintro ⟨i, rfl⟩
251 exact ⟨ULift.up i, rfl⟩
252 simpa [family, liftedFamily, hrange] using hfin
254/-- For the lifted finite free basis, the converging-set universal lift of a surjective target map
255is the target map itself. This is the concrete bridge needed when Fox constructions produce a
256right component from the universal property. -/
258 {ProC : ProCGroupPredicate.{u}} (sourceData : FreeProCSourceData ProC)
259 {n : Nat} (hbasis : Cardinal.mk sourceData.basis = n)
260 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
261 (hH : ProC (G := H))
262 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi) :
263 (freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis).liftHom hH
264 (fun i : ULift.{u} (Fin n) =>
265 psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))
267 (ProC := ProC) sourceData hbasis psi.toMonoidHom)
269 (ProC := ProC) sourceData hbasis psi hpsi) =
270 psi := by
271 let hfree :=
272 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
273 let liftedFamily : ULift.{u} (Fin n) → sourceData.carrier :=
274 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
275 let φ : ULift.{u} (Fin n) → H := fun i => psi (liftedFamily i)
276 let hconv :
277 ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ :=
278 by
279 simpa [φ, liftedFamily] using
281 (ProC := ProC) sourceData hbasis psi.toMonoidHom
282 let hgen :
284 simpa [φ, liftedFamily] using
286 (ProC := ProC) sourceData hbasis psi hpsi
287 ext g
288 have hmon :
289 psi.toMonoidHom = hfree.lift hH φ hconv hgen :=
290 hfree.lift_unique hH φ hconv hgen psi.continuous_toFun (by
291 intro i
292 rfl)
293 exact (congrArg (fun f : sourceData.carrier →* H => f g) hmon).symm
295end
297end CrowellExactSequence