constantSphereOneSingularOneSimplex
plain-language theorem explainer
Constant singular 1-simplex at the basepoint of the topological circle S^1, valued in the actual singular simplicial set of TopCat.sphere 1. Circle-parametrization and H_1 work cites it as the first API anchor before once-around generators. Built by transporting the constant continuous map across the singular-set object equivalence.
Claim. The constant singular $1$-simplex at the basepoint of $S^1$, as an element of $\mathrm{Sing}(S^1)_1$ (the degree-$1$ component of the singular simplicial set of the topological $1$-sphere).
background
The module begins a by-hand circle-$H_1$ derivation against the imported topological $1$-sphere object. It fixes the exact carrier, a checked basepoint, and the constant singular $1$-simplex face identities inside the singular simplicial set of that sphere.
The basepoint is the standard point of $\mathrm{TopCat.sphere},1$ obtained by lifting the ambient Euclidean unit vector that lies on the sphere. Singular simplices of degree $1$ are continuous maps from the standard $1$-simplex into the space; the constant map at the basepoint is the trivial such map.
As the module doc stresses: the constant simplex is not the fundamental generator. It is the first API anchor so that later once-around simplices live in the same singular simplicial set and use the same face maps.
proof idea
Definitional construction, not a tactic proof. Apply the inverse of the singular-set object equivalence for $\mathrm{TopCat.sphere},1$ at the opposite of the $1$-simplex category object, sending the constant continuous map valued at the sphere basepoint into the singular simplicial set. The body is a one-line transport of ContinuousMap.const at that basepoint.
why it matters
Anchors the constant-simplex face calculus in this module. Downstream, the left and right face maps applied to this simplex both reduce (by rfl) to the constant singular $0$-simplex at the same basepoint, and the two faces are therefore equal. Those identities certify that face operators act as expected on the trivial class before nontrivial once-around generators are introduced.
In the Recognition foundation stack this is scaffolding for the circle-$H_1$ side of the parametrization story, not a forcing-chain step (T0–T8). It keeps later generators inside the genuine Mathlib singular set of $S^1$ rather than an ad-hoc model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.