The group structure on relative homotopy groups #
Let X = (X, A, a₀) be a based pair and let n be the cardinality of the index type N. This
file makes the relative homotopy set π_{n+1}(X, A, a₀) = TauCeti.RelHomotopyGroup N X a group
when N is nonempty, that is in degrees at least two, and a commutative group when N is
nontrivial, that is in degrees at least three. It then proves that the induced maps, the boundary
map π_{n+1}(X, A, a₀) → π_n(A, a₀) and the map π_{n+1}(X, a₀) → π_{n+1}(X, A, a₀) of the long
exact sequence are homomorphisms. For N empty, π_1(X, A, a₀) remains a pointed set, and
π_2(X, A, a₀) receives no commutative structure; it is commutative when π_1(A, a₀) is trivial
(TauCeti.RelHomotopyGroup.mul_comm_of_subsingleton).
The group structure is transported from Mathlib's HomotopyGroup. Let P be the space
TauCeti.BasedTopPair.pathSpace X of paths in X from a point of A to a₀, with the
compact-open topology, pointed by the constant path c at a₀. Currying a relative cube
p : I × I^N → X in its distinguished first coordinate gives the generalized loop
t ↦ (s ↦ p (s, t)) in P, and this is a homeomorphism
TauCeti.RelGenLoop.pathSpaceHomeo : RelGenLoop N X ≃ₜ Ω^ N P c. Homotopy through relative cubes
is path connectedness in the space of relative cubes (TauCeti.RelGenLoop.homotopic_iff_joined),
and homotopy of generalized loops is path connectedness in Ω^ N P c
(GenLoop.homotopic_iff_joined), so the homeomorphism descends to a bijection
π_{n+1}(X, A, a₀) ≃ π_n(P, c). The group axioms, the independence of the direction of
concatenation and the Eckmann–Hilton argument are therefore inherited from Mathlib.
Concretely, the product of two classes is the class of the concatenation of representatives in
any direction i : N of the cube I^N (TauCeti.RelHomotopyGroup.mul_spec), never in the
distinguished direction, and in the order of Mathlib's HomotopyGroup.mul_spec.
Main declarations #
TauCeti.BasedTopPair.pathSpace: the space of paths fromAtoa₀.TauCeti.RelGenLoop.pathSpaceHomeo: relative cubes are generalized loops in the path space.TauCeti.RelGenLoop.transAt,TauCeti.RelGenLoop.symmAt: concatenation and reversal of relative cubes along a direction ofI^N, which areTauCeti.cubeTransAtandTauCeti.cubeSymmAton the underlying maps (TauCeti.RelGenLoop.coe_transAt,TauCeti.RelGenLoop.coe_symmAt).TauCeti.RelHomotopyGroup.pathSpaceEquiv,TauCeti.RelHomotopyGroup.pathSpaceMulEquiv:π_{n+1}(X, A, a₀) ≅ π_n(P, c).TauCeti.RelHomotopyGroup.group,TauCeti.RelHomotopyGroup.commGroup: the group structures, characterised byTauCeti.RelHomotopyGroup.one_def,TauCeti.RelHomotopyGroup.mul_specandTauCeti.RelHomotopyGroup.inv_spec.TauCeti.RelHomotopyGroup.mapHom,TauCeti.RelHomotopyGroup.boundaryHom,TauCeti.RelHomotopyGroup.ofHomotopyGroupHom: the maps of the long exact sequence as homomorphisms.TauCeti.RelHomotopyGroup.mul_comm_of_subsingleton:π_{n+1}(X, A, a₀)is commutative whenπ_n(A, a₀)is trivial; in particularπ_2(X, A, a₀)is commutative whenAis simply connected.
References #
- A. Hatcher, Algebraic Topology, Section 4.1, for relative homotopy groups and their group structure, and Section 4.3, where the space of paths from the subspace to the basepoint appears as the homotopy fibre of the inclusion.
The space of paths in the based pair X = (X, A, a₀) that start in A and end at a₀, as a
subspace of C(I, X) with the compact-open topology. Its homotopy groups at the constant path are
the relative homotopy groups of X, shifted down by one degree.
Instances For
The constant path at a₀, the basepoint of the path space.
Instances For
Currying a relative cube p : I × I^N → X in its distinguished first coordinate identifies it
with the generalized loop t ↦ (s ↦ p (s, t)) in the space of paths from A to a₀.
Instances For
Homotopy through relative cubes is path connectedness in the space of relative cubes.
Currying relative cubes into generalized loops in the path space preserves and reflects homotopy.
Concatenation of two relative cubes along a direction i : N of the cube I^N: the first on
the half t i ≤ 1 / 2 and the second on the other half, both reparametrised.
Instances For
Reversal of a relative cube along a direction i : N of the cube I^N, by t i ↦ 1 - t i.
Instances For
The concatenation of two relative cubes is their concatenation as maps out of the cube.
The reversal of a relative cube is its reversal as a map out of the cube.
Concatenation commutes with the action of morphisms of based pairs.
The face in the subspace of a concatenation is the concatenation of the faces.
Regarding absolute cubes as relative cubes carries a concatenation in the direction some i
of I^(Option N) to a concatenation in the direction i.
The relative homotopy set π_{n+1}(X, A, a₀) is the homotopy set π_n(P, c) of the space P
of paths from A to a₀, based at the constant path c.
Instances For
The group structure on π_{n+1}(X, A, a₀) for n ≥ 1, transported from π_n(P, c). Its
product is concatenation of relative cubes in any direction of I^N, by mul_spec.
The group isomorphism π_{n+1}(X, A, a₀) ≃* π_n(P, c), for n ≥ 1.
Instances For
π_{n+1}(X, A, a₀) is commutative for n ≥ 2.
The identity of π_{n+1}(X, A, a₀) is the class of the constant cube.
The identity of π_{n+1}(X, A, a₀) is its distinguished point.
The product of two relative homotopy classes is represented by the concatenation of
representatives along any direction i of I^N, in the order of HomotopyGroup.mul_spec.
The inverse of a relative homotopy class is represented by the reversal of a representative
along any direction i of I^N.
Homomorphisms #
The homomorphism π_{n+1}(X, A, a₀) →* π_{n+1}(Y, B, b₀) induced by a morphism of based
pairs.
Instances For
The boundary map π_{n+1}(X, A, a₀) →* π_n(A, a₀) as a homomorphism.
Instances For
The boundary homomorphism π_{n+1}(X, A, a₀) →* π_n(A, a₀) is natural in the based pair.
The map π_{n+1}(X, a₀) →* π_{n+1}(X, A, a₀) as a homomorphism, where π_{n+1}(X, a₀) is
modelled on the cube I^(Option N).
Instances For
π_{n+1}(X, A, a₀) is commutative when π_n(A, a₀) is trivial, for n ≥ 1. In degree
two this says that π_2(X, A, a₀) is commutative when π_1(A, a₀) is trivial: every relative
class then comes from the commutative group π_2(X, a₀)
(TauCeti.RelHomotopyGroup.surjective_ofHomotopyGroup_of_subsingleton).