Source: ProCGroups.InverseSystems.CofinalityAndDensity

1import ProCGroups.InverseSystems.CompatibilityAndSurjectivity

3/-!

4# Cofinal reindexing, density, and projection neighborhoods

6For inverse systems over directed preorders, this module controls neighborhoods by finitely many

7coordinates and studies the map induced by a morphism on limits. It proves density and

8surjectivity criteria, invariance of the limit under cofinal reindexing or restriction, and the

9projection-preimage basis for compact Hausdorff systems.

10-/

12open Set

13open scoped Topology

15namespace ProCGroups.InverseSystems

17universe u v w

19section

21variable {I : Type u} [Preorder I]

23attribute [instance] InverseSystem.topologicalSpace

25namespace InverseSystem

27variable (S : InverseSystem (I := I))

29/--

30Every open neighborhood in the inverse limit contains the inverse image of an open set along one

31projection.

32-/

33theorem exists_projection_preimage_subset [Nonempty I]

34 (hdir : Directed (· ≤ ·) (id : I → I)) {x : S.inverseLimit} {U : Set S.inverseLimit}

35 (hU : IsOpen U) (hx : x ∈ U) :

36 ∃ i, ∃ V : Set (S.X i), IsOpen V ∧ S.projection i x ∈ V ∧ S.projection i ⁻¹' V ⊆ U := by

37 classical

38 have hUx : U ∈ 𝓝 x := hU.mem_nhds hx

39 rw [nhds_subtype_eq_comap, Filter.mem_comap] at hUx

40 rcases hUx with ⟨W, hW, hWU⟩

41 rw [mem_nhds_iff] at hW

42 rcases hW with ⟨W', hW'W, hW'open, hxW'⟩

