Paracompact topological spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_locally_compact_sigma_compact. Moreover, we can choose a locally finite refinement with sets in a given collection of filter bases of 𝓝 x,x : X, seerefinement_of_locally_compact_sigma_compact_of_nhds_basis. For example, in a proper metric space every open covering⋃ i, s iadmits 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 emetric_space is a paracompact space, see instance emetric_space.paracompact_space in topology/metric_space/emetric_paracompact.

TODO #

Prove (some of) Michael's theorems.

Tags #

compact space, paracompact space, locally finite covering

source

@[class]

structure paracompact_space (X : Type v) [topological_space X] :

Prop

locally_finite_refinement : ∀ (α : Type ?) (s : α → set X), (∀ (a : α), is_open (s a)) → (⋃ (a : α), s a) = set.univ → (∃ (β : Type ?) (t : β → set X) (ho : ∀ (b : β), is_open (t b)) (hc : (⋃ (b : β), t b) = set.univ), locally_finite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a)

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 paracompact_space.{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.

Instances of this typeclass

source

theorem precise_refinement {ι : Type u} {X : Type v} [topological_space X] [paracompact_space X] (u : ι → set X) (uo : ∀ (a : ι), is_open (u a)) (uc : (⋃ (i : ι), u i) = set.univ) :

∃ (v : ι → set X), (∀ (a : ι), is_open (v a)) ∧ (⋃ (i : ι), v i) = set.univ ∧ locally_finite 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.

source

theorem precise_refinement_set {ι : Type u} {X : Type v} [topological_space X] [paracompact_space X] {s : set X} (hs : is_closed s) (u : ι → set X) (uo : ∀ (i : ι), is_open (u i)) (us : s ⊆ ⋃ (i : ι), u i) :

∃ (v : ι → set X), (∀ (i : ι), is_open (v i)) ∧ (s ⊆ ⋃ (i : ι), v i) ∧ locally_finite 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.

source

@[protected, instance]

def paracompact_of_compact {X : Type v} [topological_space X] [compact_space X] :

paracompact_space X

A compact space is paracompact.

source

theorem refinement_of_locally_compact_sigma_compact_of_nhds_basis_set {X : Type v} [topological_space X] [locally_compact_space X] [sigma_compact_space X] [t2_space X] {ι : X → Type u} {p : Π (x : X), ι x → Prop} {B : Π (x : X), ι x → set X} {s : set X} (hs : is_closed s) (hB : ∀ (x : X), x ∈ s → (nhds x).has_basis (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)) ∧ locally_finite (λ (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 λ 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.has_basis.restrict_subset or a similar lemma, see the proof of paracompact_of_locally_compact_sigma_compact for an example.

The formalization is based on two ncatlab proofs:

See also refinement_of_locally_compact_sigma_compact_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.

source

theorem refinement_of_locally_compact_sigma_compact_of_nhds_basis {X : Type v} [topological_space X] [locally_compact_space X] [sigma_compact_space X] [t2_space X] {ι : X → Type u} {p : Π (x : X), ι x → Prop} {B : Π (x : X), ι x → set X} (hB : ∀ (x : X), (nhds x).has_basis (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 ∧ locally_finite (λ (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 λ i, B (c i) (r i) of X such that each r i satisfies p (c i)

The formalization is based on two ncatlab proofs:

See also refinement_of_locally_compact_sigma_compact_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.

source

@[protected, instance]

def paracompact_of_locally_compact_sigma_compact {X : Type v} [topological_space X] [locally_compact_space X] [sigma_compact_space X] [t2_space X] :

paracompact_space X

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

source

theorem normal_of_paracompact_t2 {X : Type v} [topological_space X] [t2_space X] [paracompact_space X] :

normal_space X