Weak homotopy equivalences

A continuous map f : X → Y is a weak homotopy equivalence if it induces a bijection on path components and a bijection π_n(X, x) → π_n(Y, f x) for every n ≥ 1 and every point x : X (Hatcher, Algebraic Topology, Section 4.1). This file defines the predicate ContinuousMap.IsWeakHomotopyEquivalence on Mathlib's cubical homotopy groups and proves its closure properties: homotopy equivalences are weak homotopy equivalences, the predicate depends only on the homotopy class of the map, and it is closed under composition, under left and right cancellation, and under retracts. In a commuting square whose two parallel maps are weak homotopy equivalences, the other two maps have the same connectivity.

Whitehead's theorem, that a weak homotopy equivalence between spaces of CW type is a homotopy equivalence, is ContinuousMap.IsWeakHomotopyEquivalence.homotopyEquiv in TauCeti.AlgebraicTopology.Homotopy.Whitehead.

Main declarations

• ContinuousMap.IsWeakHomotopyEquivalence: the predicate.
• ContinuousMap.IsWeakHomotopyEquivalence.map_bijective: the induced map on the homotopy group indexed by any finite type of cube directions is bijective.
• ContinuousMap.IsWeakHomotopyEquivalence.joined_iff: a weak homotopy equivalence is injective on path components.
• ContinuousMap.IsWeakHomotopyEquivalence.mapOfEq_bijective: a weak homotopy equivalence induces bijections of fundamental groups.
• ContinuousMap.isWeakHomotopyEquivalence_iff_forall_bijective: on a path-connected space it suffices to check bijectivity on homotopy groups at a single base point.
• HomotopyGroup.map_injective_of_isEmpty_of_joined, HomotopyGroup.map_surjective_of_isEmpty_of_exists_joined: in degree zero, the induced map is injective or surjective as soon as the map is on path components.
• ContinuousMap.isWeakHomotopyEquivalence_iff_joined: a weak homotopy equivalence is a bijection on path components inducing bijections on the positive-dimensional homotopy groups.
• ContinuousMap.HomotopyEquiv.isWeakHomotopyEquivalence: a homotopy equivalence is a weak homotopy equivalence.
• ContinuousMap.IsWeakHomotopyEquivalence.of_homotopic, ContinuousMap.IsWeakHomotopyEquivalence.comp, ContinuousMap.IsWeakHomotopyEquivalence.of_postcomp, ContinuousMap.IsWeakHomotopyEquivalence.of_precomp: invariance under homotopy, composition, and left and right cancellation (two out of three).
• ContinuousMap.IsWeakHomotopyEquivalence.of_retract: a retract of a weak homotopy equivalence is a weak homotopy equivalence.
• ContinuousMap.isWeakHomotopyEquivalence_of_contractibleSpace: every map between contractible spaces is a weak homotopy equivalence.
• ContinuousMap.IsWeakHomotopyEquivalence.forall_surjective_map_iff_of_comp_eq, ContinuousMap.IsWeakHomotopyEquivalence.forall_injective_map_iff_of_comp_eq: in a square g ∘ i = j ∘ f with f and g weak homotopy equivalences, j induces surjections (injections) on a homotopy group at every base point exactly when i does.

References

• A. Hatcher, Algebraic Topology, Section 4.1, the definition of weak homotopy equivalence preceding Theorem 4.5.

theorem HomotopyGroup.map_injective_of_isEmpty_of_joined {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty N] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (h : ∀ (a b : X), Joined (f a) (f b) → Joined a b) : Function.Injective (map f hf)

Injectivity in degree zero through path components. For an empty type N of cube directions, π_N(X, x) is the set of path components of X, so the map induced by f is injective when two points of X are joined whenever their images are.

theorem HomotopyGroup.map_surjective_of_isEmpty_of_exists_joined {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty N] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (h : ∀ (b : Y), ∃ (a : X), Joined (f a) b) : Function.Surjective (map f hf)

