sphereOneBasepoint
plain-language theorem explainer
Canonical basepoint of Mathlib's exact topological circle object TopCat.sphere 1. It packages the ambient Euclidean unit vector e₀=(1,0) with a checked sphere-membership proof and a ULift. Anyone building singular simplices or face identities on S¹ cites this point. The body is a one-line subtype-plus-ULift construction.
Claim. The basepoint of the unit circle $S^1$ (as the object $\mathrm{TopCat.sphere}\,1$) is the point obtained from the ambient Euclidean vector $(1,0)\in\mathbb{R}^2$, which lies on the metric unit sphere centered at the origin.
background
The module begins a by-hand derivation of $H_1(S^1)$ against Mathlib's imported TopCat.sphere 1, rather than a hand-rolled model. It first fixes the ambient Euclidean plane (SphereOneAmbient), the unit-sphere carrier, and a concrete base vector.
Upstream, sphereOneBaseVector is the first coordinate unit vector $\mathrm{EuclideanSpace.single},0,1$ in $\mathbb{R}^2$. The theorem sphereOneBaseVector_mem_sphere records that this vector lies on the metric unit sphere: its distance to the origin equals 1 (proved by a one-line simp after unfolding distance).
TopCat.sphere 1 is realized via an ULift of that metric sphere subtype, so the basepoint must be packaged as an ULift of a subtype pair. The constant singular 0- and 1-simplices later live in TopCat.toSSet.obj (TopCat.sphere 1) and are anchored at this same point.
proof idea
Pure definition, not a tactic proof. Form the subtype pair ⟨sphereOneBaseVector, sphereOneBaseVector_mem_sphere⟩ (vector plus membership) and apply ULift.up so the result inhabits the exact type of TopCat.sphere 1. No further rewriting is required.
why it matters
This is the first API anchor of the circle-parametrization stack. Downstream, the constant singular 0-simplex and constant singular 1-simplex are the continuous maps constantly equal to this basepoint inside TopCat.toSSet.obj (TopCat.sphere 1). The trigonometric parametrization theorems trigCirclePoint_zero and trigCirclePoint_two_pi identify the start and end of one full turn with the same point, so the once-around loop is closed.
In CircleFundamentalSimplex, both face maps $\delta_0$ and $\delta_1$ of the fundamental singular 1-simplex evaluate to the constant 0-simplex at this basepoint (angles $2\pi$ and $0$ respectively). The module doc stresses that the constant simplex is not the fundamental generator; it is the shared face target that later once-around simplices must match. Within Recognition Science this supplies the topological $S^1$ base needed before any eight-tick or octave identification is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.