Source: ProCGroups.InverseSystems.ProjectionImageSystems

1import ProCGroups.InverseSystems.CofinalityAndDensity

3/-!

4# Inverse systems formed from projection images

6A subset of an inverse limit determines an inverse system of its stagewise projection images.

7This module constructs the comparison lift, proves reconstruction for closed subsets of compact

8Hausdorff systems, and derives closure and equality criteria from stagewise images. It also

9handles systems whose transition maps are surjective by identifying their projection images.

10-/

12open Set

13open scoped Topology

15namespace ProCGroups.InverseSystems

17universe u v w

19/-- The inverse system formed by the projection images of a subset of an inverse limit. -/

20def InverseSystem.projectionImageSystem {I : Type u} [Preorder I]

21 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :

22 InverseSystem (I := I) where

23 X := fun i => S.projection i '' Y

24 topologicalSpace := fun _ => inferInstance

25 map := fun {i j} hij x => ⟨S.map hij x.1, by

26 rcases x.2 with ⟨y, hy, hxy⟩

27 refine ⟨y, hy, ?_⟩

28 simpa [← hxy] using (S.projection_compatible y i j hij).symm⟩

29 continuous_map := fun {i j} hij =>

30 Continuous.subtype_mk

31 ((S.continuous_map hij).comp continuous_subtype_val) (fun x => by

32 rcases x.2 with ⟨y, hy, hxy⟩

33 refine ⟨y, hy, ?_⟩

34 simpa [Function.comp, ← hxy] using (S.projection_compatible y i j hij).symm)

35 map_id := fun i => by

36 funext x

37 apply Subtype.ext

38 simp only [map_id_apply, id_eq]

39 map_comp := fun {i j k} hij hjk => by

40 funext x

41 apply Subtype.ext

42 simp only [Function.comp_apply, S.map_comp_apply hij hjk]

44/-- The canonical morphism from the projection-image system into the ambient inverse system. -/

45def projectionImageInclusion {I : Type u} [Preorder I]

46 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :

47 (S.projectionImageSystem Y).Morphism S where

48 map := fun _ => Subtype.val

49 continuous_map := fun _ => continuous_subtype_val

50 comm := fun {i j} hij => by

51 funext x

52 rfl

54/--

55The coordinatewise section map from a subset of an inverse limit to its projection-image system.

56-/

57def projectionImageSectionMap {I : Type u} [Preorder I]

58 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) (i : I) :

59 Y → (S.projectionImageSystem Y).X i :=

60 fun y => ⟨S.projection i y.1, ⟨y.1, y.2, rfl⟩⟩

62/--

63The section map from the projection-image inverse limit back to the closed subspace is

64continuous.

65-/

66theorem continuous_projectionImageSectionMap {I : Type u} [Preorder I]

67 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) (i : I) :

68 Continuous (projectionImageSectionMap S Y i) := by

69 exact Continuous.subtype_mk ((S.continuous_projection i).comp continuous_subtype_val)

70 (fun y => ⟨y.1, y.2, rfl⟩)

72/-- The projection-image section maps are compatible with the inverse-system transition maps. -/

73theorem compatible_projectionImageSectionMap {I : Type u} [Preorder I]

74 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :

75 (S.projectionImageSystem Y).CompatibleMaps (projectionImageSectionMap S Y) := by

76 intro i j hij

77 funext y

78 apply Subtype.ext

79 exact S.projection_compatible y.1 i j hij

81/-- Each coordinate section map onto a projection image is surjective. -/

82theorem surjective_projectionImageSectionMap {I : Type u} [Preorder I]

83 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) (i : I) :

84 Function.Surjective (projectionImageSectionMap S Y i) := by

85 intro x

86 rcases x.2 with ⟨y, hy, hxy⟩

87 refine ⟨⟨y, hy⟩, ?_⟩

88 apply Subtype.ext

89 change S.projection i y = x.1

90 exact hxy

92/--

93The canonical lift from a subset of an inverse limit to the inverse limit of its

94projection-image system.

95-/

96def projectionImageLift {I : Type u} [Preorder I]

97 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :

98 Y → (S.projectionImageSystem Y).inverseLimit :=

99 (S.projectionImageSystem Y).inverseLimitLift (projectionImageSectionMap S Y)

100 (compatible_projectionImageSectionMap S Y)

101

102/--

103The lift from a closed subspace into the inverse limit of its projection images is continuous.

104-/

105theorem continuous_projectionImageLift {I : Type u} [Preorder I]

106 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :

107 Continuous (projectionImageLift S Y) := by

108 exact (S.projectionImageSystem Y).continuous_inverseLimitLift (projectionImageSectionMap S Y)

109 (continuous_projectionImageSectionMap S Y) (compatible_projectionImageSectionMap S Y)

