Simplicial complexes

In this file, we define simplicial complexes in 𝕜-modules. A simplicial complex is a collection of simplices closed by inclusion (of vertices) and intersection (of underlying sets).

We model them by a downward-closed set of affine independent finite sets whose convex hulls "glue nicely", each finite set and its convex hull corresponding respectively to the vertices and the underlying set of a simplex.

Main declarations

• SimplicialComplex 𝕜 E: A simplicial complex in the 𝕜-module E.
• SimplicialComplex.vertices: The zero dimensional faces of a simplicial complex.
• SimplicialComplex.facets: The maximal faces of a simplicial complex.

Notation

s ∈ K means that s is a face of K.

K ≤ L means that the faces of K are faces of L.

Implementation notes

"glue nicely" usually means that the intersection of two faces (as sets in the ambient space) is a face. Given that we store the vertices, not the faces, this would be a bit awkward to spell. Instead, SimplicialComplex.inter_subset_convexHull is an equivalent condition which works on the vertices.

TODO

Simplicial complexes can be generalized to affine spaces once ConvexHull has been ported.

structure Geometry.SimplicialComplex (𝕜 : Type u_1) (E : Type u_2) [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : Type u_2

A simplicial complex in a 𝕜-module is a collection of simplices which glue nicely together. Note that the textbook meaning of "glue nicely" is given in Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull. It is mostly useless, as Geometry.SimplicialComplex.convexHull_inter_convexHull is enough for all purposes.

• faces : Set (Finset E)

  the faces of this simplicial complex: currently, given by their spanning vertices

• not_empty_mem : ∅ ∉ self.faces

  the empty set is not a face: hence, all faces are non-empty

• indep : ∀ {s : Finset E}, s ∈ self.faces → AffineIndependent 𝕜 Subtype.val

  the vertices in each face are affine independent: this is an implementation detail

• down_closed : ∀ {s t : Finset E}, s ∈ self.faces → t ⊆ s → t ≠ ∅ → t ∈ self.faces

  faces are downward closed: a non-empty subset of its spanning vertices spans another face

• inter_subset_convexHull : ∀ {s t : Finset E}, s ∈ self.faces → t ∈ self.faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)

theorem Geometry.SimplicialComplex.ext {𝕜 : Type u_1} {E : Type u_2} : ∀ {inst : OrderedRing 𝕜} {inst_1 : AddCommGroup E} {inst_2 : Module 𝕜 E} {x y : Geometry.SimplicialComplex 𝕜 E}, x.faces = y.faces → x = y

