Base-point change for higher homotopy groups

A path γ from x to y induces an isomorphism π_n(X, x) ≃* π_n(X, y). This file proves it, in the form TauCeti.homotopyGroupMulEquivOfPath : HomotopyGroup N X x ≃* HomotopyGroup N X y for a finite nonempty index type N, together with its functoriality: transport along a constant path is the identity, transport along a concatenation is the composite, and transport depends only on the homotopy class of the path.

The construction of the transported generalized loop and the key canonicity statement — a homotopy of generalized loops whose boundary traces γ ends at the transported loop, up to homotopy relative to the cube boundary — are in TauCeti/Topology/Homotopy/HomotopyGroup/Collar.lean. Canonicity is what makes all four properties routine: each is obtained by exhibiting some homotopy along the relevant path and then invoking TauCeti.GenLoop.HomotopyAlong.homotopic_transport. The homotopies are:

• concatenating two collar homotopies in the time direction, for the concatenation law;
• the constant homotopy, for the constant path;
• concatenating two collar homotopies in the i-th cube direction, for multiplicativity.

Two statements are instead proved by deforming the outer half of the collar directly, using the file-local transportFamily, the collar attached to a continuous family: that transport respects homotopy of generalized loops, which is what makes it descend to homotopy groups, and that it only depends on the homotopy class of the path.

The group structure enters only through Mathlib's HomotopyGroup.mul_spec, which computes a product as the class of a concatenation GenLoop.transAt i in any cube direction i.

Main declarations

• TauCeti.homotopyGroupTransport: transport of homotopy classes along a path, with TauCeti.homotopyGroupTransport_refl, TauCeti.homotopyGroupTransport_trans and TauCeti.homotopyGroupTransport_congr.
• TauCeti.homotopyGroupEquivOfPath: transport is a bijection, with inverse the transport along the reversed path, with TauCeti.homotopyGroupEquivOfPath_apply, TauCeti.homotopyGroupEquivOfPath_symm_apply and the same four functoriality laws TauCeti.homotopyGroupEquivOfPath_refl, TauCeti.homotopyGroupEquivOfPath_trans, TauCeti.homotopyGroupEquivOfPath_congr and TauCeti.homotopyGroupEquivOfPath_symm.
• TauCeti.homotopyGroupMulEquivOfPath: a path from x to y induces a group isomorphism HomotopyGroup N X x ≃* HomotopyGroup N X y.
• TauCeti.nonempty_homotopyGroupMulEquiv: on a path-connected space, all the homotopy groups in a fixed dimension are isomorphic.

References

This closes the base-point-change part of the higher-homotopy API requested in TauCetiRoadmap/UniversalCovers/README.md, Stage 3, item 9. It is the higher-dimensional analogue of Mathlib's FundamentalGroup.fundamentalGroupMulEquivOfPath; see Hatcher, Algebraic Topology, Section 4.1.

The collar of a continuous family

Transport respects homotopy

theorem TauCeti.GenLoop.homotopic_transport_of_homotopic {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) {f f' : ↑(GenLoop N X x)} (h : GenLoop.Homotopic f f') : GenLoop.Homotopic (transport γ f) (transport γ f')

Transport along a fixed path sends homotopic generalized loops to homotopic generalized loops.

theorem TauCeti.GenLoop.homotopic_transport_of_path_homotopic {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} {γ δ : Path x y} (h : γ.Homotopic δ) (f : ↑(GenLoop N X x)) : GenLoop.Homotopic (transport γ f) (transport δ f)

Transport along homotopic paths gives homotopic generalized loops.

Functoriality of transport

def TauCeti.GenLoop.HomotopyAlong.refl {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x : X} (f : ↑(GenLoop N X x)) : HomotopyAlong (Path.refl x) f f

The constant homotopy is a homotopy along the constant path.

Equations

• TauCeti.GenLoop.HomotopyAlong.refl f = TauCeti.GenLoop.HomotopyAlong.ofHomotopyRel (ContinuousMap.HomotopyRel.refl (↑f) (Cube.boundary N))

theorem TauCeti.GenLoop.homotopic_transport_refl {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} (f : ↑(GenLoop N X x)) : GenLoop.Homotopic f (transport (Path.refl x) f)

Transport along a constant path does nothing, up to homotopy.

noncomputable def TauCeti.GenLoop.HomotopyAlong.trans {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x y w : X} {γ : Path x y} {δ : Path y w} {f : ↑(GenLoop N X x)} {g : ↑(GenLoop N X y)} {k : ↑(GenLoop N X w)} (h₁ : HomotopyAlong γ f g) (h₂ : HomotopyAlong δ g k) : HomotopyAlong (γ.trans δ) f k

Concatenating two homotopies along paths, in the time direction, gives a homotopy along the concatenated path.

Equations

• h₁.trans h₂ = { toHomotopy := h₁.trans h₂.toHomotopy, map_boundary := ⋯ }

theorem TauCeti.GenLoop.homotopic_transport_trans {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y w : X} (γ : Path x y) (δ : Path y w) (f : ↑(GenLoop N X x)) : GenLoop.Homotopic (transport δ (transport γ f)) (transport (γ.trans δ) f)

Transport along a concatenation is the composite of the transports.

theorem TauCeti.GenLoop.homotopic_transport_symm_transport {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X x)) : GenLoop.Homotopic (transport γ.symm (transport γ f)) f