110

111/--

112For a closed subset of a compact Hausdorff inverse limit, the canonical projection-image lift is

113surjective.

114-/

115theorem surjective_projectionImageLift {I : Type u} [Preorder I] [Nonempty I]

116 (S : InverseSystem (I := I)) [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

117 (hdir : Directed (· ≤ ·) (id : I → I)) (Y : Set S.inverseLimit) (hY : IsClosed Y) :

118 Function.Surjective (projectionImageLift S Y) := by

119 let T := S.projectionImageSystem Y

120 letI : CompactSpace Y := by

121 simpa using hY.isClosedEmbedding_subtypeVal.compactSpace

122 letI : ∀ i, T2Space (T.X i) := fun i => by

123 change T2Space (S.projection i '' Y)

124 infer_instance

125 exact T.surjective_inverseLimitLift (projectionImageSectionMap S Y)

126 (continuous_projectionImageSectionMap S Y)

127 (compatible_projectionImageSectionMap S Y) (surjective_projectionImageSectionMap S Y) hdir

128

129/--

130Composing the projection-image lift with the inclusion morphism recovers the underlying point of

131the original inverse limit.

132-/

133theorem projectionImageLift_comp_subtype {I : Type u} [Preorder I]

134 (S : InverseSystem (I := I)) (Y : Set S.inverseLimit) :

135 (S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) ∘

136 projectionImageLift S Y = Subtype.val := by

137 funext y

138 apply S.ext

139 intro i

140 have hpi :

141 (S.projectionImageSystem Y).projection i (projectionImageLift S Y y) =

142 projectionImageSectionMap S Y i y := by

143 simpa [Function.comp, projectionImageLift] using

144 congrFun

145 ((S.projectionImageSystem Y).projection_comp_inverseLimitLift (projectionImageSectionMap

146 S Y)

147 (compatible_projectionImageSectionMap S Y) i) y

148 calc

149 S.projection i ((S.projectionImageSystem Y).limMap (projectionImageInclusion S Y)

150 (projectionImageLift S Y y))

151 = (projectionImageInclusion S Y).map i

152 ((S.projectionImageSystem Y).projection i (projectionImageLift S Y y)) := by

153 simpa [Function.comp] using

154 congrFun

155 ((S.projectionImageSystem Y).π_comp_limMap

156 (Θ := projectionImageInclusion S Y) i) (projectionImageLift S Y y)

157 _ = ((S.projectionImageSystem Y).projection i (projectionImageLift S Y y)).1 := rfl

158 _ = (projectionImageSectionMap S Y i y).1 := by rw [hpi]

159 _ = S.projection i y.1 := rfl

160

161/-- The transition maps in the projection-image system are always surjective. -/

162theorem InverseSystem.surjective_projectionImageSystem_map

163 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) (Y : Set S.inverseLimit)

164 {i j : I} (hij : i ≤ j) :

165 Function.Surjective ((S.projectionImageSystem Y).map hij) := by

166 intro x

167 rcases x.2 with ⟨y, hy, hxy⟩

168 refine ⟨⟨S.projection j y, ⟨y, hy, rfl⟩⟩, ?_⟩

169 apply Subtype.ext

170 change S.map hij (S.projection j y) = x.1

171 rw [S.projection_compatible y i j hij]

172 exact hxy

173

174/--

175A closed subset of an inverse limit is homeomorphic to the inverse limit of its projection-image

176system.

177-/

178noncomputable def InverseSystem.homeomorph_projectionImageSystem_of_isClosed

179 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]

180 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

181 (hdir : Directed (· ≤ ·) (id : I → I))

182 (Y : Set S.inverseLimit) (hY : IsClosed Y) :

183 Y ≃ₜ (S.projectionImageSystem Y).inverseLimit := by

184 classical

185 letI : CompactSpace Y := by

186 simpa using hY.isClosedEmbedding_subtypeVal.compactSpace

187 letI : ∀ i, T2Space ((S.projectionImageSystem Y).X i) := fun i => by

188 change T2Space (S.projection i '' Y)

189 infer_instance

190 let e := projectionImageLift S Y

191 have he_inj : Function.Injective e := by

192 intro y y' hyy

193 have hy : y.1 = y'.1 := by

194 calc

195 y.1 = (S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) (e y) := by

196 simpa [Function.comp] using (congrFun (projectionImageLift_comp_subtype S Y) y).symm

197 _ = (S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) (e y') := by

198 rw [hyy]

199 _ = y'.1 := by

200 simpa [Function.comp] using congrFun (projectionImageLift_comp_subtype S Y) y'

201 exact Subtype.ext hy

202 exact Continuous.homeoOfEquivCompactToT2

203 (f := Equiv.ofBijective e

204 ⟨he_inj, surjective_projectionImageLift S hdir Y hY⟩)

205 (continuous_projectionImageLift S Y)

206

207/-- The range of the limit map is exactly the compatible inverse limit of the projection images. -/

208theorem range_limMap_projectionImageInclusion_eq

209 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]

