Cones of geometric simplicial complexes

Let K be a geometric simplicial complex in a module E over an ordered field and let p be a point. The cone pK has as faces the faces of K, the faces of K with p adjoined, and the vertex {p}. It is a simplicial complex when p "sees" |K| injectively: p ∉ |K|, and every segment from p to a point of |K| meets |K| only at that endpoint (Geometry.SimplicialComplex.IsConeApex). Under this condition the apex lies outside the affine span of every face of K (IsConeApex.notMem_affineSpan), the cone glues along common faces, it contains K as a subcomplex, and its underlying space is the convex join of p with |K| together with p itself (the apex matters only when K is empty).

The main application is coning a triangulated boundary of a convex body to an interior point. If C is convex and K triangulates its intrinsic frontier, every point of the intrinsic interior of C is a cone apex for K (IsConeApex.of_space_eq_intrinsicFrontier). If moreover C is compact, the cone triangulates all of C (space_cone_of_space_eq_intrinsicFrontier) and retains K as its boundary triangulation. This is the coning step in the inductive construction of simplicial subdivisions of convex polytopes compatible with prescribed boundary triangulations.

Main definitions

• Geometry.SimplicialComplex.IsConeApex: p is outside |K| and each segment from p to a point of |K| meets |K| only at that endpoint.
• Geometry.SimplicialComplex.cone: the cone on K with apex p.

Main results

• Geometry.SimplicialComplex.IsConeApex.notMem_affineSpan: a cone apex lies outside the affine span of every face.
• Geometry.SimplicialComplex.vertices_cone: the vertices of the cone are the apex and the vertices of K.
• Geometry.SimplicialComplex.space_cone: |pK| = {p} ∪ convexJoin {p} |K|.
• Geometry.SimplicialComplex.le_cone and mem_cone_faces_iff_of_notMem: the faces of the cone not containing the apex are exactly the faces of K.
• Geometry.SimplicialComplex.restrict_cone: the cone has the same restriction as K to any set avoiding the apex.
• Geometry.SimplicialComplex.erase_mem_faces_of_mem_convexHull: a point of |K| carried by a face of the cone is carried by the opposite face of K.
• Geometry.SimplicialComplex.space_cone_of_space_eq_intrinsicFrontier: coning a triangulation of the intrinsic frontier of a compact convex set to an intrinsic interior point triangulates the whole set.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 1 (joins and cones) and Chapter 2 (simplicial complexes).

structure Geometry.SimplicialComplex.IsConeApex {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] (K : SimplicialComplex 𝕜 E) (p : E) : Prop

A point p is a cone apex for a geometric simplicial complex K if p ∉ |K| and every segment from p to a point y ∈ |K| meets |K| only at y. These are the conditions under which joining p to the faces of K gives a simplicial complex, the cone K.cone p h.

• notMem_space : p ∉ K.space

  The apex is not in the underlying space.

• eq_of_mem_segment ⦃x y : E⦄ : x ∈ K.space → y ∈ K.space → x ∈ segment 𝕜 p y → x = y

  A segment from the apex to a point y of the underlying space meets it only at y.

theorem Geometry.SimplicialComplex.IsConeApex.notMem_of_mem_faces {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p : E} {s : Finset E} (h : K.IsConeApex p) (hs : s ∈ K.faces) : p ∉ s

A cone apex is not a vertex of any face.

theorem Geometry.SimplicialComplex.IsConeApex.notMem_affineSpan {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p : E} {s : Finset E} (h : K.IsConeApex p) (hs : s ∈ K.faces) : p ∉ affineSpan 𝕜 ↑s

A cone apex lies outside the affine span of every face, so adjoining it to a face keeps the vertices affinely independent.

theorem Geometry.SimplicialComplex.IsConeApex.of_space_eq_intrinsicFrontier {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p : E} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {C : Set E} (hC : Convex 𝕜 C) (hK : K.space = intrinsicFrontier 𝕜 C) (hp : p ∈ intrinsicInterior 𝕜 C) : K.IsConeApex p

If K triangulates the intrinsic frontier of a convex set C, every point of the intrinsic interior of C is a cone apex for K.

