Homotopy groups are invariant under homotopy equivalence

Postcomposition with a continuous map induces a map on homotopy groups, and maps homotopic relative to the base point induce the same one. A free homotopy H from f to g moves the base point along its trace H.evalAt x, and the two induced maps then differ exactly by base-point change. This is immediate from the machinery already in place: dragging a generalized loop p through H is a homotopy along the trace, in the sense of TauCeti.GenLoop.HomotopyAlong, from f ∘ p to g ∘ p, and such a homotopy is canonical by TauCeti.GenLoop.HomotopyAlong.homotopic_transport.

The trace formula takes the base points of the two induced maps as equations, as HomotopyGroup.map does, and the trace is recast along them with Path.cast. This is what lets a round trip g ∘ f ≃ id be stated at the base points g (f x) and x themselves, rather than at (g.comp f) x and (ContinuousMap.id X) x.

Applied to a homotopy equivalence e : X ≃ₕ Y, this makes each round trip of e bijective on homotopy groups after correcting the base point. Both round trips are needed: a homotopy inverse recovers the identity only up to a free homotopy, so one composite alone gives injectivity of the map induced by e.toFun and surjectivity of the map induced by e.invFun, and the other composite is what upgrades the latter to a bijection. The inverse of the resulting bijection is the map induced by e.invFun, corrected by base-point change along the trace of the round trip.

The statements about the induced map alone need no finiteness of the index type beyond [Finite N]; the statements that mention transport, which uses the collar construction, ask for the [Fintype N] that the cube radius uses.

Main declarations

• TauCeti.GenLoop.homotopyAlongMap: dragging a generalized loop through a homotopy is a homotopy along the trace of that homotopy at the base point.
• TauCeti.homotopyGroupTransport_map: freely homotopic maps induce the same map on homotopy groups, up to transport along the trace of the homotopy.
• TauCeti.homotopyGroupTransport_map_map: the case of a round trip g ∘ f ≃ id.
• HomotopyGroup.map_bijective_of_homotopyEquiv: a homotopy equivalence induces a bijection on homotopy groups.
• HomotopyGroup.equivOfHomotopyEquiv, HomotopyGroup.mulEquivOfHomotopyEquiv: that bijection, as an equivalence and, in positive dimensions, as a group isomorphism, with their identity and composition laws.

References

That a homotopy equivalence induces isomorphisms on all homotopy groups is Proposition 4.21 of [hatcher02]; the trace formula for a free homotopy is the discussion preceding it in Section 4.1.

def TauCeti.GenLoop.homotopyAlongMap {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (H : f.Homotopy g) {x : X} {y₀ y₁ : Y} (hf : f x = y₀) (hg : g x = y₁) (p : ↑(GenLoop N X x)) : HomotopyAlong ((H.evalAt x).cast ⋯ ⋯) (GenLoop.map f hf p) (GenLoop.map g hg p)

Dragging a generalized loop p based at x through a homotopy H from f to g is a homotopy from f ∘ p to g ∘ p along the trace of H at x: on the cube boundary p is constant at x, so there the dragged loop traces H.evalAt x.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.GenLoop.homotopic_map_transport {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Fintype N] {f g : C(X, Y)} (H : f.Homotopy g) {x : X} {y₀ y₁ : Y} (hf : f x = y₀) (hg : g x = y₁) (p : ↑(GenLoop N X x)) : GenLoop.Homotopic (GenLoop.map g hg p) (transport ((H.evalAt x).cast ⋯ ⋯) (GenLoop.map f hf p))

Freely homotopic maps agree on generalized loops, up to transport along the trace of the homotopy at the base point.

theorem TauCeti.homotopyGroupTransport_map {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Fintype N] {f g : C(X, Y)} (H : f.Homotopy g) {x : X} {y₀ y₁ : Y} (hf : f x = y₀) (hg : g x = y₁) (a : HomotopyGroup N X x) : homotopyGroupTransport ((H.evalAt x).cast ⋯ ⋯) (HomotopyGroup.map f hf a) = HomotopyGroup.map g hg a

Freely homotopic maps induce the same map on homotopy groups, after transporting along the trace of the homotopy at the base point. For a homotopy that fixes the base point the trace is constant, and this is the pointed statement HomotopyGroup.map_eq_of_homotopicRel.

theorem TauCeti.homotopyGroupTransport_map_map {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Fintype N] {f : C(X, Y)} {g : C(Y, X)} (H : (g.comp f).Homotopy (ContinuousMap.id X)) (x : X) (a : HomotopyGroup N X x) : homotopyGroupTransport ((H.evalAt x).cast ⋯ ⋯) (HomotopyGroup.map g ⋯ (HomotopyGroup.map f ⋯ a)) = a

If g ∘ f is freely homotopic to the identity, then transport along the trace of the homotopy undoes the composite of the maps that f and g induce on homotopy groups.

theorem HomotopyGroup.map_comp_map_bijective_of_homotopy_id {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Finite N] {f : C(X, Y)} {g : C(Y, X)} (H : (g.comp f).Homotopy (ContinuousMap.id X)) (x : X) : Function.Bijective (map g ⋯ ∘ map f ⋯)

If g ∘ f is freely homotopic to the identity, the composite of the maps that f and g induce on homotopy groups is a bijection: it is base-point change along the trace of the homotopy, reversed.

theorem HomotopyGroup.map_bijective_of_homotopyEquiv {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Finite N] (e : ContinuousMap.HomotopyEquiv X Y) (x : X) : Function.Bijective (map e.toFun ⋯)

A homotopy equivalence induces a bijection on homotopy groups.

noncomputable def HomotopyGroup.equivOfHomotopyEquiv {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Finite N] (e : ContinuousMap.HomotopyEquiv X Y) (x : X) : HomotopyGroup N X x ≃ HomotopyGroup N Y (e.toFun x)

The bijection on homotopy groups induced by a homotopy equivalence.

Equations

• HomotopyGroup.equivOfHomotopyEquiv e x = Equiv.ofBijective (HomotopyGroup.map e.toFun ⋯) ⋯

@[simp]

theorem HomotopyGroup.equivOfHomotopyEquiv_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Finite N] (e : ContinuousMap.HomotopyEquiv X Y) (x : X) (a : HomotopyGroup N X x) : (equivOfHomotopyEquiv e x) a = map e.toFun ⋯ a

