faceMap_zero_coord_two
plain-language theorem explainer
On the coface δ₀ : Δ¹ → Δ², the image point has third barycentric coordinate equal to the second coordinate of the source. Algebraic topologists and anyone tracking cone lifts of singular 1-simplices on S¹ cite this coordinate identity. The proof reduces the affine face map to Fin.succ and collapses the finite support sum to the single index 1.
Claim. For every point $x$ of the standard $1$-simplex $\Delta^1 = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$, the topological face map induced by the coface $\delta_0 : [1] \to [2]$ sends $x$ to a point of $\Delta^2$ whose barycentric coordinate at vertex $2$ equals the barycentric coordinate $x_1$ of the source.
background
The module lifts path winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for any singular $2$-simplex $F$, $\mathrm{disp}(\delta_0 F) - \mathrm{disp}(\delta_1 F) + \mathrm{disp}(\delta_2 F) = 0$. That identity, with the generator evaluation, gives the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
Here $\mathrm{faceMap},i$ is the continuous affine map $\Delta^1 \to \Delta^2$ induced by the simplicial coface $\delta i : [1] \to [2]$. Points of standard simplices are barycentric coordinate tuples summing to $1$. The $i$-th face of a singular $2$-simplex is composition with this map.
The companion identity $\mathrm{faceMap_apply}$ simply unfolds the definition to $\mathrm{stdSimplex.map}$ of the underlying vertex map. The present lemma specialises to $i=0$ and reads off coordinate $2$.
proof idea
Unfold via $\mathrm{faceMap_apply}$. Identify the concrete vertex map of $\mathrm{SimplexCategory.}\delta,0$ with $\mathrm{Fin.succ} : \mathrm{Fin},2 \to \mathrm{Fin},3$ by exhaustive $\mathrm{fin_cases}$. After $\mathrm{FunOnFinite.linearMap_apply_apply}$, the image coordinate at $2$ is a finite sum over preimages under succ. Only index $1$ maps to $2$, so $\mathrm{Finset.sum_eq_single}$ collapses the sum to $x,1$; the off-diagonal and missing-term side conditions are discharged by $\mathrm{fin_cases}$ and $\mathrm{simp}$.
why it matters
Coordinate bookkeeping for the $\delta_0$ side face is required throughout the cone-lift calculus that proves winding is a homology invariant. Downstream, $\mathrm{coneLiftAngle_faceMap_zero}$ and its closed-edge specialisation use this equality to write the lifted cone angle on $\delta_0$ as the linear join $(1-x_1),\mathrm{pathLift},\gamma,1 + x_1,\mathrm{pathLift},\gamma,0$. The base-parameter lemma $\mathrm{coneBaseParam_faceMap_zero_coe_of_not_apex}$ likewise rewrites through both $\mathrm{faceMap_zero_coord_one}$ and this result. The affine model $\mathrm{linearTwoSimplexMap_face_zero}$ identifies the $\delta_0$ face with the geodesic from $q$ to $r$ by the same two coordinate facts.
In the module narrative this supports the $2$-simplex telescoping that yields $\mathrm{simplexDisplacement_boundary}$, the chain-level "winding kills boundaries" step toward $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. It does not itself touch the T0–T8 forcing chain; it is pure singular-homology infrastructure for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.