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

FoxDifferential/Completed/Continuous/SemidirectKernelBasis.lean

1import FoxDifferential.Completed.Continuous.Topology
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/Continuous/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# Standard rectangular neighbourhoods for completed Fox semidirect products
14The componentwise kernel-basis theorem in `FoxDifferential.Free.SemidirectKernelBasis` is purely algebraic and
15uses a named rectangular-neighbourhood property. This file proves that property for the standard
16product topology on `Z_C[[H]]^X ⋊ H`, and then specializes the componentwise kernel-basis theorem
17to actual `Z_C[[H]]` bifiltered stage maps.
18-/
20namespace FoxDifferential
22noncomputable section
24open scoped Topology
25open ProCGroups.ProC
27universe u v
30section CoordinateRectangularNeighbourhoods
32variable {A : Type u} [AddCommMonoid A] [TopologicalSpace A]
33variable {X : Type u}
35/-- Finite-coordinate product neighbourhoods in a function space contain coordinate rectangles.
37This is the generic topological input needed to pass from coefficient-kernel bases for
38`Z_C[[H]]` to coordinate-kernel bases for `Z_C[[H]]^X`. It uses the product topology directly and
39keeps no algebraic assumptions. -/
42 intro U hU hUzero
43 classical
44 rcases (isOpen_pi_iff.mp hU) (0 : X → A) hUzero with ⟨J, W, hW, hJU⟩
45 let V : X → Set A := fun x => if hx : x ∈ J then W x else Set.univ
46 refine ⟨V, ?_, ?_⟩
47 · intro x
48 by_cases hx : x ∈ J
49 · simpa [V, hx] using hW x hx
50 · simp only [dite_eq_ite, hx, ↓reduceIte, isOpen_univ, Set.mem_univ, and_self, V]
51 · intro v hv
52 apply hJU
53 intro x hx
54 have hvx := hv x
55 have hxJ : x ∈ J := by
56 simpa using hx
57 have hVx : V x = W x := by
58 simp only [dite_eq_ite, hxJ, ↓reduceIte, V]
59 rwa [hVx] at hvx
61/-- Standard product-topology coordinate rectangles for completed Fox-coordinate families. -/
63 (C : ProCGroups.FiniteGroupClass.{u}) (X H : Type u)
64 [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
66 (A := ZCCompletedGroupAlgebra C H) (X := X) :=
69end CoordinateRectangularNeighbourhoods
71section RectangularNeighbourhoods
73variable (C : ProCGroups.FiniteGroupClass.{u})
75variable (X : Type u) [DecidableEq X]
76variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
78omit [Fact C.FiniteOnly] [DecidableEq X] in
79/-- In the standard topology on `Z_C[[H]]^X ⋊ H`, every identity neighbourhood contains a product
80rectangle around `(0,1)` in the coordinate and target components. -/
83 (X := X) (H := H) C := by
84 intro U hU hUone
85 rcases isOpen_induced_iff.mp hU with ⟨V, hVopen, hVeq⟩
86 have hVone :
87 ((0 : ZCFreeFoxCoordinates C (X := X) (H := H)), (1 : H)) ∈ V := by
88 have hpre :
90 (fun a : ZCCompletedFoxSemidirect C X H => (a.left, a.right)) ⁻¹' V := by
91 simpa [hVeq]
92 using hUone
93 simpa using hpre
94 have hVnhds : V ∈ 𝓝 ((0 : ZCFreeFoxCoordinates C (X := X) (H := H)), (1 : H)) :=
95 hVopen.mem_nhds hVone
96 rcases mem_nhds_prod_iff.mp hVnhds with ⟨UL₀, hUL₀, UR₀, hUR₀, hprod⟩
97 rcases mem_nhds_iff.mp hUL₀ with ⟨UL, hULsub, hULopen, hULzero⟩
98 rcases mem_nhds_iff.mp hUR₀ with ⟨UR, hURsub, hURopen, hURone⟩
99 refine ⟨UL, UR, hULopen, hULzero, hURopen, hURone, ?_⟩
100 intro y hyL hyR
101 have hyV : (y.left, y.right) ∈ V :=
102 hprod (show (y.left, y.right) ∈ UL₀ ×ˢ UR₀ from ⟨hULsub hyL, hURsub hyR⟩)
103 have hyUpre : y ∈
104 (fun a : ZCCompletedFoxSemidirect C X H => (a.left, a.right)) ⁻¹' V := hyV
105 simpa [hVeq] using hyUpre
107end RectangularNeighbourhoods
109section BifilteredZCStandardTopology
112variable {X H : Type u}
113variable [DecidableEq X]
114variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
115variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
116variable {J : Type v} [Preorder J]
117variable (Nstage : J → Subgroup (FreeGroup X)) [∀ j, (Nstage j).Normal]
118variable (nstage : J → ℕ) [∀ j, Fact (0 < nstage j)]
119variable (hN : ∀ {i j : J}, i ≤ j → Nstage j ≤ Nstage i)
120variable (hn : ∀ {i j : J}, i ≤ j → nstage i ∣ nstage j)
121variable (zcIndex : J → ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H)
122variable (hzcIndex : ∀ {i j : J}, i ≤ j → zcIndex i ≤ zcIndex j)
123variable (hmod : ∀ j : J, nstage j ∣ (zcIndex j).1.modulus)
124variable (qmap : ∀ j : J,
125 CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2 →*
126 finiteFoxStageTargetQuotient (X := X) (Nstage j))
128omit [Fact ProC.finiteQuotientClass.FiniteOnly] [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in
129/-- Standard-topology form of the componentwise kernel-basis theorem for actual `Z_C[[H]]`
130bifiltered finite stages. -/
132 (hdir : Directed (· ≤ ·) (id : J → J))
133 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
134 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
136 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
138 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
139 (hzcIndex hij).1 a) =
140 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
142 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
143 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
144 ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
145 qmap i
146 ((OpenNormalSubgroupInClass.map
147 (C := ProC.finiteQuotientClass) (G := H)
148 (U := OrderDual.ofDual (zcIndex i).2)
149 (V := OrderDual.ofDual (zcIndex j).2)
150 (hzcIndex hij).2) q) =
151 finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
152 (hleft_basis :
154 (A := ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
155 (fun j : J =>
157 (ProC := ProC) (X := X) (H := H) Nstage nstage
159 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j))
160 (hright_basis :
162 (Y := H)
163 (fun j : J =>
165 (ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap j)) :
167 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
168 (fun j : J =>
170 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j) := by
171 exact
173 (ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
174 hmod qmap
176 (C := ProC.finiteQuotientClass) X H)
177 hdir hcoeff_mod hqmap_transition hleft_basis hright_basis
180omit [Fact ProC.finiteQuotientClass.FiniteOnly] [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in
181/-- Standard-topology additive kernel basis for completed Fox coordinates, reduced to the
182coefficient-ring kernel basis.
184For finite Fox coordinate families, product neighbourhoods give the coordinate rectangles needed
185for the coordinate-kernel theorem. -/
187 [Fintype X] [Nonempty J]
188 (hdir : Directed (· ≤ ·) (id : J → J))
189 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
190 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
192 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
194 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
195 (hzcIndex hij).1 a) =
196 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
198 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
199 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
200 ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
201 qmap i
202 ((OpenNormalSubgroupInClass.map
203 (C := ProC.finiteQuotientClass) (G := H)
204 (U := OrderDual.ofDual (zcIndex i).2)
205 (V := OrderDual.ofDual (zcIndex j).2)
206 (hzcIndex hij).2) q) =
207 finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
208 (hcoeff_basis :
210 (A := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
211 (fun j : J =>
213 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j).toAddMonoidHom)) :
215 (A := ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
216 (fun j : J =>
218 (ProC := ProC) (X := X) (H := H) Nstage nstage
220 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j) := by
221 exact
223 (ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
224 hmod qmap
226 (C := ProC.finiteQuotientClass) X H)
227 hdir hcoeff_mod hqmap_transition hcoeff_basis
229omit [Fact ProC.finiteQuotientClass.FiniteOnly] [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in
230/-- Standard-topology semidirect kernel basis from coefficient and target component bases.
232This is the componentwise kernel-basis theorem with the left coordinate basis built internally
233from the coefficient maps `Z_C[[H]] -> (Z/n_j)[F/N_j]`. -/
235 [Fintype X] [Nonempty J]
236 (hdir : Directed (· ≤ ·) (id : J → J))
237 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
238 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
240 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
242 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
243 (hzcIndex hij).1 a) =
244 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
246 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
247 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
248 ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
249 qmap i
250 ((OpenNormalSubgroupInClass.map
251 (C := ProC.finiteQuotientClass) (G := H)
252 (U := OrderDual.ofDual (zcIndex i).2)
253 (V := OrderDual.ofDual (zcIndex j).2)
254 (hzcIndex hij).2) q) =
255 finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
256 (hcoeff_basis :
258 (A := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
259 (fun j : J =>
261 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j).toAddMonoidHom))
262 (hright_basis :
264 (Y := H)
265 (fun j : J =>
267 (ProC := ProC) (X := X) (H := H) Nstage zcIndex qmap j)) :
269 (Y := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
270 (fun j : J =>
272 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j) := by
273 exact
275 (ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
276 hmod qmap hdir hcoeff_mod hqmap_transition
278 (ProC := ProC) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex
279 hmod qmap hdir hcoeff_mod hqmap_transition hcoeff_basis)
280 hright_basis
282end BifilteredZCStandardTopology
284end
286end FoxDifferential