Semilocally simple connectivity: characterizations and path-homotopy-trivial neighbourhoods

This file characterizes the based pointwise predicate SemilocallySimplyConnectedAt x from TauCeti.AlgebraicTopology.SemilocallySimplyConnected.Basic by open neighbourhoods, by the triviality of the map on fundamental groups induced by the inclusion of a neighbourhood, and by homotopy of paths with a common endpoint. It introduces SemilocallySimplyConnectedOn, and shows that on a locally path-connected space the based condition yields open, path-connected, IsPathHomotopyTrivial neighbourhoods, in which all loops, at every basepoint, are null-homotopic in the ambient space (the unbased form, Brazas, Definition 2.2), which is what the universal-cover construction consumes.

Combined with the tube neighbourhoods of TauCeti.Topology.Homotopy.TubeNeighborhood, this shows that path-homotopy classes are open in the compact-open topology (Path.isOpen_setOf_homotopic), so that Path.Homotopic.Quotient x y is discrete (Path.Homotopic.Quotient.discreteTopology).

It is adapted from the Mathlib drafts #31449, #31576, and #38292 by Kim Morrison, for Stage 0.1 of the TauCetiRoadmap/UniversalCovers roadmap, following the earlier Tau Ceti work in #42.

SemilocallySimplyConnectedAt

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

Characterization of SemilocallySimplyConnectedAt x by open neighbourhoods whose loops based at x are null-homotopic in the ambient space.

theorem semilocallySimplyConnectedAt_iff_range_eq_bot {X : Type u_1} [TopologicalSpace X] {x : X} : SemilocallySimplyConnectedAt x ↔ ∃ U ∈ nhds x, ∀ (hx : x ∈ U), (FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } ⟨x, hx⟩).range = ⊥

Characterization of SemilocallySimplyConnectedAt x by the fundamental group: the map π₁(U, x) → π₁(X, x) induced by the inclusion of some neighbourhood U is trivial.

