Documentation

Mathlib.Topology.Homotopy.Contractible

Contractible spaces #

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

source
🔹 coverage
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
    Instances For
      source
      📐 coverage
      theorem ContinuousMap.nullhomotopic_of_constant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (y : Y) :
      (const X y).Nullhomotopic
      source
      📐 coverage
      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
      source
      📐 coverage
      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
      source
      🔶 coverage
      class ContractibleSpace (X : Type u_1) [TopologicalSpace X] :
      Prop

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

      Instances
        source
        📐 coverage
        theorem ContractibleSpace.hequiv_unit (X : Type u_1) [TopologicalSpace X] [ContractibleSpace X] :
        Nonempty (ContinuousMap.HomotopyEquiv X Unit)
        source
        📐 coverage
        theorem id_nullhomotopic (X : Type u_1) [TopologicalSpace X] [ContractibleSpace X] :
        (ContinuousMap.id X).Nullhomotopic
        source
        📐 coverage
        theorem contractible_iff_id_nullhomotopic (Y : Type u_1) [TopologicalSpace Y] :
        ContractibleSpace Y ↔ (ContinuousMap.id Y).Nullhomotopic
        source
        📐 coverage
        theorem ContinuousMap.HomotopyEquiv.contractibleSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [ContractibleSpace Y] (e : HomotopyEquiv X Y) :
        ContractibleSpace X
        source
        📐 coverage
        theorem ContinuousMap.HomotopyEquiv.contractibleSpace_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) :
        ContractibleSpace X ↔ ContractibleSpace Y
        source
        📐 coverage
        theorem Homeomorph.contractibleSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [ContractibleSpace Y] (e : X ≃ₜ Y) :
        ContractibleSpace X
        source
        📐 coverage
        theorem Homeomorph.contractibleSpace_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) :
        ContractibleSpace X ↔ ContractibleSpace Y
        source
        📐 coverage
        instance ContractibleSpace.instOfNonemptyOfSubsingleton {Y : Type u_2} [TopologicalSpace Y] [Nonempty Y] [Subsingleton Y] :
        ContractibleSpace Y
        source
        📐 coverage
        theorem ContractibleSpace.hequiv (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] [ContractibleSpace X] [ContractibleSpace Y] :
        Nonempty (ContinuousMap.HomotopyEquiv X Y)
        source
        📐 coverage
        @[instance 100]
        instance ContractibleSpace.instPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [ContractibleSpace X] :
        PathConnectedSpace X
        source
        📐 coverage
        instance ContractibleSpace.instProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [ContractibleSpace X] [ContractibleSpace Y] :
        ContractibleSpace (X × Y)

        The product of two contractible spaces is contractible.