Simply connected spaces

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

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_1) [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 simply_connected_def (X : Type u_1) [TopologicalSpace X] : SimplyConnectedSpace X ↔ Nonempty (FundamentalGroupoid X ≌ CategoryTheory.Discrete Unit)

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

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

@[instance 100]

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

theorem SimplyConnectedSpace.paths_homotopic {X : Type u_1} [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) [TopologicalSpace Y] [ContractibleSpace Y] : SimplyConnectedSpace Y

theorem simply_connected_iff_paths_homotopic {Y : Type u_1} [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_1} [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_1} [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).