Simply connected spaces

This file defines simply connected spaces. A topological space is simply connected if its fundamental groupoid is equivalent to Unit.

We also define the corresponding predicate for sets.

Main theorems

• simply_connected_iff_unique_homotopic - A space is simply connected if and only if it is nonempty and there is a unique path up to homotopy between any two points

• SimplyConnectedSpace.ofContractible - A contractible space is simply connected

class SimplyConnectedSpace (X : Type u_3) [TopologicalSpace X] : Prop

A simply connected space is one whose fundamental groupoid is equivalent to Discrete Unit

• equiv_unit : Nonempty (FundamentalGroupoid X ≌ CategoryTheory.Discrete Unit)

theorem simplyConnectedSpace_iff (X : Type u_3) [TopologicalSpace X] : SimplyConnectedSpace X ↔ Nonempty (FundamentalGroupoid X ≌ CategoryTheory.Discrete Unit)

@[deprecated simplyConnectedSpace_iff (since := "2026-01-08")]

theorem simply_connected_def (X : Type u_3) [TopologicalSpace X] : SimplyConnectedSpace X ↔ Nonempty (FundamentalGroupoid X ≌ CategoryTheory.Discrete Unit)

Alias of simplyConnectedSpace_iff.

theorem simply_connected_iff_unique_homotopic (X : Type u_3) [TopologicalSpace X] : SimplyConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))

theorem ContinuousMap.HomotopyEquiv.simplyConnectedSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [hY : SimplyConnectedSpace Y] (e : HomotopyEquiv X Y) : SimplyConnectedSpace X

theorem ContinuousMap.HomotopyEquiv.simplyConnectedSpace_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) : SimplyConnectedSpace X ↔ SimplyConnectedSpace Y

instance SimplyConnectedSpace.instSubsingletonQuotient {X : Type u_3} [TopologicalSpace X] [SimplyConnectedSpace X] (x y : X) : Subsingleton (Path.Homotopic.Quotient x y)

@[instance 100]

instance SimplyConnectedSpace.instPathConnectedSpace {X : Type u_3} [TopologicalSpace X] [SimplyConnectedSpace X] : PathConnectedSpace X

theorem SimplyConnectedSpace.paths_homotopic {X : Type u_3} [TopologicalSpace X] [SimplyConnectedSpace X] {x y : X} (p₁ p₂ : Path x y) : p₁.Homotopic p₂

In a simply connected space, any two paths are homotopic

@[instance 100]

instance SimplyConnectedSpace.ofContractible (Y : Type u_4) [TopologicalSpace Y] [ContractibleSpace Y] : SimplyConnectedSpace Y

theorem simply_connected_iff_paths_homotopic {Y : Type u_2} [TopologicalSpace Y] : SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)

A space is simply connected iff it is path connected, and there is at most one path up to homotopy between any two points.

theorem simply_connected_iff_paths_homotopic' {Y : Type u_2} [TopologicalSpace Y] : SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂

Another version of simply_connected_iff_paths_homotopic

theorem simply_connected_iff_loops_nullhomotopic {Y : Type u_2} [TopologicalSpace Y] : SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)

A space is simply connected if and only if it is path-connected and every loop at any basepoint is null-homotopic (i.e., homotopic to the constant loop).

Simply connected sets

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

We say that a set is simply connected if it's a simply connected topological space in the induced topology.

theorem IsSimplyConnected.simplyConnectedSpace {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsSimplyConnected s) : SimplyConnectedSpace ↑s

theorem IsSimplyConnected.isPathConnected {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsSimplyConnected s) : IsPathConnected s

theorem IsSimplyConnected.nonempty {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsSimplyConnected s) : s.Nonempty

theorem Topology.IsEmbedding.isSimplyConnected_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsEmbedding f) {s : Set X} : IsSimplyConnected (f '' s) ↔ IsSimplyConnected s

@[simp]

theorem Homeomorph.isSimplyConnected_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y) {s : Set X} : IsSimplyConnected (⇑f '' s) ↔ IsSimplyConnected s

@[simp]

theorem Homeomorph.isSimplyConnected_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y) {s : Set Y} : IsSimplyConnected (⇑f ⁻¹' s) ↔ IsSimplyConnected s

theorem isSimplyConnected_iff_exists_homotopy_refl_forall_mem {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsSimplyConnected s ↔ IsPathConnected s ∧ ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ (F : p.Homotopy (Path.refl x)), ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s

A set is simply connected iff it's path connected and any loop is homotopic to the constant path within s.

@[simp]

theorem isSimplyConnected_smul_set_iff {X : Type u_1} [TopologicalSpace X] {G : Type u_3} [Group G] [MulAction G X] [ContinuousConstSMul G X] {c : G} {s : Set X} : IsSimplyConnected (c • s) ↔ IsSimplyConnected s

@[simp]

theorem isSimplyConnected_vadd_set_iff {X : Type u_1} [TopologicalSpace X] {G : Type u_3} [AddGroup G] [AddAction G X] [ContinuousConstVAdd G X] {c : G} {s : Set X} : IsSimplyConnected (c +ᵥ s) ↔ IsSimplyConnected s

@[simp]

theorem isSimplyConnected_smul_set₀_iff {X : Type u_1} [TopologicalSpace X] {G : Type u_3} [GroupWithZero G] [MulAction G X] [ContinuousConstSMul G X] {c : G} {s : Set X} (hc : c ≠ 0) : IsSimplyConnected (c • s) ↔ IsSimplyConnected s