210 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

211 (hdir : Directed (· ≤ ·) (id : I → I))

212 (Y : Set S.inverseLimit) (hY : IsClosed Y) :

213 Set.range ((S.projectionImageSystem Y).limMap (projectionImageInclusion S Y)) = Y := by

214 classical

215 apply le_antisymm

216 · rintro x ⟨z, rfl⟩

217 rcases surjective_projectionImageLift S hdir Y hY z with ⟨y, hy⟩

218 have hx :

219 (S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) z = y.1 := by

220 calc

221 (S.projectionImageSystem Y).limMap (projectionImageInclusion S Y) z

222 = (S.projectionImageSystem Y).limMap

223 (projectionImageInclusion S Y) (projectionImageLift S Y y) := by

224 rw [hy]

225 _ = y.1 := by

226 simpa [Function.comp] using congrFun (projectionImageLift_comp_subtype S Y) y

227 exact hx ▸ y.2

228 · intro y hy

229 refine ⟨projectionImageLift S Y ⟨y, hy⟩, ?_⟩

230 simpa [Function.comp] using congrFun (projectionImageLift_comp_subtype S Y) ⟨y, hy⟩

231

232/-- Membership in the projected image system can be checked coordinatewise. -/

233theorem InverseSystem.mem_isClosed_iff_forall_projection_mem

234 {I : Type u} [Preorder I] {S : InverseSystem (I := I)} [Nonempty I]

235 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

236 (hdir : Directed (· ≤ ·) (id : I → I))

237 {Y : Set S.inverseLimit} (hY : IsClosed Y) {x : S.inverseLimit} :

238 x ∈ Y ↔ ∀ i, S.projection i x ∈ S.projection i '' Y := by

239 classical

240 constructor

241 · intro hx i

242 exact ⟨x, hx, rfl⟩

243 · intro hx

244 let T := S.projectionImageSystem Y

245 let incl : T.Morphism S := projectionImageInclusion S Y

246 have hcompat :

247 T.CompatibleMaps (fun (i : I) (_ : Unit) => (⟨S.projection i x, hx i⟩ : T.X i)) := by

248 intro i j hij

249 funext _

250 apply Subtype.ext

251 exact S.projection_compatible x i j hij

252 let z : T.inverseLimit :=

253 T.inverseLimitLift (fun (i : I) (_ : Unit) => (⟨S.projection i x, hx i⟩ : T.X i)) hcompat ()

254 have hz : T.limMap incl z = x := by

255 apply S.ext

256 intro i

257 have hpi : T.projection i z = (⟨S.projection i x, hx i⟩ : T.X i) := by

258 simpa [Function.comp, z] using

259 congrFun

260 (T.projection_comp_inverseLimitLift (fun (i : I) (_ : Unit) => (⟨S.projection i x,

261 hx i⟩ : T.X i)) hcompat i) ()

262 calc

263 S.projection i (T.limMap incl z) = incl.map i (T.projection i z) := by

264 simpa [Function.comp] using congrFun (T.π_comp_limMap (Θ := incl) i) z

265 _ = (T.projection i z).1 := rfl

266 _ = S.projection i x := by rw [hpi]

267 have hxrange : x ∈ Set.range (T.limMap incl) := ⟨z, hz⟩

268 rw [range_limMap_projectionImageInclusion_eq S hdir Y hY] at hxrange

269 exact hxrange

270

271/-- A closed subspace of an inverse limit is again an inverse limit of its projection images. -/

272theorem InverseSystem.exists_homeomorph_closed_subspace_projection_images

273 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]

274 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

275 (hdir : Directed (· ≤ ·) (id : I → I))

276 (Y : Set S.inverseLimit) (hY : IsClosed Y) :

277 (∀ i, Nonempty (((S.projectionImageSystem Y).X i) ≃ₜ (S.projection i '' Y))) ∧

278 Nonempty (Y ≃ₜ (S.projectionImageSystem Y).inverseLimit) := by

279 constructor

280 · intro i

281 exact ⟨Homeomorph.refl _⟩

282 · exact ⟨S.homeomorph_projectionImageSystem_of_isClosed hdir Y hY⟩

283

284/-- The projection of the closure of a subset equals the closure of the projection image. -/

285theorem InverseSystem.projection_image_closure_eq_closure_projection_image

286 {I : Type u} [Preorder I] (S : InverseSystem (I := I))

287 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

288 (i : I) (Y : Set S.inverseLimit) :