Surjectivity in degree zero through path components. For an empty type N of cube directions, π_N(Y, y) is the set of path components of Y, so the map induced by f is surjective when every point of Y is joined to a point of the image of f.

structure ContinuousMap.IsWeakHomotopyEquivalence {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : Prop

A continuous map f : X → Y is a weak homotopy equivalence if every point of Y is joined by a path to a point of the image of f, and f induces a bijection π_n(X, x) → π_n(Y, f x) for every n and every x : X.

Since π_0(X, x) is the set of path components of X, the condition in degree 0 says that f is injective on path components, and also surjective on them as soon as X is nonempty. The field exists_joined, surjectivity on path components, adds to this only when X is empty: it then forces Y to be empty as well.

• exists_joined (y : Y) : ∃ (x : X), Joined (f x) y

  Every point of the target is joined by a path to a point of the image.

• bijective (n : ℕ) (x : X) : Function.Bijective (HomotopyGroup.map f ⋯)

  The induced map π_n(X, x) → π_n(Y, f x) is bijective for every n and every x.

theorem ContinuousMap.IsWeakHomotopyEquivalence.map_bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : f.IsWeakHomotopyEquivalence) (N : Type u_4) [Finite N] (x : X) : Function.Bijective (HomotopyGroup.map f ⋯)

A weak homotopy equivalence induces a bijection on the homotopy groups indexed by any finite type of cube directions, not only on the groups π_n indexed by Fin n.

@[simp]

theorem ContinuousMap.IsWeakHomotopyEquivalence.joined_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : f.IsWeakHomotopyEquivalence) {a b : X} : Joined (f a) (f b) ↔ Joined a b

A weak homotopy equivalence is injective on path components: two points of X are joined by a path exactly when their images are.

theorem ContinuousMap.IsWeakHomotopyEquivalence.of_homotopic {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (hf : f₀.IsWeakHomotopyEquivalence) (h : f₀.Homotopic f₁) : f₁.IsWeakHomotopyEquivalence

A map homotopic to a weak homotopy equivalence is a weak homotopy equivalence.

theorem ContinuousMap.IsWeakHomotopyEquivalence.id {X : Type u_1} [TopologicalSpace X] : (ContinuousMap.id X).IsWeakHomotopyEquivalence

The identity map is a weak homotopy equivalence.

theorem ContinuousMap.IsWeakHomotopyEquivalence.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} {g : C(Y, Z)} (hg : g.IsWeakHomotopyEquivalence) (hf : f.IsWeakHomotopyEquivalence) : (g.comp f).IsWeakHomotopyEquivalence

A composite of weak homotopy equivalences is a weak homotopy equivalence.

theorem ContinuousMap.IsWeakHomotopyEquivalence.of_postcomp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} {g : C(Y, Z)} (hg : g.IsWeakHomotopyEquivalence) (hgf : (g.comp f).IsWeakHomotopyEquivalence) : f.IsWeakHomotopyEquivalence

Two out of three, left cancellation. If g and g ∘ f are weak homotopy equivalences, then so is f.

theorem ContinuousMap.IsWeakHomotopyEquivalence.of_precomp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} {g : C(Y, Z)} (hf : f.IsWeakHomotopyEquivalence) (hgf : (g.comp f).IsWeakHomotopyEquivalence) : g.IsWeakHomotopyEquivalence

Two out of three, right cancellation. If f and g ∘ f are weak homotopy equivalences, then so is g. At a point y of Y, the induced map on homotopy groups is compared, by base-point change along a path from a point f x to y and along its image under g, with the induced map at f x, which is bijective by cancellation on the right.

