Relabeling combinatorial balls and spheres #
An injective map of ambient vertex types sends a combinatorial ball to a combinatorial ball or sphere of the same dimension. This allows local models described using disjoint tagged vertex types, such as joins, to be compared with the original complexes.
The transport uses StellarEquivalentUpToRelabeling.map: injectively relabel the stellar
equivalence to a standard simplex (resp. simplex boundary), whose image is again a standard
simplex (resp. simplex boundary) with the same number of vertices.
References #
- C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 2 and 3 (stellar equivalence, combinatorial balls and spheres).
theorem
PreAbstractSimplicialComplex.IsCombinatorialBall.map
{ι : Type u_1}
{κ : Type u_2}
[DecidableEq ι]
[DecidableEq κ]
{K : PreAbstractSimplicialComplex ι}
{n : ℕ}
(h : K.IsCombinatorialBall n)
(f : ι → κ)
(hf : Function.Injective f)
:
(K.map f).IsCombinatorialBall n
Injectively relabeling a combinatorial ball preserves its dimension and ball structure.
theorem
PreAbstractSimplicialComplex.IsCombinatorialSphere.map
{ι : Type u_1}
{κ : Type u_2}
[DecidableEq ι]
[DecidableEq κ]
{K : PreAbstractSimplicialComplex ι}
{n : ℕ}
(h : K.IsCombinatorialSphere n)
(f : ι → κ)
(hf : Function.Injective f)
:
(K.map f).IsCombinatorialSphere n
Injectively relabeling a combinatorial sphere preserves its dimension and sphere structure.