mathlib3 documentation

topology.homotopy.contractible

Contractible spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we define contractible_space, a space that is homotopy equivalent to unit.

source
def continuous_map.nullhomotopic {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (f : C(X, Y)) :
Prop

A map is nullhomotopic if it is homotopic to a constant map.

Equations
source
theorem continuous_map.nullhomotopic_of_constant {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (y : Y) :
(continuous_map.const X y).nullhomotopic
source
theorem continuous_map.nullhomotopic.comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] [topological_space Y] [topological_space Z] {f : C(X, Y)} (hf : f.nullhomotopic) (g : C(Y, Z)) :
(g.comp f).nullhomotopic
source
theorem continuous_map.nullhomotopic.comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] [topological_space Y] [topological_space Z] {f : C(Y, Z)} (hf : f.nullhomotopic) (g : C(X, Y)) :
(f.comp g).nullhomotopic
source
@[class]
structure contractible_space (X : Type u_1) [topological_space X] :
Prop

A contractible space is one that is homotopy equivalent to unit.

Instances of this typeclass
source
theorem id_nullhomotopic (X : Type u_1) [topological_space X] [contractible_space X] :
(continuous_map.id X).nullhomotopic
source
theorem contractible_iff_id_nullhomotopic (Y : Type u_1) [topological_space Y] :
contractible_space Y ↔ (continuous_map.id Y).nullhomotopic
source
@[protected]
theorem continuous_map.homotopy_equiv.contractible_space {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] [contractible_space Y] (e : continuous_map.homotopy_equiv X Y) :
contractible_space X
source
@[protected]
theorem continuous_map.homotopy_equiv.contractible_space_iff {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (e : continuous_map.homotopy_equiv X Y) :
contractible_space X ↔ contractible_space Y
source
@[protected]
theorem homeomorph.contractible_space {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] [contractible_space Y] (e : X ≃ₜ Y) :
contractible_space X
source
@[protected]
theorem homeomorph.contractible_space_iff {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (e : X ≃ₜ Y) :
contractible_space X ↔ contractible_space Y
source
@[protected, instance]
def contractible_space.path_connected_space {X : Type u_1} [topological_space X] [contractible_space X] :
path_connected_space X