Source: ProCGroups.InverseSystems.CompatibilityAndSurjectivity

1import ProCGroups.InverseSystems.Basic

2import ProCGroups.InverseSystems.Utilities

4/-!

5# Morphisms of inverse systems and maps on their limits

7Compactness gives nonemptiness of directed inverse limits of nonempty Hausdorff stages. This

8module then defines continuous stagewise morphisms, constructs their induced maps on inverse

9limits, and gives stagewise hypotheses ensuring that those maps are injective, embeddings, or

10surjective.

11-/

13open Set

14open scoped Topology

16namespace ProCGroups.InverseSystems

18universe u v w

20section

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

24attribute [instance] InverseSystem.topologicalSpace

26namespace InverseSystem

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

30/--

31Compatibility restricted to indices below a fixed stage ensures nonemptiness of the inverse

32limit.

33-/

34private def CompatibleUpTo (j : I) (x : ∀ i, S.X i) : Prop :=

35 ∀ k, ∀ hkj : k ≤ j, S.map hkj (x j) = x k

37/--

38For a fixed stage `j`, the product families whose earlier coordinates are determined by their

39`j`-coordinate form a closed subset when all stages are Hausdorff.

40-/

41private theorem isClosed_setOf_compatibleUpTo [∀ i, T2Space (S.X i)] (j : I) :

42 IsClosed {x : ∀ i, S.X i | S.CompatibleUpTo j x} := by

43 simp only [CompatibleUpTo, setOf_forall]

44 refine isClosed_iInter fun k => isClosed_iInter fun hkj => ?_

45 exact isClosed_eq ((S.continuous_map hkj).comp (continuous_apply j)) (continuous_apply k)

47/--

48A point at stage `j`, transported to every earlier stage and completed arbitrarily elsewhere,

49gives a family compatible up to `j`.

50-/

51private theorem compatibleUpTo_nonempty (j : I) [∀ i, Nonempty (S.X i)] :

52 ({x : ∀ i, S.X i | S.CompatibleUpTo j x} : Set (∀ i, S.X i)).Nonempty := by

53 classical

54 let xj : S.X j := Classical.choice (inferInstance : Nonempty (S.X j))

55 let x : ∀ i, S.X i := fun i =>

56 if hij : i ≤ j then S.map hij xj else Classical.choice (inferInstance : Nonempty (S.X i))

57 refine ⟨x, ?_⟩

58 intro k hkj

59 simp only [le_refl, ↓reduceDIte, map_id_apply, hkj, x]

61/-- Compatibility up to a later stage implies compatibility up to every earlier stage. -/