def Geometry.SimplicialComplex.cone {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [DecidableEq E] (K : SimplicialComplex 𝕜 E) (p : E) (h : K.IsConeApex p) : SimplicialComplex 𝕜 E

The cone pK on a simplicial complex K with apex p. Its faces are the nonempty finite sets whose vertices other than p form a face of K or are empty: the faces of K, the faces of K with p adjoined, and the vertex {p}.

@[simp]

theorem Geometry.SimplicialComplex.mem_cone_faces {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p : E} {s : Finset E} [DecidableEq E] (h : K.IsConeApex p) : s ∈ (K.cone p h).faces ↔ s.Nonempty ∧ (s.erase p = ∅ ∨ s.erase p ∈ K.faces)

theorem Geometry.SimplicialComplex.mem_cone_faces_iff_of_notMem {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p : E} {s : Finset E} [DecidableEq E] (h : K.IsConeApex p) (hs : p ∉ s) : s ∈ (K.cone p h).faces ↔ s ∈ K.faces

The faces of the cone not containing the apex are exactly the faces of K.

theorem Geometry.SimplicialComplex.le_cone {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p : E} [DecidableEq E] (h : K.IsConeApex p) : K ≤ K.cone p h

The cone contains K as a subcomplex.

theorem Geometry.SimplicialComplex.restrict_cone {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p : E} [DecidableEq E] (h : K.IsConeApex p) {B : Set E} (hpB : p ∉ B) : (K.cone p h).restrict B = K.restrict B

Coning to an apex outside B does not change the faces with all vertices in B: the cone retains the restriction of K to B, for instance a prescribed triangulation of a face of a convex body whose boundary is coned to an interior point.

theorem Geometry.SimplicialComplex.insert_mem_cone_faces {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p : E} {s : Finset E} [DecidableEq E] (h : K.IsConeApex p) (hs : s ∈ K.faces) : insert p s ∈ (K.cone p h).faces

Adjoining the apex to a face of K gives a face of the cone.

theorem Geometry.SimplicialComplex.erase_mem_faces_of_mem_convexHull {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p x : E} {s : Finset E} [DecidableEq E] (h : K.IsConeApex p) (hs : s ∈ (K.cone p h).faces) (hx : x ∈ (convexHull 𝕜) ↑s) (hxK : x ∈ K.space) : s.erase p ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑(s.erase p)

A point of |K| in the convex hull of a face s of the cone lies in the convex hull of the face s.erase p of K opposite the apex.

@[simp]

theorem Geometry.SimplicialComplex.vertices_cone {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p : E} [DecidableEq E] (h : K.IsConeApex p) : (K.cone p h).vertices = insert p K.vertices

The vertices of the cone are the apex together with the vertices of K.

theorem Geometry.SimplicialComplex.mem_vertices_cone {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p : E} [DecidableEq E] (h : K.IsConeApex p) : p ∈ (K.cone p h).vertices

The apex is a vertex of the cone.

theorem Geometry.SimplicialComplex.finite_faces_cone_iff {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p : E} [DecidableEq E] (h : K.IsConeApex p) : (K.cone p h).faces.Finite ↔ K.faces.Finite

The cone has finitely many faces exactly when K does.

theorem Geometry.SimplicialComplex.space_cone {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {p : E} [DecidableEq E] (h : K.IsConeApex p) : (K.cone p h).space = insert p (convexJoin 𝕜 {p} K.space)

The underlying space of the cone is the convex join of the apex with |K|, together with the apex itself (which matters only when K is empty).

theorem Geometry.SimplicialComplex.space_cone_of_space_eq_intrinsicFrontier {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [DecidableEq E] {K : SimplicialComplex ℝ E} {C : Set E} {p : E} (hCc : IsCompact C) (hC : Convex ℝ C) (hK : K.space = intrinsicFrontier ℝ C) (hp : p ∈ intrinsicInterior ℝ C) : (K.cone p ⋯).space = C

Coning a triangulation of the intrinsic frontier of a compact convex set C to a point of the intrinsic interior of C triangulates C: every point of C is either the apex or lies on a segment from the apex to a point of the intrinsic frontier.