theorem Geometry.SimplicialComplex.not_empty_mem {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (self : Geometry.SimplicialComplex 𝕜 E) : ∅ ∉ self.faces

the empty set is not a face: hence, all faces are non-empty

theorem Geometry.SimplicialComplex.indep {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (self : Geometry.SimplicialComplex 𝕜 E) {s : Finset E} : s ∈ self.faces → AffineIndependent 𝕜 Subtype.val

the vertices in each face are affine independent: this is an implementation detail

theorem Geometry.SimplicialComplex.down_closed {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (self : Geometry.SimplicialComplex 𝕜 E) {s : Finset E} {t : Finset E} : s ∈ self.faces → t ⊆ s → t ≠ ∅ → t ∈ self.faces

faces are downward closed: a non-empty subset of its spanning vertices spans another face

theorem Geometry.SimplicialComplex.inter_subset_convexHull {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (self : Geometry.SimplicialComplex 𝕜 E) {s : Finset E} {t : Finset E} : s ∈ self.faces → t ∈ self.faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)

instance Geometry.SimplicialComplex.instMembershipFinset {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : Membership (Finset E) (Geometry.SimplicialComplex 𝕜 E)

A Finset belongs to a SimplicialComplex if it's a face of it.

Equations

• Geometry.SimplicialComplex.instMembershipFinset = { mem := fun (K : Geometry.SimplicialComplex 𝕜 E) (s : Finset E) => s ∈ K.faces }

def Geometry.SimplicialComplex.space {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (K : Geometry.SimplicialComplex 𝕜 E) : Set E

The underlying space of a simplicial complex is the union of its faces.

Equations

• K.space = ⋃ s ∈ K.faces, (convexHull 𝕜) ↑s

theorem Geometry.SimplicialComplex.mem_space_iff {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {x : E} : x ∈ K.space ↔ ∃ s ∈ K.faces, x ∈ (convexHull 𝕜) ↑s

theorem Geometry.SimplicialComplex.convexHull_subset_space {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E} (hs : s ∈ K.faces) : (convexHull 𝕜) ↑s ⊆ K.space

theorem Geometry.SimplicialComplex.subset_space {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E} (hs : s ∈ K.faces) : ↑s ⊆ K.space

theorem Geometry.SimplicialComplex.convexHull_inter_convexHull {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E} {t : Finset E} (hs : s ∈ K.faces) (ht : t ∈ K.faces) : (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) (↑s ∩ ↑t)

theorem Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E} {t : Finset E} (hs : s ∈ K.faces) (ht : t ∈ K.faces) : Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∨ ∃ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) ↑u

The conclusion is the usual meaning of "glue nicely" in textbooks. It turns out to be quite unusable, as it's about faces as sets in space rather than simplices. Further, additional structure on 𝕜 means the only choice of u is s ∩ t (but it's hard to prove).

def Geometry.SimplicialComplex.ofErase {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (faces : Set (Finset E)) (indep : ∀ s ∈ faces, AffineIndependent 𝕜 Subtype.val) (down_closed : ∀ s ∈ faces, ∀ t ⊆ s, t ∈ faces) (inter_subset_convexHull : ∀ s ∈ faces, ∀ t ∈ faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)) : Geometry.SimplicialComplex 𝕜 E

Construct a simplicial complex by removing the empty face for you.

Equations

• Geometry.SimplicialComplex.ofErase faces indep down_closed inter_subset_convexHull = { faces := faces \ {∅}, not_empty_mem := ⋯, indep := ⋯, down_closed := ⋯, inter_subset_convexHull := ⋯ }

@[simp]

theorem Geometry.SimplicialComplex.ofErase_faces {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (faces : Set (Finset E)) (indep : ∀ s ∈ faces, AffineIndependent 𝕜 Subtype.val) (down_closed : ∀ s ∈ faces, ∀ t ⊆ s, t ∈ faces) (inter_subset_convexHull : ∀ s ∈ faces, ∀ t ∈ faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)) : (Geometry.SimplicialComplex.ofErase faces indep down_closed inter_subset_convexHull).faces = faces \ {∅}

def Geometry.SimplicialComplex.ofSubcomplex {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (K : Geometry.SimplicialComplex 𝕜 E) (faces : Set (Finset E)) (subset : faces ⊆ K.faces) (down_closed : ∀ {s t : Finset E}, s ∈ faces → t ⊆ s → t ∈ faces) : Geometry.SimplicialComplex 𝕜 E

Construct a simplicial complex as a subset of a given simplicial complex.

Equations

• K.ofSubcomplex faces subset down_closed = { faces := faces, not_empty_mem := ⋯, indep := ⋯, down_closed := ⋯, inter_subset_convexHull := ⋯ }

@[simp]

theorem Geometry.SimplicialComplex.ofSubcomplex_faces {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (K : Geometry.SimplicialComplex 𝕜 E) (faces : Set (Finset E)) (subset : faces ⊆ K.faces) (down_closed : ∀ {s t : Finset E}, s ∈ faces → t ⊆ s → t ∈ faces) : (K.ofSubcomplex faces subset down_closed).faces = faces

Vertices

def Geometry.SimplicialComplex.vertices {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (K : Geometry.SimplicialComplex 𝕜 E) : Set E

The vertices of a simplicial complex are its zero dimensional faces.

Equations

• K.vertices = {x : E | {x} ∈ K.faces}

theorem Geometry.SimplicialComplex.mem_vertices {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {x : E} : x ∈ K.vertices ↔ {x} ∈ K.faces

theorem Geometry.SimplicialComplex.vertices_eq {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} : K.vertices = ⋃ k ∈ K.faces, ↑k

theorem Geometry.SimplicialComplex.vertices_subset_space {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} : K.vertices ⊆ K.space

theorem Geometry.SimplicialComplex.vertex_mem_convexHull_iff {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E} {x : E} (hx : x ∈ K.vertices) (hs : s ∈ K.faces) : x ∈ (convexHull 𝕜) ↑s ↔ x ∈ s

theorem Geometry.SimplicialComplex.face_subset_face_iff {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E} {t : Finset E} (hs : s ∈ K.faces) (ht : t ∈ K.faces) : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t ↔ s ⊆ t

A face is a subset of another one iff its vertices are.

Facets

def Geometry.SimplicialComplex.facets {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (K : Geometry.SimplicialComplex 𝕜 E) : Set (Finset E)

A facet of a simplicial complex is a maximal face.

Equations

• K.facets = {s : Finset E | s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t}

theorem Geometry.SimplicialComplex.mem_facets {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E} : s ∈ K.facets ↔ s ∈ K.faces ∧ ∀ t ∈ K.faces, s ⊆ t → s = t

theorem Geometry.SimplicialComplex.facets_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} : K.facets ⊆ K.faces

theorem Geometry.SimplicialComplex.not_facet_iff_subface {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E} (hs : s ∈ K.faces) : s ∉ K.facets ↔ ∃ t ∈ K.faces, s ⊂ t

The semilattice of simplicial complexes

K ≤ L means that K.faces ⊆ L.faces.

instance Geometry.SimplicialComplex.instInf (𝕜 : Type u_1) (E : Type u_2) [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : Inf (Geometry.SimplicialComplex 𝕜 E)

The complex consisting of only the faces present in both of its arguments.

Equations

• One or more equations did not get rendered due to their size.

instance Geometry.SimplicialComplex.instSemilatticeInf (𝕜 : Type u_1) (E : Type u_2) [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : SemilatticeInf (Geometry.SimplicialComplex 𝕜 E)

Equations

• Geometry.SimplicialComplex.instSemilatticeInf 𝕜 E = SemilatticeInf.mk ⋯ ⋯ ⋯

instance Geometry.SimplicialComplex.hasBot (𝕜 : Type u_1) (E : Type u_2) [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : Bot (Geometry.SimplicialComplex 𝕜 E)

Equations

• Geometry.SimplicialComplex.hasBot 𝕜 E = { bot := { faces := ∅, not_empty_mem := ⋯, indep := ⋯, down_closed := ⋯, inter_subset_convexHull := ⋯ } }

instance Geometry.SimplicialComplex.instOrderBot (𝕜 : Type u_1) (E : Type u_2) [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : OrderBot (Geometry.SimplicialComplex 𝕜 E)

Equations

• Geometry.SimplicialComplex.instOrderBot 𝕜 E = OrderBot.mk ⋯

instance Geometry.SimplicialComplex.instInhabited (𝕜 : Type u_1) (E : Type u_2) [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : Inhabited (Geometry.SimplicialComplex 𝕜 E)

Equations

• Geometry.SimplicialComplex.instInhabited 𝕜 E = { default := ⊥ }

theorem Geometry.SimplicialComplex.faces_bot {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : ⊥.faces = ∅

theorem Geometry.SimplicialComplex.space_bot {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : ⊥.space = ∅

theorem Geometry.SimplicialComplex.facets_bot {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : ⊥.facets = ∅