mathlib documentation

analysis.convex.simplicial_complex.basic

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 #

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, simplicial_complex.inter_subset_convex_hull is an equivalent condition which works on the vertices.

TODO #

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

theorem geometry.simplicial_complex.ext_iff {π•œ : Type u_1} {E : Type u_2} {_inst_1 : ordered_ring π•œ} {_inst_2 : add_comm_group E} {_inst_3 : module π•œ E} (x y : geometry.simplicial_complex π•œ E) :
x = y ↔ x.faces = y.faces
@[ext]
structure geometry.simplicial_complex (π•œ : Type u_1) (E : Type u_2) [ordered_ring π•œ] [add_comm_group 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.simplicial_complex.disjoint_or_exists_inter_eq_convex_hull. It is mostly useless, as geometry.simplicial_complex.convex_hull_inter_convex_hull is enough for all purposes.

Instances for geometry.simplicial_complex
theorem geometry.simplicial_complex.ext {π•œ : Type u_1} {E : Type u_2} {_inst_1 : ordered_ring π•œ} {_inst_2 : add_comm_group E} {_inst_3 : module π•œ E} (x y : geometry.simplicial_complex π•œ E) (h : x.faces = y.faces) :
x = y
@[protected, instance]
def geometry.simplicial_complex.has_mem {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] :

A finset belongs to a simplicial_complex if it's a face of it.

Equations
def geometry.simplicial_complex.space {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (K : geometry.simplicial_complex π•œ E) :
set E

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

Equations
theorem geometry.simplicial_complex.mem_space_iff {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} {x : E} :
x ∈ K.space ↔ βˆƒ (s : finset E) (H : s ∈ K.faces), x ∈ ⇑(convex_hull π•œ) ↑s
theorem geometry.simplicial_complex.convex_hull_subset_space {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} {s : finset E} (hs : s ∈ K.faces) :
@[protected]
theorem geometry.simplicial_complex.subset_space {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} {s : finset E} (hs : s ∈ K.faces) :
theorem geometry.simplicial_complex.convex_hull_inter_convex_hull {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} {s t : finset E} (hs : s ∈ K.faces) (ht : t ∈ K.faces) :
theorem geometry.simplicial_complex.disjoint_or_exists_inter_eq_convex_hull {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} {s t : finset E} (hs : s ∈ K.faces) (ht : t ∈ K.faces) :
disjoint (⇑(convex_hull π•œ) ↑s) (⇑(convex_hull π•œ) ↑t) ∨ βˆƒ (u : finset E) (H : u ∈ K.faces), ⇑(convex_hull π•œ) ↑s ∩ ⇑(convex_hull π•œ) ↑t = ⇑(convex_hull π•œ) ↑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.simplicial_complex.of_erase {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (faces : set (finset E)) (indep : βˆ€ (s : finset E), s ∈ faces β†’ affine_independent π•œ coe) (down_closed : βˆ€ (s : finset E), s ∈ faces β†’ βˆ€ (t : finset E), t βŠ† s β†’ t ∈ faces) (inter_subset_convex_hull : βˆ€ (s : finset E), s ∈ faces β†’ βˆ€ (t : finset E), t ∈ faces β†’ ⇑(convex_hull π•œ) ↑s ∩ ⇑(convex_hull π•œ) ↑t βŠ† ⇑(convex_hull π•œ) (↑s ∩ ↑t)) :

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

Equations
@[simp]
theorem geometry.simplicial_complex.of_erase_faces {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (faces : set (finset E)) (indep : βˆ€ (s : finset E), s ∈ faces β†’ affine_independent π•œ coe) (down_closed : βˆ€ (s : finset E), s ∈ faces β†’ βˆ€ (t : finset E), t βŠ† s β†’ t ∈ faces) (inter_subset_convex_hull : βˆ€ (s : finset E), s ∈ faces β†’ βˆ€ (t : finset E), t ∈ faces β†’ ⇑(convex_hull π•œ) ↑s ∩ ⇑(convex_hull π•œ) ↑t βŠ† ⇑(convex_hull π•œ) (↑s ∩ ↑t)) :
(geometry.simplicial_complex.of_erase faces indep down_closed inter_subset_convex_hull).faces = faces \ {βˆ…}
@[simp]
theorem geometry.simplicial_complex.of_subcomplex_faces {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (K : geometry.simplicial_complex π•œ E) (faces : set (finset E)) (subset : faces βŠ† K.faces) (down_closed : βˆ€ {s t : finset E}, s ∈ faces β†’ t βŠ† s β†’ t ∈ faces) :
(K.of_subcomplex faces subset down_closed).faces = faces
def geometry.simplicial_complex.of_subcomplex {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (K : geometry.simplicial_complex π•œ E) (faces : set (finset E)) (subset : faces βŠ† K.faces) (down_closed : βˆ€ {s t : finset E}, s ∈ faces β†’ t βŠ† s β†’ t ∈ faces) :

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

Equations

Vertices #

def geometry.simplicial_complex.vertices {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (K : geometry.simplicial_complex π•œ E) :
set E

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

Equations
theorem geometry.simplicial_complex.mem_vertices {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} {x : E} :
theorem geometry.simplicial_complex.vertices_eq {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} :
K.vertices = ⋃ (k : finset E) (H : k ∈ K.faces), ↑k
theorem geometry.simplicial_complex.vertices_subset_space {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} :
theorem geometry.simplicial_complex.vertex_mem_convex_hull_iff {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} {s : finset E} {x : E} (hx : x ∈ K.vertices) (hs : s ∈ K.faces) :
theorem geometry.simplicial_complex.face_subset_face_iff {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} {s t : finset E} (hs : s ∈ K.faces) (ht : t ∈ K.faces) :

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

Facets #

def geometry.simplicial_complex.facets {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] (K : geometry.simplicial_complex π•œ E) :

A facet of a simplicial complex is a maximal face.

Equations
theorem geometry.simplicial_complex.mem_facets {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} {s : finset E} :
s ∈ K.facets ↔ s ∈ K.faces ∧ βˆ€ (t : finset E), t ∈ K.faces β†’ s βŠ† t β†’ s = t
theorem geometry.simplicial_complex.facets_subset {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} :
theorem geometry.simplicial_complex.not_facet_iff_subface {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] {K : geometry.simplicial_complex π•œ E} {s : finset E} (hs : s ∈ K.faces) :
s βˆ‰ K.facets ↔ βˆƒ (t : finset E), t ∈ K.faces ∧ s βŠ‚ t

The semilattice of simplicial complexes #

K ≀ L means that K.faces βŠ† L.faces.

@[protected, instance]
def geometry.simplicial_complex.has_inf (π•œ : Type u_1) (E : Type u_2) [ordered_ring π•œ] [add_comm_group E] [module π•œ E] :

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

Equations
@[protected, instance]
def geometry.simplicial_complex.has_bot (π•œ : Type u_1) (E : Type u_2) [ordered_ring π•œ] [add_comm_group E] [module π•œ E] :
Equations
@[protected, instance]
def geometry.simplicial_complex.order_bot (π•œ : Type u_1) (E : Type u_2) [ordered_ring π•œ] [add_comm_group E] [module π•œ E] :
Equations
@[protected, instance]
def geometry.simplicial_complex.inhabited (π•œ : Type u_1) (E : Type u_2) [ordered_ring π•œ] [add_comm_group E] [module π•œ E] :
Equations
theorem geometry.simplicial_complex.faces_bot {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] :
theorem geometry.simplicial_complex.space_bot {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] :
theorem geometry.simplicial_complex.facets_bot {π•œ : Type u_1} {E : Type u_2} [ordered_ring π•œ] [add_comm_group E] [module π•œ E] :