theorem ContinuousMap.IsWeakHomotopyEquivalence.of_retract {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {X' : Type u_4} {Y' : Type u_5} [TopologicalSpace X'] [TopologicalSpace Y'] {g : C(X', Y')} (i : C(X, X')) (r : C(X', X)) (j : C(Y, Y')) (s : C(Y', Y)) (hri : r.comp i = ContinuousMap.id X) (hsj : s.comp j = ContinuousMap.id Y) (hi : g.comp i = j.comp f) (hr : f.comp r = s.comp g) (hg : g.IsWeakHomotopyEquivalence) : f.IsWeakHomotopyEquivalence

Retracts. A retract of a weak homotopy equivalence is a weak homotopy equivalence: if f : X → Y is a retract of g : X' → Y', through i : X → X' and j : Y → Y' with retractions r and s such that g ∘ i = j ∘ f and f ∘ r = s ∘ g, and g is a weak homotopy equivalence, then so is f. On every homotopy group the map induced by f is a retract of the map induced by g, and a retract of a bijection is a bijection.

theorem ContinuousMap.IsWeakHomotopyEquivalence.mapOfEq_bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (hf : f.IsWeakHomotopyEquivalence) {x : X} {y : Y} (hxy : f x = y) : Function.Bijective ⇑(FundamentalGroup.mapOfEq f hxy)

A weak homotopy equivalence induces a bijection of fundamental groups at every base point.

Squares of weak homotopy equivalences

Let g ∘ i = j ∘ f for maps i : X → X' and j : Y → Y', where f : X → Y and g : X' → Y' are weak homotopy equivalences. Then i and j have the same connectivity: each of the following properties holds for i exactly when it holds for j. Every point of the target is joined by a path to a point of the image, and the induced map on a given homotopy group is surjective, or injective, at every base point.

theorem ContinuousMap.IsWeakHomotopyEquivalence.forall_exists_joined_iff_of_comp_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {X' : Type u_4} {Y' : Type u_5} [TopologicalSpace X'] [TopologicalSpace Y'] {g : C(X', Y')} {i : C(X, X')} {j : C(Y, Y')} (hf : f.IsWeakHomotopyEquivalence) (hg : g.IsWeakHomotopyEquivalence) (hi : g.comp i = j.comp f) : (∀ (y' : Y'), ∃ (y : Y), Joined (j y) y') ↔ ∀ (x' : X'), ∃ (x : X), Joined (i x) x'

In a square g ∘ i = j ∘ f whose maps f and g are weak homotopy equivalences, every point of Y' is joined to a point of the image of j exactly when every point of X' is joined to a point of the image of i.

theorem ContinuousMap.IsWeakHomotopyEquivalence.surjective_map_iff_of_comp_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {X' : Type u_4} {Y' : Type u_5} [TopologicalSpace X'] [TopologicalSpace Y'] {g : C(X', Y')} {i : C(X, X')} {j : C(Y, Y')} (hf : f.IsWeakHomotopyEquivalence) (hg : g.IsWeakHomotopyEquivalence) (hi : g.comp i = j.comp f) (N : Type u_6) [Finite N] (x : X) : Function.Surjective (HomotopyGroup.map j ⋯) ↔ Function.Surjective (HomotopyGroup.map i ⋯)

In a square g ∘ i = j ∘ f whose maps f and g are weak homotopy equivalences, the map π_N(Y, f x) → π_N(Y', j (f x)) induced by j is surjective exactly when the map π_N(X, x) → π_N(X', i x) induced by i is.

theorem ContinuousMap.IsWeakHomotopyEquivalence.injective_map_iff_of_comp_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {X' : Type u_4} {Y' : Type u_5} [TopologicalSpace X'] [TopologicalSpace Y'] {g : C(X', Y')} {i : C(X, X')} {j : C(Y, Y')} (hf : f.IsWeakHomotopyEquivalence) (hg : g.IsWeakHomotopyEquivalence) (hi : g.comp i = j.comp f) (N : Type u_6) [Finite N] (x : X) : Function.Injective (HomotopyGroup.map j ⋯) ↔ Function.Injective (HomotopyGroup.map i ⋯)

In a square g ∘ i = j ∘ f whose maps f and g are weak homotopy equivalences, the map π_N(Y, f x) → π_N(Y', j (f x)) induced by j is injective exactly when the map π_N(X, x) → π_N(X', i x) induced by i is.

theorem ContinuousMap.IsWeakHomotopyEquivalence.forall_surjective_map_iff_of_comp_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {X' : Type u_4} {Y' : Type u_5} [TopologicalSpace X'] [TopologicalSpace Y'] {g : C(X', Y')} {i : C(X, X')} {j : C(Y, Y')} (hf : f.IsWeakHomotopyEquivalence) (hg : g.IsWeakHomotopyEquivalence) (hi : g.comp i = j.comp f) (N : Type u_6) [Finite N] : (∀ (y : Y), Function.Surjective (HomotopyGroup.map j ⋯)) ↔ ∀ (x : X), Function.Surjective (HomotopyGroup.map i ⋯)

In a square g ∘ i = j ∘ f whose maps f and g are weak homotopy equivalences, j induces surjections π_N(Y, y) → π_N(Y', j y) at every point y exactly when i induces surjections π_N(X, x) → π_N(X', i x) at every point x.

theorem ContinuousMap.IsWeakHomotopyEquivalence.forall_injective_map_iff_of_comp_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {X' : Type u_4} {Y' : Type u_5} [TopologicalSpace X'] [TopologicalSpace Y'] {g : C(X', Y')} {i : C(X, X')} {j : C(Y, Y')} (hf : f.IsWeakHomotopyEquivalence) (hg : g.IsWeakHomotopyEquivalence) (hi : g.comp i = j.comp f) (N : Type u_6) [Finite N] : (∀ (y : Y), Function.Injective (HomotopyGroup.map j ⋯)) ↔ ∀ (x : X), Function.Injective (HomotopyGroup.map i ⋯)

In a square g ∘ i = j ∘ f whose maps f and g are weak homotopy equivalences, j induces injections π_N(Y, y) → π_N(Y', j y) at every point y exactly when i induces injections π_N(X, x) → π_N(X', i x) at every point x.

theorem ContinuousMap.isWeakHomotopyEquivalence_iff_forall_bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} [PathConnectedSpace X] (x : X) : f.IsWeakHomotopyEquivalence ↔ ∀ (n : ℕ), Function.Bijective (HomotopyGroup.map f ⋯)

On a path-connected space, weak homotopy equivalences can be detected at one point. A map out of a path-connected space is a weak homotopy equivalence exactly when it induces a bijection π_n(X, x) → π_n(Y, f x) for every n at a single base point x. In degree 0 this says that Y is path-connected as well.

theorem ContinuousMap.isWeakHomotopyEquivalence_iff_joined {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} : f.IsWeakHomotopyEquivalence ↔ (∀ (y : Y), ∃ (x : X), Joined (f x) y) ∧ (∀ (a b : X), Joined (f a) (f b) → Joined a b) ∧ ∀ (n : ℕ) (x : X), Function.Bijective (HomotopyGroup.map f ⋯)

Weak homotopy equivalences through path components. A map is a weak homotopy equivalence exactly when it induces a bijection on path components, that is, every point of Y is joined to a point of the image and two points of X are joined when their images are, and a bijection π_(n+1)(X, x) → π_(n+1)(Y, f x) for every n and every point x.

theorem ContinuousMap.HomotopyEquiv.isWeakHomotopyEquivalence {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) : e.toFun.IsWeakHomotopyEquivalence

A homotopy equivalence is a weak homotopy equivalence.

theorem ContinuousMap.isWeakHomotopyEquivalence_of_contractibleSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [ContractibleSpace X] [ContractibleSpace Y] (f : C(X, Y)) : f.IsWeakHomotopyEquivalence

A map between contractible spaces is a weak homotopy equivalence. It is homotopic to a homotopy equivalence, since any two maps into a contractible space are homotopic.