The exact homotopy sequence of a based pair #
Let X = (X, A, a₀) be a based pair and let n be the cardinality of the index type N. This
file constructs the map j : π_{n+1}(X, a₀) → π_{n+1}(X, A, a₀) and proves that the sequence of
pointed sets
π_{n+1}(A, a₀) → π_{n+1}(X, a₀) → π_{n+1}(X, A, a₀) → π_n(A, a₀) → π_n(X, a₀)
is exact at its three middle terms, for every N. Here the first and last maps are induced by
the inclusion A ↪ X, and the third is TauCeti.RelHomotopyGroup.boundary. Exactness of a
sequence of pointed sets f, g means that the elements sent by g to the distinguished point
are exactly the image of f.
The absolute group π_{n+1}(X, a₀) is Mathlib's HomotopyGroup (Option N) X a₀, whose cube
I^(Option N) is the relative cube I × I^N with the coordinate none as the distinguished first
direction (TauCeti.piOptionEquivProdHomeomorph, Cube.boundary_option_iff). The map j regards
an absolute cube as a relative one.
Since N is arbitrary (and may be empty), the three statements cover every term of the long exact
sequence
⋯ → π_{n+1}(X, A) → π_n(A) → π_n(X) → π_n(X, A) → ⋯ → π_1(X, A) → π_0(A) → π_0(X)
of pointed sets. To chain two consecutive degrees, the group π_n(X, a₀) receiving the inclusion
from π_n(A, a₀) (modelled on I^N) is matched with the source of j (modelled on I^(Option M)
for an index type M with Option M ≃ N) by reindexing the cube along
HomotopyGroup.congrEquiv.
Implementation notes #
The three exactness proofs are the standard cube manipulations of Hatcher, Algebraic Topology, Theorem 4.3.
- At
π_n(A): a relative cube is literally a null-homotopy inXof its face inA, and conversely. - At
π_{n+1}(X, A): if the face of a relative cubepis null-homotopic inA, glue that null-homotopy in front ofpalong the distinguished direction. Shrinking the glued part gives a homotopy through relative cubes frompto a cube whose distinguished face is constant, that is, to an absolute cube. - At
π_{n+1}(X): by the compression criterion (TauCeti.RelGenLoop.exists_homotopicRel_of_homotopic_const), an absolute cube that is trivial as a relative cube is homotopic, relative to the boundary, to a cube inA.
Main declarations #
TauCeti.RelGenLoop.ofGenLoop,TauCeti.RelHomotopyGroup.ofHomotopyGroup: the mapπ_{n+1}(X, a₀) → π_{n+1}(X, A, a₀), natural byTauCeti.RelHomotopyGroup.map_ofHomotopyGroup.TauCeti.RelHomotopyGroup.mem_range_homotopyGroupMap_iff: exactness atπ_{n+1}(X, a₀).TauCeti.RelHomotopyGroup.mem_range_ofHomotopyGroup_iff: exactness atπ_{n+1}(X, A, a₀).TauCeti.RelHomotopyGroup.mem_range_boundary_iff: exactness atπ_n(A, a₀).TauCeti.RelHomotopyGroup.subsingleton_of_injective_of_surjective:π_{n+1}(X, A, a₀)is trivial whenπ_n(A, a₀) → π_n(X, a₀)is injective andπ_{n+1}(A, a₀) → π_{n+1}(X, a₀)is surjective, andTauCeti.RelHomotopyGroup.subsingleton_of_subsingleton_homotopyGroupin particular whenπ_n(A, a₀)andπ_{n+1}(X, a₀)are trivial.TauCeti.RelHomotopyGroup.surjective_ofHomotopyGroup_of_subsingleton: every class ofπ_{n+1}(X, A, a₀)comes fromπ_{n+1}(X, a₀)whenπ_n(A, a₀)is trivial.
Absolute cubes as relative cubes #
An absolute generalized loop I^(Option N) → X at the basepoint, regarded as a relative cube
I × I^N → X with the coordinate none as the distinguished first direction. Its face
{0} × I^N is constant at the basepoint.
Instances For
The face of an absolute cube in the distinguished direction is constant.
Regarding absolute cubes as relative cubes commutes with the action of morphisms of based pairs.
A homotopy of absolute cubes relative to the boundary is a homotopy through relative cubes.
Exactness at π_n(A) #
A relative cube is a null-homotopy in X, relative to the boundary, of its face in A.
A generalized loop in A that is null-homotopic in X is the face of a relative cube.
Exactness at π_{n+1}(X, A) #
If the face of a relative cube is null-homotopic in A, the cube is homotopic through
relative cubes to an absolute cube.
Exactness at π_{n+1}(X) #
If the relative cube of an absolute cube γ is homotopic through relative cubes to the
constant cube, then γ is homotopic relative to the boundary to a cube in A.
The map π_{n+1}(X, a₀) → π_{n+1}(X, A, a₀) regarding an absolute cube as a relative cube,
where π_{n+1}(X, a₀) is modelled on the cube I^(Option N).
Instances For
The map π_{n+1}(X, a₀) → π_{n+1}(X, A, a₀) preserves the distinguished points.
The map π_{n+1}(X, a₀) → π_{n+1}(X, A, a₀) is natural in the based pair.
The composite π_{n+1}(X, a₀) → π_{n+1}(X, A, a₀) → π_n(A, a₀) is trivial.
The composite π_{n+1}(A, a₀) → π_{n+1}(X, a₀) → π_{n+1}(X, A, a₀) is trivial.
The composite π_{n+1}(X, A, a₀) → π_n(A, a₀) → π_n(X, a₀) is trivial.
Exactness at π_{n+1}(X, a₀). A class in π_{n+1}(X, a₀) comes from π_{n+1}(A, a₀)
exactly when it becomes trivial in π_{n+1}(X, A, a₀).
Exactness at π_{n+1}(X, A, a₀). A relative class comes from π_{n+1}(X, a₀) exactly
when its boundary in π_n(A, a₀) is trivial.
Exactness at π_n(A, a₀). A class in π_n(A, a₀) is the boundary of a relative class
exactly when it becomes trivial in π_n(X, a₀).
If the inclusion A ↪ X induces an injection π_n(A, a₀) → π_n(X, a₀) and a surjection
π_{n+1}(A, a₀) → π_{n+1}(X, a₀), then the relative homotopy set π_{n+1}(X, A, a₀) is
trivial.
If π_n(A, a₀) and π_{n+1}(X, a₀) are trivial, then so is π_{n+1}(X, A, a₀).
If π_n(A, a₀) is trivial, then every class of π_{n+1}(X, A, a₀) comes from
π_{n+1}(X, a₀).