62private theorem compatibleUpTo_mono {j j' : I} (hjj' : j ≤ j') :

63 {x : ∀ i, S.X i | S.CompatibleUpTo j' x} ⊆ {x : ∀ i, S.X i | S.CompatibleUpTo j x} := by

64 intro x hx k hkj

65 calc

66 S.map hkj (x j) = S.map hkj (S.map hjj' (x j')) := by rw [hx j hjj']

67 _ = S.map (hkj.trans hjj') (x j') := by rw [S.map_comp_apply hkj hjj']

68 _ = x k := hx k (hkj.trans hjj')

70/-- The inverse limit of nonempty compact Hausdorff spaces is nonempty. -/

71theorem nonempty_inverseLimit [∀ i, Nonempty (S.X i)] [∀ i, CompactSpace (S.X i)]

72 [∀ i, T2Space (S.X i)] (hdir : Directed (· ≤ ·) (id : I → I)) :

73 Nonempty S.inverseLimit := by

74 classical

75 let Y : I → Set (∀ i, S.X i) := fun j => {x | S.CompatibleUpTo j x}

76 have hclosed : ∀ j, IsClosed (Y j) := fun j => S.isClosed_setOf_compatibleUpTo j

77 have hfinite : ∀ s : Finset I, (⋂ i ∈ s, Y i).Nonempty := by

78 intro s

79 by_cases hs : s.Nonempty

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

81 rcases S.compatibleUpTo_nonempty j with ⟨x, hx⟩

82 refine ⟨x, ?_⟩

83 simp only [Y, mem_iInter]

84 intro i hi

85 exact S.compatibleUpTo_mono (hj i hi) hx

86 · have hs' : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hs

87 subst hs'

88 refine ⟨fun i => Classical.choice (inferInstance : Nonempty (S.X i)), ?_⟩

89 simp only [Finset.notMem_empty, iInter_of_empty, iInter_univ, mem_univ]

90 rcases CompactSpace.iInter_nonempty hclosed hfinite with ⟨x, hx⟩

91 refine ⟨⟨x, ?_⟩⟩

92 intro i j hij

93 exact (mem_iInter.mp hx j) i hij

95/-- Special case for inverse systems of nonempty finite discrete spaces. -/

96theorem nonempty_inverseLimit_of_finite [∀ i, Finite (S.X i)] [∀ i, Nonempty (S.X i)]

97 [∀ i, DiscreteTopology (S.X i)] (hdir : Directed (· ≤ ·) (id : I → I)) :

98 Nonempty S.inverseLimit := by

99 letI : ∀ i, CompactSpace (S.X i) := fun _ => inferInstance

100 letI : ∀ i, T2Space (S.X i) := fun _ => inferInstance

101 exact S.nonempty_inverseLimit hdir

102

103/-- A morphism of inverse systems over the same directed preorder. -/

104structure Morphism (T : InverseSystem (I := I)) where

105 /-- The map from the source stage to the target stage at each index. -/

106 map : ∀ i, S.X i → T.X i

107 /-- Every stage map is continuous. -/

108 continuous_map : ∀ i, Continuous (map i)

109 /-- The stage maps form a natural transformation: they commute with all transition maps. -/

110 comm : ∀ {i j : I} (hij : i ≤ j), T.map hij ∘ map j = map i ∘ S.map hij

111

112namespace Morphism

113

114variable {S}

115variable {T U : InverseSystem (I := I)}

116

117/-- A morphism of inverse systems commutes pointwise with transition maps. -/

118@[simp] theorem comm_apply (Θ : S.Morphism T) {i j : I} (hij : i ≤ j) (x : S.X j) :

119 T.map hij (Θ.map j x) = Θ.map i (S.map hij x) := by

120 simpa [Function.comp] using congrFun (Θ.comm hij) x

121

122/-- The identity morphism of an inverse system. -/

123def id (S : InverseSystem (I := I)) : S.Morphism S where

124 map := fun _ => fun x => x

125 continuous_map := fun _ => continuous_id

126 comm := fun _ => by

127 funext x

128 rfl

129

130/-- The identity morphism of an inverse system acts as the identity at each stage. -/

131@[simp] theorem id_apply (i : I) (x : S.X i) :

132 (id S).map i x = x := rfl

133

134/-- Morphisms of inverse systems compose stagewise. -/

135def comp (Φ : T.Morphism U) (Θ : S.Morphism T) : S.Morphism U where

136 map := fun i => Φ.map i ∘ Θ.map i

137 continuous_map := fun i => (Φ.continuous_map i).comp (Θ.continuous_map i)

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

139 funext x

140 calc

141 U.map hij ((Φ.map j ∘ Θ.map j) x) = U.map hij (Φ.map j (Θ.map j x)) := rfl

142 _ = Φ.map i (T.map hij (Θ.map j x)) := by

143 exact congrFun (Φ.comm hij) (Θ.map j x)

144 _ = Φ.map i (Θ.map i (S.map hij x)) := by

145 rw [Θ.comm_apply hij x]

146 _ = ((Φ.map i ∘ Θ.map i) ∘ S.map hij) x := by

147 rfl

148

149/-- At stage `i`, the composite morphism applies the stage map of `Θ` followed by that of `Φ`. -/

150@[simp] theorem comp_apply (Φ : T.Morphism U) (Θ : S.Morphism T) (i : I) (x : S.X i) :

151 (comp Φ Θ).map i x = Φ.map i (Θ.map i x) := rfl

152

153end Morphism

154

155/-- A morphism of inverse systems sends inverse-limit projections to a compatible family. -/

156theorem compatibleMaps_morphism {T : InverseSystem (I := I)} (Θ : S.Morphism T) :

157 T.CompatibleMaps (fun i => Θ.map i ∘ S.projection i) := by

158 intro i j hij

159 funext x

160 calc

161 T.map hij (Θ.map j (S.projection j x)) = Θ.map i (S.map hij (S.projection j x)) := by

162 exact Θ.comm_apply hij (S.projection j x)

163 _ = Θ.map i (S.projection i x) := by rw [S.projection_compatible x i j hij]

164

165/-- A morphism of inverse systems induces a map on inverse limits. -/

166def limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T) :

167 S.inverseLimit → T.inverseLimit :=

168 T.inverseLimitLift (fun i => Θ.map i ∘ S.projection i) (S.compatibleMaps_morphism Θ)

169

170/-- Projection after the inverse-system limit map agrees with the corresponding stage map. -/

171@[simp] theorem π_comp_limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T) (i : I) :

172 T.projection i ∘ S.limMap Θ = Θ.map i ∘ S.projection i := by

173 simp only [limMap, projection_comp_inverseLimitLift]

174

175/--

176Projecting the induced map on inverse limits to stage \(i\) gives the corresponding stage map

177after projection.

178-/

179@[simp] theorem π_limMap_apply {T : InverseSystem (I := I)} (Θ : S.Morphism T)

180 (i : I) (x : S.inverseLimit) :

181 T.projection i (S.limMap Θ x) = Θ.map i (S.projection i x) := by

182 simpa [Function.comp] using congrFun (S.π_comp_limMap (Θ := Θ) i) x

183

184/--

185A projection after the induced map on inverse limits is the corresponding stage map after

186projection.

187-/

188theorem continuous_limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T) :

189 Continuous (S.limMap Θ) := by

190 refine T.continuous_inverseLimitLift (fun i => Θ.map i ∘ S.projection i) ?_

191 (S.compatibleMaps_morphism Θ)

192 intro i

193 exact (Θ.continuous_map i).comp (S.continuous_projection i)

194

195/-- The inverse-limit map induced by the identity morphism is the identity. -/

196@[simp] theorem limMap_id :

197 S.limMap (Morphism.id S) = id := by

198 funext x

199 apply S.ext

200 intro i

201 change S.projection i (S.limMap (Morphism.id S) x) = S.projection i x

202 rw [S.π_limMap_apply (Θ := Morphism.id S)]

203 rfl

204

205/-- The inverse-limit map induced by a composite morphism is the composite of the induced maps. -/

206@[simp] theorem limMap_comp {T U : InverseSystem (I := I)} (Φ : T.Morphism U) (Θ : S.Morphism T) :

207 S.limMap (Morphism.comp Φ Θ) = T.limMap Φ ∘ S.limMap Θ := by

208 funext x

209 apply U.ext

210 intro i

211 calc

212 U.projection i (S.limMap (Morphism.comp Φ Θ) x) = (Morphism.comp Φ Θ).map i (S.projection i

213 x) := by

214 rw [S.π_limMap_apply (Θ := Morphism.comp Φ Θ)]

215 _ = Φ.map i (Θ.map i (S.projection i x)) := rfl

216 _ = U.projection i ((T.limMap Φ ∘ S.limMap Θ) x) := by

217 rw [Function.comp, T.π_limMap_apply (Θ := Φ), S.π_limMap_apply (Θ := Θ)]

218

219/-- The induced map on inverse limits is injective when all stage maps are injective. -/

220theorem injective_limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T)

