Source: ProCGroups.FoxDifferential.Completed.Continuous.SemidirectKernelBasis

1import ProCGroups.FoxDifferential.Completed.Continuous.Topology

3/-!

4# Fox differential: completed — continuous — semidirect kernel basis

6The principal declarations in this module are:

8- `finiteCoordinateZeroRectangularNeighbourhoods_pi`

9 Finite-coordinate product neighborhoods in a function space contain coordinate rectangles. This is

10 the generic topological input needed to pass from coefficient-kernel bases for

11 \(\mathbb{Z}_C\llbracket H\rrbracket\) to coordinate-kernel bases for \(\mathbb{Z}_C\llbracket

12 H\rrbracket^{X}\). It uses the product topology directly and keeps no algebraic assumptions.

13- `zcFreeFoxCoordinates_hasFiniteCoordinateZeroRectangularNeighbourhoods`

14 Standard product-topology coordinate rectangles for completed Fox-coordinate families.

15- `zcCompletedFoxSemidirect_hasRectangularIdentityNeighbourhoods`

16 In the standard topology on \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H\), every identity

17 neighborhood contains a product rectangle around (0,1) in the coordinate and target components.

18- `freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases_standardTopology`

19 Standard-topology form of the componentwise kernel-basis theorem for actual

20 \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered finite stages.

21-/

23namespace FoxDifferential

25noncomputable section

27open scoped Topology

28open ProCGroups.ProC

30universe u v

33section CoordinateRectangularNeighbourhoods

35variable {A : Type u} [AddCommMonoid A] [TopologicalSpace A]

36variable {X : Type u}

38/--

39Finite-coordinate product neighborhoods in a function space contain coordinate rectangles. This

40is the generic topological input needed to pass from coefficient-kernel bases for

41\(\mathbb{Z}_C\llbracket H\rrbracket\) to coordinate-kernel bases for \(\mathbb{Z}_C\llbracket

42H\rrbracket^{X}\). It uses the product topology directly and keeps no algebraic assumptions.

43-/

44theorem finiteCoordinateZeroRectangularNeighbourhoods_pi :

45 HasFiniteCoordinateZeroRectangularNeighbourhoods (A := A) (X := X) := by

46 intro U hU hUzero

47 classical

48 rcases (isOpen_pi_iff.mp hU) (0 : X → A) hUzero with ⟨J, W, hW, hJU⟩

49 let V : X → Set A := fun x => if hx : x ∈ J then W x else Set.univ

50 refine ⟨V, ?_, ?_⟩

51 · intro x

52 by_cases hx : x ∈ J

53 · simpa [V, hx] using hW x hx

54 · simp only [dite_eq_ite, hx, ↓reduceIte, isOpen_univ, Set.mem_univ, and_self, V]

55 · intro v hv

56 apply hJU

57 intro x hx

58 have hvx := hv x

59 have hxJ : x ∈ J := by

60 simpa using hx

61 have hVx : V x = W x := by

62 simp only [dite_eq_ite, hxJ, ↓reduceIte, V]

63 rwa [hVx] at hvx

65/-- Standard product-topology coordinate rectangles for completed Fox-coordinate families. -/

66theorem zcFreeFoxCoordinates_hasFiniteCoordinateZeroRectangularNeighbourhoods

67 (C : ProCGroups.FiniteGroupClass.{u}) (X H : Type u)

68 [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :

69 HasFiniteCoordinateZeroRectangularNeighbourhoods

70 (A := ZCCompletedGroupAlgebra C H) (X := X) :=

71 finiteCoordinateZeroRectangularNeighbourhoods_pi

73end CoordinateRectangularNeighbourhoods

75section RectangularNeighbourhoods

77variable (C : ProCGroups.FiniteGroupClass.{u})

78variable (X : Type u) [DecidableEq X]

79variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

81omit [DecidableEq X] in

82/--

83In the standard topology on \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H\), every identity

84neighborhood contains a product rectangle around (0,1) in the coordinate and target components.

85-/

86theorem zcCompletedFoxSemidirect_hasRectangularIdentityNeighbourhoods :

87 HasSemidirectRectangularIdentityNeighbourhoods

88 (X := X) (H := H) C := by

89 intro U hU hUone

90 rcases isOpen_induced_iff.mp hU with ⟨V, hVopen, hVeq⟩

91 have hVone :

92 ((0 : ZCFreeFoxCoordinates C (X := X) (H := H)), (1 : H)) ∈ V := by

93 have hpre :

94 (1 : ZCCompletedFoxSemidirect C X H) ∈

