Paracompact topological spaces

A topological space X is said to be paracompact if every open covering of X admits a locally finite refinement.

The definition requires that each set of the new covering is a subset of one of the sets of the initial covering. However, one can ensure that each open covering s : ι → Set X admits a precise locally finite refinement, i.e., an open covering t : ι → Set X with the same index set such that ∀ i, t i ⊆ s i, see lemma precise_refinement. We also provide a convenience lemma precise_refinement_set that deals with open coverings of a closed subset of X instead of the whole space.

We also prove the following facts.

• Every compact space is paracompact, see instance paracompact_of_compact.

• A locally compact sigma compact Hausdorff space is paracompact, see instance paracompact_of_locallyCompact_sigmaCompact. Moreover, we can choose a locally finite refinement with sets in a given collection of filter bases of 𝓝 x, x : X, see refinement_of_locallyCompact_sigmaCompact_of_nhds_basis. For example, in a proper metric space every open covering ⋃ i, s i admits a refinement ⋃ i, Metric.ball (c i) (r i).

• Every paracompact Hausdorff space is normal. This statement is not an instance to avoid loops in the instance graph.

• Every EMetricSpace is a paracompact space, see instance EMetric.instParacompactSpace in Topology/EMetricSpace/Paracompact.

TODO

Prove (some of) Michael's theorems.

Tags

compact space, paracompact space, locally finite covering

class ParacompactSpace (X : Type v) [TopologicalSpace X] : Prop

A topological space is called paracompact, if every open covering of this space admits a locally finite refinement. We use the same universe for all types in the definition to avoid creating a class like ParacompactSpace.{u v}. Due to lemma precise_refinement below, every open covering s : α → Set X indexed on α : Type v has a precise locally finite refinement, i.e., a locally finite refinement t : α → Set X indexed on the same type such that each ∀ i, t i ⊆ s i.

• locallyFinite_refinement : ∀ (α : Type v) (s : α → Set X), (∀ (a : α), IsOpen (s a)) → ⋃ (a : α), s a = Set.univ → ∃ (β : Type v) (t : β → Set X), (∀ (b : β), IsOpen (t b)) ∧ ⋃ (b : β), t b = Set.univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a

  Every open cover of a paracompact space assumes a locally finite refinement.

theorem ParacompactSpace.locallyFinite_refinement {X : Type v} [TopologicalSpace X] [self : ParacompactSpace X] (α : Type v) (s : α → Set X) : (∀ (a : α), IsOpen (s a)) → ⋃ (a : α), s a = Set.univ → ∃ (β : Type v) (t : β → Set X), (∀ (b : β), IsOpen (t b)) ∧ ⋃ (b : β), t b = Set.univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a

Every open cover of a paracompact space assumes a locally finite refinement.

theorem precise_refinement {ι : Type u} {X : Type v} [TopologicalSpace X] [ParacompactSpace X] (u : ι → Set X) (uo : ∀ (a : ι), IsOpen (u a)) (uc : ⋃ (i : ι), u i = Set.univ) : ∃ (v : ι → Set X), (∀ (a : ι), IsOpen (v a)) ∧ ⋃ (i : ι), v i = Set.univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a

Any open cover of a paracompact space has a locally finite precise refinement, that is, one indexed on the same type with each open set contained in the corresponding original one.

theorem precise_refinement_set {ι : Type u} {X : Type v} [TopologicalSpace X] [ParacompactSpace X] {s : Set X} (hs : IsClosed s) (u : ι → Set X) (uo : ∀ (i : ι), IsOpen (u i)) (us : s ⊆ ⋃ (i : ι), u i) : ∃ (v : ι → Set X), (∀ (i : ι), IsOpen (v i)) ∧ s ⊆ ⋃ (i : ι), v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i

In a paracompact space, every open covering of a closed set admits a locally finite refinement indexed by the same type.

theorem ClosedEmbedding.paracompactSpace {X : Type v} {Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] [ParacompactSpace Y] {e : X → Y} (he : ClosedEmbedding e) : ParacompactSpace X

