The standard $n$-simplex is contractible: it is a convex subset of $\mathbf{R}^{n+1}$ and hence has the homotopy type of a point (used to verify acyclicity of star-shaped chain complexes, Proposition 5.13).
Any two singular $n$-simplices in the one-point space PUnit are equal, because all maps
into a subsingleton agree.
Every singular $n$-chain on PUnit is an integer multiple of a fixed generating
$n$-simplex, since all singular simplices in PUnit coincide.
If an integer multiple m • FreeAbelianGroup.of a vanishes in a free abelian group, then the
scalar m itself must be zero (since the generator a is non-torsion).
The alternating sum $\sum_{i<N} (-1)^i$ equals $1$ when $N$ is odd and $0$ otherwise.
The boundary of a singular $(n+1)$-simplex on PUnit equals the alternating sum
$\sum_i (-1)^i$ times a fixed $n$-simplex generator, since all face simplices in PUnit agree.
Given a point $t$ in the standard $(n+1)$-simplex, drop its first coordinate and rescale the remaining coordinates by $1/(1-t_0)$ to land in the standard $n$-simplex; this is the inverse to the front-face inclusion away from the apex $t_0 = 1$.
Instances For
The set-theoretic (pre-continuity) cone map: for a base point $b$ and an $(n+1)$-simplex $\sigma$ in the standard $m$-simplex, send $t \in \Delta^{n+1}$ to the convex combination $t_0 \cdot b + (1 - t_0) \cdot \sigma(\text{rescaleTail}(t))$.
Instances For
Every coordinate of a point in the standard $m$-simplex is at most $1$, because the coordinates are nonnegative and sum to $1$.
The raw cone map coneRawSimplex is continuous on the standard $(n+1)$-simplex; the apex
$t_0 = 1$ is handled separately since the factor $(1 - t_0)$ kills the discontinuity of the
rescaleTail map there.
The cone (as a continuous map) on a singular $(n+1)$-simplex σ with apex b in a single
standard simplex; bundles coneRawSimplex with its continuity proof.
Instances For
Cone construction on a singular $n$-simplex valued in the product of two standard simplices $\Delta^p \times \Delta^q$, with apex the pair of base vertices; this produces an $(n+1)$-simplex used to witness acyclicity of the product chain complex.
Instances For
The chain-level cone operator $h: S_n(\Delta^p \times \Delta^q) \to S_{n+1}(\Delta^p \times \Delta^q)$ obtained by extending coneSimplex linearly; it serves as the chain homotopy from the
identity to the augmentation map.
Instances For
The zeroth face of the cone $c(\sigma)$ on a simplex $\sigma$ recovers $\sigma$ itself, because the $0$-th face of $\Delta^{n+2}$ corresponds to the bottom face $t_0 = 0$ of the cone.
Compatibility of Fin.insertNth with the successor map: inserting at i.succ on the
succ-shifted index equals inserting at i on the shifted tail.
Compatibility of rescaleTail with the $i$-th face inclusion (for $i > 0$): rescaling after
inclusion equals inclusion after rescaling. This is the key combinatorial identity behind
coneSimplex_face_succ.
For positive face indices i.succ, the face of the cone equals the cone of the face:
$d_{i+1}(c(\sigma)) = c(d_i \sigma)$. This together with coneSimplex_face_zero is what makes
coneChain a chain homotopy.
The chain-level cone formula $d \circ h + h \circ d = \mathrm{id}$ on chains in
$\Delta^p \times \Delta^q$: the boundary of the cone of $c$ equals $c$ minus the cone of its
boundary. This realises coneChain as a chain contraction.
Acyclicity of the singular chain complex on a product of standard simplices in positive degrees: every $(n+1)$-cycle in $\Delta^p \times \Delta^q$ is a boundary. This is the technical heart of Proposition 5.13 ($S_*(X) \to \mathbf{Z}$ is a chain homotopy equivalence for star-shaped $X$) for the case of products of simplices.