fundamentalSphereOneSingularOneSimplex_face_zero
plain-language theorem explainer
The δ₀ face of the once-around singular 1-simplex on S¹ equals the constant 0-simplex at the chosen basepoint. Algebraic topologists computing H₁(S¹) in the singular simplicial set cite this as one endpoint of the geometric generator. The proof reduces via the TopCat-to-sSet equivalence to the identity trigCirclePoint(2π) = basepoint after the face map forces the second barycentric coordinate to 1.
Claim. In the singular simplicial set of the topological 1-sphere, the face operator $\delta_0$ applied to the once-around singular 1-simplex equals the constant singular 0-simplex at the chosen basepoint of $S^1$.
background
The module builds the once-around singular 1-simplex inside the actual singular simplicial set TopCat.toSSet.obj (TopCat.sphere 1) and shows both faces land on the same basepoint, so the simplex is a loop.
The path map sends a point of the standard 1-simplex to trigCirclePoint(2π · x₁), using the second barycentric coordinate as the angle parameter; endpoints therefore sit at angles 0 and 2π. The singular 1-simplex is the image of that continuous map under the standard equivalence between continuous maps from the geometric simplex and 1-simplices in the singular set. The constant 0-simplex is the image of the constant map at sphereOneBasepoint.
Upstream, trigCirclePoint_two_pi records that one full turn returns to the basepoint: "The trigonometric parametrization returns to the basepoint after one full turn."
proof idea
Apply injectivity of TopCat.toSSetObjEquiv at dimension 0, then extensionality on the underlying continuous map. Unfolding the singular-set face, the path map, and the constant 0-simplex reduces the goal to
trigCirclePoint(2π · (δ₀x)₁) = sphereOneBasepoint.
A short computation with stdSimplex.map_coe and the definition of SimplexCategory.δ 0 shows that the second barycentric coordinate of δ₀x is identically 1. The goal collapses to trigCirclePoint(2π) = sphereOneBasepoint, discharged by trigCirclePoint_two_pi.
why it matters
This is one of the two face identities needed for fundamentalSphereOneSingularOneSimplex_faces_eq, which states that "the fundamental once-around singular 1-simplex is a loop: its two faces are equal." Together the faces supply a closed singular 1-cycle that is the geometric generator candidate for the later H₁ computation on the exact TopCat.sphere 1 object.
In the Recognition foundation stack the circle and its winding data underwrite the eight-tick octave (T7) and the discrete recognition clock; a rigorously closed once-around simplex is the topological carrier for that period. The result is fully proved (no sorry) and sits strictly upstream of the faces-equal theorem in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.