Simplicial subdivision of a family of compact convex cells

Let (P i) be a locally finite family of nonempty compact convex sets (cells) in a finite-dimensional real normed space, with pairwise disjoint intrinsic interiors, such that the intrinsic frontier of each cell is covered by the other cells contained in it. For instance, the cells may be compact convex polytopes, each proper face of which is a finite union of lower-dimensional cells of the family. Such a family has a simplicial subdivision: a geometric simplicial complex K with |K| = ⋃ i, P i in which every cell is triangulated by finitely many simplices of K and every simplex of K lies in a cell (Geometry.SimplicialComplex.exists_subdivision). The complex is locally finite, by the criterion Geometry.SimplicialComplex.locallyFinite_convexHull_of_finite_restrict.

The subdivision may be required to use a prescribed point p i of the intrinsic interior of each cell P i as a vertex: every simplex of K then lies in a cell P i and has p i as a vertex. Taking the cells to be the simplices of a simplicial complex and p their centroids subdivides the complex from the centroids of its simplices, as in the barycentric subdivision.

The file also defines the subdivision relation between complexes: K' is a subdivision of K (Geometry.SimplicialComplex.IsSubdivision K' K) when both have the same underlying space and every simplex of K' lies in a simplex of K. It is reflexive and transitive.

The construction retains a prescribed triangulation L of part of the frontiers of the cells (Geometry.SimplicialComplex.exists_subdivision_extending): it suffices that L meets every cell in a finite subcomplex, avoids the intrinsic interiors of the cells, and covers whatever part of the frontier of a cell the smaller cells do not. The resulting K contains L and adds no simplex with all its vertices in |L|.

The proof is by induction on the dimension of the cells. A cell contained in the frontier of another one has strictly smaller dimension (TauCeti.finrank_vectorSpan_lt_of_disjoint_intrinsicInterior). Once the cells of dimension < n are triangulated, the frontier of each n-dimensional cell is a subcomplex, and each such cell is triangulated by coning its frontier to its prescribed point. These cones are glued to the complex built so far (Geometry.SimplicialComplex.exists_extension_of_intrinsicFrontier_subset_space); two distinct n-dimensional cells meet only inside |L| and smaller cells, so the cones meet properly.

The hypotheses imply that two cells meet in a union of points of |L| and of cells contained in both of them (TauCeti.mem_intrinsicInterior_or_of_mem); for two distinct cells of the same dimension these common cells are smaller. So this need not be assumed.

Main definitions

• Geometry.SimplicialComplex.IsSubdivision K' K: K' is a subdivision of K, with the same underlying space and each simplex of K' lying in a simplex of K.

Main results

• Geometry.SimplicialComplex.exists_extension_of_intrinsicFrontier_subset_space: a complex L extends over a family of compact convex cells attached to L along subcomplexes covering their intrinsic frontiers, by coning each cell to a prescribed point.
• Geometry.SimplicialComplex.isSubdivision_of_cells: a complex whose faces lie in finitely many convex cells covering K, each inside a simplex of K, is a finite subdivision of K.
• Geometry.SimplicialComplex.exists_subdivision_extending: the relative subdivision of a family of compact convex cells, extending a prescribed triangulation L.
• Geometry.SimplicialComplex.exists_subdivision: a locally finite simplicial subdivision of a locally finite family of compact convex cells.

References

• S. Łojasiewicz, Triangulation of semi-analytic sets, Ann. Scuola Norm. Sup. Pisa (3) 18 (1964), 449–474 (the simplicial subdivision of the rectilinear cells in the proof of the triangulation theorem).
• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 2 (cell complexes and their simplicial subdivisions).

