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

FoxDifferential/Completed/FreeProC/SemidirectKernelBasis.lean

1import FoxDifferential.Completed.FreeProC.ProCIntegerBifilteredStageRightProjection
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FreeProC/SemidirectKernelBasis.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Componentwise kernel bases for completed Fox semidirect stages
14The completed density route needs the finite semidirect stage kernels to form a neighbourhood
15basis at the identity of `Z_C[[H]]^X ⋊ H`. For actual finite quotients this is usually proved in
16components: the completed Fox-coordinate projections separate the additive coordinate direction,
17and the target quotient maps separate the group direction. This file packages that componentwise
18argument.
20No finite-stage exactness is hidden here. The only mathematical input is that identity
21neighbourhoods in the semidirect product contain a rectangle in the coordinate and target
22components; the continuous/topological file proves this for the standard product topology.
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/-- Additive-coordinate quotient kernels form a neighbourhood basis at zero.
42This is the additive analogue of `HasIdentityQuotientKernelNeighbourhoodBasis`. It is used for
43the left coordinate `Z_C[[H]]^X`, whose finite-stage maps are additive homomorphisms rather than
44multiplicative homomorphisms. -/
46 ∀ U : Set A, IsOpen U → (0 : A) ∈ U →
47 ∃ j : J, ∀ z : A, π j z = 0 → z ∈ U
49end AdditiveKernelBasis
51section CoordinateKernelBasis
53variable {A : Type u} [AddCommMonoid A] [TopologicalSpace A]
54variable {J : Type v} [Preorder J] [Nonempty J]
55variable {B : J → Type*} [∀ j, AddCommMonoid (B j)]
56variable {X : Type u} [Fintype X]
58/-- A finite product neighbourhood around zero in `X -> A`, stated in a form convenient for
59coordinatewise kernel-basis arguments. -/
61 ∀ U : Set (X → A), IsOpen U → (0 : X → A) ∈ U →
62 ∃ V : X → Set A,
63 (∀ x : X, IsOpen (V x) ∧ (0 : A) ∈ V x) ∧
64 ∀ v : X → A, (∀ x : X, v x ∈ V x) → v ∈ U
66/-- Coordinatewise additive homomorphism induced by a stage coefficient map. -/
68 (π : ∀ j : J, A →+ B j) (j : J) :
69 (X → A) →+ (X → B j) where
70 toFun v := fun x => π j (v x)
71 map_zero' := by
72 funext x
73 exact map_zero (π j)
74 map_add' v w := by
75 funext x
76 exact map_add (π j) (v x) (w x)
78omit [TopologicalSpace A] [Preorder J] [Nonempty J] [Fintype X] in
79@[simp]
81 (π : ∀ j : J, A →+ B j) (j : J) (v : X → A) (x : X) :
82 coordinatewiseAddMonoidHom (X := X) π j v x = π j (v x) :=
83 rfl
85/-- If coefficient kernels form a zero-neighbourhood basis and stage kernels are monotone along a
86directed finite-stage system, then the coordinatewise finite product maps also form a
87zero-neighbourhood kernel basis. -/
89 (π : ∀ j : J, A →+ B j)
91 (hdir : Directed (· ≤ ·) (id : J → J))
93 (hmono : ∀ {i j : J}, i ≤ j → ∀ a : A, π j a = 0 → π i a = 0) :
95 (A := X → A)
96 (fun j : J => coordinatewiseAddMonoidHom (X := X) π j) := by
97 intro U hU hUzero
98 rcases hrect U hU hUzero with ⟨V, hV, hrectU⟩
99 have hstage : ∀ x : X, ∃ j : J, ∀ a : A, π j a = 0 → a ∈ V x := by
100 intro x
101 exact hbasis (V x) (hV x).1 (hV x).2
102 choose jx hjx using hstage
103 classical
104 have hupper : ∀ s : Finset X, ∃ k : J, ∀ x : X, x ∈ s → jx x ≤ k := by
105 intro s
106 induction s using Finset.induction_on with
107 | empty =>
108 exact ⟨Classical.choice (inferInstance : Nonempty J), by simp only [Finset.notMem_empty, IsEmpty.forall_iff, implies_true]⟩
109 | insert x s hxs ih =>
110 rcases ih with ⟨k, hk⟩
111 rcases hdir (jx x) k with ⟨l, hxl, hkl⟩
112 refine ⟨l, ?_⟩
113 intro y hy
114 rw [Finset.mem_insert] at hy
115 rcases hy with rfl | hy
116 · exact hxl
117 · exact (hk y hy).trans hkl
118 rcases hupper (Finset.univ : Finset X) with ⟨k, hk⟩
119 refine ⟨k, ?_⟩
120 intro v hv
121 refine hrectU v ?_
122 intro x
123 exact hjx x (v x) (hmono (hk x (by simp only [Finset.mem_univ])) (v x) (by
124 have hvx := congrArg (fun f : X → B k => f x) hv
125 simpa [coordinatewiseAddMonoidHom] using hvx))
127end CoordinateKernelBasis
129section AbstractSemidirectComponentBasis
132variable {X H : Type u}
133variable [DecidableEq X]
134variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
135variable [TopologicalSpace (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)]
136variable [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
137variable {J : Type v} [Preorder J]
138variable (Nstage : J → Subgroup (FreeGroup X)) [∀ j, (Nstage j).Normal]
139variable (nstage : J → ℕ) [∀ j, Fact (0 < nstage j)]
141/-- Identity neighbourhoods in the completed Fox semidirect product contain component rectangles.
143For the standard product topology this follows from the homeomorphism
144`Z_C[[H]]^X ⋊ H ≃ Z_C[[H]]^X × H`; it is kept as a named property so the algebraic componentwise
145kernel-basis theorem below is independent of the concrete topology construction. -/
147 (C : ProCGroups.FiniteGroupClass.{u})
148 [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
149 [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] : Prop :=
150 ∀ U : Set (ZCCompletedFoxSemidirect C X H),
151 IsOpen U → (1 : ZCCompletedFoxSemidirect C X H) ∈ U →
152 ∃ UL : Set (ZCFreeFoxCoordinates C (X := X) (H := H)),
153 ∃ UR : Set H,
154 IsOpen UL ∧ (0 : ZCFreeFoxCoordinates C (X := X) (H := H)) ∈ UL ∧
155 IsOpen UR ∧ (1 : H) ∈ UR ∧
157 y.left ∈ UL → y.right ∈ UR → y ∈ U
159omit [∀ (j : J), Fact (0 < nstage j)] in
160omit [DecidableEq X] in
161/-- If the coordinate kernels and target kernels are neighbourhood bases in the two components,
162and the finite-stage kernels are monotone along the directed stage system, then the semidirect
163stage kernels are a neighbourhood basis at the identity.
165This is the topological bridge needed to feed actual finite quotient projections into the completed
166Fox density theorem. -/
169 (X := X) (H := H) ProC.finiteQuotientClass)
170 (hdir : Directed (· ≤ ·) (id : J → J))
171 (stageLeft : ∀ j : J,
172 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) →+
173 finiteFoxStageCoordinateVector (X := X) (Nstage j) (nstage j))
174 (stageRight : ∀ j : J, H →* finiteFoxStageTargetQuotient (X := X) (Nstage j))
175 (hscalar : ∀ j : J, ∀ (h : H)
176 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)),
177 stageLeft j (zcGroupLike ProC.finiteQuotientClass H h • v) =
178 (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
179 (finiteFoxStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
180 stageLeft j v)
181 (hleft_basis :
183 (A := ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
184 stageLeft)
185 (hright_basis :
187 (hleft_mono : ∀ {i j : J}, i ≤ j →
188 ∀ v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
189 stageLeft j v = 0 → stageLeft i v = 0)
190 (hright_mono : ∀ {i j : J}, i ≤ j → ∀ h : H,
191 stageRight j h = 1 → stageRight i h = 1) :
193 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
194 (fun j : J =>
196 (ProC := ProC) (X := X) (H := H) (Nstage j) (nstage j)
197 (stageLeft j) (stageRight j) (hscalar j)) := by
198 intro U hU hUone
199 rcases hrect U hU hUone with
200 ⟨UL, UR, hULopen, hULzero, hURopen, hURone, hrectangle⟩
201 rcases hleft_basis UL hULopen hULzero with ⟨i, hi⟩
202 rcases hright_basis UR hURopen hURone with ⟨j, hj⟩
203 rcases hdir i j with ⟨k, hik, hjk⟩
204 refine ⟨k, ?_⟩
205 intro y hy
206 have hycoords : stageLeft k y.left = 0 ∧ stageRight k y.right = 1 := by
207 exact
209 (ProC := ProC) (X := X) (H := H) (N := Nstage k) (n := nstage k)
210 (stageLeft := stageLeft k) (stageRight := stageRight k)
211 (hscalar := hscalar k) (y := y)).1 hy
212 exact hrectangle y
213 (hi y.left (hleft_mono hik y.left hycoords.1))
214 (hj y.right (hright_mono hjk y.right hycoords.2))
216end AbstractSemidirectComponentBasis
218section BifilteredZCBasis
221variable {X H : Type u}
222variable [DecidableEq X]
223variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
224variable [TopologicalSpace (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)]
225variable [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
226variable [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
227variable {J : Type v} [Preorder J]
228variable (Nstage : J → Subgroup (FreeGroup X)) [∀ j, (Nstage j).Normal]
229variable (nstage : J → ℕ) [∀ j, Fact (0 < nstage j)]
230variable (hN : ∀ {i j : J}, i ≤ j → Nstage j ≤ Nstage i)
231variable (hn : ∀ {i j : J}, i ≤ j → nstage i ∣ nstage j)
232variable (zcIndex : J → ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H)
233variable (hzcIndex : ∀ {i j : J}, i ≤ j → zcIndex i ≤ zcIndex j)
234variable (hmod : ∀ j : J, nstage j ∣ (zcIndex j).1.modulus)
235variable (qmap : ∀ j : J,
236 CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2 →*
237 finiteFoxStageTargetQuotient (X := X) (Nstage j))
239omit [TopologicalSpace (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)] in
240omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in
241omit [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
242/-- The left coordinate kernels of the actual `Z_C[[H]]` bifiltered stage maps are monotone along
243stage refinement. -/
245 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
246 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
248 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
250 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
251 (hzcIndex hij).1 a) =
252 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
254 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
255 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
256 ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
257 qmap i
258 ((OpenNormalSubgroupInClass.map
259 (C := ProC.finiteQuotientClass) (G := H)
260 (U := OrderDual.ofDual (zcIndex i).2)
261 (V := OrderDual.ofDual (zcIndex j).2)
262 (hzcIndex hij).2) q) =
263 finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
264 {i j : J} (hij : i ≤ j)
265 (v : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
266 (hv :
268 (ProC := ProC) (X := X) (H := H) Nstage nstage
270 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
271 j v = 0) :
273 (ProC := ProC) (X := X) (H := H) Nstage nstage
275 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
276 i v = 0 := by
277 have htransition :=
279 (ProC := ProC) (X := X) (H := H) Nstage nstage hN hn
281 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
282 (fun hij a =>
284 (ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
285 hmod qmap hcoeff_mod hqmap_transition hij a)
286 hij v
287 -- The coefficient-map transition theorem above packages the exact finite target transition.
288 -- Reading the displayed equality backwards shows that the coarser coordinate is the transition
289 -- of the finer coordinate, hence a finer zero maps to a coarser zero.
290 calc
292 (ProC := ProC) (X := X) (H := H) Nstage nstage
294 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
295 i v
298 (ProC := ProC) (X := X) (H := H) Nstage nstage
300 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
301 j v) := htransition.symm
302 _ = 0 := by
303 rw [hv]
304 funext x
307omit [TopologicalSpace (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)] in
308omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in
309omit [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
310/-- The coefficient kernels of actual `Z_C[[H]]` bifiltered finite-stage maps are monotone along
311stage refinement. -/
313 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
314 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
316 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
318 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
319 (hzcIndex hij).1 a) =
320 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
322 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
323 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
324 ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
325 qmap i
326 ((OpenNormalSubgroupInClass.map
327 (C := ProC.finiteQuotientClass) (G := H)
328 (U := OrderDual.ofDual (zcIndex i).2)
329 (V := OrderDual.ofDual (zcIndex j).2)
330 (hzcIndex hij).2) q) =
331 finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
332 {i j : J} (hij : i ≤ j)
333 (a : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
334 (ha :
336 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j a = 0) :
338 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap i a = 0 := by
339 have htransition :=
341 (ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
342 hmod qmap hcoeff_mod hqmap_transition hij a
343 calc
345 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap i a
348 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j a) :=
349 htransition.symm
350 _ = 0 := by
351 rw [ha]
354omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
355/-- Additive kernel basis for completed Fox-coordinate projections, reduced to the coefficient
356ring projections. This is the next component-level target after semidirect kernel bases: prove the
357coefficient maps `Z_C[[H]] -> (Z/n_j)[F/N_j]` have kernel neighbourhood basis, and the coordinate
358result follows for finite `X`. -/
360 [Fintype X] [Nonempty J]
361 (hcoord_rect :
363 (A := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) (X := X))
364 (hdir : Directed (· ≤ ·) (id : J → J))
365 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
366 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
368 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
370 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
371 (hzcIndex hij).1 a) =
372 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
374 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
375 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
376 ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
377 qmap i
378 ((OpenNormalSubgroupInClass.map
379 (C := ProC.finiteQuotientClass) (G := H)
380 (U := OrderDual.ofDual (zcIndex i).2)
381 (V := OrderDual.ofDual (zcIndex j).2)
382 (hzcIndex hij).2) q) =
383 finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
384 (hcoeff_basis :
386 (A := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
387 (fun j : J =>
389 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j).toAddMonoidHom)) :
391 (A := ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
392 (fun j : J =>
394 (ProC := ProC) (X := X) (H := H) Nstage nstage
396 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j) := by
397 change
399 (A := X → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
400 (fun j : J =>
402 (fun k : J =>
404 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k).toAddMonoidHom) j)
405 exact
407 (X := X)
408 (fun k : J =>
410 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k).toAddMonoidHom)
411 hcoord_rect hdir hcoeff_basis
412 (fun hij a ha =>
414 (ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
415 hmod qmap hcoeff_mod hqmap_transition hij a ha)
417omit [TopologicalSpace (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)] in
418omit [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
419/-- The right kernels of the automatically defined bifiltered stage maps are monotone along stage
420refinement. -/
422 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
423 ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
424 qmap i
425 ((OpenNormalSubgroupInClass.map
426 (C := ProC.finiteQuotientClass) (G := H)
427 (U := OrderDual.ofDual (zcIndex i).2)
428 (V := OrderDual.ofDual (zcIndex j).2)
429 (hzcIndex hij).2) q) =
430 finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
431 {i j : J} (hij : i ≤ j) (h : H)
432 (hh :
434 (ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap j h = 1) :
436 (ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap i h = 1 := by
437 calc
439 (ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap i h
442 (ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap j h) :=
444 (ProC := ProC) (X := X) (H := H) (Nstage := Nstage) (hN := hN)
445 (zcIndex := zcIndex) (hzcIndex := hzcIndex) (qmap := qmap)
446 hqmap_transition hij h).symm
447 _ = 1 := by
448 rw [hh]
449 exact map_one (finiteFoxStageTargetQuotientMap (X := X) (hN hij))
451omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
452/-- Componentwise zero/identity kernel bases imply the identity-neighbourhood kernel basis for
453the actual `Z_C[[H]]` bifiltered semidirect stage maps.
455This removes the need to prove the semidirect kernel basis in one monolithic step: it is enough to
456prove it for the completed Fox-coordinate projections and for the target quotient maps. -/
459 (X := X) (H := H) ProC.finiteQuotientClass)
460 (hdir : Directed (· ≤ ·) (id : J → J))
461 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
462 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
464 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
466 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
467 (hzcIndex hij).1 a) =
468 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
470 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
471 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
472 ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
473 qmap i
474 ((OpenNormalSubgroupInClass.map
475 (C := ProC.finiteQuotientClass) (G := H)
476 (U := OrderDual.ofDual (zcIndex i).2)
477 (V := OrderDual.ofDual (zcIndex j).2)
478 (hzcIndex hij).2) q) =
479 finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
480 (hleft_basis :
482 (A := ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
483 (fun j : J =>
485 (ProC := ProC) (X := X) (H := H) Nstage nstage
487 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j))
488 (hright_basis :
490 (Y := H)
491 (fun j : J =>
493 (ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap j)) :
495 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
496 (fun j : J =>
498 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j) := by
499 refine
501 (ProC := ProC) (X := X) (H := H) Nstage nstage hrect hdir
502 (fun j =>
504 (ProC := ProC) (X := X) (H := H) Nstage nstage
506 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j)
507 (fun j =>
509 (ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap j)
510 (fun j h v =>
512 (ProC := ProC) (X := X) (H := H) Nstage nstage
514 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
516 (ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap)
518 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k h)
519 j h v)
520 hleft_basis hright_basis ?_ ?_
521 · intro i j hij v hv
523 (ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
524 hmod qmap hcoeff_mod hqmap_transition hij v hv
525 · intro i j hij h hh
527 (ProC := ProC) (X := X) (H := H) Nstage hN zcIndex hzcIndex qmap
528 hqmap_transition hij h hh
530end BifilteredZCBasis
532end
534end FoxDifferential