Source: ProCGroups.FoxDifferential.Completed.FreeProC.RelationSubmoduleApproximation
1import ProCGroups.FoxDifferential.Completed.FreeProC.StageApproximation
2import ProCGroups.FoxDifferential.Completed.FiniteStage.RelationSubmodule
3import ProCGroups.FoxDifferential.Completed.FiniteStage.RelationIdealDerivative
5/-!
6# Fox differential: completed — free pro-\(C\) — relation submodule approximation
8The principal declarations in this module are:
10- `boundaryCycles_subset_kernelClosure_of_relSubmoduleExact`
11 Completed Fox density from finite-stage relation-submodule exactness.
12- `freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_relSubmodule_exact`
13 The same finite relation-submodule input places completed boundary cycles in the closed generated
14 Fox graph target.
15- `boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction`
16 Completed Fox density holds when, at every finite stage, every source-coordinate lift whose source
17 boundary lies in the explicit relation augmentation ideal projects to a relation-boundary vector.
18- `boundaryCycles_subset_closedGenTarget_of_sourceBoundaryReduction`
19 The source-boundary relation-ideal route also places completed boundary cycles inside the
20 closed-generated Fox graph target.
21-/
23namespace FoxDifferential
25noncomputable section
27universe u v
29section CompletedFoxRelationSubmoduleExact
31open scoped Topology
33variable {C : ProCGroups.FiniteGroupClass}
34variable {X H : Type u}
35variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
36variable [DecidableEq X]
37variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
38variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
40omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
41/-- Completed Fox density from finite-stage relation-submodule exactness. -/
42theorem boundaryCycles_subset_kernelClosure_of_relSubmoduleExact
43 [Fintype X] (φ : X → H)
44 {J : Type v}
45 (Nstage : J → Subgroup (FreeGroup X))
46 [∀ j, (Nstage j).Normal]
47 (nstage : J → ℕ)
48 (π : ∀ j : J,
49 ZCCompletedFoxSemidirect C X H →*
50 FoxAlgebraicStageSemidirect (X := X) (Nstage j) (nstage j))
51 (hbasis :
52 HasLeftQuotientKernelNeighbourhoodBasis
53 (Y := ZCCompletedFoxSemidirect C X H) π)
54 (hboundary_stage :
55 ∀ y : ZCCompletedFoxSemidirect C X H,
56 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
57 ∀ j : J,
58 π j y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet
59 (X := X) (Nstage j) (nstage j))
60 (hstage_module_exact :
61 ∀ j : J,
62 foxAlgebraicStageRelationBoundaryModuleExact
63 (X := X) (Nstage j) (nstage j))
64 (hNstage_kernel :
65 ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
66 (hkernel_word_projection :
67 ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
68 π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
69 foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
70 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
71 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) := by
72 refine
73 freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_semi_exact
74 (C := C) φ Nstage nstage π hbasis hboundary_stage ?_
75 hNstage_kernel hkernel_word_projection
76 intro j
77 exact foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact
78 (X := X) (Nstage j) (nstage j) (hstage_module_exact j)
80/--
81The same finite relation-submodule input places completed boundary cycles in the closed
82generated Fox graph target.
83-/
84theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_relSubmodule_exact
85 [Fintype X] (φ : X → H)
86 {J : Type v}
87 (Nstage : J → Subgroup (FreeGroup X))
88 [∀ j, (Nstage j).Normal]
89 (nstage : J → ℕ)
90 (π : ∀ j : J,
91 ZCCompletedFoxSemidirect C X H →*
92 FoxAlgebraicStageSemidirect (X := X) (Nstage j) (nstage j))
93 (hbasis :
94 HasLeftQuotientKernelNeighbourhoodBasis
95 (Y := ZCCompletedFoxSemidirect C X H) π)
96 (hboundary_stage :
97 ∀ y : ZCCompletedFoxSemidirect C X H,
98 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
99 ∀ j : J,
100 π j y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet
101 (X := X) (Nstage j) (nstage j))
102 (hstage_module_exact :
103 ∀ j : J,
104 foxAlgebraicStageRelationBoundaryModuleExact
105 (X := X) (Nstage j) (nstage j))
106 (hNstage_kernel :
107 ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
108 (hkernel_word_projection :
109 ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
110 π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
111 foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
112 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
113 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
114 (ZCCompletedFoxSemidirect C X H)) : Set
115 (ZCCompletedFoxSemidirect C X H)) := by
116 exact
117 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density (C := C) φ
118 (boundaryCycles_subset_kernelClosure_of_relSubmoduleExact
119 (C := C) φ Nstage nstage π hbasis hboundary_stage
120 hstage_module_exact hNstage_kernel hkernel_word_projection)
122omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
123/--
124Completed Fox density holds when, at every finite stage, every source-coordinate lift whose
125source boundary lies in the explicit relation augmentation ideal projects to a relation-boundary
126vector.
127-/
128theorem boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction
129 [Fintype X] (φ : X → H)
130 {J : Type v}
131 (Nstage : J → Subgroup (FreeGroup X))
132 [∀ j, (Nstage j).Normal]
133 (nstage : J → ℕ)
134 (π : ∀ j : J,
135 ZCCompletedFoxSemidirect C X H →*
136 FoxAlgebraicStageSemidirect (X := X) (Nstage j) (nstage j))
137 (hbasis :
138 HasLeftQuotientKernelNeighbourhoodBasis
139 (Y := ZCCompletedFoxSemidirect C X H) π)
140 (hboundary_stage :
141 ∀ y : ZCCompletedFoxSemidirect C X H,
142 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
143 ∀ j : J,
144 π j y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet
145 (X := X) (Nstage j) (nstage j))
146 (hstage_reduce :
147 ∀ j : J,
148 foxAlgebraicStageSourceBoundaryRelationIdealReduction
149 (X := X) (Nstage j) (nstage j))
150 (hNstage_kernel :
151 ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
152 (hkernel_word_projection :
153 ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
154 π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
155 foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
156 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
157 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) := by
158 refine
159 boundaryCycles_subset_kernelClosure_of_relSubmoduleExact
160 (C := C) φ Nstage nstage π hbasis hboundary_stage ?_
161 hNstage_kernel hkernel_word_projection
162 intro j
163 exact foxAlgebraicStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction
164 (X := X) (Nstage j) (nstage j) (hstage_reduce j)
166/--
167The source-boundary relation-ideal route also places completed boundary cycles inside the
168closed-generated Fox graph target.
169-/
170theorem boundaryCycles_subset_closedGenTarget_of_sourceBoundaryReduction
171 [Fintype X] (φ : X → H)
172 {J : Type v}
173 (Nstage : J → Subgroup (FreeGroup X))
174 [∀ j, (Nstage j).Normal]
175 (nstage : J → ℕ)
176 (π : ∀ j : J,
177 ZCCompletedFoxSemidirect C X H →*
178 FoxAlgebraicStageSemidirect (X := X) (Nstage j) (nstage j))
179 (hbasis :
180 HasLeftQuotientKernelNeighbourhoodBasis
181 (Y := ZCCompletedFoxSemidirect C X H) π)
182 (hboundary_stage :
183 ∀ y : ZCCompletedFoxSemidirect C X H,
184 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
185 ∀ j : J,
186 π j y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet
187 (X := X) (Nstage j) (nstage j))
188 (hstage_reduce :
189 ∀ j : J,
190 foxAlgebraicStageSourceBoundaryRelationIdealReduction
191 (X := X) (Nstage j) (nstage j))
192 (hNstage_kernel :
193 ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
194 (hkernel_word_projection :
195 ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
196 π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
197 foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
198 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
199 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
200 (ZCCompletedFoxSemidirect C X H)) : Set
201 (ZCCompletedFoxSemidirect C X H)) := by
202 exact
203 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density (C := C) φ
204 (boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction
205 (C := C) φ Nstage nstage π hbasis hboundary_stage
206 hstage_reduce hNstage_kernel hkernel_word_projection)
210section
211omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
212/--
213The finite-stage relation-ideal derivative theorem, quotient-kernel neighborhood basis, and
214projection compatibility imply completed Fox density.
215-/
216theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_relDeriv
217 [Fintype X] (φ : X → H)
218 {J : Type v}
219 (Nstage : J → Subgroup (FreeGroup X))
220 [∀ j, (Nstage j).Normal]
221 (nstage : J → ℕ)
222 (π : ∀ j : J,
223 ZCCompletedFoxSemidirect C X H →*
224 FoxAlgebraicStageSemidirect (X := X) (Nstage j) (nstage j))
225 (hbasis :
226 HasLeftQuotientKernelNeighbourhoodBasis
227 (Y := ZCCompletedFoxSemidirect C X H) π)
228 (hboundary_stage :
229 ∀ y : ZCCompletedFoxSemidirect C X H,
230 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
231 ∀ j : J,
232 π j y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet
233 (X := X) (Nstage j) (nstage j))
234 (hNstage_kernel :
235 ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
236 (hkernel_word_projection :
237 ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
238 π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
239 foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
240 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
241 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) := by
242 refine
243 boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction
244 (C := C) φ Nstage nstage π hbasis hboundary_stage ?_
245 hNstage_kernel hkernel_word_projection
246 intro j
247 exact foxAlgebraicStageSourceBoundaryRelationIdealReduction_of_relationIdeal_derivatives
248 (X := X) (Nstage j) (nstage j)
250end
252/--
253Completed boundary cycles lie in the closed-generated Fox graph target using the finite-stage
254relation-ideal derivative theorem.
255-/
256theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_relDeriv
257 [Fintype X] (φ : X → H)
258 {J : Type v}
259 (Nstage : J → Subgroup (FreeGroup X))
260 [∀ j, (Nstage j).Normal]
261 (nstage : J → ℕ)
262 (π : ∀ j : J,
263 ZCCompletedFoxSemidirect C X H →*
264 FoxAlgebraicStageSemidirect (X := X) (Nstage j) (nstage j))
265 (hbasis :
266 HasLeftQuotientKernelNeighbourhoodBasis
267 (Y := ZCCompletedFoxSemidirect C X H) π)
268 (hboundary_stage :
269 ∀ y : ZCCompletedFoxSemidirect C X H,
270 y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
271 ∀ j : J,
272 π j y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet
273 (X := X) (Nstage j) (nstage j))
274 (hNstage_kernel :
275 ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
276 (hkernel_word_projection :
277 ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
278 π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
279 foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
280 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
281 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
282 (ZCCompletedFoxSemidirect C X H)) : Set
283 (ZCCompletedFoxSemidirect C X H)) := by
284 exact
285 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density (C := C) φ
286 (freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_relDeriv
287 (C := C) φ Nstage nstage π hbasis hboundary_stage
288 hNstage_kernel hkernel_word_projection)
290end CompletedFoxRelationSubmoduleExact
292end
294end FoxDifferential