structure Geometry.SimplicialComplex.IsSubdivision {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] (K' K : SimplicialComplex 𝕜 E) : Prop

A geometric simplicial complex K' is a subdivision of K when both have the same underlying space and every simplex of K' lies in a simplex of K.

• space_eq : K'.space = K.space

  The two complexes have the same underlying space.

• exists_convexHull_subset ⦃s : Finset E⦄ : s ∈ K'.faces → ∃ t ∈ K.faces, (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t

  Every simplex of the subdivision lies in a simplex of the subdivided complex.

theorem Geometry.SimplicialComplex.IsSubdivision.refl {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] (K : SimplicialComplex 𝕜 E) : K.IsSubdivision K

Every complex is a subdivision of itself.

theorem Geometry.SimplicialComplex.IsSubdivision.trans {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K K' K'' : SimplicialComplex 𝕜 E} (h' : K''.IsSubdivision K') (h : K'.IsSubdivision K) : K''.IsSubdivision K

A subdivision of a subdivision of K is a subdivision of K.

theorem Geometry.SimplicialComplex.isSubdivision_of_cells {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {J : Type u_3} [Finite J] {P : J → Set E} {σ : J → Finset E} {M : SimplicialComplex 𝕜 E} (hσ : ∀ (p : J), σ p ∈ K.faces) (hPσ : ∀ (p : J), P p ⊆ (convexHull 𝕜) ↑(σ p)) (hPv : ∀ (p : J), Convex 𝕜 (P p)) (hcov : ∀ x ∈ K.space, ∃ (q : J), x ∈ P q) (hMs : M.space = ⋃ (p : J), P p) (hMP : ∀ (p : J), (M.restrict (P p)).faces.Finite) (hMface : ∀ s ∈ M.faces, ∃ (p : J), ↑s ⊆ P p) : M.IsSubdivision K ∧ M.faces.Finite ∧ ∀ s ∈ M.faces, ∃ (p : J), (convexHull 𝕜) ↑s ⊆ P p

A complex whose faces lie in finitely many convex cells subdivides the covered complex. Let finitely many convex cells P p, each inside a simplex σ p of K, cover K, and let a complex M with space the union of the cells have finitely many faces on each cell, each face inside a cell. Then M is a finite subdivision of K, and the convex hull of each face of M lies in a cell.

theorem Geometry.SimplicialComplex.exists_extension_of_intrinsicFrontier_subset_space {E : Type u_1} {J : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : SimplicialComplex ℝ E) (C : J → Set E) (hCc : ∀ (j : J), IsCompact (C j)) (hCv : ∀ (j : J), Convex ℝ (C j)) (p : J → E) (hp : ∀ (j : J), p j ∈ intrinsicInterior ℝ (C j)) (hfr : ∀ (j : J), intrinsicFrontier ℝ (C j) ⊆ (L.restrict (C j)).space) (hint : ∀ (j : J), Disjoint (intrinsicInterior ℝ (C j)) L.space) (hCC : Pairwise fun (j k : J) => C j ∩ C k ⊆ L.space) : ∃ (K : SimplicialComplex ℝ E), K.space = L.space ∪ ⋃ (j : J), C j ∧ (∀ (B : Set E), (∀ (j : J), Disjoint (intrinsicInterior ℝ (C j)) B) → K.restrict B = L.restrict B) ∧ (∀ (j : J), (K.restrict (C j)).space = C j ∧ ((L.restrict (C j)).faces.Finite → (K.restrict (C j)).faces.Finite)) ∧ ∀ s ∈ K.faces, s ∈ L.faces ∨ ∃ (j : J), p j ∈ s ∧ ↑s ⊆ C j

Attaching compact convex cells to a simplicial complex. Let C j be compact convex sets with prescribed points p j of their intrinsic interiors, whose intrinsic interiors avoid |L|, each meeting L in a subcomplex covering its intrinsic frontier, and any two of which meet only inside |L|. Then L extends to a complex K with |K| = |L| ∪ ⋃ j, C j. Every simplex of K is a simplex of L or lies in a single C j and has p j as a vertex; each C j is triangulated by the simplices of K it contains, finitely many when L has finitely many simplices in C j; and K has the same simplices as L with all their vertices in any set avoiding the intrinsic interiors of the cells.

theorem Geometry.SimplicialComplex.exists_subdivision_extending {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : SimplicialComplex ℝ E) (P : ι → Set E) (hPc : ∀ (i : ι), IsCompact (P i)) (hPv : ∀ (i : ι), Convex ℝ (P i)) (p : ι → E) (hp : ∀ (i : ι), p i ∈ intrinsicInterior ℝ (P i)) (hPlf : LocallyFinite P) (hri : Pairwise fun (i j : ι) => Disjoint (intrinsicInterior ℝ (P i)) (intrinsicInterior ℝ (P j))) (hfr : ∀ (i : ι), intrinsicFrontier ℝ (P i) ⊆ L.space ∪ ⋃ (j : ι), ⋃ (_ : j ≠ i ∧ P j ⊆ P i), P j) (hL : ∀ (i : ι), P i ∩ L.space ⊆ (L.restrict (P i)).space) (hLi : ∀ (i : ι), Disjoint (intrinsicInterior ℝ (P i)) L.space) (hLfin : ∀ (i : ι), (L.restrict (P i)).faces.Finite) : ∃ (K : SimplicialComplex ℝ E), K.restrict L.space = L ∧ K.space = L.space ∪ ⋃ (i : ι), P i ∧ (∀ (i : ι), (K.restrict (P i)).space = P i ∧ (K.restrict (P i)).faces.Finite) ∧ ∀ s ∈ K.faces, s ∈ L.faces ∨ ∃ (i : ι), p i ∈ s ∧ ↑s ⊆ P i

Relative simplicial subdivision of a family of compact convex cells. Let P i be a locally finite family of compact convex sets with pairwise disjoint intrinsic interiors, with prescribed points p i of their intrinsic interiors, and let L be a simplicial complex meeting every cell in a finite subcomplex and avoiding the intrinsic interiors of all cells. Suppose the intrinsic frontier of each cell is covered by |L| and the other cells contained in it. Then there is a simplicial complex K with |K| = |L| ∪ ⋃ i, P i which contains L, has no other simplex with all its vertices in |L|, triangulates every cell by finitely many of its simplices, and each of whose simplices outside L lies in a single cell P i and has p i as a vertex.

theorem Geometry.SimplicialComplex.exists_subdivision {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (P : ι → Set E) (hPc : ∀ (i : ι), IsCompact (P i)) (hPv : ∀ (i : ι), Convex ℝ (P i)) (p : ι → E) (hp : ∀ (i : ι), p i ∈ intrinsicInterior ℝ (P i)) (hPlf : LocallyFinite P) (hri : Pairwise fun (i j : ι) => Disjoint (intrinsicInterior ℝ (P i)) (intrinsicInterior ℝ (P j))) (hfr : ∀ (i : ι), intrinsicFrontier ℝ (P i) ⊆ ⋃ (j : ι), ⋃ (_ : j ≠ i ∧ P j ⊆ P i), P j) : ∃ (K : SimplicialComplex ℝ E), K.space = ⋃ (i : ι), P i ∧ (∀ (i : ι), (K.restrict (P i)).space = P i ∧ (K.restrict (P i)).faces.Finite) ∧ (∀ s ∈ K.faces, ∃ (i : ι), p i ∈ s ∧ ↑s ⊆ P i) ∧ LocallyFinite fun (σ : ↑K.faces) => (convexHull ℝ) ↑↑σ

Simplicial subdivision of a family of compact convex cells. Let P i be a locally finite family of compact convex sets with pairwise disjoint intrinsic interiors, such that the intrinsic frontier of each cell is covered by the other cells contained in it; for instance, compact convex polytopes each proper face of which is a union of lower-dimensional cells of the family. Let p i be a point of the intrinsic interior of P i. Then there is a locally finite simplicial complex K with |K| = ⋃ i, P i which triangulates every cell by finitely many of its simplices, and each simplex of which lies in a single cell P i and has p i as a vertex.