theorem Homeomorph.paracompactSpace_iff {X : Type v} {Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : ParacompactSpace X ↔ ParacompactSpace Y

instance instParacompactSpaceProdOfCompactSpace {X : Type v} {Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [ParacompactSpace Y] : ParacompactSpace (X × Y)

The product of a compact space and a paracompact space is a paracompact space. The formalization is based on https://dantopology.wordpress.com/2009/10/24/compact-x-paracompact-is-paracompact/ with some minor modifications.

This version assumes that X in X × Y is compact and Y is paracompact, see next lemma for the other case.

Equations

• ⋯ = ⋯

instance instParacompactSpaceProdOfCompactSpace_1 {X : Type v} {Y : Type w} [TopologicalSpace X] [TopologicalSpace Y] [ParacompactSpace X] [CompactSpace Y] : ParacompactSpace (X × Y)

Equations

• ⋯ = ⋯

instance paracompact_of_compact {X : Type v} [TopologicalSpace X] [CompactSpace X] : ParacompactSpace X

A compact space is paracompact.

Equations

• ⋯ = ⋯

theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set {X : Type v} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] [T2Space X] {ι : X → Type u} {p : (x : X) → ι x → Prop} {B : (x : X) → ι x → Set X} {s : Set X} (hs : IsClosed s) (hB : ∀ x ∈ s, (nhds x).HasBasis (p x) (B x)) : ∃ (α : Type v) (c : α → X) (r : (a : α) → ι (c a)), (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun (a : α) => B (c a) (r a)

Let X be a locally compact sigma compact Hausdorff topological space, let s be a closed set in X. Suppose that for each x ∈ s the sets B x : ι x → Set X with the predicate p x : ι x → Prop form a basis of the filter 𝓝 x. Then there exists a locally finite covering fun i ↦ B (c i) (r i) of s such that all “centers” c i belong to s and each r i satisfies p (c i).

The notation is inspired by the case B x r = Metric.ball x r but the theorem applies to nhds_basis_opens as well. If the covering must be subordinate to some open covering of s, then the user should use a basis obtained by Filter.HasBasis.restrict_subset or a similar lemma, see the proof of paracompact_of_locallyCompact_sigmaCompact for an example.

The formalization is based on two ncatlab proofs:

• locally compact and sigma compact spaces are paracompact;
• open cover of smooth manifold admits locally finite refinement by closed balls.

See also refinement_of_locallyCompact_sigmaCompact_of_nhds_basis for a version of this lemma dealing with a covering of the whole space.

In most cases (namely, if B c r ∪ B c r' is again a set of the form B c r'') it is possible to choose α = X. This fact is not yet formalized in mathlib.

theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis {X : Type v} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] [T2Space X] {ι : X → Type u} {p : (x : X) → ι x → Prop} {B : (x : X) → ι x → Set X} (hB : ∀ (x : X), (nhds x).HasBasis (p x) (B x)) : ∃ (α : Type v) (c : α → X) (r : (a : α) → ι (c a)), (∀ (a : α), p (c a) (r a)) ∧ ⋃ (a : α), B (c a) (r a) = Set.univ ∧ LocallyFinite fun (a : α) => B (c a) (r a)

Let X be a locally compact sigma compact Hausdorff topological space. Suppose that for each x the sets B x : ι x → Set X with the predicate p x : ι x → Prop form a basis of the filter 𝓝 x. Then there exists a locally finite covering fun i ↦ B (c i) (r i) of X such that each r i satisfies p (c i).

The notation is inspired by the case B x r = Metric.ball x r but the theorem applies to nhds_basis_opens as well. If the covering must be subordinate to some open covering of s, then the user should use a basis obtained by Filter.HasBasis.restrict_subset or a similar lemma, see the proof of paracompact_of_locallyCompact_sigmaCompact for an example.

The formalization is based on two ncatlab proofs:

• locally compact and sigma compact spaces are paracompact;
• open cover of smooth manifold admits locally finite refinement by closed balls.

See also refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set for a version of this lemma dealing with a covering of a closed set.

In most cases (namely, if B c r ∪ B c r' is again a set of the form B c r'') it is possible to choose α = X. This fact is not yet formalized in mathlib.

instance paracompact_of_locallyCompact_sigmaCompact {X : Type v} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] [T2Space X] : ParacompactSpace X

A locally compact sigma compact Hausdorff space is paracompact. See also refinement_of_locallyCompact_sigmaCompact_of_nhds_basis for a more precise statement.

Equations

• ⋯ = ⋯

instance T4Space.of_paracompactSpace_t2Space {X : Type v} [TopologicalSpace X] [T2Space X] [ParacompactSpace X] : T4Space X

Dieudonné's theorem: a paracompact Hausdorff space is normal. Formalization is based on the proof at ncatlab.

Equations

• ⋯ = ⋯