Yamaguchi Lean 4 Library
FoxDifferential/Completed/FreeProC/PrimePowerStageProjection.lean
FoxDifferential/Completed/FreeProC/PrimePowerStageProjection/Source

FoxDifferential/Completed/FreeProC/PrimePowerStageProjection.lean

1import FoxDifferential.Completed.FreeProC.StageProjection
2import FoxDifferential.Completed.FreeProC.CofinalQuotientKernelBasis
3import FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.Semidirect
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Completed/FreeProC/PrimePowerStageProjection.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Prime-power completed-to-finite Fox stage projections
16This file specializes the completed-to-finite semidirect projection layer to a fixed relation
17quotient and prime-power coefficient stages. It also constructs the induced map from the completed
18semidirect product to the inverse limit of the prime-power finite Fox semidirect stages.
20This is the next structural layer toward the completed Crowell density theorem: after the finite
21relation-ideal derivative theorem is available, the remaining proof needs actual compatible
22finite-stage projections and a quotient-kernel neighbourhood basis.
23-/
25namespace FoxDifferential
27noncomputable section
29open scoped Topology
30open ProCGroups.ProC
32universe u v
34section PrimePowerStageMaps
37variable (ℓ : ℕ) [Fact (0 < ℓ)]
38variable {X H : Type u}
39variable [DecidableEq X]
40variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
41variable [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
42variable [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
43variable (N : Subgroup (FreeGroup X)) [N.Normal]
45/-- A completed Fox semidirect projection to the `ℓ^a` finite stage. -/
47 (a : ℕ)
48 (stageLeft :
49 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
50 finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
51 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)
52 (hscalar :
53 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
54 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =
55 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
56 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
57 stageLeft v) :
58 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
59 FiniteFoxStageSemidirect (X := X) N (ℓ ^ a) :=
61 (ProC := ProC) (X := X) (H := H) N (ℓ ^ a) stageLeft stageRight hscalar
63omit [Fact (0 < ℓ)] [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
64@[simp]
66 (a : ℕ)
67 (stageLeft :
68 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
69 finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
70 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)
71 (hscalar :
72 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
73 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =
74 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
75 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
76 stageLeft v)
77 (y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :
79 (ProC := ProC) (X := X) (H := H) ℓ N a stageLeft stageRight hscalar y).left =
80 stageLeft y.left :=
81 rfl
83omit [Fact (0 < ℓ)] [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
84@[simp]
86 (a : ℕ)
87 (stageLeft :
88 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
89 finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
90 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)
91 (hscalar :
92 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
93 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =
94 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
95 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
96 stageLeft v)
97 (y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :
99 (ProC := ProC) (X := X) (H := H) ℓ N a stageLeft stageRight hscalar y).right =
100 stageRight y.right :=
101 rfl
103omit [Fact (0 < ℓ)] [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
104omit [DecidableEq X] in
105/-- Boundary-cycle preservation for a prime-power completed-to-finite stage map. -/
107 [Fintype X]
108 (φ : X → H) (a : ℕ)
109 (stageLeft :
110 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
111 finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
112 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)
113 (hscalar :
114 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
115 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =
116 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
117 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
118 stageLeft v)
119 (stageBoundary :
120 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
122 (hboundary :
123 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
124 finiteFoxStageFoxBoundary (X := X) N (ℓ ^ a) (stageLeft v) =
125 stageBoundary
126 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
127 {y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H}
128 (hy : y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ) :
130 (ProC := ProC) (X := X) (H := H) ℓ N a stageLeft stageRight hscalar y ∈
132 exact
134 (ProC := ProC) (X := X) (H := H) N (ℓ ^ a) φ
135 stageLeft stageRight hscalar stageBoundary hboundary hy
137omit [Fact (0 < ℓ)] [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
138/-- Kernel-word points project to kernel-word points at prime-power finite stages. -/
140 (φ : X → H) (a : ℕ)
141 (stageLeft :
142 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
143 finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
144 (stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)
145 (hscalar :
146 ∀ (h : H) (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
147 stageLeft (zcGroupLike ProC.finiteQuotientClass H h • v) =
148 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
149 (finiteFoxStageTargetQuotient (X := X) N) (stageRight h)) •
150 stageLeft v)
151 (hderivative :
152 ∀ w : FreeGroup X,
153 stageLeft
154 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
155 (FreeGroup.lift φ) w) =
156 finiteFoxStageDerivativeVector (X := X) N (ℓ ^ a) w)
157 (w : FreeGroup X) :
159 (ProC := ProC) (X := X) (H := H) ℓ N a stageLeft stageRight hscalar
161 finiteFoxStageSemidirectKernelWordPoint (X := X) N (ℓ ^ a) w := by
162 exact
164 (ProC := ProC) (X := X) (H := H) N (ℓ ^ a) φ
165 stageLeft stageRight hscalar hderivative w
167/-- Assemble compatible prime-power stage maps into a map to the inverse limit of finite
168semidirect stages. -/
170 (π : ∀ a : ℕ,
171 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
172 FiniteFoxStageSemidirect (X := X) N (ℓ ^ a))
173 (hπ : ∀ {a b : ℕ} (hab : a ≤ b),
174 (finiteFoxStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab).comp (π b) =
175 π a) :
176 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
177 FiniteFoxStagePrimePowerSemidirectLimit (ℓ := ℓ) (X := X) N where
178 toFun y :=
179 ⟨fun a => π a y, by
180 intro a b hab
181 exact congrArg (fun f => f y) (hπ hab)⟩
182 map_one' := by
183 apply Subtype.ext
184 funext a
185 exact map_one (π a)
186 map_mul' y z := by
187 apply Subtype.ext
188 funext a
189 exact map_mul (π a) y z
191omit [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
192@[simp]
194 (π : ∀ a : ℕ,
195 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
196 FiniteFoxStageSemidirect (X := X) N (ℓ ^ a))
197 (hπ : ∀ {a b : ℕ} (hab : a ≤ b),
198 (finiteFoxStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab).comp (π b) =
199 π a)
200 (a : ℕ) (y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :
203 (ProC := ProC) (X := X) (H := H) ℓ N π hπ y) =
204 π a y :=
205 rfl
207omit [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
208/-- A completed boundary-cycle point maps to a stagewise boundary-cycle point in the prime-power
209inverse limit. -/
211 [Fintype X] (φ : X → H)
212 (π : ∀ a : ℕ,
213 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
214 FiniteFoxStageSemidirect (X := X) N (ℓ ^ a))
215 (hπ : ∀ {a b : ℕ} (hab : a ≤ b),
216 (finiteFoxStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab).comp (π b) =
217 π a)
218 (hboundary_stage :
219 ∀ y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
221 ∀ a : ℕ, π a y ∈ finiteFoxStageSemidirectBoundaryCycleSet (X := X) N (ℓ ^ a))
222 {y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H}
223 (hy : y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ) :
225 (ProC := ProC) (X := X) (H := H) ℓ N π hπ y ∈
227 intro a
228 simpa using hboundary_stage y hy a
230omit [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
231/-- Kernel-word points commute with the prime-power inverse-limit map. -/
233 (φ : X → H)
234 (π : ∀ a : ℕ,
235 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H →*
236 FiniteFoxStageSemidirect (X := X) N (ℓ ^ a))
237 (hπ : ∀ {a b : ℕ} (hab : a ≤ b),
238 (finiteFoxStagePrimePowerSemidirectTransition (ℓ := ℓ) (X := X) N hab).comp (π b) =
239 π a)
240 (hkernel_word_projection :
241 ∀ a : ℕ, ∀ w : FreeGroup X,
244 (w : FreeGroup X) :
246 (ProC := ProC) (X := X) (H := H) ℓ N π hπ
249 apply Subtype.ext
250 funext a
251 exact hkernel_word_projection a w
253omit [Fact (0 < ℓ)] in
254/-- Completed Fox density from prime-power stage maps and the finite relation-ideal derivative
255theorem. -/
257 [Fintype X] (φ : X → H)
258 (stageLeft : ∀ a : ℕ,
259 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
260 finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
261 (stageRight : ∀ _a : ℕ,
263 (hscalar :
264 ∀ a : ℕ, ∀ (h : H)
265 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
266 stageLeft a (zcGroupLike ProC.finiteQuotientClass H h • v) =
267 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
268 (finiteFoxStageTargetQuotient (X := X) N) (stageRight a h)) •
269 stageLeft a v)
270 (hidentity_basis :
272 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
273 (fun a : ℕ =>
275 (ProC := ProC) (X := X) (H := H) ℓ N a
276 (stageLeft a) (stageRight a) (hscalar a)))
277 (stageBoundary : ∀ a : ℕ,
278 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
280 (hboundary :
281 ∀ a : ℕ,
282 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
283 finiteFoxStageFoxBoundary (X := X) N (ℓ ^ a) (stageLeft a v) =
284 stageBoundary a
285 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
286 (hN_kernel : ∀ {w : FreeGroup X}, w ∈ N → FreeGroup.lift φ w = 1)
287 (hderivative :
288 ∀ a : ℕ, ∀ w : FreeGroup X,
289 stageLeft a
290 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
291 (FreeGroup.lift φ) w) =
292 finiteFoxStageDerivativeVector (X := X) N (ℓ ^ a) w) :
294 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) := by
295 refine
297 (ProC := ProC) φ (fun _ : ℕ => N) (fun a : ℕ => ℓ ^ a)
298 stageLeft stageRight hscalar ?_ stageBoundary hboundary ?_ hderivative
300 · intro _ w hw
301 exact hN_kernel hw
303omit [Fact (0 < ℓ)] in
304/-- Closed-generated-target version of the prime-power stage-map density theorem. -/
306 [Fintype X] (φ : X → H)
307 (stageLeft : ∀ a : ℕ,
308 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
309 finiteFoxStageCoordinateVector (X := X) N (ℓ ^ a))
310 (stageRight : ∀ _a : ℕ,
312 (hscalar :
313 ∀ a : ℕ, ∀ (h : H)
314 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
315 stageLeft a (zcGroupLike ProC.finiteQuotientClass H h • v) =
316 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ a))
317 (finiteFoxStageTargetQuotient (X := X) N) (stageRight a h)) •
318 stageLeft a v)
319 (hidentity_basis :
321 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
322 (fun a : ℕ =>
324 (ProC := ProC) (X := X) (H := H) ℓ N a
325 (stageLeft a) (stageRight a) (hscalar a)))
326 (stageBoundary : ∀ a : ℕ,
327 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+
329 (hboundary :
330 ∀ a : ℕ,
331 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
332 finiteFoxStageFoxBoundary (X := X) N (ℓ ^ a) (stageLeft a v) =
333 stageBoundary a
334 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v))
335 (hN_kernel : ∀ {w : FreeGroup X}, w ∈ N → FreeGroup.lift φ w = 1)
336 (hderivative :
337 ∀ a : ℕ, ∀ w : FreeGroup X,
338 stageLeft a
339 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
340 (FreeGroup.lift φ) w) =
341 finiteFoxStageDerivativeVector (X := X) N (ℓ ^ a) w) :
344 (ProC := ProC) φ : Subgroup
345 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
346 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
347 exact
349 (ProC := ProC) φ
351 (ProC := ProC) (X := X) (H := H) ℓ N φ
352 stageLeft stageRight hscalar hidentity_basis stageBoundary hboundary hN_kernel
353 hderivative)
355end PrimePowerStageMaps
357end
359end FoxDifferential