43 rcases (isOpen_pi_iff.mp hW'open) x.1 hxW' with ⟨s, Us, hUs, hsW'⟩

44 by_cases hs : s.Nonempty

45 · rcases exists_upperBound_finset (I := I) hdir s hs with ⟨j, hj⟩

46 let V : Set (S.X j) := ⋂ i ∈ s, if hi : i ∈ s then S.map (hj i hi) ⁻¹' Us i else univ

47 refine ⟨j, V, ?_, ?_, ?_⟩

48 · refine isOpen_biInter_finset fun i hi => ?_

49 simpa [hi] using (hUs i hi).1.preimage (S.continuous_map (hj i hi))

50 · change S.projection j x ∈ ⋂ i ∈ s, if hi : i ∈ s then S.map (hj i hi) ⁻¹' Us i else univ

51 rw [Set.mem_iInter]

52 intro i

53 rw [Set.mem_iInter]

54 intro hi

55 have hxji : S.map (hj i hi) (S.projection j x) ∈ Us i := by

56 rw [S.projection_compatible x i j (hj i hi)]

57 exact (hUs i hi).2

58 simpa [hi, Set.mem_preimage] using hxji

59 · intro y hy

60 apply hWU

61 apply hW'W

62 apply hsW'

63 change S.projection j y ∈ ⋂ i ∈ s, if hi : i ∈ s then S.map (hj i hi) ⁻¹' Us i else univ at hy

64 rw [Set.mem_iInter] at hy

65 intro i hi

66 have hyi : S.map (hj i hi) (S.projection j y) ∈ Us i := by

67 have hyji := Set.mem_iInter.1 (hy i) hi

68 have hif :

69 (if hi' : i ∈ s then S.map (hj i hi') ⁻¹' Us i else univ) =

70 S.map (hj i hi) ⁻¹' Us i := by

71 ext z

72 by_cases h : i ∈ s

73 · rw [dif_pos h]

74 · exact (h.elim hi)

75 rw [hif] at hyji

76 simpa [Set.mem_preimage] using hyji

77 rw [S.projection_compatible y i j (hj i hi)] at hyi

78 exact hyi

79 · let j : I := Classical.choice ‹Nonempty I›

80 refine ⟨j, univ, isOpen_univ, mem_univ _, ?_⟩

81 intro y hy

82 apply hWU

83 apply hW'W

84 apply hsW'

85 have hs' : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hs

86 have : y.1 ∈ ((↑s : Set I).pi Us) := by

87 simp only [hs', Finset.coe_empty, empty_pi, mem_univ]

88 exact this

90/--

91A compatible family of surjections over a nonempty directed index preorder induces a dense map

92to the inverse limit.

93-/

94theorem denseRange_lift {X : Type w} [Nonempty I]

95 (ρ : ∀ i, X → S.X i) (hρ : S.CompatibleMaps ρ)

96 (hsurj : ∀ i, Function.Surjective (ρ i)) (hdir : Directed (· ≤ ·) (id : I → I)) :

97 DenseRange (S.inverseLimitLift ρ hρ) := by

98 rw [DenseRange, dense_iff_inter_open]

99 intro U hU hUne

100 rcases hUne with ⟨y, hyU⟩

101 rcases S.exists_projection_preimage_subset hdir hU hyU with ⟨i, V, hVopen, hyV, hVU⟩

102 rcases hsurj i (S.projection i y) with ⟨x, hx⟩

103 refine ⟨S.inverseLimitLift ρ hρ x, hVU ?_, ⟨x, rfl⟩⟩

104 change ρ i x ∈ V

105 rw [hx]

106 exact hyV

107

108/-- Reindexing an inverse system along a monotone map. -/

109def reindex {K : Type w} [Preorder K] (σ : K → I) (hσ : Monotone σ) :

110 InverseSystem (I := K) where

111 X := fun k => S.X (σ k)

112 topologicalSpace := fun k => inferInstance

113 map := fun {i j} hij => S.map (hσ hij)

114 continuous_map := fun {i j} hij => S.continuous_map (hσ hij)

115 map_id := fun k => by

116 simpa using S.map_id (σ k)

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

118 simpa using S.map_comp (hσ hij) (hσ hjk)

119

120/-- The inverse system obtained by restricting the index preorder to a subset. -/

121def restrict (J : Set I) : InverseSystem (I := J) :=

122 S.reindex (fun j : J => j.1) (fun {_ _} hij => hij)

123

124/-- The inverse limit is unchanged after reindexing along a monotone cofinal map. -/

125noncomputable def homeomorph_reindex_cofinal {K : Type w} [Preorder K]

126 (σ : K → I) (hσ : Monotone σ) (hdirK : Directed (· ≤ ·) (id : K → K))

127 (hcofinal : ∀ i : I, ∃ k : K, i ≤ σ k) :

128 S.inverseLimit ≃ₜ (S.reindex σ hσ).inverseLimit := by

129 classical

130 let R := S.reindex σ hσ

131 have hcompatR : R.CompatibleMaps (fun k => S.projection (σ k)) := by

132 intro i j hij

133 funext x

134 exact S.projection_compatible x (σ i) (σ j) (hσ hij)

135 let r : S.inverseLimit → R.inverseLimit := R.inverseLimitLift (fun k => S.projection (σ k))

136 hcompatR

137 choose τ hτ using hcofinal

138 let ψ : ∀ i, R.inverseLimit → S.X i := fun i => S.map (hτ i) ∘ R.projection (τ i)

139 have hψ_eq :

140 ∀ {i : I} (k : K) (hik : i ≤ σ k) (x : R.inverseLimit),

141 ψ i x = S.map hik (R.projection k x) := by

142 intro i k hik x

143 rcases hdirK (τ i) k with ⟨ℓ, hτℓ, hkℓ⟩

144 calc

145 ψ i x = S.map (hτ i) (R.projection (τ i) x) := rfl

146 _ = S.map (hτ i) (S.map (hσ hτℓ) (R.projection ℓ x)) := by

147 simpa [R, reindex] using congrArg (S.map (hτ i)) ((R.projection_compatible x (τ i) ℓ

148 hτℓ).symm)

149 _ = S.map ((hτ i).trans (hσ hτℓ)) (R.projection ℓ x) := by

150 rw [S.map_comp_apply (hτ i) (hσ hτℓ)]

151 _ = S.map (hik.trans (hσ hkℓ)) (R.projection ℓ x) := by

152 have hproof : (hτ i).trans (hσ hτℓ) = hik.trans (hσ hkℓ) := Subsingleton.elim _ _

153 rw [hproof]

154 _ = S.map hik (S.map (hσ hkℓ) (R.projection ℓ x)) := by

155 rw [S.map_comp_apply hik (hσ hkℓ)]

156 _ = S.map hik (R.projection k x) := by

157 simpa [R, reindex] using congrArg (S.map hik) (R.projection_compatible x k ℓ hkℓ)

158 have hcompatψ : S.CompatibleMaps ψ := by

159 intro i j hij

160 funext x

161 calc

162 S.map hij (ψ j x) = S.map hij (S.map (hτ j) (R.projection (τ j) x)) := rfl

163 _ = S.map (hij.trans (hτ j)) (R.projection (τ j) x) := by

164 rw [S.map_comp_apply hij (hτ j)]

165 _ = ψ i x := by

166 symm

167 exact hψ_eq (k := τ j) (hik := hij.trans (hτ j)) x

168 let s : R.inverseLimit → S.inverseLimit := S.inverseLimitLift ψ hcompatψ

169 refine

170 { toFun := r

171 invFun := s

172 left_inv := ?_

173 right_inv := ?_

174 continuous_toFun := R.continuous_inverseLimitLift (fun k => S.projection (σ k))

175 (fun k => S.continuous_projection (σ k)) hcompatR

176 continuous_invFun := S.continuous_inverseLimitLift ψ

177 (fun i => (S.continuous_map (hτ i)).comp (R.continuous_projection (τ i))) hcompatψ } <;>

178 intro x

179 · apply S.ext

180 intro i

181 calc

182 S.projection i (s (r x)) = ψ i (r x) := by

183 rfl

184 _ = S.map (hτ i) (R.projection (τ i) (r x)) := rfl

185 _ = S.map (hτ i) (S.projection (σ (τ i)) x) := by

186 have hrproj :=

187 R.projection_inverseLimitLift_apply

188 (fun k => S.projection (σ k)) hcompatR (τ i) x

189 change R.projection (τ i) (r x) = S.projection (σ (τ i)) x at hrproj

190 exact congrArg (S.map (hτ i)) hrproj

191 _ = S.projection i x := S.projection_compatible x i (σ (τ i)) (hτ i)

192 · apply R.ext

193 intro k

194 calc

195 R.projection k (r (s x)) = S.projection (σ k) (s x) := by

196 have hrproj :=

197 R.projection_inverseLimitLift_apply

198 (fun k => S.projection (σ k)) hcompatR k (s x)

199 change R.projection k (r (s x)) = S.projection (σ k) (s x) at hrproj

200 exact hrproj

201 _ = ψ (σ k) x := by

202 rfl

203 _ = S.map (le_rfl : σ k ≤ σ k) (R.projection k x) := by

204 exact hψ_eq (k := k) (hik := le_rfl) x

205 _ = (show S.X (σ k) from R.projection k x) := by

206 exact S.map_id_apply (σ k) (R.projection k x)

207

208/--

209After cofinal reindexing, the projection to \(k\) composed with the reindexing homeomorphism is

210the original projection to \(\sigma k\).

211-/

212@[simp 900] theorem π_comp_homeomorph_reindex_cofinal {K : Type w} [Preorder K]

213 (σ : K → I) (hσ : Monotone σ) (hdirK : Directed (· ≤ ·) (id : K → K))

214 (hcofinal : ∀ i : I, ∃ k : K, i ≤ σ k) (k : K) :

215 (S.reindex σ hσ).projection k ∘ S.homeomorph_reindex_cofinal σ hσ hdirK hcofinal =

216 S.projection (σ k) := by

217 classical

218 let R := S.reindex σ hσ

219 have hcompatR : R.CompatibleMaps (fun k => S.projection (σ k)) := by

220 intro i j hij

221 funext x

222 exact S.projection_compatible x (σ i) (σ j) (hσ hij)

223 funext x

224 change

225 R.projection k

226 (R.inverseLimitLift (fun k => S.projection (σ k)) hcompatR x) =

227 S.projection (σ k) x

228 exact

229 R.projection_inverseLimitLift_apply

230 (fun k => S.projection (σ k)) hcompatR k x

231

232/-- The cofinal reindexing homeomorphism is characterized by its projections. -/

233noncomputable def homeomorph_restrict_cofinal (J : Set I)

234 (hdirJ : Directed (· ≤ ·) (id : J → J)) (hcofinal : ∀ i, ∃ j : J, i ≤ j.1) :

235 S.inverseLimit ≃ₜ (S.restrict J).inverseLimit :=

236 S.homeomorph_reindex_cofinal (fun j : J => j.1) (fun {_ _} hij => hij) hdirJ hcofinal

237

238/--

239For a cofinal restriction, projecting to \(j\) after the restriction homeomorphism is the same

240as the original projection to the underlying index of \(j\).

241-/

242@[simp 900] theorem π_comp_homeomorph_restrict_cofinal (J : Set I)

243 (hdirJ : Directed (· ≤ ·) (id : J → J)) (hcofinal : ∀ i, ∃ j : J, i ≤ j.1) (j : J) :

244 (S.restrict J).projection j ∘ S.homeomorph_restrict_cofinal J hdirJ hcofinal = S.projection

245 j.1 := by

246 exact

247 (S.π_comp_homeomorph_reindex_cofinal (σ := fun j : J => j.1)

248 (hσ := fun {_ _} hij => hij) hdirJ hcofinal j)

249

250/--

251In a surjective inverse system of compact Hausdorff nonempty spaces, each projection from the

252inverse limit is surjective.

253-/

254theorem surjective_π [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

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

256 (hsurj : ∀ {i j : I} (hij : i ≤ j), Function.Surjective (S.map hij)) (j : I) :

257 Function.Surjective (S.projection j) := by

258 let J : Set I := Set.Ici j

259 have hdirJ : Directed (· ≤ ·) (id : J → J) := by

260 intro a b

261 rcases hdir a.1 b.1 with ⟨k, hak, hbk⟩

262 refine ⟨⟨k, a.2.trans hak⟩, hak, hbk⟩

263 have hcofinal : ∀ i, ∃ k : J, i ≤ k.1 := by

264 intro i

265 rcases hdir i j with ⟨k, hik, hjk⟩

266 exact ⟨⟨k, hjk⟩, hik⟩

267 let e := S.homeomorph_restrict_cofinal J hdirJ hcofinal

268 let j0 : J := ⟨j, le_rfl⟩

269 intro xj

270 let T : InverseSystem (I := J) := {

271 X := fun k => {x : S.X k.1 // S.map k.2 x = xj}

272 topologicalSpace := fun _ => inferInstance

273 map := fun {a b} hab x =>

274 ⟨S.map hab x.1, by

275 have hproof : a.2.trans hab = b.2 := Subsingleton.elim _ _

276 calc

277 S.map a.2 (S.map hab x.1) = S.map (a.2.trans hab) x.1 := by rw [S.map_comp_apply a.2 hab]

278 _ = S.map b.2 x.1 := by rw [hproof]

279 _ = xj := x.2⟩

280 continuous_map := fun {a b} hab =>

281 Continuous.subtype_mk ((S.continuous_map hab).comp continuous_subtype_val) fun x => by

282 have hproof : a.2.trans hab = b.2 := Subsingleton.elim _ _

283 calc

284 S.map a.2 (S.map hab x.1) = S.map (a.2.trans hab) x.1 := by rw [S.map_comp_apply a.2 hab]

285 _ = S.map b.2 x.1 := by rw [hproof]

286 _ = xj := x.2

287 map_id := fun a => by

288 funext x

289 apply Subtype.ext

290 simp only [map_id_apply, id_eq]

291 map_comp := fun {a b c} hab hbc => by

292 funext x

293 apply Subtype.ext

294 simp only [Function.comp_apply, S.map_comp_apply hab hbc]}

295 letI : ∀ k, Nonempty (T.X k) := fun k => by

296 rcases hsurj k.2 xj with ⟨x, hx⟩

297 exact ⟨⟨x, hx⟩⟩

298 letI : ∀ k, T2Space (T.X k) := fun _ => inferInstance

299 letI : ∀ k, CompactSpace (T.X k) := fun k => by

300 let hs : IsClosed {x : S.X k.1 | S.map k.2 x = xj} :=

301 isClosed_eq (S.continuous_map k.2) continuous_const

302 change CompactSpace {x : S.X k.1 // S.map k.2 x = xj}

303 exact hs.isClosedEmbedding_subtypeVal.compactSpace

304 rcases InverseSystem.nonempty_inverseLimit (S := T) hdirJ with ⟨y⟩

305 let xlimJ : (S.restrict J).inverseLimit := ⟨fun k => (y.1 k).1, by

306 intro a b hab

307 exact congrArg Subtype.val (y.2 a b hab)⟩

308 have hj0 : (S.restrict J).projection j0 xlimJ = xj := by

309 change (y.1 j0).1 = xj

310 have hprop := (y.1 j0).2

311 have hproof : j0.2 = (le_rfl : j ≤ j) := Subsingleton.elim _ _

312 rw [hproof] at hprop

313 exact (S.map_id_apply j (y.1 j0).1).symm.trans hprop

314 have hstep : S.projection j (e.symm xlimJ) = (S.restrict J).projection j0 xlimJ := by

315 have he :=

316 congrFun (S.π_comp_homeomorph_restrict_cofinal J hdirJ hcofinal j0)

317 (e.symm xlimJ)

318 change

319 (S.restrict J).projection j0 (e (e.symm xlimJ)) =

320 S.projection j (e.symm xlimJ) at he

321 rw [e.apply_symm_apply] at he

322 exact he.symm

323 refine ⟨e.symm xlimJ, ?_⟩

324 rw [hstep]

325 exact hj0

326

327end InverseSystem

328end

329

330/--

331If each component has a chosen basis, then the inverse images of basis elements under the

332projection maps form a basis of the inverse limit.

333-/

334theorem InverseSystem.isTopologicalBasis_projection_preimages {I : Type u} [Preorder I]

335 (S : InverseSystem (I := I)) [Nonempty I] (hdir : Directed (· ≤ ·) (id : I → I))

336 (B : ∀ i, Set (Set (S.X i))) (hB : ∀ i, TopologicalSpace.IsTopologicalBasis (B i)) :

337 TopologicalSpace.IsTopologicalBasis

338 {W : Set S.inverseLimit | ∃ i, ∃ V ∈ B i, W = S.projection i ⁻¹' V} := by

339 classical

340 refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds ?_ ?_

341 · rintro W ⟨i, V, hV, rfl⟩

342 exact ((hB i).isOpen hV).preimage (S.continuous_projection i)

343 · intro x U hx hU

344 rcases S.exists_projection_preimage_subset hdir hU hx with ⟨i, V, hVopen, hxV, hVU⟩

345 rcases (hB i).exists_subset_of_mem_open hxV hVopen with ⟨W, hW, hxW, hWV⟩

346 refine ⟨S.projection i ⁻¹' W, ⟨i, W, hW, rfl⟩, hxW, ?_⟩

347 exact (Set.preimage_mono hWV).trans hVU

348

349end ProCGroups.InverseSystems