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

    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: TODO: drop this definition.

    Instances For

      Any homeomorphism is a homotopy equivalence.

      Instances For

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

        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.

          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.

            Instances For

              Any topological space is homotopy equivalent to itself.

              Instances For
                @[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), ↑(ContinuousMap.HomotopyEquiv.trans h₁ 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.

                Instances For

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

                  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.

                    Instances For