CW approximation: the inductive step #
A CW approximation of a space X is built by attaching cells, one dimension at a time, to a space
mapping to X (Hatcher, Proposition 4.13). This file carries out one step. Let f : Z ⟶ X be a
map, z a point of Z and n ≥ 1. Attach (n + 1)-cells to Z of two kinds:
- one along the attaching map
GenLoop.diskBoundaryMap pof every generalized looppof dimensionnatzwhose classfsends to the identity ofπₙ(X, f z); - one along the constant map at
zfor every generalized loopγof dimensionn + 1ofXatf z.
The result is TauCeti.cwApproximationStep f z n, a cell attachment by definition, so the
general API of TauCeti.cellAttachment applies to it. The map f extends to
TauCeti.cwApproximationStepMap f z n out of it: over a cell of the first kind through a
null-homotopy of the composite of its attaching map with f, and over the cell attached for γ by
γ itself, read on the disk through TauCeti.diskHomeomorphCube. On homotopy groups at the base
point, the first two items below assume that Z is Hausdorff, while the third holds for any Z:
- attaching
(n + 1)-cells changes noπₖwithk < nand is surjective onπₙ(Hatcher, Corollary 4.12), so the extension is bijective onπₖfork < nexactly whenfis (TauCeti.bijective_homotopyGroupMap_cwApproximationStepMap_iff_of_lt); - the cells of the first kind kill the kernel of
fonπₙ, so the extension is injective onπₙ(TauCeti.injective_homotopyGroupMap_cwApproximationStepMap), and bijective exactly whenfis surjective onπₙ(TauCeti.bijective_homotopyGroupMap_cwApproximationStepMap_iff_surjective); - the cell attached for
γis a sphere sent ontoγ, so the extension is surjective onπₙ₊₁(TauCeti.surjective_homotopyGroupMap_cwApproximationStepMap_succ).
So if Z is Hausdorff and f is bijective on πₖ for k < n and surjective on πₙ, the
extension is bijective on πₖ for k ≤ n and surjective on πₙ₊₁, which is the inductive step
of Hatcher's construction.
All statements are about the homotopy groups at z and at its images.
Main definitions #
TauCeti.cwApproximationAttachingMap f z n: the attaching maps of the cells.TauCeti.cwApproximationStep f z n: the space obtained by attaching them, with the inclusionTauCeti.cwApproximationStepIncl f z nofZ.TauCeti.cwApproximationStepMap f z n: the extension off.
Main results #
TauCeti.injective_homotopyGroupMap_cwApproximationStepMap: for HausdorffZ, the extension is injective onπₙ.TauCeti.surjective_homotopyGroupMap_cwApproximationStepMap_succ: the extension is surjective onπₙ₊₁.TauCeti.bijective_homotopyGroupMap_cwApproximationStepMap_iff_of_lt: for HausdorffZ, belown, the extension is bijective onπₖexactly whenfis.TauCeti.bijective_homotopyGroupMap_cwApproximationStepMap_iff_surjective: for HausdorffZ, the extension is bijective onπₙexactly whenfis surjective onπₙ.
References #
- A. Hatcher, Algebraic Topology, Section 4.1, Proposition 4.13 (CW approximation) and Corollary 4.12.
The attaching maps of the (n + 1)-cells of the inductive step of CW approximation for
f : Z ⟶ X at z. A generalized loop p of dimension n at z whose class f sends to the
identity of πₙ(X, f z) gives a cell attached along GenLoop.diskBoundaryMap p, which kills the
class of p. A generalized loop of dimension n + 1 of X at f z gives a cell attached along
the constant map at z, a sphere on which f is extended by that loop.
Instances For
A cell killing the class of p is attached along GenLoop.diskBoundaryMap p.
The cell attached for a generalized loop of X is attached along the constant map at z.
The space of the inductive step of CW approximation for f : Z ⟶ X at z: Z with the
(n + 1)-cells TauCeti.cwApproximationAttachingMap f z n attached. It is reducibly a
TauCeti.cellAttachment, so it is Hausdorff when Z is and carries the cell-attachment API.
Instances For
The inclusion of Z into TauCeti.cwApproximationStep f z n.
Instances For
The extension of f over TauCeti.cwApproximationStep f z n. It agrees with f on Z
(TauCeti.cwApproximationStepIncl_comp_cwApproximationStepMap), and on the cell attached for a
generalized loop γ of dimension n + 1 of X it is γ, read on the disk through
TauCeti.diskHomeomorphCube (TauCeti.cellAttachmentCell_inr_comp_cwApproximationStepMap).
Instances For
The extension TauCeti.cwApproximationStepMap f z n restricts to f on Z.
The extension TauCeti.cwApproximationStepMap f z n restricts to f on Z.
The extension TauCeti.cwApproximationStepMap f z n agrees with f on the points of Z.
On the cell attached for a generalized loop γ of dimension n + 1 of X, the extension
TauCeti.cwApproximationStepMap f z n is γ, read on the disk (GenLoop.diskMap γ).
On the cell attached for a generalized loop γ of dimension n + 1 of X, the extension
TauCeti.cwApproximationStepMap f z n is γ, read on the disk (GenLoop.diskMap γ).
On homotopy groups at the base point, the extension TauCeti.cwApproximationStepMap f z n
composed with the inclusion of Z induces the map induced by f.
The extension is surjective on πₙ₊₁. Every class of πₙ₊₁(X, f z) is the image under
TauCeti.cwApproximationStepMap f z n of the sphere formed by the cell attached for a
representative.
The extension is injective on πₙ. The cells attached along generalized loops whose
classes f kills make the map πₙ(cwApproximationStep f z n) → πₙ(X, f z) injective, for a
Hausdorff space Z.
The extension is bijective below n exactly when f is. For k < n, the extension
TauCeti.cwApproximationStepMap f z n induces a bijection on πₖ if and only if f does, for a
Hausdorff space Z: attaching (n + 1)-cells does not change πₖ. Here k = Nat.card N.
The extension is bijective on πₙ exactly when f is surjective on πₙ. The extension
TauCeti.cwApproximationStepMap f z n is always injective on πₙ, and it is surjective on πₙ
exactly when f is, for a Hausdorff space Z.