95 (fun a : ZCCompletedFoxSemidirect C X H => (a.left, a.right)) ⁻¹' V := by

96 simpa [hVeq]

97 using hUone

98 simpa using hpre

99 have hVnhds : V ∈ 𝓝 ((0 : ZCFreeFoxCoordinates C (X := X) (H := H)), (1 : H)) :=

100 hVopen.mem_nhds hVone

101 rcases mem_nhds_prod_iff.mp hVnhds with ⟨UL₀, hUL₀, UR₀, hUR₀, hprod⟩

102 rcases mem_nhds_iff.mp hUL₀ with ⟨UL, hULsub, hULopen, hULzero⟩

103 rcases mem_nhds_iff.mp hUR₀ with ⟨UR, hURsub, hURopen, hURone⟩

104 refine ⟨UL, UR, hULopen, hULzero, hURopen, hURone, ?_⟩

105 intro y hyL hyR

106 have hyV : (y.left, y.right) ∈ V :=

107 hprod (show (y.left, y.right) ∈ UL₀ ×ˢ UR₀ from ⟨hULsub hyL, hURsub hyR⟩)

108 have hyUpre : y ∈

109 (fun a : ZCCompletedFoxSemidirect C X H => (a.left, a.right)) ⁻¹' V := hyV

110 simpa [hVeq] using hyUpre

111

112end RectangularNeighbourhoods

113

114section BifilteredZCStandardTopology

115

116variable {C : ProCGroups.FiniteGroupClass}

117variable {X H : Type u}

118variable [DecidableEq X]

119variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

120variable {J : Type v} [Preorder J]

121variable (Nstage : J → Subgroup (FreeGroup X)) [∀ j, (Nstage j).Normal]

122variable (nstage : J → ℕ) [∀ j, Fact (0 < nstage j)]

123variable (hN : ∀ {i j : J}, i ≤ j → Nstage j ≤ Nstage i)

124variable (hn : ∀ {i j : J}, i ≤ j → nstage i ∣ nstage j)

125variable (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)

126variable (hzcIndex : ∀ {i j : J}, i ≤ j → zcIndex i ≤ zcIndex j)

127variable (hmod : ∀ j : J, nstage j ∣ (zcIndex j).1.modulus)

128variable (qmap : ∀ j : J,

129 CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2 →*

130 foxAlgebraicStageTargetQuotient (X := X) (Nstage j))

131

132omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in

133/--

134Standard-topology form of the componentwise kernel-basis theorem for actual

135\(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered finite stages.

136-/

137theorem freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases_standardTopology

138 (hdir : Directed (· ≤ ·) (id : J → J))

139 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),

140 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,

141 modNCompletedCoeffMap

142 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)

143 (modNCompletedCoeffMap

144 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)

145 (hzcIndex hij).1 a) =

146 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)

147 (modNCompletedCoeffMap

148 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))

149 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),

150 ∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,

151 qmap i

152 ((OpenNormalSubgroupInClass.map

153 (C := C) (G := H)

154 (U := OrderDual.ofDual (zcIndex i).2)

155 (V := OrderDual.ofDual (zcIndex j).2)

156 (hzcIndex hij).2) q) =

157 foxAlgebraicStageTargetQuotientMap (X := X) (hN hij) (qmap j q))

158 (hleft_basis :

159 HasAdditiveIdentityQuotientKernelNeighbourhoodBasis

160 (A := ZCFreeFoxCoordinates C (X := X) (H := H))

161 (fun j : J =>

162 zcFreeFoxCoordinatesBifilteredStageMap

163 (C := C) (X := X) (H := H) Nstage nstage

164 (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap

165 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j))

166 (hright_basis :

167 HasIdentityQuotientKernelNeighbourhoodBasis

168 (Y := H)

169 (fun j : J =>

170 zcCompletedGroupAlgebraBifilteredStageRightMap

171 (C := C) (X := X) (H := H) Nstage zcIndex qmap j)) :

172 HasIdentityQuotientKernelNeighbourhoodBasis

173 (Y := ZCCompletedFoxSemidirect C X H)

174 (fun j : J =>

175 freeProCZCCompletedFoxSemidirectZCBifilteredStageMap

176 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j) := by

177 exact

178 freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases

179 (C := C) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex

180 hmod qmap

181 (zcCompletedFoxSemidirect_hasRectangularIdentityNeighbourhoods

182 (C := C) X H)

183 hdir hcoeff_mod hqmap_transition hleft_basis hright_basis

184

185

186omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in

187/--

188Standard-topology additive kernel basis for completed Fox coordinates, reduced to the

189coefficient-ring kernel basis. For finite Fox coordinate families, product neighborhoods give

190the coordinate rectangles needed for the coordinate-kernel theorem.

191-/

192theorem zcFreeFoxCoordinatesBifilteredStageMap_additive_basis_of_coeff_basis_standardTopology

193 [Finite X] [Nonempty J]

194 (hdir : Directed (· ≤ ·) (id : J → J))

195 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),