Transport along the reversed path undoes transport, up to homotopy.

theorem TauCeti.GenLoop.homotopic_transport_transport_symm {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X y)) : GenLoop.Homotopic (transport γ (transport γ.symm f)) f

Transport undoes transport along the reversed path, up to homotopy.

Transport and concatenation of generalized loops

noncomputable def TauCeti.GenLoop.HomotopyAlong.transAt {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x y : X} [DecidableEq N] (i : N) {γ : Path x y} {f f' : ↑(GenLoop N X x)} {g g' : ↑(GenLoop N X y)} (h₁ : HomotopyAlong γ f g) (h₂ : HomotopyAlong γ f' g') : HomotopyAlong γ (GenLoop.transAt i f f') (GenLoop.transAt i g g')

Concatenating two homotopies along the same path, in the i-th cube direction, gives a homotopy along that path between the concatenated generalized loops.

Equations

• TauCeti.GenLoop.HomotopyAlong.transAt i h₁ h₂ = { toHomotopy := TauCeti.GenLoop.transAtHomotopy✝ i h₁ h₂, map_boundary := ⋯ }

theorem TauCeti.GenLoop.homotopic_transAt_transport {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} [DecidableEq N] (i : N) (γ : Path x y) (f f' : ↑(GenLoop N X x)) : GenLoop.Homotopic (GenLoop.transAt i (transport γ f) (transport γ f')) (transport γ (GenLoop.transAt i f f'))

Transport commutes with concatenation of generalized loops, up to homotopy.

Naturality of transport

@[simp]

theorem TauCeti.GenLoop.map_transport {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} {Y : Type u_3} [TopologicalSpace Y] (F : C(X, Y)) (γ : Path x y) (f : ↑(GenLoop N X x)) : GenLoop.map F ⋯ (transport γ f) = transport (γ.map ⋯) (GenLoop.map F ⋯ f)

Postcomposition with a continuous map commutes with transport, along the image path.

Base-point change on homotopy groups

noncomputable def TauCeti.homotopyGroupTransport {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) : HomotopyGroup N X x → HomotopyGroup N X y

Transport of homotopy classes along a path.

Equations

• TauCeti.homotopyGroupTransport γ = Quotient.map (TauCeti.GenLoop.transport γ) ⋯

@[simp]

theorem TauCeti.homotopyGroupTransport_mk {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X x)) : homotopyGroupTransport γ ⟦f⟧ = ⟦GenLoop.transport γ f⟧

@[simp]

theorem TauCeti.homotopyGroupTransport_refl {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} : homotopyGroupTransport (Path.refl x) = id

Transport along the constant path is the identity on homotopy groups.

@[simp]

theorem TauCeti.homotopyGroupTransport_trans {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y w : X} (γ : Path x y) (δ : Path y w) : homotopyGroupTransport (γ.trans δ) = homotopyGroupTransport δ ∘ homotopyGroupTransport γ

Transport along a concatenation of paths is the composite of the two transports.

theorem TauCeti.homotopyGroupTransport_congr {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} {γ δ : Path x y} (h : γ.Homotopic δ) : homotopyGroupTransport γ = homotopyGroupTransport δ

Homotopic paths induce the same transport on homotopy groups.

noncomputable def TauCeti.homotopyGroupEquivOfPath {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) : HomotopyGroup N X x ≃ HomotopyGroup N X y

Transport along a path is a bijection on homotopy classes, with inverse the transport along the reversed path.

Equations

• TauCeti.homotopyGroupEquivOfPath γ = { toFun := TauCeti.homotopyGroupTransport γ, invFun := TauCeti.homotopyGroupTransport γ.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.homotopyGroupEquivOfPath_mk {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X x)) : (homotopyGroupEquivOfPath γ) ⟦f⟧ = ⟦GenLoop.transport γ f⟧

@[simp]

theorem TauCeti.homotopyGroupEquivOfPath_apply {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (a : HomotopyGroup N X x) : (homotopyGroupEquivOfPath γ) a = homotopyGroupTransport γ a

Base-point change, as an equivalence, acts by transport.

@[simp]

theorem TauCeti.homotopyGroupEquivOfPath_symm_apply {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (a : HomotopyGroup N X y) : (homotopyGroupEquivOfPath γ).symm a = homotopyGroupTransport γ.symm a

The inverse base-point-change equivalence acts by transport along the reversed path.

@[simp]

theorem TauCeti.homotopyGroupEquivOfPath_symm_mk {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑(GenLoop N X y)) : (homotopyGroupEquivOfPath γ).symm ⟦f⟧ = ⟦GenLoop.transport γ.symm f⟧

@[simp]

theorem TauCeti.homotopyGroupEquivOfPath_refl {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} : homotopyGroupEquivOfPath (Path.refl x) = Equiv.refl (HomotopyGroup N X x)

The equivalence for a constant path is the identity.

@[simp]

theorem TauCeti.homotopyGroupEquivOfPath_trans {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y w : X} (γ : Path x y) (δ : Path y w) : homotopyGroupEquivOfPath (γ.trans δ) = (homotopyGroupEquivOfPath γ).trans (homotopyGroupEquivOfPath δ)

The equivalence for a concatenated path is the composite equivalence.

theorem TauCeti.homotopyGroupEquivOfPath_congr {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} {γ δ : Path x y} (h : γ.Homotopic δ) : homotopyGroupEquivOfPath γ = homotopyGroupEquivOfPath δ

Homotopic paths induce the same base-point-change equivalence.

theorem TauCeti.homotopyGroupEquivOfPath_symm {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) : (homotopyGroupEquivOfPath γ).symm = homotopyGroupEquivOfPath γ.symm

Reversing the path gives the inverse equivalence.

noncomputable def TauCeti.homotopyGroupMulEquivOfPath {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} [Nonempty N] [DecidableEq N] (γ : Path x y) : HomotopyGroup N X x ≃* HomotopyGroup N X y

Base-point change for higher homotopy groups. A path from x to y induces a group isomorphism between the homotopy groups based at x and at y.

Equations

• TauCeti.homotopyGroupMulEquivOfPath γ = { toEquiv := TauCeti.homotopyGroupEquivOfPath γ, map_mul' := ⋯ }

@[simp]

theorem TauCeti.homotopyGroupMulEquivOfPath_apply {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} [Nonempty N] [DecidableEq N] (γ : Path x y) (a : HomotopyGroup N X x) : (homotopyGroupMulEquivOfPath γ) a = homotopyGroupTransport γ a

The multiplicative base-point-change equivalence acts by transport.

@[simp]

theorem TauCeti.homotopyGroupMulEquivOfPath_symm_apply {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} [Nonempty N] [DecidableEq N] (γ : Path x y) (a : HomotopyGroup N X y) : (homotopyGroupMulEquivOfPath γ).symm a = homotopyGroupTransport γ.symm a

The inverse multiplicative base-point-change equivalence acts by transport along the reversed path.

@[simp]

theorem TauCeti.homotopyGroupMulEquivOfPath_refl {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x : X} [Nonempty N] [DecidableEq N] : homotopyGroupMulEquivOfPath (Path.refl x) = MulEquiv.refl (HomotopyGroup N X x)

The multiplicative equivalence for a constant path is the identity.

@[simp]

theorem TauCeti.homotopyGroupMulEquivOfPath_trans {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} [Nonempty N] [DecidableEq N] {w : X} (γ : Path x y) (δ : Path y w) : homotopyGroupMulEquivOfPath (γ.trans δ) = (homotopyGroupMulEquivOfPath γ).trans (homotopyGroupMulEquivOfPath δ)

The multiplicative equivalence for a concatenated path is the composite equivalence.

theorem TauCeti.homotopyGroupMulEquivOfPath_congr {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} [Nonempty N] [DecidableEq N] {γ δ : Path x y} (h : γ.Homotopic δ) : homotopyGroupMulEquivOfPath γ = homotopyGroupMulEquivOfPath δ

Homotopic paths induce the same multiplicative base-point-change equivalence.

theorem TauCeti.homotopyGroupMulEquivOfPath_symm {N : Type u_1} [Fintype N] {X : Type u_2} [TopologicalSpace X] {x y : X} [Nonempty N] [DecidableEq N] (γ : Path x y) : (homotopyGroupMulEquivOfPath γ).symm = homotopyGroupMulEquivOfPath γ.symm

Reversing the path gives the inverse multiplicative equivalence.

theorem TauCeti.nonempty_homotopyGroupMulEquiv {N : Type u_1} {X : Type u_2} [TopologicalSpace X] {x y : X} [Finite N] [Nonempty N] [DecidableEq N] [PathConnectedSpace X] : Nonempty (HomotopyGroup N X x ≃* HomotopyGroup N X y)

On a path-connected space the homotopy groups in a fixed dimension at any two base points are isomorphic.