Injectivity of the barycentric-subdivision realization map #
The canonical realization map sends a face-vertex of the barycentric subdivision to the
barycenter of that face. This file proves that the map is injective, and hence bijective by the
surjectivity theorem in Subdivision.Surjective.
The key point is positivity. A point of a subdivision simplex is a nonnegative linear combination of the barycenters of a chain of faces. The greatest face in the support is exactly the support of the resulting point in the original realization. Moreover, that greatest face has a vertex which belongs to no smaller face in the chain; evaluating there recovers its coefficient. Removing the greatest face and inducting proves uniqueness of all the coefficients.
This is the second bijectivity step in the subdivision-realization milestone in Layer 11 of the
GeometricTopology roadmap. Subdivision.Homeomorph proves continuity of the inverse and packages
the resulting bijection as a homeomorphism.
The argument follows the standard uniqueness proof for barycentric subdivision in Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2, "Derived Subdivisions".
Main results #
AbstractSimplicialComplex.barycentricSubdivisionRealizationMap_injective: the canonical realization map is one-to-one.AbstractSimplicialComplex.barycentricSubdivisionRealizationMap_bijective: the canonical realization map is a bijection.
The canonical map from the realization of the barycentric subdivision to the realization of the original complex is injective.
The canonical map from the realization of the barycentric subdivision to the realization of the original complex is bijective.