196 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,

197 modNCompletedCoeffMap

198 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)

199 (modNCompletedCoeffMap

200 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)

201 (hzcIndex hij).1 a) =

202 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)

203 (modNCompletedCoeffMap

204 (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))

205 (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),

206 ∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,

207 qmap i

208 ((OpenNormalSubgroupInClass.map

209 (C := C) (G := H)

210 (U := OrderDual.ofDual (zcIndex i).2)

211 (V := OrderDual.ofDual (zcIndex j).2)

212 (hzcIndex hij).2) q) =

213 foxAlgebraicStageTargetQuotientMap (X := X) (hN hij) (qmap j q))

214 (hcoeff_basis :

215 HasAdditiveIdentityQuotientKernelNeighbourhoodBasis

216 (A := ZCCompletedGroupAlgebra C H)

217 (fun j : J =>

218 (zcCompletedGroupAlgebraBifilteredStageCoeffMap

219 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j).toAddMonoidHom)) :

220 HasAdditiveIdentityQuotientKernelNeighbourhoodBasis

221 (A := ZCFreeFoxCoordinates C (X := X) (H := H))

222 (fun j : J =>

223 zcFreeFoxCoordinatesBifilteredStageMap

224 (C := C) (X := X) (H := H) Nstage nstage

225 (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap

226 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j) := by

227 exact

228 zcFreeFoxCoordinatesBifilteredStageMap_additive_basis_of_coeff_basis

229 (C := C) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex

230 hmod qmap

231 (zcFreeFoxCoordinates_hasFiniteCoordinateZeroRectangularNeighbourhoods

232 (C := C) X H)

233 hdir hcoeff_mod hqmap_transition hcoeff_basis

234

235omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in

236/--

237The semidirect kernel basis for the standard topology from coefficient and target component

238bases. This is the componentwise kernel-basis theorem with the left coordinate basis built

239internally from the coefficient maps \(\mathbb{Z}_C\llbracket H\rrbracket \to

240(\mathbb{Z}/n_j\mathbb{Z})[F/N_j]\).

241-/

242theorem semiZCBiStageMap_identityBasis_of_coeff_rightBases

243 [Finite X] [Nonempty J]

244 (hdir : Directed (· ≤ ·) (id : J → J))

245 (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),

246 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,

247 modNCompletedCoeffMap

248 (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)

249 (modNCompletedCoeffMap

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)

253 (modNCompletedCoeffMap

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 C (zcIndex j).2,

257 qmap i

258 ((OpenNormalSubgroupInClass.map

259 (C := C) (G := H)

260 (U := OrderDual.ofDual (zcIndex i).2)

261 (V := OrderDual.ofDual (zcIndex j).2)

262 (hzcIndex hij).2) q) =

263 foxAlgebraicStageTargetQuotientMap (X := X) (hN hij) (qmap j q))

264 (hcoeff_basis :

265 HasAdditiveIdentityQuotientKernelNeighbourhoodBasis

266 (A := ZCCompletedGroupAlgebra C H)

267 (fun j : J =>

268 (zcCompletedGroupAlgebraBifilteredStageCoeffMap

269 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j).toAddMonoidHom))

270 (hright_basis :

271 HasIdentityQuotientKernelNeighbourhoodBasis

272 (Y := H)

273 (fun j : J =>

274 zcCompletedGroupAlgebraBifilteredStageRightMap

275 (C := C) (X := X) (H := H) Nstage zcIndex qmap j)) :

276 HasIdentityQuotientKernelNeighbourhoodBasis

277 (Y := ZCCompletedFoxSemidirect C X H)

278 (fun j : J =>

279 freeProCZCCompletedFoxSemidirectZCBifilteredStageMap

280 (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j) := by

281 exact

282 freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases_standardTopology

283 (C := C) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex

284 hmod qmap hdir hcoeff_mod hqmap_transition

285 (zcFreeFoxCoordinatesBifilteredStageMap_additive_basis_of_coeff_basis_standardTopology

286 (C := C) (X := X) (H := H) Nstage nstage hN hn zcIndex hzcIndex

287 hmod qmap hdir hcoeff_mod hqmap_transition hcoeff_basis)

288 hright_basis

289

290end BifilteredZCStandardTopology

291

292end

293

294end FoxDifferential