Documentation

Mathlib.Topology.Homotopy.Contractible

Contractible spaces #

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

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

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

    Instances
      source
      theorem ContractibleSpace.hequiv_unit (X : Type u_1) [TopologicalSpace X] [ContractibleSpace X] :
      Nonempty (ContinuousMap.HomotopyEquiv X Unit)
      source
      theorem id_nullhomotopic (X : Type u_1) [TopologicalSpace X] [ContractibleSpace X] :
      (ContinuousMap.id X).Nullhomotopic
      source
      theorem contractible_iff_id_nullhomotopic (Y : Type u_1) [TopologicalSpace Y] :
      ContractibleSpace Y ↔ (ContinuousMap.id Y).Nullhomotopic
      source
      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
      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
      theorem Homeomorph.contractibleSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [ContractibleSpace Y] (e : X ≃ₜ Y) :
      ContractibleSpace X
      source
      theorem Homeomorph.contractibleSpace_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) :
      ContractibleSpace X ↔ ContractibleSpace Y
      source
      theorem homotopic_of_indiscrete {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [IndiscreteTopology Y] (f g : C(X, Y)) :
      f.Homotopic g
      source
      theorem nullhomotopic_of_indiscrete {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Nonempty Y] [IndiscreteTopology Y] (f : C(X, Y)) :
      f.Nullhomotopic
      source
      instance ContractibleSpace.instOfNonemptyOfSubsingleton {Y : Type u_2} [TopologicalSpace Y] [Nonempty Y] [Subsingleton Y] :
      ContractibleSpace Y
      source
      instance ContractibleSpace.instOfNonemptyOfIndiscreteTopology {Y : Type u_2} [TopologicalSpace Y] [Nonempty Y] [IndiscreteTopology Y] :
      ContractibleSpace Y
      source
      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
      @[instance 100]
      instance ContractibleSpace.instPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [ContractibleSpace X] :
      PathConnectedSpace X
      source
      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.