Documentation

LeanPool.Rado.Topology.PoincareVolterra

The Poincaré–Volterra lemma #

If Z is a connected, Hausdorff, locally compact, locally connected, locally second-countable topological space and f : Z → Y is a continuous map into a second-countable Hausdorff space whose fibers are discrete, then Z is second countable.

This is the purely topological endgame of Radó's theorem; see Forster, Lectures on Riemann Surfaces, Lemma 23.2 (= Rainer's notes 23.2, full proof in reference/rado/rainer.txt), or Anghel–Stan arXiv:2008.12189, Appendix C.

Proof sketch. Let V be a countable basis of Y and let 𝒰 be the family of all connected components U of preimages f ⁻¹' V, VV, such that U is second countable (as a subspace). Then:

  1. 𝒰 covers Z: given z, discreteness of the fiber through z, local compactness and local second countability give a relatively compact open W ∋ z with second-countable compact closure and closure W ∩ f ⁻¹' {f z} = {z}; pick VV with f zV ⊆ Y \ f '' (frontier W) (the image of the frontier is compact, hence closed, and misses f z); the component U ∋ z of f ⁻¹' V avoids frontier W, meets W, hence U ⊆ W (connectedness), so U is second countable, open (local connectedness), and U ∈ 𝒰.
  2. Each U₀ ∈ 𝒰 meets only countably many members of 𝒰: for fixed V, the components of f ⁻¹' V are pairwise disjoint, so those meeting U₀ trace a pairwise-disjoint family of nonempty opens in the second-countable U₀ (ccc), countable; sum over the countable basis.
  3. Chain argument: the members reachable from a fixed U₀ ∈ 𝒰 by finite chains form a countable subfamily R whose union G is open; G is also closed (a boundary point z lies in some U ∈ 𝒰 by 1, which meets G, hence is reachable, hence z ∈ G); connectedness gives G = Z, so countably many second-countable open sets cover Z.
theorem Rado.poincare_volterra {Z : Type u_1} [TopologicalSpace Z] [T2Space Z] [ConnectedSpace Z] [LocallyCompactSpace Z] [LocallyConnectedSpace Z] (hloc : ∀ (z : Z), ∃ (U : Set Z), z U IsOpen U SecondCountableTopology U) {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [SecondCountableTopology Y] {f : ZY} (hf : Continuous f) (hdisc : ∀ (z : Z), Unhds z, wU, f w = f zw = z) :

Poincaré–Volterra lemma (Forster 23.2). A connected Hausdorff, locally compact, locally connected, locally second-countable space admitting a continuous map with discrete fibers into a second-countable Hausdorff space is second countable.