Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectKernelBasis
ProCGroups/FoxDifferential/Completed/FreeProC/SemidirectKernelBasis/Source

Source: ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectKernelBasis

1import ProCGroups.FoxDifferential.Completed.FreeProC.ProCIntegerBifilteredStageRightProjection
3/-!
4# Fox differential: completed — free pro-\(C\) — semidirect kernel basis
6The principal declarations in this module are:
8- `HasAdditiveIdentityQuotientKernelNeighbourhoodBasis`
9 Additive-coordinate quotient kernels form a neighborhood basis at zero. This is the additive
10 analogue of HasIdentityQuotientKernelNeighborhoodBasis. It is used for the left coordinate
11 \(\mathbb{Z}_C\llbracket H\rrbracket^{X}\), whose finite-stage maps are additive homomorphisms
12 rather than multiplicative homomorphisms.
13- `HasFiniteCoordinateZeroRectangularNeighbourhoods`
14 A finite product neighborhood around zero in \(X \to A\), formulated for coordinatewise
15 kernel-basis statements.
16- `coordinatewiseAddMonoidHom_apply`
17 The coordinatewise additive homomorphism evaluates by applying the chosen additive map to each
18 coordinate.
19- `coordinatewiseAdditiveKernelBasis_of_component_basis`
20 If coefficient kernels form a zero-neighborhood basis and stage kernels are monotone along a
21 directed finite-stage system, then the coordinatewise finite product maps also form a
22 zero-neighborhood kernel basis.
23-/
25namespace FoxDifferential
27noncomputable section
29open scoped Topology
30open ProCGroups.ProC
32universe u v
34section AdditiveKernelBasis
36variable {A : Type u} [AddZeroClass A] [TopologicalSpace A]
37variable {J : Type v} {B : J → Type*} [∀ j, AddZeroClass (B j)]
38variable (π : ∀ j : J, A →+ B j)
40/--
41Additive-coordinate quotient kernels form a neighborhood basis at zero. This is the additive
42analogue of HasIdentityQuotientKernelNeighborhoodBasis. It is used for the left coordinate
43\(\mathbb{Z}_C\llbracket H\rrbracket^{X}\), whose finite-stage maps are additive homomorphisms
44rather than multiplicative homomorphisms.
45-/
46def HasAdditiveIdentityQuotientKernelNeighbourhoodBasis : Prop :=
47 ∀ U : Set A, IsOpen U → (0 : A) ∈ U →
48 ∃ j : J, ∀ z : A, π j z = 0 → z ∈ U
50end AdditiveKernelBasis
52section CoordinateKernelBasis
54variable {A : Type u} [AddCommMonoid A] [TopologicalSpace A]
55variable {J : Type v} [Preorder J] [Nonempty J]
56variable {B : J → Type*} [∀ j, AddCommMonoid (B j)]
57variable {X : Type u} [Finite X]
59/--
60A finite product neighborhood around zero in \(X \to A\), formulated for coordinatewise
61kernel-basis statements.
62-/
63def HasFiniteCoordinateZeroRectangularNeighbourhoods : Prop :=
64 ∀ U : Set (X → A), IsOpen U → (0 : X → A) ∈ U →
65 ∃ V : X → Set A,
66 (∀ x : X, IsOpen (V x) ∧ (0 : A) ∈ V x) ∧
67 ∀ v : X → A, (∀ x : X, v x ∈ V x) → v ∈ U
69/-- A stage coefficient map induces a coordinatewise additive homomorphism. -/
70def coordinatewiseAddMonoidHom
71 (π : ∀ j : J, A →+ B j) (j : J) :
72 (X → A) →+ (X → B j) where
73 toFun v := fun x => π j (v x)
74 map_zero' := by
75 funext x
76 exact map_zero (π j)
77 map_add' v w := by
78 funext x
79 exact map_add (π j) (v x) (w x)
81omit [TopologicalSpace A] [Preorder J] [Nonempty J] [Finite X] in
82/--
83The coordinatewise additive homomorphism evaluates by applying the chosen additive map to each
84coordinate.
85-/
86@[simp]
87theorem coordinatewiseAddMonoidHom_apply
88 (π : ∀ j : J, A →+ B j) (j : J) (v : X → A) (x : X) :
89 coordinatewiseAddMonoidHom (X := X) π j v x = π j (v x) :=
90 rfl
92/--
93If coefficient kernels form a zero-neighborhood basis and stage kernels are monotone along a
94directed finite-stage system, then the coordinatewise finite product maps also form a
95zero-neighborhood kernel basis.
96-/
97theorem coordinatewiseAdditiveKernelBasis_of_component_basis
98 (π : ∀ j : J, A →+ B j)
99 (hrect : HasFiniteCoordinateZeroRectangularNeighbourhoods (A := A) (X := X))
100 (hdir : Directed (· ≤ ·) (id : J → J))
101 (hbasis : HasAdditiveIdentityQuotientKernelNeighbourhoodBasis (A := A) π)
102 (hmono : ∀ {i j : J}, i ≤ j → ∀ a : A, π j a = 0 → π i a = 0) :
103 HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
104 (A := X → A)
105 (fun j : J => coordinatewiseAddMonoidHom (X := X) π j) := by
106 intro U hU hUzero
107 rcases hrect U hU hUzero with ⟨V, hV, hrectU⟩
108 have hstage : ∀ x : X, ∃ j : J, ∀ a : A, π j a = 0 → a ∈ V x := by
109 intro x
110 exact hbasis (V x) (hV x).1 (hV x).2
111 choose jx hjx using hstage
112 classical
113 letI : Fintype X := Fintype.ofFinite X
114 have hupper : ∀ s : Finset X, ∃ k : J, ∀ x : X, x ∈ s → jx x ≤ k := by
115 intro s
116 induction s using Finset.induction_on with
117 | empty =>
118 exact ⟨Classical.choice (inferInstance : Nonempty J), by simp only [Finset.notMem_empty,
119 IsEmpty.forall_iff, implies_true]⟩
120 | insert x s hxs ih =>
121 rcases ih with ⟨k, hk⟩
122 rcases hdir (jx x) k with ⟨l, hxl, hkl⟩
123 refine ⟨l, ?_⟩
124 intro y hy
125 rw [Finset.mem_insert] at hy
126 rcases hy with rfl | hy
127 · exact hxl
128 · exact (hk y hy).trans hkl
129 rcases hupper (Finset.univ : Finset X) with ⟨k, hk⟩
130 refine ⟨k, ?_⟩
131 intro v hv
132 refine hrectU v ?_
133 intro x
134 exact hjx x (v x) (hmono (hk x (by simp only [Finset.mem_univ])) (v x) (by
135 have hvx := congrArg (fun f : X → B k => f x) hv
136 simpa [coordinatewiseAddMonoidHom] using hvx))
138end CoordinateKernelBasis
140section AbstractSemidirectComponentBasis
143variable {X H : Type u}
144variable [DecidableEq X]
145variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
146variable [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
147variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
148variable {J : Type v} [Preorder J]
149variable (Nstage : J → Subgroup (FreeGroup X)) [∀ j, (Nstage j).Normal]
150variable (nstage : J → ℕ) [∀ j, Fact (0 < nstage j)]
152/--
153Identity neighborhoods in the completed Fox semidirect product contain component rectangles; the
154standard product homeomorphism identifies the semidirect carrier with \(\mathbb{Z}_C\llbracket
155H\rrbracket^{X} \times H\).
156-/
157def HasSemidirectRectangularIdentityNeighbourhoods
158 (C : ProCGroups.FiniteGroupClass.{u})
159 [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
160 [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] : Prop :=
161 ∀ U : Set (ZCCompletedFoxSemidirect C X H),
162 IsOpen U → (1 : ZCCompletedFoxSemidirect C X H) ∈ U →
163 ∃ UL : Set (ZCFreeFoxCoordinates C (X := X) (H := H)),
164 ∃ UR : Set H,
165 IsOpen UL ∧ (0 : ZCFreeFoxCoordinates C (X := X) (H := H)) ∈ UL ∧
166 IsOpen UR ∧ (1 : H) ∈ UR ∧
167 ∀ y : ZCCompletedFoxSemidirect C X H,
168 y.left ∈ UL → y.right ∈ UR → y ∈ U
170omit [∀ (j : J), Fact (0 < nstage j)] in
171omit [DecidableEq X] in
172/--
173If the coordinate kernels and target kernels are neighborhood bases in the two components, and
174the finite-stage kernels are monotone along the directed stage system, then the semidirect stage
175kernels are a neighborhood basis at the identity. This is the topological bridge needed to feed
176actual finite quotient projections into the completed Fox density theorem.
177-/
178theorem freeProCZCCompletedFoxSemidirectStageMap_identity_basis_of_component_bases
179 (hrect : HasSemidirectRectangularIdentityNeighbourhoods
180 (X := X) (H := H) C)
181 (hdir : Directed (· ≤ ·) (id : J → J))
182 (stageLeft : ∀ j : J,
183 ZCFreeFoxCoordinates C (X := X) (H := H) →+
184 foxAlgebraicStageCoordinateVector (X := X) (Nstage j) (nstage j))
185 (stageRight : ∀ j : J, H →* foxAlgebraicStageTargetQuotient (X := X) (Nstage j))
186 (hscalar : ∀ j : J, ∀ (h : H)
187 (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
188 stageLeft j (zcGroupLike C H h • v) =
189 (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
190 (foxAlgebraicStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
191 stageLeft j v)
192 (hleft_basis :
193 HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
194 (A := ZCFreeFoxCoordinates C (X := X) (H := H))
195 stageLeft)
196 (hright_basis :
197 HasIdentityQuotientKernelNeighbourhoodBasis (Y := H) stageRight)
198 (hleft_mono : ∀ {i j : J}, i ≤ j →
199 ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
200 stageLeft j v = 0 → stageLeft i v = 0)
201 (hright_mono : ∀ {i j : J}, i ≤ j → ∀ h : H,
202 stageRight j h = 1 → stageRight i h = 1) :
203 HasIdentityQuotientKernelNeighbourhoodBasis
204 (Y := ZCCompletedFoxSemidirect C X H)
205 (fun j : J =>
206 freeProCZCCompletedFoxSemidirectStageMap
207 (C := C) (X := X) (H := H) (Nstage j) (nstage j)
208 (stageLeft j) (stageRight j) (hscalar j)) := by
209 intro U hU hUone
210 rcases hrect U hU hUone with
211 ⟨UL, UR, hULopen, hULzero, hURopen, hURone, hrectangle⟩
212 rcases hleft_basis UL hULopen hULzero with ⟨i, hi⟩
213 rcases hright_basis UR hURopen hURone with ⟨j, hj⟩
214 rcases hdir i j with ⟨k, hik, hjk⟩
215 refine ⟨k, ?_⟩
216 intro y hy
217 have hycoords : stageLeft k y.left = 0 ∧ stageRight k y.right = 1 := by
218 exact
219 (freeProCZCCompletedFoxSemidirectStageMap_mem_ker_iff
220 (C := C) (X := X) (H := H) (N := Nstage k) (n := nstage k)
221 (stageLeft := stageLeft k) (stageRight := stageRight k)
222 (hscalar := hscalar k) (y := y)).1 hy
223 exact hrectangle y
224 (hi y.left (hleft_mono hik y.left hycoords.1))
225 (hj y.right (hright_mono hjk y.right hycoords.2))
227end AbstractSemidirectComponentBasis
229section BifilteredZCBasis
232variable {X H : Type u}
233variable [DecidableEq X]
234variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
235variable [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
236variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
237variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
238variable {J : Type v} [Preorder J]
239variable (Nstage : J → Subgroup (FreeGroup X)) [∀ j, (Nstage j).Normal]
240variable (nstage : J → ℕ) [∀ j, Fact (0 < nstage j)]
241variable (hN : ∀ {i j : J}, i ≤ j → Nstage j ≤ Nstage i)
242variable (hn : ∀ {i j : J}, i ≤ j → nstage i ∣ nstage j)
243variable (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)
244variable (hzcIndex : ∀ {i j : J}, i ≤ j → zcIndex i ≤ zcIndex j)
245variable (hmod : ∀ j : J, nstage j ∣ (zcIndex j).1.modulus)
246variable (qmap : ∀ j : J,
247 CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2 →*
248 foxAlgebraicStageTargetQuotient (X := X) (Nstage j))
250omit [TopologicalSpace (ZCCompletedGroupAlgebra C H)] in
251omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in
252omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
253 (ZCCompletedFoxSemidirect C X H)] in
254/--
255The left coordinate kernels of the actual \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered
256stage maps are monotone along stage refinement.
257-/
258theorem zcFreeFoxCoordinatesBifilteredStageMap_kernel_mono
259 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
260 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
261 modNCompletedCoeffMap
262 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
263 (modNCompletedCoeffMap
264 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
265 (hzcIndex hij).1 a) =
266 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
267 (modNCompletedCoeffMap
268 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
269 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
270 ∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,
271 qmap i
272 ((OpenNormalSubgroupInClass.map
273 (C := C) (G := H)
274 (U := OrderDual.ofDual (zcIndex i).2)
275 (V := OrderDual.ofDual (zcIndex j).2)
276 (hzcIndex hij).2) q) =
277 foxAlgebraicStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
278 {i j : J} (hij : i ≤ j)
279 (v : ZCFreeFoxCoordinates C (X := X) (H := H))
280 (hv :
281 zcFreeFoxCoordinatesBifilteredStageMap
282 (C := C) (X := X) (H := H) Nstage nstage
283 (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
284 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
285 j v = 0) :
286 zcFreeFoxCoordinatesBifilteredStageMap
287 (C := C) (X := X) (H := H) Nstage nstage
288 (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
289 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
290 i v = 0 := by
291 have htransition :=
292 zcFreeFoxCoordinatesBifilteredStageMap_transition
293 (C := C) (X := X) (H := H) Nstage nstage hN hn
294 (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
295 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
296 (fun hij a =>
297 zcCompletedGroupAlgebraBifilteredStageCoeffMap_transition
298 (C := C) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
299 hmod qmap hcoeff_mod hqmap_transition hij a)
300 hij v
301 -- The coefficient-map transition theorem above packages the exact finite target transition.
302 -- Reading the displayed equality backwards shows that the coarser coordinate is the transition
303 -- of the finer coordinate, hence a finer zero maps to a coarser zero.
304 calc
305 zcFreeFoxCoordinatesBifilteredStageMap
306 (C := C) (X := X) (H := H) Nstage nstage
307 (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
308 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
309 i v
310 = foxAlgebraicStageBifilteredCoordinateVectorMap (X := X) (hN hij) (hn hij)
311 (zcFreeFoxCoordinatesBifilteredStageMap
312 (C := C) (X := X) (H := H) Nstage nstage
313 (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
314 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
315 j v) := htransition.symm
316 _ = 0 := by
317 rw [hv]
318 funext x
319 exact map_zero (foxAlgebraicStageBifilteredTargetGroupAlgebraMap (X := X) (hN hij) (hn hij))
321omit [TopologicalSpace (ZCCompletedGroupAlgebra C H)] in
322omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in
323omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
324 (ZCCompletedFoxSemidirect C X H)] in
325/--
326The coefficient kernels of actual \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered finite-stage
327maps are monotone along stage refinement.
328-/
329theorem zcCompletedGroupAlgebraBifilteredStageCoeffMap_kernel_mono
330 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
331 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
332 modNCompletedCoeffMap
333 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
334 (modNCompletedCoeffMap
335 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
336 (hzcIndex hij).1 a) =
337 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
338 (modNCompletedCoeffMap
339 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
340 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
341 ∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,
342 qmap i
343 ((OpenNormalSubgroupInClass.map
344 (C := C) (G := H)
345 (U := OrderDual.ofDual (zcIndex i).2)
346 (V := OrderDual.ofDual (zcIndex j).2)
347 (hzcIndex hij).2) q) =
348 foxAlgebraicStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
349 {i j : J} (hij : i ≤ j)
350 (a : ZCCompletedGroupAlgebra C H)
351 (ha :
352 zcCompletedGroupAlgebraBifilteredStageCoeffMap
353 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j a = 0) :
354 zcCompletedGroupAlgebraBifilteredStageCoeffMap
355 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap i a = 0 := by
356 have htransition :=
357 zcCompletedGroupAlgebraBifilteredStageCoeffMap_transition
358 (C := C) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
359 hmod qmap hcoeff_mod hqmap_transition hij a
360 calc
361 zcCompletedGroupAlgebraBifilteredStageCoeffMap
362 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap i a
363 = foxAlgebraicStageBifilteredTargetGroupAlgebraMap (X := X) (hN hij) (hn hij)
364 (zcCompletedGroupAlgebraBifilteredStageCoeffMap
365 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j a) :=
366 htransition.symm
367 _ = 0 := by
368 rw [ha]
369 exact map_zero (foxAlgebraicStageBifilteredTargetGroupAlgebraMap (X := X) (hN hij) (hn hij))
371omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] [TopologicalSpace
372 (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
373/-- A finite-coordinate additive kernel-basis criterion for completed Fox-coordinate projections
374in terms of the coefficient projections. -/
375theorem zcFreeFoxCoordinatesBifilteredStageMap_additive_basis_of_coeff_basis
376 [Finite X] [Nonempty J]
377 (hcoord_rect :
378 HasFiniteCoordinateZeroRectangularNeighbourhoods
379 (A := ZCCompletedGroupAlgebra C H) (X := X))
380 (hdir : Directed (· ≤ ·) (id : J → J))
381 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
382 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
383 modNCompletedCoeffMap
384 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
385 (modNCompletedCoeffMap
386 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
387 (hzcIndex hij).1 a) =
388 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
389 (modNCompletedCoeffMap
390 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
391 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
392 ∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,
393 qmap i
394 ((OpenNormalSubgroupInClass.map
395 (C := C) (G := H)
396 (U := OrderDual.ofDual (zcIndex i).2)
397 (V := OrderDual.ofDual (zcIndex j).2)
398 (hzcIndex hij).2) q) =
399 foxAlgebraicStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
400 (hcoeff_basis :
401 HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
402 (A := ZCCompletedGroupAlgebra C H)
403 (fun j : J =>
404 (zcCompletedGroupAlgebraBifilteredStageCoeffMap
405 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j).toAddMonoidHom)) :
406 HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
407 (A := ZCFreeFoxCoordinates C (X := X) (H := H))
408 (fun j : J =>
409 zcFreeFoxCoordinatesBifilteredStageMap
410 (C := C) (X := X) (H := H) Nstage nstage
411 (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
412 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j) := by
413 change
414 HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
415 (A := X → ZCCompletedGroupAlgebra C H)
416 (fun j : J =>
417 coordinatewiseAddMonoidHom (X := X)
418 (fun k : J =>
419 (zcCompletedGroupAlgebraBifilteredStageCoeffMap
420 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k).toAddMonoidHom) j)
421 exact
422 coordinatewiseAdditiveKernelBasis_of_component_basis
423 (X := X)
424 (fun k : J =>
425 (zcCompletedGroupAlgebraBifilteredStageCoeffMap
426 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k).toAddMonoidHom)
427 hcoord_rect hdir hcoeff_basis
428 (fun hij a ha =>
429 zcCompletedGroupAlgebraBifilteredStageCoeffMap_kernel_mono
430 (C := C) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
431 hmod qmap hcoeff_mod hqmap_transition hij a ha)
433omit [TopologicalSpace (ZCCompletedGroupAlgebra C H)] in
434omit [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
435 (ZCCompletedFoxSemidirect C X H)] in
436/--
437The right kernels of the automatically defined bifiltered stage maps are monotone along stage
438refinement.
439-/
440theorem zcCompletedGroupAlgebraBifilteredStageRightMap_kernel_mono
441 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
442 ∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,
443 qmap i
444 ((OpenNormalSubgroupInClass.map
445 (C := C) (G := H)
446 (U := OrderDual.ofDual (zcIndex i).2)
447 (V := OrderDual.ofDual (zcIndex j).2)
448 (hzcIndex hij).2) q) =
449 foxAlgebraicStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
450 {i j : J} (hij : i ≤ j) (h : H)
451 (hh :
452 zcCompletedGroupAlgebraBifilteredStageRightMap
453 (C := C) (X := X) (H := H) Nstage zcIndex qmap j h = 1) :
454 zcCompletedGroupAlgebraBifilteredStageRightMap
455 (C := C) (X := X) (H := H) Nstage zcIndex qmap i h = 1 := by
456 calc
457 zcCompletedGroupAlgebraBifilteredStageRightMap
458 (C := C) (X := X) (H := H) Nstage zcIndex qmap i h
459 = foxAlgebraicStageTargetQuotientMap (X := X) (hN hij)
460 (zcCompletedGroupAlgebraBifilteredStageRightMap
461 (C := C) (X := X) (H := H) Nstage zcIndex qmap j h) :=
462 (zcCompletedGroupAlgebraBifilteredStageRightMap_transition
463 (C := C) (X := X) (H := H) (Nstage := Nstage) (hN := hN)
464 (zcIndex := zcIndex) (hzcIndex := hzcIndex) (qmap := qmap)
465 hqmap_transition hij h).symm
466 _ = 1 := by
467 rw [hh]
468 exact map_one (foxAlgebraicStageTargetQuotientMap (X := X) (hN hij))
470omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] [IsTopologicalGroup
471 (ZCCompletedFoxSemidirect C X H)] in
472/--
473Componentwise zero and identity kernel bases imply the identity-neighborhood kernel basis for
474the actual \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered semidirect stage maps.
475-/
476theorem freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases
477 (hrect : HasSemidirectRectangularIdentityNeighbourhoods
478 (X := X) (H := H) C)
479 (hdir : Directed (· ≤ ·) (id : J → J))
480 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
481 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
482 modNCompletedCoeffMap
483 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
484 (modNCompletedCoeffMap
485 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
486 (hzcIndex hij).1 a) =
487 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
488 (modNCompletedCoeffMap
489 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
490 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
491 ∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,
492 qmap i
493 ((OpenNormalSubgroupInClass.map
494 (C := C) (G := H)
495 (U := OrderDual.ofDual (zcIndex i).2)
496 (V := OrderDual.ofDual (zcIndex j).2)
497 (hzcIndex hij).2) q) =
498 foxAlgebraicStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
499 (hleft_basis :
500 HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
501 (A := ZCFreeFoxCoordinates C (X := X) (H := H))
502 (fun j : J =>
503 zcFreeFoxCoordinatesBifilteredStageMap
504 (C := C) (X := X) (H := H) Nstage nstage
505 (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
506 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j))
507 (hright_basis :
508 HasIdentityQuotientKernelNeighbourhoodBasis
509 (Y := H)
510 (fun j : J =>
511 zcCompletedGroupAlgebraBifilteredStageRightMap
512 (C := C) (X := X) (H := H) Nstage zcIndex qmap j)) :
513 HasIdentityQuotientKernelNeighbourhoodBasis
514 (Y := ZCCompletedFoxSemidirect C X H)
515 (fun j : J =>
516 freeProCZCCompletedFoxSemidirectZCBifilteredStageMap
517 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j) := by
518 refine
519 freeProCZCCompletedFoxSemidirectStageMap_identity_basis_of_component_bases
520 (C := C) (X := X) (H := H) Nstage nstage hrect hdir
521 (fun j =>
522 zcFreeFoxCoordinatesBifilteredStageMap
523 (C := C) (X := X) (H := H) Nstage nstage
524 (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
525 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j)
526 (fun j =>
527 zcCompletedGroupAlgebraBifilteredStageRightMap
528 (C := C) (X := X) (H := H) Nstage zcIndex qmap j)
529 (fun j h v =>
530 zcFreeFoxCoordinatesBifilteredStageMap_smul_groupLike
531 (C := C) (X := X) (H := H) Nstage nstage
532 (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
533 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
534 (zcCompletedGroupAlgebraBifilteredStageRightMap
535 (C := C) (X := X) (H := H) Nstage zcIndex qmap)
536 (fun k h => zcCompletedGroupAlgebraBifilteredStageCoeffMap_groupLike_autoRight
537 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k h)
538 j h v)
539 hleft_basis hright_basis ?_ ?_
540 · intro i j hij v hv
541 exact zcFreeFoxCoordinatesBifilteredStageMap_kernel_mono
542 (C := C) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
543 hmod qmap hcoeff_mod hqmap_transition hij v hv
544 · intro i j hij h hh
545 exact zcCompletedGroupAlgebraBifilteredStageRightMap_kernel_mono
546 (C := C) (X := X) (H := H) Nstage hN zcIndex hzcIndex qmap
547 hqmap_transition hij h hh
549end BifilteredZCBasis
551end
553end FoxDifferential