Semilocally simply connected spaces

A topological space X is semilocally simply connected if every point x has a neighbourhood U such that every loop in U based at x is null-homotopic in X. This is the standing point-set hypothesis (alongside path-connectedness and local path-connectedness) under which the universal cover of a space exists; see the universal-covers roadmap. Mathlib master has SimplyConnectedSpace and the local notions LocallyContractibleSpace and StronglyLocallyContractibleSpace, but no semilocal simple connectivity; the predicate follows Kim Morrison's unmerged mathlib4#38292 (see the References below).

The condition is genuinely semilocal: the null-homotopy is allowed to leave U and use the whole of X. It is therefore weaker than asking each U to be simply connected on its own (the local notion); the constructor SemilocallySimplyConnectedSpace.of_forall_exists_mem_nhds_isSimplyConnected records that implication. The classical local-contractibility hypothesis LocallyContractibleSpace is also enough (SemilocallySimplyConnectedSpace.of_locallyContractibleSpace), and through it every strongly locally contractible space is semilocally simply connected. Discrete spaces are also instances, witnessed by singleton neighbourhoods.

Main declarations

• SemilocallySimplyConnectedAt: the pointwise predicate.
• TauCeti.SemilocallySimplyConnectedSpace: the predicate at every point, as a typeclass.
• SemilocallySimplyConnectedAt.exists_mem_nhds_subset_loops_nullhomotopic: the witnessing neighbourhood can be taken inside any prescribed neighbourhood.
• SemilocallySimplyConnectedAt.exists_isOpen_mem_nhds_subset_loops_nullhomotopic: the witnessing neighbourhood can moreover be taken open.
• TauCeti.SemilocallySimplyConnectedSpace.of_forall_exists_mem_nhds_isSimplyConnected: a space in which every point has a simply connected neighbourhood is semilocally simply connected.
• TauCeti.SemilocallySimplyConnectedSpace.of_locallyContractibleSpace: a locally contractible space is semilocally simply connected.
• Instances deriving the property for simply connected spaces, strongly locally contractible spaces, discrete spaces, and binary products.

References

This file supplies the semilocal-simple-connectivity hypothesis required by the Tau Ceti universal-covers roadmap (TauCetiRoadmap/UniversalCovers); see the standing hypotheses there. The predicate follows the one Kim Morrison introduces (as SemilocallySimplyConnectedSpace, the classical based notion of Brazas, Definition 2.1, https://arxiv.org/abs/1102.0993) in mathlib4 PRs #31576 and #38292, which state the universal-cover construction over [SemilocallySimplyConnectedSpace X]; neither has merged, so the predicate is not yet in Mathlib. The API here is a streamlined single-field restatement sufficient for the roadmap's Stage 0.2.

def SemilocallySimplyConnectedAt {X : Type u_1} [TopologicalSpace X] (x : X) : Prop

A space is semilocally simply connected at x if x has a neighbourhood U such that every loop in U based at x is null-homotopic in the whole space. The null-homotopy is allowed to leave U, which is what makes this weaker than local simple connectivity. This is the based notion of Brazas, Definition 2.1 (see the References below).

Equations

• SemilocallySimplyConnectedAt x = ∃ U ∈ nhds x, ∀ (γ : Path x x), Set.range ⇑γ ⊆ U → γ.Homotopic (Path.refl x)

theorem semilocallySimplyConnectedAt_def {X : Type u_1} [TopologicalSpace X] {x : X} : SemilocallySimplyConnectedAt x ↔ ∃ U ∈ nhds x, ∀ (γ : Path x x), Set.range ⇑γ ⊆ U → γ.Homotopic (Path.refl x)

The defining characterization of semilocal simple connectivity at a point.

class TauCeti.SemilocallySimplyConnectedSpace (X : Type u_3) [TopologicalSpace X] : Prop

A space is semilocally simply connected if it is semilocally simply connected at every point: every point x has a neighbourhood U such that every loop in U based at x is null-homotopic in the whole space.

• semilocallySimplyConnectedAt (x : X) : SemilocallySimplyConnectedAt x

  Every point has a neighbourhood in which every based loop is null-homotopic in X.

theorem SemilocallySimplyConnectedAt.exists_mem_nhds_subset_loops_nullhomotopic {X : Type u_1} [TopologicalSpace X] {x : X} (h : SemilocallySimplyConnectedAt x) {V : Set X} (hV : V ∈ nhds x) : ∃ U ∈ nhds x, U ⊆ V ∧ ∀ (γ : Path x x), Set.range ⇑γ ⊆ U → γ.Homotopic (Path.refl x)

The witnessing neighbourhood of a point can be shrunk to lie inside any prescribed neighbourhood: loops contained in a smaller set are in particular contained in the larger one.

theorem SemilocallySimplyConnectedAt.exists_isOpen_mem_nhds_subset_loops_nullhomotopic {X : Type u_1} [TopologicalSpace X] {x : X} (h : SemilocallySimplyConnectedAt x) {V : Set X} (hV : V ∈ nhds x) : ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ U ⊆ V ∧ ∀ (γ : Path x x), Set.range ⇑γ ⊆ U → γ.Homotopic (Path.refl x)

The witnessing neighbourhood can be taken open and inside any prescribed neighbourhood. This is the form consumed by the universal-cover construction, where the sheets must be open.

theorem TauCeti.SemilocallySimplyConnectedSpace.of_forall_exists_mem_nhds_isSimplyConnected {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), ∃ U ∈ nhds x, IsSimplyConnected U) : SemilocallySimplyConnectedSpace X

If every point of X has a simply connected neighbourhood, then X is semilocally simply connected: a loop inside such a neighbourhood is already null-homotopic there, hence in X.

theorem TauCeti.SemilocallySimplyConnectedSpace.of_locallyContractibleSpace {X : Type u_1} [TopologicalSpace X] (h : LocallyContractibleSpace X) : SemilocallySimplyConnectedSpace X

A locally contractible space (each neighbourhood of a point contains a smaller neighbourhood whose inclusion into the larger one is null-homotopic) is semilocally simply connected. A based loop in the smaller neighbourhood becomes null-homotopic once pushed forward along the null-homotopic inclusion into X.

@[instance 100]

instance TauCeti.instSemilocallySimplyConnectedSpaceOfSimplyConnectedSpace {X : Type u_1} [TopologicalSpace X] [SimplyConnectedSpace X] : SemilocallySimplyConnectedSpace X

A simply connected space is semilocally simply connected: the whole space already witnesses the condition, since every loop is null-homotopic.

@[instance 100]

instance TauCeti.instSemilocallySimplyConnectedSpaceOfStronglyLocallyContractibleSpace {X : Type u_1} [TopologicalSpace X] [StronglyLocallyContractibleSpace X] : SemilocallySimplyConnectedSpace X

A strongly locally contractible space (each point has a basis of contractible neighbourhoods) is semilocally simply connected, since strong local contractibility implies the classical local contractibility hypothesis.

@[instance 100]

instance TauCeti.instSemilocallySimplyConnectedSpaceOfDiscreteTopology {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] : SemilocallySimplyConnectedSpace X

A discrete space is semilocally simply connected: the singleton neighbourhood of a point contains only the constant loop.

instance TauCeti.instSemilocallySimplyConnectedSpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SemilocallySimplyConnectedSpace X] [SemilocallySimplyConnectedSpace Y] : SemilocallySimplyConnectedSpace (X × Y)

A product of semilocally simply connected spaces is semilocally simply connected: a loop in a product of witnessing neighbourhoods projects to loops in each factor, and their null-homotopies combine into a null-homotopy of the original loop.