221 (hinj : ∀ i, Function.Injective (Θ.map i)) :

222 Function.Injective (S.limMap Θ) := by

223 intro x y hxy

224 apply S.ext

225 intro i

226 apply hinj i

227 calc

228 Θ.map i (S.projection i x) = T.projection i (S.limMap Θ x) :=

229 (S.π_limMap_apply Θ i x).symm

230 _ = T.projection i (S.limMap Θ y) :=

231 congrArg (T.projection i) hxy

232 _ = Θ.map i (S.projection i y) :=

233 S.π_limMap_apply Θ i y

234

235/--

236If all components of a morphism of inverse systems are embeddings, then the induced map on

237inverse limits is an embedding.

238-/

239theorem embedding_limMap {T : InverseSystem (I := I)} (Θ : S.Morphism T)

240 (hemb : ∀ i, Topology.IsEmbedding (Θ.map i)) :

241 Topology.IsEmbedding (S.limMap Θ) := by

242 let hsubS : Topology.IsEmbedding (Subtype.val : S.inverseLimit → ∀ i, S.X i) :=

243 Topology.IsEmbedding.subtypeVal

244 let hpi : Topology.IsEmbedding (Pi.map fun i => Θ.map i : (∀ i, S.X i) → ∀ i, T.X i) :=

245 Topology.IsEmbedding.piMap fun i => hemb i

246 have hcomp :

247 Topology.IsEmbedding

248 (((Subtype.val : T.inverseLimit → ∀ i, T.X i) ∘ S.limMap Θ) : S.inverseLimit → ∀ i, T.X

249 i) := by

250 have heq :

251 ((Subtype.val : T.inverseLimit → ∀ i, T.X i) ∘ S.limMap Θ) =

