Contractible spaces

In this file, we define ContractibleSpace, a space that is homotopy equivalent to Unit.

def ContinuousMap.Nullhomotopic {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : Prop

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

Equations

• ContinuousMap.Nullhomotopic f = ∃ (y : Y), ContinuousMap.Homotopic f (ContinuousMap.const X y)

theorem ContinuousMap.nullhomotopic_of_constant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (y : Y) : ContinuousMap.Nullhomotopic (ContinuousMap.const X y)

theorem ContinuousMap.Nullhomotopic.comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : ContinuousMap.Nullhomotopic f) (g : C(Y, Z)) : ContinuousMap.Nullhomotopic (ContinuousMap.comp g f)

theorem ContinuousMap.Nullhomotopic.comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(Y, Z)} (hf : ContinuousMap.Nullhomotopic f) (g : C(X, Y)) : ContinuousMap.Nullhomotopic (ContinuousMap.comp f g)

class ContractibleSpace (X : Type u_1) [TopologicalSpace X] : Prop

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

• hequiv_unit' : Nonempty (ContinuousMap.HomotopyEquiv X Unit)

theorem ContractibleSpace.hequiv_unit (X : Type u_1) [TopologicalSpace X] [ContractibleSpace X] : Nonempty (ContinuousMap.HomotopyEquiv X Unit)

theorem id_nullhomotopic (X : Type u_1) [TopologicalSpace X] [ContractibleSpace X] : ContinuousMap.Nullhomotopic (ContinuousMap.id X)

theorem contractible_iff_id_nullhomotopic (Y : Type u_1) [TopologicalSpace Y] : ContractibleSpace Y ↔ ContinuousMap.Nullhomotopic (ContinuousMap.id Y)

theorem ContinuousMap.HomotopyEquiv.contractibleSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [ContractibleSpace Y] (e : ContinuousMap.HomotopyEquiv X Y) : ContractibleSpace X

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

theorem Homeomorph.contractibleSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [ContractibleSpace Y] (e : X ≃ₜ Y) : ContractibleSpace X

theorem Homeomorph.contractibleSpace_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : ContractibleSpace X ↔ ContractibleSpace Y

instance ContractibleSpace.instContractibleSpace {Y : Type u_2} [TopologicalSpace Y] [Unique Y] : ContractibleSpace Y

Equations

• (_ : ContractibleSpace Y) = (_ : ContractibleSpace Y)

theorem ContractibleSpace.hequiv (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [ContractibleSpace X] [ContractibleSpace Y] : Nonempty (ContinuousMap.HomotopyEquiv X Y)

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

Equations

• (_ : PathConnectedSpace X) = (_ : PathConnectedSpace X)