Lifting points to an ordered simplicial product

Every pair of points in the realizations of two ordered simplicial complexes admits a lift to their staircase product. Its barycentric coordinates are nonnegative joint weights with the prescribed marginals, and its carrier is a chain in the coordinatewise order.

This is the existence part of identifying the realization of an ordered simplicial product with the product of realizations. In particular, it applies to the simplicial cylinder. No finiteness hypothesis on the vertex types or complexes is required: each pair of points has finite support.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2 (triangulating products of polyhedra).

theorem AbstractSimplicialComplex.exists_realization_orderedProd {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (K : AbstractSimplicialComplex α) (L : AbstractSimplicialComplex β) (x : K.Realization) (y : L.Realization) : ∃ (z : (K.orderedProd L).Realization), ((PreAbstractSimplicialComplex.SimplicialMap.orderedProdFst K.toPreAbstractSimplicialComplex L.toPreAbstractSimplicialComplex).domainRestrict ⋯).realizationMap z = x ∧ ((PreAbstractSimplicialComplex.SimplicialMap.orderedProdSnd K.toPreAbstractSimplicialComplex L.toPreAbstractSimplicialComplex).domainRestrict ⋯).realizationMap z = y

Every pair of realization points has a lift to the ordered product under the two canonical realization projections.