289 S.projection i '' closure Y = closure (S.projection i '' Y) := by

290 let hclosed : IsClosedMap (S.projection i) := (S.continuous_projection i).isClosedMap

291 simpa using (hclosed.closure_image_eq_of_continuous (S.continuous_projection i) Y).symm

292

293/-

294Projection images of an arbitrary subset need not be closed, even for an inverse system indexed

295by a singleton, so raw projection images cannot reconstruct the closure of that subset. The

296statements below instead form the projection-image system from `closure Y`; the preceding theorem

297then identifies each of its stage images with the closure of the corresponding image of `Y`.

298-/

299/--

300The closure of a subset of an inverse limit is homeomorphic to the inverse limit of the

301projection-image system of that closure.

302-/

303theorem InverseSystem.exists_homeomorph_closure_projection_images

304 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]

305 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

306 (hdir : Directed (· ≤ ·) (id : I → I))

307 (Y : Set S.inverseLimit) :

308 (∀ i, Nonempty (((S.projectionImageSystem (closure Y)).X i) ≃ₜ (S.projection i '' closure Y))) ∧

309 Nonempty (closure Y ≃ₜ (S.projectionImageSystem (closure Y)).inverseLimit) := by

310 simpa using S.exists_homeomorph_closed_subspace_projection_images hdir (Y := closure Y)

311 isClosed_closure

312

313/--

314Closed subsets of the inverse limit are equal when their projection images agree at every stage.

315-/

316theorem InverseSystem.closure_eq_of_projection_images_eq

317 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]

318 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

319 (hdir : Directed (· ≤ ·) (id : I → I))

320 (Y Y' : Set S.inverseLimit)

321 (hproj : ∀ i, S.projection i '' closure Y = S.projection i '' closure Y') :

322 closure Y = closure Y' := by

323 ext x

324 constructor

325 · intro hx

326 rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure] at hx

327 rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure]

328 intro i

329 rw [← hproj i]

330 exact hx i

331 · intro hx

332 rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure] at hx

333 rw [S.mem_isClosed_iff_forall_projection_mem hdir isClosed_closure]

334 intro i

335 rw [hproj i]

336 exact hx i

337

338/--

339Equal raw projection images of two subsets force their closures in the inverse limit to be

340equal.

341-/

342theorem InverseSystem.closure_eq_of_projection_images_eq_of_subsets

343 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]

344 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

345 (hdir : Directed (· ≤ ·) (id : I → I))

346 (Y Y' : Set S.inverseLimit)

347 (hproj : ∀ i, S.projection i '' Y = S.projection i '' Y') :

348 closure Y = closure Y' := by

349 apply S.closure_eq_of_projection_images_eq hdir Y Y'

350 intro i

351 calc

352 S.projection i '' closure Y = closure (S.projection i '' Y) := by

353 exact S.projection_image_closure_eq_closure_projection_image i Y

354 _ = closure (S.projection i '' Y') := by rw [hproj i]

355 _ = S.projection i '' closure Y' := by

356 symm

357 exact S.projection_image_closure_eq_closure_projection_image i Y'

358

359/--

360Any inverse system of compact Hausdorff spaces admits a surjective projection-image system with

361the same inverse limit.

362-/

363noncomputable def InverseSystem.homeomorph_surjectiveProjectionImageSystem

364 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]

365 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

366 (hdir : Directed (· ≤ ·) (id : I → I)) :

367 S.inverseLimit ≃ₜ (S.projectionImageSystem (Set.univ : Set S.inverseLimit)).inverseLimit :=

368 (Homeomorph.Set.univ S.inverseLimit).symm.trans

369 (S.homeomorph_projectionImageSystem_of_isClosed hdir Set.univ isClosed_univ)

370

371/--

372The projection-image system of the full inverse limit is surjective and has the same inverse

373limit as the original system.

374-/

375theorem InverseSystem.exists_homeomorph_surjectiveProjectionImageSystem

376 {I : Type u} [Preorder I] (S : InverseSystem (I := I)) [Nonempty I]

377 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

378 (hdir : Directed (· ≤ ·) (id : I → I)) :

379 (∀ {i j : I} (hij : i ≤ j),

380 Function.Surjective ((S.projectionImageSystem (Set.univ : Set S.inverseLimit)).map hij)) ∧

381 Nonempty (S.inverseLimit ≃ₜ

382 (S.projectionImageSystem (Set.univ : Set S.inverseLimit)).inverseLimit) := by

383 constructor

384 · intro i j hij

385 exact S.surjective_projectionImageSystem_map (Y := (Set.univ : Set S.inverseLimit)) hij

386 · exact ⟨S.homeomorph_surjectiveProjectionImageSystem hdir⟩

387

388end ProCGroups.InverseSystems