Base-point change for relative homotopy groups #
Let X = (X, A, a) be a based pair and let γ be a path in A from a to a point b, so that
⟨X.pair, b⟩ is the based pair (X, A, b). This file constructs the base-point-change map
TauCeti.RelHomotopyGroup.transport γ : π_{n+1}(X, A, a) → π_{n+1}(X, A, b),
proves that it is a bijection with inverse the transport along the reversed path, and, in
degrees at least two, a group isomorphism TauCeti.RelHomotopyGroup.mulEquivOfPath γ. It is
compatible with the maps of the long exact sequence of the pair: with the boundary map to
π_n(A) and the absolute base-point change in A, and with the map from π_{n+1}(X) and the
absolute base-point change in X. It is natural in morphisms of based pairs.
A homotopy along γ (TauCeti.RelGenLoop.HomotopyAlong) from a relative cube p at a to a
relative cube q at b is a homotopy whose stage at time t sends the face {0} × I^N into A,
and the face {1} × I^N and the sides I × ∂I^N to γ t. The transport is characterised by
these homotopies: whenever there is one from p to q, the transport of the class of p is the
class of q (TauCeti.RelGenLoop.HomotopyAlong.transport_mk). All the laws are read off from
this characterisation, by composing, reversing or restricting homotopies along paths.
Construction #
- Existence. Every relative cube
padmits a homotopy alongγ(TauCeti.RelGenLoop.collarHomotopyAlong), ending at the cubeTauCeti.RelGenLoop.transport γ p. Doublepalong its distinguished coordinate to the absolute cube(u, z) ↦ p (|2u - 1|, z)ofI^(Option N), which is constant on the boundary, and apply the collar homotopyTauCeti.GenLoop.collarHomotopyof absolute base-point change. On the halfu ≥ 1 / 2this is a homotopy alongγ: the collar shrinks towards the centre of the cube, which lies on the hyperplaneu = 1 / 2corresponding to the face{0} × I^N, so that face only sees values ofpon it and values ofγ, all inA. - Canonicity. Relative cubes at
bare generalized loops in the spaceP_bof paths fromAtob(TauCeti.RelGenLoop.pathSpaceHomeo). Following each path ofP_abyγis a mapP_a → P_b, and following the paths of a homotopy alongγat timetby the tailγ.subpath t 1turns it into an absolute homotopy along a fixed path inP_b. By canonicity of absolute transport (TauCeti.GenLoop.HomotopyAlong.homotopic_transport) its end is determined up to homotopy by its start. Hence the transport, defined as the composite of these maps on homotopy groups, sends the class ofpto the class ofq.
Main declarations #
TauCeti.RelGenLoop.HomotopyAlong: homotopies of relative cubes along a path in the subspace, which are homotopies through maps of pairs (TauCeti.RelGenLoop.HomotopyAlong.homotopicWith).TauCeti.RelGenLoop.transport,TauCeti.RelGenLoop.collarHomotopyAlong: a relative cube transported along a path, with a homotopy along the path.TauCeti.RelGenLoop.HomotopyAlong.homotopic_transport: canonicity, any homotopy alongγstarting atpends at a cube homotopic toTauCeti.RelGenLoop.transport γ p.TauCeti.RelGenLoop.homotopic_transport_of_path_homotopic: transport along homotopic paths gives homotopic cubes.TauCeti.RelHomotopyGroup.transport: base-point change on relative homotopy sets, withtransport_refl,transport_trans,transport_congr,transport_symm_transportandtransport_default.TauCeti.RelHomotopyGroup.equivOfPath,TauCeti.RelHomotopyGroup.mulEquivOfPath: a path fromatobinAinduces a bijectionπ_{n+1}(X, A, a) ≃ π_{n+1}(X, A, b), which is a group isomorphism whenn ≥ 1. SoTauCeti.RelHomotopyGroup.subsingleton_iff_of_joined: triviality of the relative homotopy set does not depend on the base point in a path component.TauCeti.RelHomotopyGroup.boundary_transport,TauCeti.RelHomotopyGroup.transport_ofHomotopyGroup,TauCeti.RelHomotopyGroup.map_transport: compatibility with the long exact sequence and naturality.
References #
- A. Hatcher, Algebraic Topology,
Section 4.1, the change of base point for relative homotopy groups along a path in
A.
Homotopies along a path in the subspace #
A homotopy from a relative cube p of the based pair X = (X, A, a) to a relative cube q of
(X, A, b), along a path γ in A from a to b: at time t it sends the face {0} × I^N into
A, and the face {1} × I^N and the sides I × ∂I^N to γ t.
- toFun : ↑unitInterval × ↑unitInterval × (N → ↑unitInterval) → ↑TopPair.fst
- continuous_toFun : Continuous self.toFun
- apply_zero_mem_range (t : ↑unitInterval) (z : N → ↑unitInterval) : self.toHomotopy (t, 0, z) ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)
at every time the face
{0} × I^Ngoes into the subspace - apply_eq_path (t s : ↑unitInterval) (z : N → ↑unitInterval) : s = 1 ∨ z ∈ Cube.boundary N → self.toHomotopy (t, s, z) = (CategoryTheory.ConcreteCategory.hom TopPair.map) (γ t)
at every time the rest of the boundary goes to the moving basepoint
Instances For
The constant homotopy is a homotopy along the constant path.
Instances For
Reversing a homotopy along γ in time gives a homotopy along the reversed path.
Instances For
Concatenating two homotopies along paths, in the time direction, gives a homotopy along the concatenated path.
Instances For
A morphism of based pairs f : X ⟶ Y carries a homotopy along γ to a homotopy along the
image of γ, which starts at the basepoint of Y.
Instances For
Restricting a homotopy along γ to the face {0} × I^N gives a homotopy along γ of
generalized loops in the subspace.
Instances For
An absolute homotopy along the image of γ in X, of cubes I^(Option N), is a homotopy
along γ of the corresponding relative cubes.
Instances For
The constant cube at γ t is a homotopy along γ between the constant relative cubes.
Instances For
A homotopy along a path in the subspace is a homotopy through maps of pairs
(I × I^N, ∂(I × I^N)) → (X, A).
Existence: the doubled collar #
A relative cube transported along a path in the subspace: the end of the collar homotopy of its doubling, restricted to the upper half of the cube.
Instances For
The collar homotopy of the doubling is a homotopy along γ from p to its transport.
Instances For
Transport along homotopic paths gives homotopic relative cubes. Collaring the doubled cube along the paths of a homotopy between the two paths deforms one transported cube into the other through relative cubes.
Canonicity, through the path space #
Base-point change for relative homotopy sets. The map
π_{n+1}(X, A, a) → π_{n+1}(X, A, b) induced by a path γ in A from a to b. A homotopy
along γ from a relative cube p to q carries the class of p to the class of q
(TauCeti.RelGenLoop.HomotopyAlong.transport_mk).
Instances For
The characterisation of relative base-point change. If there is a homotopy along γ from
p to q, then transport along γ sends the class of p to the class of q.
Canonicity of the transported relative cube. A homotopy along γ starting at p ends at
a relative cube homotopic to transport γ p.
Transport of the class of a relative cube is the class of its transport.
Transport along a constant path is the identity.
Transport along a concatenation of paths is the composite of the transports.
Homotopic paths induce the same transport.
Transport along the reversed path undoes transport.
Transport along a path undoes transport along the reversed path.
Transport preserves the distinguished point.
Base-point change for relative homotopy sets. A path from a to b in the subspace
induces a bijection π_{n+1}(X, A, a) ≃ π_{n+1}(X, A, b).
Instances For
The equivalence for a constant path is the identity.
The equivalence for a concatenated path is the composite equivalence.
Reversing the path gives the inverse equivalence.
Homotopic paths induce the same equivalence.
The relative homotopy set at a is trivial if and only if it is trivial at any point b of
the subspace joined to a by a path in the subspace.
Transport commutes with the boundary map: restricted to the face in A, it is base-point
change of homotopy groups of A.
Transport commutes with the map π_{n+1}(X, a) → π_{n+1}(X, A, a): on absolute classes it is
base-point change of homotopy groups of X along the image of γ.
Transport is natural in morphisms of based pairs f : X ⟶ Y, along the image of the path,
which starts at the basepoint of Y.
In degrees at least two, transport is a homomorphism.
Base-point change for relative homotopy groups. A path from a to b in the subspace
induces a group isomorphism π_{n+1}(X, A, a) ≃* π_{n+1}(X, A, b) for n ≥ 1.
Instances For
The group isomorphism for a constant path is the identity.
The group isomorphism for a concatenated path is the composite isomorphism.
Reversing the path gives the inverse group isomorphism.
Homotopic paths induce the same group isomorphism.