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

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

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 SimplyConnectedSpace.equiv_unit {X : Type u_1} [TopologicalSpace X] [self : 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 : X) (y : X) : Subsingleton (Path.Homotopic.Quotient x y)

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

theorem SimplyConnectedSpace.paths_homotopic {X : Type u_1} [TopologicalSpace X] [SimplyConnectedSpace X] {x : X} {y : X} (p₁ : Path x y) (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

Equations

• ⋯ = ⋯

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