252 (Pi.map (fun i => Θ.map i) ∘

253 (Subtype.val : S.inverseLimit → ∀ i, S.X i)) := by

254 funext x i

255 exact S.π_limMap_apply Θ i x

256 rw [heq]

257 exact hpi.comp hsubS

258 exact Topology.IsEmbedding.of_comp (S.continuous_limMap Θ) continuous_subtype_val hcomp

259

260/--

261If all components of a morphism of inverse systems are surjective, then the induced map on

262inverse limits is surjective.

263-/

264theorem surjective_limMap {T : InverseSystem (I := I)} [∀ i, CompactSpace (S.X i)]

265 [∀ i, T2Space (S.X i)] [∀ i, T2Space (T.X i)] (hdir : Directed (· ≤ ·) (id : I → I))

266 (Θ : S.Morphism T) (hsurj : ∀ i, Function.Surjective (Θ.map i)) :

267 Function.Surjective (S.limMap Θ) := by

268 intro xlim

269 let F : InverseSystem (I := I) := {

270 X := fun i => {x : S.X i // Θ.map i x = T.projection i xlim}

271 topologicalSpace := fun _ => inferInstance

272 map := fun {i j} hij x =>

273 ⟨S.map hij x.1, by

274 calc

275 Θ.map i (S.map hij x.1) = T.map hij (Θ.map j x.1) := by

276 symm

277 exact Θ.comm_apply hij x.1

278 _ = T.map hij (T.projection j xlim) := by rw [x.2]

279 _ = T.projection i xlim := T.projection_compatible xlim i j hij⟩

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

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

282 calc

283 Θ.map i (S.map hij x.1) = T.map hij (Θ.map j x.1) := by

284 symm

285 exact Θ.comm_apply hij x.1

286 _ = T.map hij (T.projection j xlim) := by rw [x.2]

287 _ = T.projection i xlim := T.projection_compatible xlim i j hij

288 map_id := fun i => by

289 funext x

290 apply Subtype.ext

291 simp only [projection_apply, map_id_apply, id_eq]

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

293 funext x

294 apply Subtype.ext

295 simp only [projection_apply, Function.comp_apply, S.map_comp_apply hij hjk]}

296 letI : ∀ i, Nonempty (F.X i) := fun i => by

297 rcases hsurj i (T.projection i xlim) with ⟨x, hx⟩

298 exact ⟨⟨x, hx⟩⟩

299 letI : ∀ i, T2Space (F.X i) := fun _ => inferInstance

300 letI : ∀ i, CompactSpace (F.X i) := fun i => by

301 let hs : IsClosed {x : S.X i | Θ.map i x = T.projection i xlim} :=

302 isClosed_eq (Θ.continuous_map i) continuous_const

303 exact hs.isClosedEmbedding_subtypeVal.compactSpace

304 rcases InverseSystem.nonempty_inverseLimit (S := F) hdir with ⟨y⟩

305 refine ⟨⟨fun i => (y.1 i).1, ?_⟩, ?_⟩

306 · intro i j hij

307 exact congrArg Subtype.val (y.2 i j hij)

308 · apply T.ext

309 intro i

310 calc

311 T.projection i

312 (S.limMap Θ ⟨fun i => (y.1 i).1, by

313 intro j k hjk

314 exact congrArg Subtype.val (y.2 j k hjk)⟩) =

315 Θ.map i (y.1 i).1 := S.π_limMap_apply Θ i _

316 _ = T.projection i xlim := (y.1 i).2

317

318/-- Compatible surjections from a compact space induce a surjection onto the inverse limit. -/

319theorem surjective_inverseLimitLift {X : Type w} [TopologicalSpace X] [CompactSpace X]

320 [Nonempty I]

321 (ψ : ∀ i, X → S.X i) (hψ : ∀ i, Continuous (ψ i)) (hcompat : S.CompatibleMaps ψ)

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

323 [∀ i, T2Space (S.X i)] :

324 Function.Surjective (S.inverseLimitLift ψ hcompat) := by

325 intro xlim

326 let Z : I → Set X := fun i => {x | ψ i x = S.projection i xlim}

327 have hclosed : ∀ i, IsClosed (Z i) := fun i => isClosed_eq (hψ i) continuous_const

328 have hfinite : ∀ s : Finset I, (⋂ i ∈ s, Z i).Nonempty := by

329 intro s

330 by_cases hs : s.Nonempty

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

332 rcases hsurj j (S.projection j xlim) with ⟨x, hx⟩

333 refine ⟨x, ?_⟩

334 simp only [Z, mem_iInter]

335 intro i hi

336 have hfac : S.map (hj i hi) (ψ j x) = ψ i x := by

337 simpa [Function.comp] using congrFun (hcompat i j (hj i hi)) x

338 calc

339 ψ i x = S.map (hj i hi) (ψ j x) := hfac.symm

340 _ = S.map (hj i hi) (S.projection j xlim) := by rw [hx]

341 _ = S.projection i xlim := S.projection_compatible xlim i j (hj i hi)

342 · have hs' : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hs

343 subst hs'

344 let j : I := Classical.choice ‹Nonempty I›

345 rcases hsurj j (S.projection j xlim) with ⟨x, hx⟩

346 exact ⟨x, by simp only [Finset.notMem_empty, iInter_of_empty, iInter_univ, mem_univ]⟩

347 rcases CompactSpace.iInter_nonempty hclosed hfinite with ⟨x, hx⟩

348 refine ⟨x, ?_⟩

349 apply S.ext

350 intro i

351 calc

352 S.projection i (S.inverseLimitLift ψ hcompat x) = ψ i x := by

353 rfl

354 _ = S.projection i xlim := mem_iInter.mp hx i

355

356/-- If an inverse limit over a directed index set is finite, one projection separates all points. -/

357theorem exists_injective_projection_of_finite_inverseLimit [Nonempty I]

358 (hdir : Directed (· ≤ ·) (id : I → I)) [Finite S.inverseLimit] :

359 ∃ k, Function.Injective (S.projection k) := by

360 classical

361 letI : Fintype S.inverseLimit := Fintype.ofFinite S.inverseLimit

362 let pairs : Finset (S.inverseLimit × S.inverseLimit) :=

363 Finset.univ.filter fun p => p.1 ≠ p.2

364 have hseparate :

365 ∀ p : S.inverseLimit × S.inverseLimit, p ∈ pairs →

366 ∃ i, S.projection i p.1 ≠ S.projection i p.2 := by

367 intro p hp

368 have hpne : p.1 ≠ p.2 := by

369 exact (Finset.mem_filter.mp hp).2

370 by_contra h

371 apply hpne

372 apply S.ext

373 intro i

374 by_contra hneq

375 exact h ⟨i, hneq⟩

376 have hfinset :

377 ∀ t : Finset (S.inverseLimit × S.inverseLimit),

378 (∀ p, p ∈ t → ∃ i, S.projection i p.1 ≠ S.projection i p.2) →

379 ∃ k, ∀ p, p ∈ t → S.projection k p.1 ≠ S.projection k p.2 := by

380 intro t

381 induction t using Finset.induction_on with

382 | empty =>

383 intro _

384 exact ⟨Classical.choice ‹Nonempty I›, by simp only [Finset.notMem_empty,

385 projection_apply, ne_eq, IsEmpty.forall_iff, implies_true]⟩

386 | insert p t hpt ih =>

387 intro ht

388 rcases ht p (by simp only [Finset.mem_insert, true_or]) with ⟨j, hj⟩

389 have ht_rest : ∀ q, q ∈ t → ∃ i, S.projection i q.1 ≠ S.projection i q.2 := by

390 intro q hq

391 exact ht q (by simp only [Finset.mem_insert, hq, or_true])

392 rcases ih ht_rest with ⟨i, hi⟩

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

394 refine ⟨k, ?_⟩

395 intro q hq

396 rw [Finset.mem_insert] at hq

397 rcases hq with rfl | hq

398 · intro heq

399 apply hj

400 have hmap :=

401 congrArg (fun z : S.X k => S.map hjk z) heq

402 exact

403 (S.projection_compatible q.1 j k hjk).symm.trans

404 (hmap.trans (S.projection_compatible q.2 j k hjk))

405 · intro heq

406 apply hi q hq

407 have hmap :=

408 congrArg (fun z : S.X k => S.map hik z) heq

409 exact

410 (S.projection_compatible q.1 i k hik).symm.trans

411 (hmap.trans (S.projection_compatible q.2 i k hik))

412 rcases hfinset pairs hseparate with ⟨k, hk⟩

413 refine ⟨k, ?_⟩

414 intro x y hxy

415 by_contra hne

416 exact hk (x, y) (by simp only [ne_eq, Finset.mem_filter, Finset.mem_univ, hne,

417 not_false_eq_true, and_self, pairs]) hxy

418

419end InverseSystem

420end

421end ProCGroups.InverseSystems