Mathlib.Topology.Connected.LocPathConnected

Module docstring

{"# Locally path-connected spaces

This file defines LocPathConnectedSpace X, a predicate class asserting that X is locally path-connected, in that each point has a basis of path-connected neighborhoods.

Main results

IsOpen.pathComponent / IsClosed.pathComponent: in locally path-connected spaces, path-components are both open and closed.
pathComponent_eq_connectedComponent: in locally path-connected spaces, path-components and connected components agree.
pathConnectedSpace_iff_connectedSpace: locally path-connected spaces are path-connected iff they are connected.
instLocallyConnectedSpace: locally path-connected spaces are also locally connected.
IsOpen.locPathConnectedSpace: open subsets of locally path-connected spaces are locally path-connected.
LocPathConnectedSpace.coinduced / Quotient.locPathConnectedSpace: quotients of locally path-connected spaces are locally path-connected.
Sum.locPathConnectedSpace / Sigma.locPathConnectedSpace: disjoint unions of locally path-connected spaces are locally path-connected.

Abstractly, this also shows that locally path-connected spaces form a coreflective subcategory of the category of topological spaces, although we do not prove that in this form here.

Implementation notes

In the definition of LocPathConnectedSpace X we require neighbourhoods in the basis to be path-connected, but not necessarily open; that they can also be required to be open is shown as a theorem in isOpen_isPathConnected_basis. "}

LocPathConnectedSpace structure

(X : Type*) [TopologicalSpace X]

Full source

/-- A topological space is locally path connected, at every point, path connected
neighborhoods form a neighborhood basis. -/
class LocPathConnectedSpace (X : Type*) [TopologicalSpace X] : Prop where
  /-- Each neighborhood filter has a basis of path-connected neighborhoods. -/
  path_connected_basis : ∀ x : X, (𝓝 x).HasBasis (fun s : Set X => s ∈ 𝓝 xs ∈ 𝓝 x ∧ IsPathConnected s) id

Locally path-connected space

Informal description

A topological space $X$ is called locally path-connected if every point in $X$ has a neighborhood basis consisting of path-connected sets. That is, for every point $x \in X$ and every neighborhood $U$ of $x$, there exists a path-connected neighborhood $V$ of $x$ such that $V \subseteq U$.

LocPathConnectedSpace.of_bases theorem

 {p : X → ι → Prop} {s : X → ι → Set X} (h : ∀ x, (𝓝 x).HasBasis (p x) (s x))
  (h' : ∀ x i, p x i → IsPathConnected (s x i)) : LocPathConnectedSpace X

Full source

theorem LocPathConnectedSpace.of_bases {p : X → ι → Prop} {s : X → ι → Set X}
    (h : ∀ x, (𝓝 x).HasBasis (p x) (s x)) (h' : ∀ x i, p x i → IsPathConnected (s x i)) :
    LocPathConnectedSpace X where
  path_connected_basis x := by
    rw [hasBasis_self]
    intro t ht
    rcases (h x).mem_iff.mp ht with ⟨i, hpi, hi⟩
    exact ⟨s x i, (h x).mem_of_mem hpi, h' x i hpi, hi⟩

Characterization of Locally Path-Connected Spaces via Neighborhood Bases

Informal description

Let $X$ be a topological space, and for each $x \in X$, let $p_x : \iota \to \text{Prop}$ be a predicate and $s_x : \iota \to \text{Set } X$ be a family of sets. Suppose that for every $x \in X$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of the sets $s_x(i)$ indexed by $p_x(i)$. If for every $x \in X$ and every index $i$, the condition $p_x(i)$ implies that $s_x(i)$ is path-connected, then $X$ is locally path-connected.

IsOpen.pathComponentIn theorem

(x : X) (hF : IsOpen F) : IsOpen (pathComponentIn x F)

Full source

protected theorem IsOpen.pathComponentIn (x : X) (hF : IsOpen F) :
    IsOpen (pathComponentIn x F) := by
  rw [isOpen_iff_mem_nhds]
  intro y hy
  let ⟨s, hs⟩ := (path_connected_basis y).mem_iff.mp (hF.mem_nhds (pathComponentIn_subset hy))
  exact mem_of_superset hs.1.1 <| pathComponentIn_congr hy ▸
    hs.1.2.subset_pathComponentIn (mem_of_mem_nhds hs.1.1) hs.2

Openness of Path Components in Open Subsets

Informal description

Let $X$ be a topological space and $F$ an open subset of $X$. For any point $x \in F$, the path component of $x$ in $F$ (i.e., the set of all points in $F$ that can be connected to $x$ by a path in $F$) is an open subset of $X$.

IsOpen.pathComponent theorem

(x : X) : IsOpen (pathComponent x)

Full source

/-- In a locally path connected space, each path component is an open set. -/
protected theorem IsOpen.pathComponent (x : X) : IsOpen (pathComponent x) := by
  rw [← pathComponentIn_univ]
  exact isOpen_univ.pathComponentIn _

Path Components are Open in Locally Path-Connected Spaces

Informal description

In a locally path-connected topological space $X$, for any point $x \in X$, the path component containing $x$ is an open subset of $X$.

IsClosed.pathComponent theorem

(x : X) : IsClosed (pathComponent x)

Full source

/-- In a locally path connected space, each path component is a closed set. -/
protected theorem IsClosed.pathComponent (x : X) : IsClosed (pathComponent x) := by
  rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
  intro y hxy
  rcases (path_connected_basis y).ex_mem with ⟨V, hVy, hVc⟩
  filter_upwards [hVy] with z hz hxz
  exact hxy <|  hxz.trans (hVc.joinedIn _ hz _ (mem_of_mem_nhds hVy)).joined

Path Components are Closed in Locally Path-Connected Spaces

Informal description

In a locally path-connected space $X$, for any point $x \in X$, the path component containing $x$ is a closed subset of $X$.

IsClopen.pathComponent theorem

(x : X) : IsClopen (pathComponent x)

Full source

/-- In a locally path connected space, each path component is a clopen set. -/
protected theorem IsClopen.pathComponent (x : X) : IsClopen (pathComponent x) :=
  ⟨.pathComponent x, .pathComponent x⟩

Path Components are Clopen in Locally Path-Connected Spaces

Informal description

In a locally path-connected topological space $X$, for any point $x \in X$, the path component containing $x$ is both open and closed (i.e., clopen).

pathComponentIn_mem_nhds theorem

(hF : F ∈ 𝓝 x) : pathComponentIn x F ∈ 𝓝 x

Full source

lemma pathComponentIn_mem_nhds (hF : F ∈ 𝓝 x) : pathComponentInpathComponentIn x F ∈ 𝓝 x := by
  let ⟨u, huF, hu, hxu⟩ := mem_nhds_iff.mp hF
  exact mem_nhds_iff.mpr ⟨pathComponentIn x u, pathComponentIn_mono huF,
    hu.pathComponentIn x, mem_pathComponentIn_self hxu⟩

Path Components of Neighborhoods are Neighborhoods

Informal description

Let $X$ be a topological space and $x \in X$ a point. For any neighborhood $F$ of $x$ in $X$, the path component of $x$ in $F$ (i.e., the set of all points in $F$ that can be connected to $x$ by a path in $F$) is also a neighborhood of $x$.

pathConnectedSpace_iff_connectedSpace theorem

: PathConnectedSpace X ↔ ConnectedSpace X

Full source

theorem pathConnectedSpace_iff_connectedSpace : PathConnectedSpacePathConnectedSpace X ↔ ConnectedSpace X := by
  refine ⟨fun _ ↦ inferInstance, fun h ↦ ⟨inferInstance, fun x y ↦ ?_⟩⟩
  rw [← mem_pathComponent_iff, (IsClopen.pathComponent _).eq_univ] <;> simp

Path-Connectedness Equivalence to Connectedness in Topological Spaces

Informal description

A topological space $X$ is path-connected if and only if it is connected.

pathComponent_eq_connectedComponent theorem

(x : X) : pathComponent x = connectedComponent x

Full source

theorem pathComponent_eq_connectedComponent (x : X) : pathComponent x = connectedComponent x :=
  (pathComponent_subset_component x).antisymm <|
    (IsClopen.pathComponent x).connectedComponent_subset (mem_pathComponent_self _)

Equality of Path Components and Connected Components in Locally Path-Connected Spaces

Informal description

In a locally path-connected topological space $X$, for any point $x \in X$, the path component containing $x$ is equal to the connected component containing $x$.

pathConnected_subset_basis theorem

 {U : Set X} (h : IsOpen U) (hx : x ∈ U) : (𝓝 x).HasBasis (fun s : Set X => s ∈ 𝓝 x ∧ IsPathConnected s ∧ s ⊆ U) id

Full source

theorem pathConnected_subset_basis {U : Set X} (h : IsOpen U) (hx : x ∈ U) :
    (𝓝 x).HasBasis (fun s : Set X => s ∈ 𝓝 xs ∈ 𝓝 x ∧ IsPathConnected s ∧ s ⊆ U) id :=
  (path_connected_basis x).hasBasis_self_subset (IsOpen.mem_nhds h hx)

Path-Connected Neighborhood Basis in Locally Path-Connected Spaces

Informal description

Let $X$ be a locally path-connected space, $U \subseteq X$ an open set, and $x \in U$. Then the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of path-connected neighborhoods $s$ of $x$ that are contained in $U$. That is, a set $V$ belongs to $\mathcal{N}(x)$ if and only if there exists a path-connected neighborhood $s$ of $x$ such that $s \subseteq U$ and $s \subseteq V$.

isOpen_isPathConnected_basis theorem

(x : X) : (𝓝 x).HasBasis (fun s : Set X ↦ IsOpen s ∧ x ∈ s ∧ IsPathConnected s) id

Full source

theorem isOpen_isPathConnected_basis (x : X) :
    (𝓝 x).HasBasis (fun s : Set X ↦ IsOpenIsOpen s ∧ x ∈ s ∧ IsPathConnected s) id := by
  refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ mem_nhds_iff.mpr ⟨u, hu.2, hu.1.1, hu.1.2.1⟩⟩⟩
  have ⟨u, hus, hu, hxu⟩ := mem_nhds_iff.mp hs
  exact ⟨pathComponentIn x u, ⟨hu.pathComponentIn _, ⟨mem_pathComponentIn_self hxu,
    isPathConnected_pathComponentIn hxu⟩⟩, pathComponentIn_subset.trans hus⟩

Neighborhood Basis of Open Path-Connected Sets in Locally Path-Connected Spaces

Informal description

For any point $x$ in a locally path-connected space $X$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of open, path-connected sets containing $x$. That is, a set $U$ is a neighborhood of $x$ if and only if there exists an open, path-connected set $V$ such that $x \in V \subseteq U$.

Topology.IsOpenEmbedding.locPathConnectedSpace theorem

{e : Y → X} (he : IsOpenEmbedding e) : LocPathConnectedSpace Y

Full source

theorem Topology.IsOpenEmbedding.locPathConnectedSpace {e : Y → X} (he : IsOpenEmbedding e) :
    LocPathConnectedSpace Y :=
  have (y : Y) :
      (𝓝 y).HasBasis (fun s ↦ s ∈ 𝓝 (e y)s ∈ 𝓝 (e y) ∧ IsPathConnected s ∧ s ⊆ range e) (e ⁻¹' ·) :=
    he.basis_nhds <| pathConnected_subset_basis he.isOpen_range (mem_range_self _)
  .of_bases this fun x s ⟨_, hs, hse⟩ ↦ by
    rwa [he.isPathConnected_iff, image_preimage_eq_of_subset hse]

Open Embedding Preserves Local Path-Connectedness

Informal description

Let $X$ and $Y$ be topological spaces and $e : Y \to X$ be an open embedding. If $X$ is locally path-connected, then $Y$ is also locally path-connected.

IsOpen.locPathConnectedSpace theorem

{U : Set X} (h : IsOpen U) : LocPathConnectedSpace U

Full source

theorem IsOpen.locPathConnectedSpace {U : Set X} (h : IsOpen U) : LocPathConnectedSpace U :=
  h.isOpenEmbedding_subtypeVal.locPathConnectedSpace

Open Subsets of Locally Path-Connected Spaces are Locally Path-Connected

Informal description

For any open subset $U$ of a locally path-connected topological space $X$, the subspace $U$ is also locally path-connected.

IsOpen.isConnected_iff_isPathConnected theorem

{U : Set X} (U_op : IsOpen U) : IsConnected U ↔ IsPathConnected U

Full source

theorem IsOpen.isConnected_iff_isPathConnected {U : Set X} (U_op : IsOpen U) :
    IsConnectedIsConnected U ↔ IsPathConnected U := by
  rw [isConnected_iff_connectedSpace, isPathConnected_iff_pathConnectedSpace]
  haveI := U_op.locPathConnectedSpace
  exact pathConnectedSpace_iff_connectedSpace.symm

Open Subsets are Connected if and only if Path-Connected

Informal description

For any open subset $U$ of a topological space $X$, $U$ is connected if and only if it is path-connected.

instLocallyConnectedSpace instance

: LocallyConnectedSpace X

Full source

/-- Locally path-connected spaces are locally connected. -/
instance : LocallyConnectedSpace X := by
  refine ⟨forall_imp (fun x h ↦ ⟨fun s ↦ ?_⟩) isOpen_isPathConnected_basis⟩
  refine ⟨fun hs ↦ ?_, fun ⟨u, ⟨hu, hxu, _⟩, hus⟩ ↦ mem_nhds_iff.mpr ⟨u, hus, hu, hxu⟩⟩
  let ⟨u, ⟨hu, hxu, hu'⟩, hus⟩ := (h.mem_iff' s).mp hs
  exact ⟨u, ⟨hu, hxu, hu'.isConnected⟩, hus⟩

Locally Path-Connected Spaces are Locally Connected

Informal description

Every locally path-connected space $X$ is also locally connected.

locPathConnectedSpace_iff_isOpen_pathComponentIn theorem

 {X : Type*} [TopologicalSpace X] :
  LocPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn x u)

Full source

/-- A space is locally path-connected iff all path components of open subsets are open. -/
lemma locPathConnectedSpace_iff_isOpen_pathComponentIn {X : Type*} [TopologicalSpace X] :
    LocPathConnectedSpaceLocPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn x u) :=
  ⟨fun _ _ _ hu ↦ hu.pathComponentIn _, fun h ↦ ⟨fun x ↦ ⟨fun s ↦ by
    refine ⟨fun hs ↦ ?_, fun ⟨_, ht⟩ ↦ Filter.mem_of_superset ht.1.1 ht.2⟩
    let ⟨u, hu⟩ := mem_nhds_iff.mp hs
    exact ⟨pathComponentIn x u, ⟨(h x u hu.2.1).mem_nhds (mem_pathComponentIn_self hu.2.2),
      isPathConnected_pathComponentIn hu.2.2⟩, pathComponentIn_subset.trans hu.1⟩⟩⟩⟩

Characterization of Locally Path-Connected Spaces via Open Path Components

Informal description

A topological space $X$ is locally path-connected if and only if for every point $x \in X$ and every open subset $u \subseteq X$, the path component of $x$ in $u$ (denoted $\text{pathComponentIn}(x, u)$) is an open subset of $X$.

locPathConnectedSpace_iff_pathComponentIn_mem_nhds theorem

 {X : Type*} [TopologicalSpace X] :
  LocPathConnectedSpace X ↔ ∀ x : X, ∀ u : Set X, IsOpen u → x ∈ u → pathComponentIn x u ∈ nhds x

Full source

/-- A space is locally path-connected iff all path components of open subsets are neighbourhoods. -/
lemma locPathConnectedSpace_iff_pathComponentIn_mem_nhds {X : Type*} [TopologicalSpace X] :
    LocPathConnectedSpaceLocPathConnectedSpace X ↔
    ∀ x : X, ∀ u : Set X, IsOpen u → x ∈ u → pathComponentIn x u ∈ nhds x := by
  rw [locPathConnectedSpace_iff_isOpen_pathComponentIn]
  simp_rw [forall_comm (β := Set X), ← imp_forall_iff]
  refine forall_congr' fun u ↦ imp_congr_right fun _ ↦ ?_
  exact ⟨fun h x hxu ↦ (h x).mem_nhds (mem_pathComponentIn_self hxu),
    fun h x ↦ isOpen_iff_mem_nhds.mpr fun y hy ↦
      pathComponentIn_congr hy ▸ h y <| pathComponentIn_subset hy⟩

Characterization of locally path-connected spaces via path components in neighborhoods

Informal description

A topological space $X$ is locally path-connected if and only if for every point $x \in X$ and every open subset $u \subseteq X$ containing $x$, the path component of $x$ in $u$ belongs to the neighborhood filter of $x$.

LocPathConnectedSpace.coinduced theorem

{Y : Type*} (f : X → Y) : @LocPathConnectedSpace Y (.coinduced f ‹_›)

Full source

/-- Any topology coinduced by a locally path-connected topology is locally path-connected. -/
lemma LocPathConnectedSpace.coinduced {Y : Type*} (f : X → Y) :
    @LocPathConnectedSpace Y (.coinduced f ‹_›) := by
  let _ := TopologicalSpace.coinduced f ‹_›; have hf : Continuous f := continuous_coinduced_rng
  refine locPathConnectedSpace_iff_isOpen_pathComponentIn.mpr fun y u hu ↦
    isOpen_coinduced.mpr <| isOpen_iff_mem_nhds.mpr fun x hx ↦ ?_
  have hx' := preimage_mono pathComponentIn_subset hx
  refine mem_nhds_iff.mpr ⟨pathComponentIn x (f ⁻¹' u), ?_,
    (hu.preimage hf).pathComponentIn _, mem_pathComponentIn_self hx'⟩
  rw [← image_subset_iff, ← pathComponentIn_congr hx]
  exact ((isPathConnected_pathComponentIn hx').image hf).subset_pathComponentIn
    ⟨x, mem_pathComponentIn_self hx', rfl⟩ <|
    (image_mono pathComponentIn_subset).trans <| u.image_preimage_subset f

Coinduced Topology Preserves Local Path-Connectedness

Informal description

Let $X$ be a locally path-connected topological space and $f \colon X \to Y$ a function. Then the coinduced topology on $Y$ by $f$ is also locally path-connected. That is, for any point $y \in Y$ and any neighborhood $V$ of $y$, there exists a path-connected neighborhood $W$ of $y$ such that $W \subseteq V$.

Topology.IsQuotientMap.locPathConnectedSpace theorem

{f : X → Y} (h : IsQuotientMap f) : LocPathConnectedSpace Y

Full source

/-- Quotients of locally path-connected spaces are locally path-connected. -/
lemma Topology.IsQuotientMap.locPathConnectedSpace {f : X → Y} (h : IsQuotientMap f) :
    LocPathConnectedSpace Y :=
  h.2 ▸ LocPathConnectedSpace.coinduced f

Quotient Maps Preserve Local Path-Connectedness

Informal description

Let $X$ and $Y$ be topological spaces, and let $f \colon X \to Y$ be a quotient map. If $X$ is locally path-connected, then $Y$ is also locally path-connected.

Quot.locPathConnectedSpace instance

{r : X → X → Prop} : LocPathConnectedSpace (Quot r)

Full source

/-- Quotients of locally path-connected spaces are locally path-connected. -/
instance Quot.locPathConnectedSpace {r : X → X → Prop} : LocPathConnectedSpace (Quot r) :=
  isQuotientMap_quot_mk.locPathConnectedSpace

Local Path-Connectedness of Quotient Spaces

Informal description

For any topological space $X$ with a relation $r$ on $X$, if $X$ is locally path-connected, then the quotient space $\text{Quot } r$ is also locally path-connected. This means that every point in $\text{Quot } r$ has a neighborhood basis consisting of path-connected sets.

Quotient.locPathConnectedSpace instance

{s : Setoid X} : LocPathConnectedSpace (Quotient s)

Full source

/-- Quotients of locally path-connected spaces are locally path-connected. -/
instance Quotient.locPathConnectedSpace {s : Setoid X} : LocPathConnectedSpace (Quotient s) :=
  isQuotientMap_quotient_mk'.locPathConnectedSpace

Quotient Spaces Preserve Local Path-Connectedness

Informal description

For any topological space $X$ with an equivalence relation $s$ (represented as a setoid), if $X$ is locally path-connected, then the quotient space $X/s$ is also locally path-connected.

Sum.locPathConnectedSpace instance

 {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] [LocPathConnectedSpace X] [LocPathConnectedSpace Y] :
  LocPathConnectedSpace (X ⊕ Y)

Full source

/-- Disjoint unions of locally path-connected spaces are locally path-connected. -/
instance Sum.locPathConnectedSpace.{u} {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y]
    [LocPathConnectedSpace X] [LocPathConnectedSpace Y] :
    LocPathConnectedSpace (X ⊕ Y) := by
  rw [locPathConnectedSpace_iff_pathComponentIn_mem_nhds]; intro x u hu hxu; rw [mem_nhds_iff]
  obtain x | y := x
  · refine ⟨Sum.inl '' (pathComponentIn x (Sum.inl ⁻¹' u)), ?_, ?_, ?_⟩
    · apply IsPathConnected.subset_pathComponentIn
      · exact (isPathConnected_pathComponentIn (by exact hxu)).image continuous_inl
      · exact ⟨x, mem_pathComponentIn_self hxu, rfl⟩
      · exact (image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)
    · exact isOpenMap_inl _ <| (hu.preimage continuous_inl).pathComponentIn _
    · exact ⟨x, mem_pathComponentIn_self hxu, rfl⟩
  · refine ⟨Sum.inr '' (pathComponentIn y (Sum.inr ⁻¹' u)), ?_, ?_, ?_⟩
    · apply IsPathConnected.subset_pathComponentIn
      · exact (isPathConnected_pathComponentIn (by exact hxu)).image continuous_inr
      · exact ⟨y, mem_pathComponentIn_self hxu, rfl⟩
      · exact (image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)
    · exact isOpenMap_inr _ <| (hu.preimage continuous_inr).pathComponentIn _
    · exact ⟨y, mem_pathComponentIn_self hxu, rfl⟩

Disjoint Union of Locally Path-Connected Spaces is Locally Path-Connected

Informal description

For any two topological spaces $X$ and $Y$ that are locally path-connected, their disjoint union $X \oplus Y$ is also locally path-connected. This means that every point in $X \oplus Y$ has a neighborhood basis consisting of path-connected sets.

Sigma.locPathConnectedSpace instance

 {X : ι → Type*} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → LocPathConnectedSpace (X i)] :
  LocPathConnectedSpace ((i : ι) × X i)

Full source

/-- Disjoint unions of locally path-connected spaces are locally path-connected. -/
instance Sigma.locPathConnectedSpace {X : ι → Type*}
    [(i : ι) → TopologicalSpace (X i)] [(i : ι) → LocPathConnectedSpace (X i)] :
    LocPathConnectedSpace ((i : ι) × X i) := by
  rw [locPathConnectedSpace_iff_pathComponentIn_mem_nhds]; intro x u hu hxu; rw [mem_nhds_iff]
  refine ⟨(Sigma.mk x.1) '' (pathComponentIn x.2 ((Sigma.mk x.1) ⁻¹' u)), ?_, ?_, ?_⟩
  · apply IsPathConnected.subset_pathComponentIn
    · exact (isPathConnected_pathComponentIn (by exact hxu)).image continuous_sigmaMk
    · exact ⟨x.2, mem_pathComponentIn_self hxu, rfl⟩
    · exact (image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)
  · exact isOpenMap_sigmaMk _ <| (hu.preimage continuous_sigmaMk).pathComponentIn _
  · exact ⟨x.2, mem_pathComponentIn_self hxu, rfl⟩

Disjoint Union of Locally Path-Connected Spaces is Locally Path-Connected

Informal description

For any family of topological spaces $\{X_i\}_{i \in \iota}$ where each $X_i$ is locally path-connected, the disjoint union $\Sigma_{i \in \iota} X_i$ is also locally path-connected.