Gluing geometric simplicial complexes along common faces

A family of geometric simplicial complexes K i in a module E glues to a single simplicial complex, Geometry.SimplicialComplex.glue K h, whose faces are the faces of all the K i, as soon as the convex hulls of a face of K i and a face of K j always meet inside the convex hull of their common vertices. Its underlying space is the union of the spaces |K i|, and if each K i is finite and the spaces |K i| form a locally finite family, its simplices form a locally finite family. More generally, a complex is locally finite when its simplices lie in a locally finite complex or in the cells of a locally finite family of convex sets, finitely many in each cell (locallyFinite_convexHull_of_finite_restrict).

The compatibility condition is checked geometrically when the complexes triangulate sets which meet along common faces. Suppose every point of |K i| ∩ |K j| lies in a set F which is an extreme subset of both |K i| and |K j|, and such that every face of K i with all vertices in F is a face of K j; for instance, K i and K j restrict to the same subcomplex on F. Then a face of K i and a face of K j meet properly (convexHull_inter_convexHull_subset_of_isExtreme): the point of intersection is carried by faces with all vertices in F, which are then faces of K j. Gluing retains the triangulation of each piece on its convex subsets (restrict_glue).

This is the common-face agreement and coverage step in subdividing a locally finite family of compact convex polytopes, meeting in common faces, into a single simplicial complex compatible with prescribed triangulations of their faces: each polytope is triangulated separately, by coning a triangulation of its boundary, and the pieces are glued.

Main definitions

• Geometry.SimplicialComplex.glue: the simplicial complex whose faces are the faces of a family of pairwise compatible complexes.

Main results

• Geometry.SimplicialComplex.space_glue: |glue K h| = ⋃ i, |K i|.
• Geometry.SimplicialComplex.glue_le_iff: the glued complex is the least complex containing every K i.
• Geometry.SimplicialComplex.locallyFinite_convexHull_glue: gluing a locally finite family of finite complexes gives a locally finite complex.
• Geometry.SimplicialComplex.locallyFinite_convexHull_of_finite_restrict: a complex whose simplices lie in a locally finite complex or in the cells of a locally finite family of convex sets, finitely many in each cell, is locally finite.
• Geometry.SimplicialComplex.convexHull_inter_convexHull_subset_of_isExtreme: complexes agreeing on common extreme subsets covering the intersection of their spaces meet properly.
• Geometry.SimplicialComplex.restrict_glue: gluing along common faces does not change the restriction of each piece to its convex subsets.

References

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

def Geometry.SimplicialComplex.glue {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] (K : ι → SimplicialComplex 𝕜 E) (h : ∀ (i j : ι) ⦃s t : Finset E⦄, s ∈ (K i).faces → t ∈ (K j).faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)) : SimplicialComplex 𝕜 E

The simplicial complex whose faces are the faces of all the complexes K i, provided the convex hulls of a face of K i and a face of K j always meet inside the convex hull of their common vertices.

@[simp]

theorem Geometry.SimplicialComplex.mem_glue_faces {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : ι → SimplicialComplex 𝕜 E} {s : Finset E} (h : ∀ (i j : ι) ⦃s t : Finset E⦄, s ∈ (K i).faces → t ∈ (K j).faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)) : s ∈ (glue K h).faces ↔ ∃ (i : ι), s ∈ (K i).faces

theorem Geometry.SimplicialComplex.le_glue {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : ι → SimplicialComplex 𝕜 E} (h : ∀ (i j : ι) ⦃s t : Finset E⦄, s ∈ (K i).faces → t ∈ (K j).faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)) (i : ι) : K i ≤ glue K h

theorem Geometry.SimplicialComplex.glue_le_iff {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : ι → SimplicialComplex 𝕜 E} {L : SimplicialComplex 𝕜 E} (h : ∀ (i j : ι) ⦃s t : Finset E⦄, s ∈ (K i).faces → t ∈ (K j).faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)) : glue K h ≤ L ↔ ∀ (i : ι), K i ≤ L

The glued complex is the least simplicial complex containing every K i.

@[simp]

theorem Geometry.SimplicialComplex.space_glue {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : ι → SimplicialComplex 𝕜 E} (h : ∀ (i j : ι) ⦃s t : Finset E⦄, s ∈ (K i).faces → t ∈ (K j).faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)) : (glue K h).space = ⋃ (i : ι), (K i).space

@[simp]

theorem Geometry.SimplicialComplex.vertices_glue {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : ι → SimplicialComplex 𝕜 E} (h : ∀ (i j : ι) ⦃s t : Finset E⦄, s ∈ (K i).faces → t ∈ (K j).faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)) : (glue K h).vertices = ⋃ (i : ι), (K i).vertices

theorem Geometry.SimplicialComplex.locallyFinite_convexHull_glue {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : ι → SimplicialComplex 𝕜 E} (h : ∀ (i j : ι) ⦃s t : Finset E⦄, s ∈ (K i).faces → t ∈ (K j).faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)) [TopologicalSpace E] (hfin : ∀ (i : ι), (K i).faces.Finite) (hlf : LocallyFinite fun (i : ι) => (K i).space) : LocallyFinite fun (σ : ↑(glue K h).faces) => (convexHull 𝕜) ↑↑σ

Gluing a locally finite family of finite complexes gives a complex whose simplices form a locally finite family.