The bijection induced by a homotopy equivalence acts as the map induced by e.toFun.

noncomputable def HomotopyGroup.mulEquivOfHomotopyEquiv {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Finite N] [Nonempty N] [DecidableEq N] (e : ContinuousMap.HomotopyEquiv X Y) (x : X) : HomotopyGroup N X x ≃* HomotopyGroup N Y (e.toFun x)

A homotopy equivalence induces a group isomorphism on homotopy groups. In positive dimensions the bijection induced by a homotopy equivalence is a group isomorphism, being induced by a continuous map.

Equations

• HomotopyGroup.mulEquivOfHomotopyEquiv e x = MulEquiv.ofBijective (HomotopyGroup.mapHom e.toFun ⋯) ⋯

@[simp]

theorem HomotopyGroup.mulEquivOfHomotopyEquiv_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Finite N] [Nonempty N] [DecidableEq N] (e : ContinuousMap.HomotopyEquiv X Y) (x : X) (a : HomotopyGroup N X x) : (mulEquivOfHomotopyEquiv e x) a = map e.toFun ⋯ a

The group isomorphism induced by a homotopy equivalence acts as the map induced by e.toFun.

@[simp]

theorem HomotopyGroup.equivOfHomotopyEquiv_refl {N : Type u_1} {X : Type u_2} [TopologicalSpace X] [Finite N] (x : X) : equivOfHomotopyEquiv (ContinuousMap.HomotopyEquiv.refl X) x = Equiv.refl (HomotopyGroup N X x)

The identity homotopy equivalence induces the identity on homotopy groups.

@[simp]

theorem HomotopyGroup.equivOfHomotopyEquiv_trans {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Finite N] {Z : Type u_4} [TopologicalSpace Z] (e : ContinuousMap.HomotopyEquiv X Y) (e' : ContinuousMap.HomotopyEquiv Y Z) (x : X) : equivOfHomotopyEquiv (e.trans e') x = (equivOfHomotopyEquiv e x).trans (equivOfHomotopyEquiv e' (e.toFun x))

The bijection induced by a composite of homotopy equivalences is the composite of the induced bijections.

@[simp]

theorem HomotopyGroup.mulEquivOfHomotopyEquiv_refl {N : Type u_1} {X : Type u_2} [TopologicalSpace X] [Finite N] [Nonempty N] [DecidableEq N] (x : X) : mulEquivOfHomotopyEquiv (ContinuousMap.HomotopyEquiv.refl X) x = MulEquiv.refl (HomotopyGroup N X x)

The identity homotopy equivalence induces the identity isomorphism on homotopy groups.

@[simp]

theorem HomotopyGroup.mulEquivOfHomotopyEquiv_trans {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Finite N] [Nonempty N] [DecidableEq N] {Z : Type u_4} [TopologicalSpace Z] (e : ContinuousMap.HomotopyEquiv X Y) (e' : ContinuousMap.HomotopyEquiv Y Z) (x : X) : mulEquivOfHomotopyEquiv (e.trans e') x = (mulEquivOfHomotopyEquiv e x).trans (mulEquivOfHomotopyEquiv e' (e.toFun x))

The isomorphism induced by a composite of homotopy equivalences is the composite of the induced isomorphisms.

@[simp]

theorem HomotopyGroup.equivOfHomotopyEquiv_symm_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Fintype N] (e : ContinuousMap.HomotopyEquiv X Y) (x : X) (b : HomotopyGroup N Y (e.toFun x)) : (equivOfHomotopyEquiv e x).symm b = TauCeti.homotopyGroupTransport (((Nonempty.some ⋯).evalAt x).cast ⋯ ⋯) (map e.invFun ⋯ b)

The inverse of the bijection induced by a homotopy equivalence e is the map induced by e.invFun, followed by base-point change along the trace of the round trip e.invFun ∘ e.toFun ≃ id.

@[simp]

theorem HomotopyGroup.mulEquivOfHomotopyEquiv_symm_apply {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Fintype N] [Nonempty N] [DecidableEq N] (e : ContinuousMap.HomotopyEquiv X Y) (x : X) (b : HomotopyGroup N Y (e.toFun x)) : (mulEquivOfHomotopyEquiv e x).symm b = TauCeti.homotopyGroupTransport (((Nonempty.some ⋯).evalAt x).cast ⋯ ⋯) (map e.invFun ⋯ b)

The inverse of the group isomorphism induced by a homotopy equivalence e is the map induced by e.invFun, followed by base-point change along the trace of the round trip e.invFun ∘ e.toFun ≃ id.

theorem TauCeti.nonempty_homotopyGroupMulEquiv_of_homotopyEquiv {N : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Finite N] [Nonempty N] [DecidableEq N] [PathConnectedSpace X] (e : ContinuousMap.HomotopyEquiv X Y) (x : X) (y : Y) : Nonempty (HomotopyGroup N X x ≃* HomotopyGroup N Y y)

Over a path connected space, homotopy equivalence identifies the homotopy groups in a fixed positive dimension at any pair of base points, by composing with base-point change.