Relatively compact exhaustion of a manifold

A Hausdorff, second countable manifold modelled on a locally compact space is locally compact and σ-compact, and Mathlib's CompactExhaustion gives compact sets K_0 ⊆ int K_1 ⊆ K_1 ⊆ … with ⋃ K_n = M. This module defines the relatively compact open subsets M_n := int K_{n+1} (relCompactOpen) and records their properties: each M_n is open with compact closure, closure M_n ⊆ M_{n+1}, the M_n increase, and ⋃ M_n = M.

These are the open subsets over which the analytic resolution is built compactwise and then glued: Kollár's resolution of "any analytic space that is an increasing union of its compact subsets" [Kol07, 44], Bierstone–Milman's relatively quasi-compact open subsets, over each of which the sequence of blowings-up is finite [BM97, Theorem 1.6 and the remarks after it], and Hironaka's analytic spaces, "countable at infinity" [Hir64, p. 120] and "a countable increasing union of relatively compact open subspaces" [Hir64, p. 121].

def Manifold.relCompactOpen {M : Type u_1} [TopologicalSpace M] (K : CompactExhaustion M) (n : ℕ) : TopologicalSpace.Opens M

The relatively compact open subset M_n := int K_{n+1} cut out of the compact exhaustion K, as an open of M, so that Mathlib's charted-space and manifold instances on opens apply to it.

Equations

• Manifold.relCompactOpen K n = { carrier := interior (K (n + 1)), is_open' := ⋯ }

The manifold is locally compact and σ-compact

theorem Manifold.locallyCompactSpace_of_chartedSpace (E : Type u_2) [TopologicalSpace E] (M : Type u_3) [TopologicalSpace M] [ChartedSpace E M] [LocallyCompactSpace E] : LocallyCompactSpace M

A charted space modelled on a locally compact space is locally compact (Mathlib's ChartedSpace.locallyCompactSpace).

theorem Manifold.sigmaCompactSpace_of_chartedSpace (E : Type u_2) [TopologicalSpace E] (M : Type u_3) [TopologicalSpace M] [ChartedSpace E M] [LocallyCompactSpace E] [SecondCountableTopology M] : SigmaCompactSpace M

A second countable charted space modelled on a locally compact space is σ-compact: Hironaka's "countable at infinity" [Hir64, p. 120] (Mathlib's sigmaCompactSpace_of_locallyCompact_secondCountable).

theorem Manifold.nonempty_compactExhaustion (E : Type u_2) [TopologicalSpace E] (M : Type u_3) [TopologicalSpace M] [ChartedSpace E M] [LocallyCompactSpace E] [SecondCountableTopology M] : Nonempty (CompactExhaustion M)

A second countable charted space modelled on a locally compact space admits a compact exhaustion K_0 ⊆ int K_1 ⊆ K_1 ⊆ …, ⋃ K_n = M (Mathlib's CompactExhaustion.choice).

theorem Manifold.locallyCompactSpace_of_finiteDimensional (𝕜 : Type) [RCLike 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u_3) [TopologicalSpace M] [ChartedSpace E M] [FiniteDimensional 𝕜 E] : LocallyCompactSpace M

A charted space modelled on a finite-dimensional normed space over 𝕜 ∈ {ℝ, ℂ} is locally compact (Mathlib's FiniteDimensional.proper_rclike with ChartedSpace.locallyCompactSpace).

The relatively compact opens M_n := int K_{n+1}

@[simp]

theorem Manifold.coe_relCompactOpen {M : Type u_1} [TopologicalSpace M] (K : CompactExhaustion M) (n : ℕ) : ↑(relCompactOpen K n) = interior (K (n + 1))

M_n := int K_{n+1} as a set.

theorem Manifold.closure_relCompactOpen_subset {M : Type u_1} [TopologicalSpace M] (K : CompactExhaustion M) [T2Space M] (n : ℕ) : closure ↑(relCompactOpen K n) ⊆ K (n + 1)

closure (int K_{n+1}) ⊆ K_{n+1}: compact sets are closed in a Hausdorff space.

theorem Manifold.isCompact_closure_relCompactOpen {M : Type u_1} [TopologicalSpace M] (K : CompactExhaustion M) [T2Space M] (n : ℕ) : IsCompact (closure ↑(relCompactOpen K n))

Each M_n is relatively compact: its closure is a closed subset of the compact K_{n+1}.

theorem Manifold.closure_relCompactOpen_subset_succ {M : Type u_1} [TopologicalSpace M] (K : CompactExhaustion M) [T2Space M] (n : ℕ) : closure ↑(relCompactOpen K n) ⊆ ↑(relCompactOpen K (n + 1))

closure M_n ⊆ M_{n+1}, i.e. closure (int K_{n+1}) ⊆ K_{n+1} ⊆ int K_{n+2}.

theorem Manifold.relCompactOpen_le_succ {M : Type u_1} [TopologicalSpace M] (K : CompactExhaustion M) (n : ℕ) : relCompactOpen K n ≤ relCompactOpen K (n + 1)

M_n ⊆ M_{n+1} (int K_{n+1} ⊆ K_{n+1} ⊆ int K_{n+2}).

theorem Manifold.relCompactOpen_mono {M : Type u_1} [TopologicalSpace M] (K : CompactExhaustion M) : Monotone (relCompactOpen K)

The M_n increase.

theorem Manifold.iUnion_relCompactOpen {M : Type u_1} [TopologicalSpace M] (K : CompactExhaustion M) : ⋃ (n : ℕ), ↑(relCompactOpen K n) = Set.univ

⋃ M_n = M: every point lies in some K_n ⊆ int K_{n+1} = M_n.