Documentation

Mathlib.Topology.Homotopy.Equiv

Homotopy equivalences between topological spaces #

In this file, we define homotopy equivalences between topological spaces X and Y as a pair of functions f : C(X, Y) and g : C(Y, X) such that f.comp g and g.comp f are both homotopic to ContinuousMap.id.

Main definitions #

Notation #

We introduce the notation X ≃ₕ Y for ContinuousMap.HomotopyEquiv X Y in the ContinuousMap locale.

structure ContinuousMap.HomotopyEquiv (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] :
Type (max u v)

A homotopy equivalence between topological spaces X and Y are a pair of functions toFun : C(X, Y) and invFun : C(Y, X) such that toFun.comp invFun and invFun.comp toFun are both homotopic to corresponding identity maps.

Instances For
    theorem ContinuousMap.HomotopyEquiv.ext_iff {X : Type u} {Y : Type v} {inst✝ : TopologicalSpace X} {inst✝¹ : TopologicalSpace Y} {x y : HomotopyEquiv X Y} :
    theorem ContinuousMap.HomotopyEquiv.ext {X : Type u} {Y : Type v} {inst✝ : TopologicalSpace X} {inst✝¹ : TopologicalSpace Y} {x y : HomotopyEquiv X Y} (toFun : x.toFun = y.toFun) (invFun : x.invFun = y.invFun) :
    x = y

    A homotopy equivalence between topological spaces X and Y are a pair of functions toFun : C(X, Y) and invFun : C(Y, X) such that toFun.comp invFun and invFun.comp toFun are both homotopic to corresponding identity maps.

    Equations
    Instances For

      Any homeomorphism is a homotopy equivalence.

      Equations
      Instances For
        @[simp]

        If X is homotopy equivalent to Y, then Y is homotopy equivalent to X.

        Equations
        Instances For

          See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

          Equations
          Instances For

            See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

            Equations
            Instances For

              Any topological space is homotopy equivalent to itself.

              Equations
              Instances For
                @[simp]

                If X is homotopy equivalent to Y, and Y is homotopy equivalent to Z, then X is homotopy equivalent to Z.

                Equations
                Instances For
                  @[simp]
                  theorem ContinuousMap.HomotopyEquiv.trans_apply {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : HomotopyEquiv X Y) (h₂ : HomotopyEquiv Y Z) (a✝ : X) :
                  (h₁.trans h₂).toFun a✝ = h₂.toFun (h₁.toFun a✝)
                  @[simp]
                  theorem ContinuousMap.HomotopyEquiv.trans_symm_apply {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : HomotopyEquiv X Y) (h₂ : HomotopyEquiv Y Z) (a✝ : Z) :
                  (h₁.trans h₂).symm.toFun a✝ = h₁.symm.toFun (h₂.symm.toFun a✝)
                  theorem ContinuousMap.HomotopyEquiv.symm_trans {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : HomotopyEquiv X Y) (h₂ : HomotopyEquiv Y Z) :
                  (h₁.trans h₂).symm = h₂.symm.trans h₁.symm
                  def ContinuousMap.HomotopyEquiv.prodCongr {X : Type u} {Y : Type v} {Z : Type w} {Z' : Type x} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z'] (h₁ : HomotopyEquiv X Y) (h₂ : HomotopyEquiv Z Z') :
                  HomotopyEquiv (X × Z) (Y × Z')

                  If X is homotopy equivalent to Y and Z is homotopy equivalent to Z', then X × Z is homotopy equivalent to Z × Z'.

                  Equations
                  Instances For
                    def ContinuousMap.HomotopyEquiv.piCongrRight {ι : Type u_1} {X : ιType u_2} {Y : ιType u_3} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] (h : (i : ι) → HomotopyEquiv (X i) (Y i)) :
                    HomotopyEquiv ((i : ι) → X i) ((i : ι) → Y i)

                    If X i is homotopy equivalent to Y i for each i, then the space of functions (a.k.a. the indexed product) ∀ i, X i is homotopy equivalent to ∀ i, Y i.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem Homeomorph.trans_toHomotopyEquiv {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₀ : X ≃ₜ Y) (h₁ : Y ≃ₜ Z) :