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.

theorem ContinuousMap.HomotopyEquiv.ext_iff {X : Type u} {Y : Type v} :
∀ {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y} (x y : ContinuousMap.HomotopyEquiv X Y), x = y x.toFun = y.toFun x.invFun = y.invFun
theorem ContinuousMap.HomotopyEquiv.ext {X : Type u} {Y : Type v} :
∀ {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y} (x y : ContinuousMap.HomotopyEquiv X Y), x.toFun = y.toFunx.invFun = y.invFunx = y
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.left_inv {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (self : ContinuousMap.HomotopyEquiv X Y) :
    (self.invFun.comp self.toFun).Homotopic (ContinuousMap.id X)
    theorem ContinuousMap.HomotopyEquiv.right_inv {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (self : ContinuousMap.HomotopyEquiv X Y) :
    (self.toFun.comp self.invFun).Homotopic (ContinuousMap.id Y)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Coercion of a HomotopyEquiv to function. While the Lean 4 way is to unfold coercions, this auxiliary definition will make porting of Lean 3 code easier.

      Porting note (#11215): TODO: drop this definition.

      Equations
      • e = e.toFun
      Instances For
        Equations
        • ContinuousMap.HomotopyEquiv.instCoeFunForall = { coe := ContinuousMap.HomotopyEquiv.toFun' }

        Any homeomorphism is a homotopy equivalence.

        Equations
        • h.toHomotopyEquiv = { toFun := h.toContinuousMap, invFun := h.symm.toContinuousMap, left_inv := , right_inv := }
        Instances For
          @[simp]
          theorem Homeomorph.coe_toHomotopyEquiv {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
          h.toHomotopyEquiv = h

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

          Equations
          • h.symm = { toFun := h.invFun, invFun := h.toFun, left_inv := , right_inv := }
          Instances For
            @[simp]
            theorem ContinuousMap.HomotopyEquiv.coe_invFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : ContinuousMap.HomotopyEquiv X Y) :
            h.invFun = h.symm

            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]
                  theorem ContinuousMap.HomotopyEquiv.trans_symm_apply {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : ContinuousMap.HomotopyEquiv X Y) (h₂ : ContinuousMap.HomotopyEquiv Y Z) :
                  ∀ (a : Z), (h₁.trans h₂).symm a = h₁.symm (h₂.symm a)
                  @[simp]
                  theorem ContinuousMap.HomotopyEquiv.trans_apply {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : ContinuousMap.HomotopyEquiv X Y) (h₂ : ContinuousMap.HomotopyEquiv Y Z) :
                  ∀ (a : X), (h₁.trans h₂) a = h₂ (h₁ a)

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

                  Equations
                  • h₁.trans h₂ = { toFun := h₂.toFun.comp h₁.toFun, invFun := h₁.invFun.comp h₂.invFun, left_inv := , right_inv := }
                  Instances For
                    theorem ContinuousMap.HomotopyEquiv.symm_trans {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : ContinuousMap.HomotopyEquiv X Y) (h₂ : ContinuousMap.HomotopyEquiv Y Z) :
                    (h₁.trans h₂).symm = h₂.symm.trans h₁.symm

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

                    Equations
                    • h₁.prodCongr h₂ = { toFun := h₁.toFun.prodMap h₂.toFun, invFun := h₁.invFun.prodMap h₂.invFun, left_inv := , right_inv := }
                    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 : ι) → ContinuousMap.HomotopyEquiv (X i) (Y i)) :
                      ContinuousMap.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.symm_toHomotopyEquiv {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
                        h.symm.toHomotopyEquiv = h.toHomotopyEquiv.symm
                        @[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) :
                        (h₀.trans h₁).toHomotopyEquiv = h₀.toHomotopyEquiv.trans h₁.toHomotopyEquiv