theorem semilocallySimplyConnectedAt_iff_paths {X : Type u_1} [TopologicalSpace X] {x : X} : SemilocallySimplyConnectedAt x ↔ ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ ∀ {u : X} (γ γ' : Path x u), Set.range ⇑γ ⊆ U → Set.range ⇑γ' ⊆ U → γ.Homotopic γ'

Characterization of SemilocallySimplyConnectedAt x by paths: some open neighbourhood U of x has any two paths in U from x to a common endpoint homotopic in the ambient space.

SemilocallySimplyConnectedOn

def SemilocallySimplyConnectedOn {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

A space is semilocally simply connected on s if it is semilocally simply connected at every point of s.

Equations

• SemilocallySimplyConnectedOn s = ∀ x ∈ s, SemilocallySimplyConnectedAt x

theorem SemilocallySimplyConnectedOn.at {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} (h : SemilocallySimplyConnectedOn s) (hx : x ∈ s) : SemilocallySimplyConnectedAt x

Extract the pointwise SemilocallySimplyConnectedAt x statement from SemilocallySimplyConnectedOn s and x ∈ s.

theorem SemilocallySimplyConnectedOn.mono {X : Type u_1} [TopologicalSpace X] {s t : Set X} (h : SemilocallySimplyConnectedOn t) (hst : s ⊆ t) : SemilocallySimplyConnectedOn s

Semilocal simple connectivity on a set restricts to any subset.

theorem semilocallySimplyConnectedOn_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} : SemilocallySimplyConnectedOn s ↔ ∀ x ∈ s, ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ ∀ (γ : Path x x), Set.range ⇑γ ⊆ U → γ.Homotopic (Path.refl x)

Set-level characterization of SemilocallySimplyConnectedOn: every point of s has an open neighbourhood in which every loop based at that point is null-homotopic in the ambient space.

theorem semilocallySimplyConnectedOn_iff_paths {X : Type u_1} [TopologicalSpace X] {s : Set X} : SemilocallySimplyConnectedOn s ↔ ∀ x ∈ s, ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ ∀ {u : X} (γ γ' : Path x u), Set.range ⇑γ ⊆ U → Set.range ⇑γ' ⊆ U → γ.Homotopic γ'

Set-level path characterization of SemilocallySimplyConnectedOn: every point x of s has an open neighbourhood in which paths from x to a common endpoint are homotopic in the ambient space.

theorem SemilocallySimplyConnectedOn.of_semilocallySimplyConnectedSpace {X : Type u_1} [TopologicalSpace X] [TauCeti.SemilocallySimplyConnectedSpace X] (s : Set X) : SemilocallySimplyConnectedOn s

A semilocally simply connected space is semilocally simply connected on every subset.

Path-homotopy-trivial neighbourhoods

theorem SemilocallySimplyConnectedAt.exists_isOpen_mem_isPathConnected_isPathHomotopyTrivial {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] {x : X} (h : SemilocallySimplyConnectedAt x) : ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ IsPathConnected U ∧ IsPathHomotopyTrivial U

In a locally path-connected space, a point at which the space is semilocally simply connected has an open, path-connected, path-homotopy-trivial neighbourhood, as needed in the construction of the universal cover.

theorem exists_isOpen_mem_isPathConnected_isPathHomotopyTrivial {X : Type u_1} [TopologicalSpace X] [TauCeti.SemilocallySimplyConnectedSpace X] [LocallyPathConnectedSpace X] (x : X) : ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ IsPathConnected U ∧ IsPathHomotopyTrivial U

In a locally path-connected semilocally simply connected space, every point has an open, path-connected, path-homotopy-trivial neighbourhood.

Discreteness of path-homotopy quotients

theorem Path.exists_isInTube_of_semilocallySimplyConnectedOn {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] {x y : X} (γ : Path x y) (hγ : SemilocallySimplyConnectedOn (Set.range ⇑γ)) : ∃ (n : ℕ) (part : unitInterval.Partition n) (T : Tube X n), IsInTube (⇑γ) part T

In a locally path-connected space, a path along whose range the space is semilocally simply connected lies in a tube.

theorem Path.isOpen_setOf_homotopic_of_semilocallySimplyConnectedOn {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] {x y : X} (p : Path x y) (hslsc : ∀ (q : Path x y), q.Homotopic p → SemilocallySimplyConnectedOn (Set.range ⇑q)) : IsOpen {p' : Path x y | p'.Homotopic p}

In a locally path-connected space, if semilocal simple connectivity holds along every path homotopic to p, then the set of paths homotopic to p is open in the compact-open topology.

theorem Path.isOpen_setOf_homotopic {X : Type u_1} [TopologicalSpace X] [TauCeti.SemilocallySimplyConnectedSpace X] [LocallyPathConnectedSpace X] {x y : X} (p : Path x y) : IsOpen {p' : Path x y | p'.Homotopic p}

In a semilocally simply connected, locally path-connected space, the set of paths homotopic to a given path is open in the compact-open topology.

theorem Path.Homotopic.Quotient.discreteTopology_of_semilocallySimplyConnectedOn {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] {x y : X} (hslsc : ∀ (p : Path x y), SemilocallySimplyConnectedOn (Set.range ⇑p)) : DiscreteTopology (Homotopic.Quotient x y)

In a locally path-connected space, if semilocal simple connectivity holds along every path from x to y, the quotient of these paths by homotopy is discrete.

@[instance 100]

instance Path.Homotopic.Quotient.discreteTopology {X : Type u_1} [TopologicalSpace X] [TauCeti.SemilocallySimplyConnectedSpace X] [LocallyPathConnectedSpace X] {x y : X} : DiscreteTopology (Homotopic.Quotient x y)

In a semilocally simply connected, locally path-connected space, the quotient of paths by homotopy is discrete.