faceMap_zero_coord_one
plain-language theorem explainer
On the coface embedding δ₀ : Δ¹ → Δ², the image barycentric coordinate at vertex 1 equals the source coordinate at vertex 0. Anyone computing faces of singular 2-simplices on S¹, or cone/geodesic parameterizations built from those faces, cites this identity. The proof unfolds the affine face map, identifies δ₀ with Fin.succ, and collapses the pushforward sum to a single term.
Claim. For every point $x$ of the standard $1$-simplex $\Delta^1 = \mathrm{stdSimplex}\,\mathbb{R}(\mathrm{Fin}\,2)$, if $y = \delta_0(x) \in \Delta^2$ is its image under the topological face map induced by the coface $\delta_0 : [1] \to [2]$, then the barycentric coordinate $y_1$ equals $x_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 the comparison $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 $\delta i$. The $i$-th face of a singular $2$-simplex is composition with this map.
Barycentric coordinates on $\Delta^n$ are the component functions $\mathrm{Fin},(n+1) \to \mathbb{R}$ of a point of the standard simplex (nonnegative, summing to $1$). The present lemma records how $\delta_0$ rearranges those coordinates: it skips vertex $0$, so source vertex $0$ lands on target vertex $1$.
proof idea
Unfold $\mathrm{faceMap}$ via the simp lemma $\mathrm{faceMap_apply}$, reducing to the finite-support linear map of the coface vertex function. Prove by $\mathrm{fin_cases}$ that $\mathrm{ConcreteCategory.hom}(\delta_0) : \mathrm{Fin},2 \to \mathrm{Fin},3$ equals $j \mapsto j.\mathrm{succ}$. Rewrite with $\mathrm{FunOnFinite.linearMap_apply_apply}$, obtaining a sum over $\mathrm{Fin},2$. Collapse that sum with $\mathrm{Finset.sum_eq_single}$ at index $0$: the off-diagonal terms vanish by $\mathrm{fin_cases}$ and the missing-term side condition is contradictory. The surviving term is exactly $x,0$.
why it matters
Coordinate bookkeeping for $\delta_0$ is required wherever faces of singular or affine $2$-simplices are evaluated explicitly. Downstream, $\mathrm{coneBaseParam_faceMap_zero_coe_of_not_apex}$ uses it (with the companion coordinate-$2$ identity) to show the cone base parameter is $1$ on the side face away from the apex. $\mathrm{linearTwoSimplexMap_face_zero}$ applies both coordinate lemmas to identify the $\delta_0$ face of a lift-affine $2$-simplex with the geodesic from $q$ to $r$. $\mathrm{twoSimplexCoordOneParam_face_zero}$ rewrites the coordinate-$1$ path parameter on that face as the reversed unit-interval homeomorphism of $x$.
These face evaluations feed the $2$-simplex telescoping that proves $\mathrm{simplexDisplacement}$ vanishes on boundaries, the key step toward a winding homomorphism left-inverse to the fundamental class on $H_1(S^1)$. The module notes the converse generation half still needs a simplicial prism or subdivision operator absent from Mathlib singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.