faceMap_one_coord_one
plain-language theorem explainer
On the middle face inclusion δ₁ : Δ¹ → Δ², every point has vanishing barycentric coordinate x₁. Anyone computing faces of singular 2-simplices on S¹, or cone/geodesic parameterizations of Δ², cites this coordinate identity. The proof is a short tactic argument: unwind the affine face map, identify δ₁ as the vertex map that skips index 1, and observe the pushforward mass at coordinate 1 is an empty sum.
Claim. For every point $x$ of the standard $1$-simplex $\Delta^1 = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$, the image under the topological face map $\delta_1:\Delta^1\to\Delta^2$ has barycentric coordinate $1$ equal to zero: $(\delta_1(x))_1 = 0$.
background
The module lifts path-level 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 is the chain-level half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Here faceMap i is the continuous affine map $\Delta^1\to\Delta^2$ induced by the simplicial coface $\delta i:,[1]\to,[2]$. Concretely it is stdSimplex.map of the underlying vertex function ConcreteCategory.hom (SimplexCategory.δ i). The $i$-th face of a singular $2$-simplex is composition with this map.
Barycentric coordinates on $\Delta^2$ are the three components of a point in the standard simplex in $\mathbb{R}^{\mathrm{Fin},3}$. The middle coface $\delta_1$ skips vertex $1$, so its image lies in the face opposite that vertex, where coordinate $1$ vanishes.
proof idea
Rewrite via the simp lemma faceMap_apply, exposing the underlying FunOnFinite.linearMap of the coface. Prove by fin_cases that the vertex map of $\delta_1$ is $0\mapsto 0$, $1\mapsto 2$ (skips $1$). After FunOnFinite.linearMap_apply_apply, the value at coordinate $1$ is a finite sum over preimages; both candidate indices fail the membership test, so Finset.sum_eq_zero finishes.
why it matters
This is the elementary coordinate fact that the middle face of $\Delta^2$ is the edge opposite vertex $1$. Downstream it discharges three face computations in the same module: twoSimplexCoordOneParam_face_one (the cone/coordinate parameter on $\delta_1$ is identically zero), coneBaseParam_faceMap_one_coe_of_not_apex (away from the apex, the cone base parameter on $\delta_1$ is $0$, the initial-endpoint side of the lifted cone formula), and linearTwoSimplexMap_face_one (the $\delta_1$ face of the lift-affine $2$-simplex is the geodesic from $p$ to $r$).
Those lemmas feed the $2$-simplex telescoping that proves simplexDisplacement_boundary, the kills-boundaries identity for the winding invariant. In the broader Recognition foundation this is pure singular-homology scaffolding for the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; it does not itself touch T0–T8 or the RCL, but it underwrites the topological side of the circle-winding chain used later in the forcing story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.