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

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

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

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 : f.Nullhomotopic) (g : C(Y, Z)) : (g.comp f).Nullhomotopic

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 : f.Nullhomotopic) (g : C(X, Y)) : (f.comp g).Nullhomotopic

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.id X).Nullhomotopic

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

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.instOfNonemptyOfSubsingleton {Y : Type u_2} [TopologicalSpace Y] [Nonempty Y] [Subsingleton Y] : ContractibleSpace Y

Equations

• ⋯ = ⋯

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 100]

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

Equations

• ⋯ = ⋯