faceMap_one_coord_two
plain-language theorem explainer
On the coface embedding δ₁ : Δ¹ → Δ², the image point has third barycentric coordinate equal to the second coordinate of the source. Anyone computing cone lifts or face restrictions of singular 2-simplices on S¹ cites this identity. The proof expands the affine face map, identifies δ₁ as the vertex map 0↦0, 1↦2, and collapses the resulting finite sum to a single term.
Claim. For every point $x$ of the standard $1$-simplex $\Delta^1 = \mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,2)$, the topological face map $\delta_1:\Delta^1\to\Delta^2$ satisfies $(\delta_1 x)_2 = x_1$. In other words, on the side face opposite vertex $1$, the third barycentric coordinate of the image equals the terminal barycentric coordinate of $x$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement vanishes on boundaries: for every 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}$.
Face maps are the continuous affine maps $\mathrm{faceMap},i:\Delta^1\to\Delta^2$ induced by the simplicial cofaces $\delta i:,[1]\to,[2]$. Concretely, $\mathrm{faceMap},i$ is $\mathrm{stdSimplex.map}$ of the underlying vertex function of $\mathrm{SimplexCategory}.\delta,i$. The singular face of a $2$-simplex is then composition $F\circ\mathrm{faceMap},i$.
Barycentric coordinates on $\Delta^n$ are the components of the underlying map $\mathrm{Fin},(n+1)\to\mathbb{R}$. The present lemma records how those coordinates transform under the middle coface $\delta_1$, which skips vertex $1$ and therefore sends the two vertices of $\Delta^1$ to vertices $0$ and $2$ of $\Delta^2$.
proof idea
Rewrite via the simp lemma faceMap_apply, so the claim is an equality of the affine pushforward FunOnFinite.linearMap applied to the vertex map of $\delta_1$. Identify that vertex map by fin_cases: it is $j\mapsto 0$ if $j=0$ and $j\mapsto 2$ otherwise. After FunOnFinite.linearMap_apply_apply, the coordinate-$2$ value is a two-term sum over $\mathrm{Fin},2$. Finset.sum_eq_single at index $1$ kills the $j=0$ summand (its image vertex is $0$, not $2$) and the empty-membership side goal, leaving exactly $x,1$.
why it matters
The coordinate identity is the algebraic input for every $\delta_1$-side computation in the cone-lift apparatus that proves winding kills boundaries. Downstream, coneLiftAngle_faceMap_one quotes it to show the lifted cone angle is constant (equal to the initial path lift) on the whole side face; coneLiftAngle_simplexEdge_one specialises that to the geometric edge; coneBaseParam_faceMap_one_coe_of_not_apex uses the companion coordinate facts to pin the cone base parameter at $0$ away from the apex; and linearTwoSimplexMap_face_one identifies the $\delta_1$ face of the lift-affine $2$-simplex with the geodesic from $p$ to $r$.
Those lemmas feed the $2$-simplex telescoping argument in the module doc: the boundary walk $v_0\to v_1\to v_2$ is homotopic rel endpoints inside convex $\Delta^2$ to the direct edge, so displacement is additive and homotopy-invariant, hence the alternating face sum vanishes. That is the split-injective half of the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. No Recognition forcing-chain step (T0–T8) is invoked here; the result is pure singular-homology scaffolding for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.