Restricting a geometric simplicial complex to a set

For a geometric simplicial complex K and a set B, the faces of K all of whose vertices lie in B form a subcomplex K.restrict B. When B is convex, its underlying space lies in |K| ∩ B.

When moreover B is an extreme subset of |K| (for instance a face of a convex polytope which K triangulates), the restriction triangulates exactly |K| ∩ B (Geometry.SimplicialComplex.space_restrict_of_isExtreme): the face of K carrying a point of B can be shrunk to a face with all its vertices in B. So a triangulation of a convex polytope induces a triangulation of each of its faces. This is what lets triangulations of polytopes meeting along common faces be compared, and glued, face by face.

The restriction of a locally finite complex to a compact set has finitely many faces (Geometry.SimplicialComplex.finite_faces_restrict).

Main definitions

• Geometry.SimplicialComplex.restrict: the subcomplex of the faces with all vertices in a set.

Main results

• Geometry.SimplicialComplex.exists_subset_mem_restrict_faces: a point of an extreme subset B of |K| lies in the convex hull of a face of K.restrict B, which can be chosen inside any given face of K whose convex hull contains the point.
• Geometry.SimplicialComplex.space_restrict_of_isExtreme: |K.restrict B| = |K| ∩ B when B is a convex extreme subset of |K|.

def Geometry.SimplicialComplex.restrict {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] (K : SimplicialComplex 𝕜 E) (B : Set E) : SimplicialComplex 𝕜 E

The subcomplex of K consisting of the faces all of whose vertices lie in B.

@[simp]

theorem Geometry.SimplicialComplex.mem_restrict_faces {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {B : Set E} {s : Finset E} : s ∈ (K.restrict B).faces ↔ s ∈ K.faces ∧ ↑s ⊆ B

theorem Geometry.SimplicialComplex.restrict_le {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {B : Set E} : K.restrict B ≤ K

theorem Geometry.SimplicialComplex.restrict_mono {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {B C : Set E} (h : B ⊆ C) : K.restrict B ≤ K.restrict C

@[simp]

theorem Geometry.SimplicialComplex.restrict_restrict {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {B C : Set E} : (K.restrict B).restrict C = K.restrict (B ∩ C)

theorem Geometry.SimplicialComplex.restrict_eq_self_of_space_subset {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {B : Set E} (h : K.space ⊆ B) : K.restrict B = K

theorem Geometry.SimplicialComplex.space_mono {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K L : SimplicialComplex 𝕜 E} (h : K ≤ L) : K.space ⊆ L.space

A subcomplex has a smaller underlying space.

theorem Geometry.SimplicialComplex.space_restrict_subset_space {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {B : Set E} : (K.restrict B).space ⊆ K.space

theorem Geometry.SimplicialComplex.space_restrict_subset {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {B : Set E} (hB : Convex 𝕜 B) : (K.restrict B).space ⊆ K.space ∩ B

The underlying space of the restriction of K to a convex set B lies in |K| ∩ B.

theorem Geometry.SimplicialComplex.finite_faces_restrict {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {K : SimplicialComplex 𝕜 E} {B : Set E} (hK : LocallyFinite fun (s : ↑K.faces) => (convexHull 𝕜) ↑↑s) (hB : IsCompact B) : (K.restrict B).faces.Finite

Only finitely many simplices of a locally finite complex have all their vertices in a compact set.

theorem Geometry.SimplicialComplex.exists_subset_mem_restrict_faces {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {B : Set E} {s : Finset E} {x : E} (hB : IsExtreme 𝕜 K.space B) (hs : s ∈ K.faces) (hxs : x ∈ (convexHull 𝕜) ↑s) (hxB : x ∈ B) : ∃ t ⊆ s, t ∈ (K.restrict B).faces ∧ x ∈ (convexHull 𝕜) ↑t

If B is an extreme subset of |K|, a point of B in the convex hull of a face s of K lies in the convex hull of a face of K.restrict B contained in s.

theorem Geometry.SimplicialComplex.space_restrict_of_isExtreme {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : SimplicialComplex 𝕜 E} {B : Set E} (hB : IsExtreme 𝕜 K.space B) (hBc : Convex 𝕜 B) : (K.restrict B).space = K.space ∩ B

The restriction of K to a convex extreme subset B of |K| triangulates |K| ∩ B. For instance, a triangulation of a convex polytope restricts to a triangulation of each face.

theorem Geometry.SimplicialComplex.space_restrict_eq_intrinsicFrontier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : SimplicialComplex ℝ E} {C : Set E} (hCv : Convex ℝ C) (hfr : intrinsicFrontier ℝ C ⊆ (L.restrict C).space) (hint : Disjoint (intrinsicInterior ℝ C) L.space) : (L.restrict C).space = intrinsicFrontier ℝ C

If a convex set C meets the simplicial complex L exactly in the subcomplex covering its intrinsic frontier, and its intrinsic interior avoids |L|, then the restriction of L to C has the intrinsic frontier of C as its space.