Strongly locally contractible spaces

This file defines LocallyContractibleSpace and StronglyLocallyContractibleSpace.

Main definitions

• LocallyContractibleSpace X: classical local contractibility (null-homotopic inclusions).
• StronglyLocallyContractibleSpace X: a space where each point has a neighborhood basis consisting of contractible sets (not necessarily open).

Main results

• StronglyLocallyContractibleSpace.locallyContractible: SLC implies classical LC
• instLocPathConnectedSpace: strongly locally contractible spaces are locally path-connected
• StronglyLocallyContractibleSpace.of_bases: a helper to construct strongly locally contractible spaces from a neighborhood basis
• contractible_subset_basis: basis of contractible neighborhoods contained in an open set
• IsOpenEmbedding.stronglyLocallyContractibleSpace: open embeddings preserve strong local contractibility
• IsOpen.stronglyLocallyContractibleSpace: open subsets of strongly locally contractible spaces are strongly locally contractible
• Products of strongly locally contractible spaces are strongly locally contractible

TODO

• Define contractible components and prove they are open in strongly locally contractible spaces
• Add examples: convex sets, real vector spaces, star-shaped sets

Notes

Terminology: The classical definition of locally contractible (LC) requires that for every point x and neighborhood U ∋ x, there exists a neighborhood V ∋ x with V ⊆ U such that the inclusion V ↪ U is null-homotopic. The definition here is strictly stronger: we require contractible neighborhoods to form a neighborhood basis. This is often called strongly locally contractible (SLC).

Hierarchy of notions:

• "Basis of open contractible neighborhoods" (strongest)
• "Basis of contractible neighborhoods" (this file, SLC)
• "Null-homotopic inclusions" (classical LC, weakest)

This naming is not used uniformly: according to https://ncatlab.org/nlab/show/locally+contractible+space the second and third notion here could also be called "locally contractible" and "semilocally contractible" respectively. We've enquired at https://math.stackexchange.com/questions/5109428/terminology-for-local-contractibility-locally-contractible-vs-strongly-local in the hope of getting definitive naming advice.

The Borsuk-Mazurkiewicz counterexample [borsuk_mazurkiewicz1934] shows that classical LC does not imply SLC. Moreover, from a contractible neighborhood S one generally cannot shrink to an open V ⊆ S that remains contractible, so requiring neighborhoods to be open is potentially strictly stronger than SLC.

def LocallyContractibleSpace (X : Type u_4) [TopologicalSpace X] : Prop

Classical local contractibility: for every point and every neighborhood U, there exists a neighborhood V ⊆ U such that the inclusion V ↪ U is null-homotopic.

This is weaker than StronglyLocallyContractibleSpace.

Equations

• LocallyContractibleSpace X = ∀ (x : X), ∀ U ∈ nhds x, ∃ (V : Set X) (hVU : V ⊆ U), V ∈ nhds x ∧ (ContinuousMap.inclusion hVU).Nullhomotopic

class StronglyLocallyContractibleSpace (X : Type u_4) [TopologicalSpace X] : Prop

A topological space is strongly locally contractible if, at every point, contractible neighborhoods form a neighborhood basis. Here "contractible" means contractible as a subspace.

This is strictly stronger than the classical notion of locally contractible, which only requires null-homotopic inclusions. This distinction is witnessed by an example from Borsuk-Mazurkiewicz [borsuk_mazurkiewicz1934]; see also [MO88628] for discussion and the Whitehead manifold example.

• contractible_basis (x : X) : (nhds x).HasBasis (fun (s : Set X) => s ∈ nhds x ∧ ContractibleSpace ↑s) id

  Each neighborhood filter has a basis of contractible subspace neighborhoods.

theorem StronglyLocallyContractibleSpace.of_bases {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {p : X → ι → Prop} {s : X → ι → Set X} (h : ∀ (x : X), (nhds x).HasBasis (p x) (s x)) (h' : ∀ (x : X) (i : ι), p x i → ContractibleSpace ↑(s x i)) : StronglyLocallyContractibleSpace X

A helper to construct a strongly locally contractible space from a neighborhood basis where each basis element is contractible as a subspace.

theorem contractible_subset_basis {X : Type u_1} [TopologicalSpace X] {x : X} [StronglyLocallyContractibleSpace X] {U : Set X} (h : IsOpen U) (hx : x ∈ U) : (nhds x).HasBasis (fun (s : Set X) => s ∈ nhds x ∧ ContractibleSpace ↑s ∧ s ⊆ U) id

In a strongly locally contractible space, for any open set U containing x, there is a basis of contractible neighborhoods of x contained in U.

@[instance 100]

instance instLocPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [StronglyLocallyContractibleSpace X] : LocPathConnectedSpace X

Strongly locally contractible spaces are locally path-connected.

theorem Topology.IsOpenEmbedding.stronglyLocallyContractibleSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [StronglyLocallyContractibleSpace X] {e : Y → X} (he : IsOpenEmbedding e) : StronglyLocallyContractibleSpace Y

Open embeddings preserve strong local contractibility: if X is strongly locally contractible and e : Y → X is an open embedding, then Y is strongly locally contractible.

theorem IsOpen.stronglyLocallyContractibleSpace {X : Type u_1} [TopologicalSpace X] [StronglyLocallyContractibleSpace X] {U : Set X} (h : IsOpen U) : StronglyLocallyContractibleSpace ↑U

Open subsets of strongly locally contractible spaces are strongly locally contractible.

instance instStronglyLocallyContractibleSpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [StronglyLocallyContractibleSpace X] [StronglyLocallyContractibleSpace Y] : StronglyLocallyContractibleSpace (X × Y)

The product of two strongly locally contractible spaces is strongly locally contractible.

theorem StronglyLocallyContractibleSpace.locallyContractible {X : Type u_1} [TopologicalSpace X] [StronglyLocallyContractibleSpace X] : LocallyContractibleSpace X

The strong notion (contractible neighborhood basis) implies the classical notion (null-homotopic inclusions). The converse is false by the Borsuk-Mazurkiewicz counterexample [borsuk_mazurkiewicz1934]; see also [MO88628] for discussion and the Whitehead manifold example.