theorem Geometry.SimplicialComplex.inter_convexHull_subset_convexHull_option {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {J : Type u_4} (L : SimplicialComplex 𝕜 E) (T : J → SimplicialComplex 𝕜 E) (C : J → Set E) (hT : ∀ (j : J), (T j).space = C j) (hCC : Pairwise fun (j k : J) => C j ∩ C k ⊆ L.space) (hdesc : ∀ (j : J) ⦃s : Finset E⦄ ⦃x : E⦄, s ∈ (T j).faces → x ∈ (convexHull 𝕜) ↑s → x ∈ L.space → ∃ t ⊆ s, t ∈ L.faces ∧ x ∈ (convexHull 𝕜) ↑t) (a b : Option J) ⦃s t : Finset E⦄ (hs : s ∈ (a.elim L T).faces) (ht : t ∈ (b.elim L T).faces) : (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)

The faces of the pieces L and T j of a glued family meet compatibly, provided distinct pieces T j, T k meet inside |L| and a point of |L| carried by a face of a piece is carried by a subface which is a face of L.

theorem Geometry.SimplicialComplex.locallyFinite_convexHull_of_finite_restrict {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {K L : SimplicialComplex 𝕜 E} {P : ι → Set E} (hPv : ∀ (i : ι), Convex 𝕜 (P i)) (hP : LocallyFinite P) (hL : LocallyFinite fun (σ : ↑L.faces) => (convexHull 𝕜) ↑↑σ) (hfin : ∀ (i : ι), (K.restrict (P i)).faces.Finite) (hK : ∀ s ∈ K.faces, s ∈ L.faces ∨ ∃ (i : ι), ↑s ⊆ P i) : LocallyFinite fun (σ : ↑K.faces) => (convexHull 𝕜) ↑↑σ

A complex whose simplices are those of a locally finite complex L or lie in the cells of a locally finite family of convex sets, with finitely many simplices in each cell, is locally finite.

theorem Geometry.SimplicialComplex.finite_faces_restrict_of_forall_lt {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {L K : SimplicialComplex 𝕜 E} {P : ι → Set E} (d : ι → ℕ) {n : ℕ} (k : ι) (hPc : IsCompact (P k)) (hPlf : LocallyFinite P) (hLfin : (L.restrict (P k)).faces.Finite) (hKP : ∀ (k : ι), d k < n → (K.restrict (P k)).faces.Finite) (hKf : ∀ s ∈ K.faces, s ∈ L.faces ∨ ∃ (k : ι), d k < n ∧ ↑s ⊆ P k) : (K.restrict (P k)).faces.Finite

The restriction of K to a cell P k has finitely many faces, if P k is compact, the cells are locally finite, the restriction of L to P k has finitely many faces, the restriction of K to every cell P m with d m < n has finitely many faces, and every face of K is a face of L or lies in such a cell.

theorem Geometry.SimplicialComplex.convexHull_inter_convexHull_subset_of_isExtreme {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Finset E} {K L : SimplicialComplex 𝕜 E} (hKL : ∀ x ∈ K.space ∩ L.space, ∃ (F : Set E), x ∈ F ∧ IsExtreme 𝕜 K.space F ∧ IsExtreme 𝕜 L.space F ∧ K.restrict F ≤ L.restrict F) (hs : s ∈ K.faces) (ht : t ∈ L.faces) : (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)

Two simplicial complexes K and L meet properly if every point of |K| ∩ |L| lies in a set F which is an extreme subset of both |K| and |L| and such that every face of K with all vertices in F is a face of L: the convex hulls of a face of K and a face of L then meet inside the convex hull of their common vertices.

theorem Geometry.SimplicialComplex.inter_subset_convexHull_of_isExtreme {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : ι → SimplicialComplex 𝕜 E} (hK : Pairwise fun (i j : ι) => ∀ x ∈ (K i).space ∩ (K j).space, ∃ (F : Set E), x ∈ F ∧ IsExtreme 𝕜 (K i).space F ∧ IsExtreme 𝕜 (K j).space F ∧ (K i).restrict F ≤ (K j).restrict F) (i j : ι) ⦃s t : Finset E⦄ (hs : s ∈ (K i).faces) (ht : t ∈ (K j).faces) : (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)

Suppose that for any two distinct complexes K i and K j of a family, every point of |K i| ∩ |K j| lies in a common extreme subset F of |K i| and |K j| such that the faces of K i with all vertices in F are faces of K j. Then the faces of the family pairwise meet properly, so the family can be glued.

theorem Geometry.SimplicialComplex.restrict_glue {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : ι → SimplicialComplex 𝕜 E} (hK : Pairwise fun (i j : ι) => ∀ x ∈ (K i).space ∩ (K j).space, ∃ (F : Set E), x ∈ F ∧ IsExtreme 𝕜 (K i).space F ∧ IsExtreme 𝕜 (K j).space F ∧ (K i).restrict F ≤ (K j).restrict F) {i : ι} {F : Set E} (hF : Convex 𝕜 F) (hFi : F ⊆ (K i).space) : (glue K ⋯).restrict F = (K i).restrict F

Gluing a family of complexes along common extreme subsets of their spaces does not change the restriction of any piece K i to a convex subset of |K i|. In particular, prescribed triangulations of the faces of the pieces survive in the glued complex.