Simply connected spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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
simply_connected_space.of_contractible - A contractible space is simply connected

source

@[class]

structure simply_connected_space (X : Type u_1) [topological_space X] :

Prop

equiv_unit : nonempty (fundamental_groupoid X ≌ category_theory.discrete unit)

A simply connected space is one whose fundamental groupoid is equivalent to discrete unit

Instances of this typeclass

simply_connected_space.of_contractible

source

theorem simply_connected_def (X : Type u_1) [topological_space X] :

simply_connected_space X ↔ nonempty (fundamental_groupoid X ≌ category_theory.discrete unit)

source

theorem simply_connected_iff_unique_homotopic (X : Type u_1) [topological_space X] :

simply_connected_space X ↔ nonempty X ∧ ∀ (x y : X), nonempty (unique (path.homotopic.quotient x y))

source

@[protected, instance]

def simply_connected_space.path.homotopic.quotient.subsingleton {X : Type u_1} [topological_space X] [simply_connected_space X] (x y : X) :

subsingleton (path.homotopic.quotient x y)

source

@[protected, instance]

def simply_connected_space.path_connected_space {X : Type u_1} [topological_space X] [simply_connected_space X] :

path_connected_space X

source

theorem simply_connected_space.paths_homotopic {X : Type u_1} [topological_space X] [simply_connected_space X] {x y : X} (p₁ p₂ : path x y) :

p₁.homotopic p₂

In a simply connected space, any two paths are homotopic

source

@[protected, instance]

def simply_connected_space.of_contractible (Y : Type) [topological_space Y] [contractible_space Y] :

simply_connected_space Y

source

theorem simply_connected_iff_paths_homotopic {Y : Type u_1} [topological_space Y] :

simply_connected_space Y ↔ path_connected_space 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.

source

theorem simply_connected_iff_paths_homotopic' {Y : Type u_1} [topological_space Y] :

simply_connected_space Y ↔ path_connected_space Y ∧ ∀ {x y : Y} (p₁ p₂ : path x y), p₁.homotopic p₂

Another version of simply_connected_iff_paths_homotopic