The goal of this project is to introduce abstract simplicial complexes and to prove some results about them; the main goal is shellability and its application to the calculation of the Euler-Poincaré characteristic. We also introduce the category of abstract simplicial complexes, prove that it is equivalence to the category of concrete presheaves on the category of nonempty fintypes, and construct the geometric realization as a left Kan extension of the obvious functor on nonempty fintype.
Here is a quick description of the files in alphabetical order:
This file contains basic definitions and results about abstract simplicial complexes.
Definitions:
- The structure of an abstract simplicial complex, as well as faces, facets, vertices.
- Partial order on abstract simplicial complexes (on a fixed type) and CompleteDistribLattice structure on them.
- Finite complexes (= having a finite set of faces).
- Dimension (the iSup in ENat of the function sending a face s to card(s)-1).
- A finite complex is finite dimensional.
- Pure complexes (a complex is pure if its dimension is equal to card(s)-1 for every facet s).
- n-skeleton.
- Link of a face.
- Possibly infinite simplex on a type (i.e. the set of finite subsets of the type). This is used to define the functor from nonempty fintypes to abstract simplicial complexes.
- Simplicial map: this is defined as a map on vertices and a map on faces satisfying two compatiblities. (It was simpler in the categorical file later.) Composition and identity are also defined.
- Subcomplex generated by a set of faces.
- Boundary of a face (as a subcomplex).
There are also some basic properties of these notions.
Imports FacePoset, FintypeNECat and Equivalence.
This contains the definition of the category of abstract simplicial complexes, the construction of its equivalence with the category of concrete presheaves on FintypeNECat (the category of nonempty fintypes), and the definition of the geometric realization.
Main definitions and results:
- AbstractSimplicialComplexCat: The category of abstract simplicial complexes (in a universe u).
- Forgetful functor to types (sending an abstract simplicial complex to its set of vertices).
- Forgetful functor to partially ordered types (sending an abstract simplicial complex to its face poset).
- Functor from FintypeNECat to the category of abstract simplicial complexes.
- Functor G from the category of abstract simplicial complexes to the category of presheaves on FintypeNECat (two definitions, an "obvious" abstract one and one better suited for calculations; we prove that they give isomorphic functors).
- Functor F from the category of presheaves on FintypeNECat to the category of abstract simplicial complexes.
- Adjunction between F and G.
- The counit of this adjunction is an isomorphism, hence F is a reflective functor.
- Definition of concrete presheaves.
- Proof that the full subcategory concrete presheaves is the essential image of F.
- Definition of the geometric realization functor on abstract simplicial complexes, as a left Kan extension of the functor sending a nonempty fintype to the corresponding topological simplex.
Imports FacePoset and OrderOnFacets.
An abstract simplicial K is called decomposable if there is map R (the restriction map) from the set of facets of K to the set {faces of K}\cup{emptyset} such that the set of faces of K is equal to the disjoint union [R(s),s] over all facets s. In that case, we also have a map DF ("distinguished facet") from faces of K to facets of K, sending a face t to the unique facet s such that t is in [R(s),s]. This files contains basic concepts about decomposability. We put both R and DF in the definition of a decomposable complex, then prove that R determines DF.
Main definitions and results:
- IsDecomposition: given maps R and DF, defines what it means for them to constitute a decomposition of K.
- Proof that R determines DF.
- Definition of face intervals and DecompositionIntervals (i.e. the intervals [R(s),s]).
- Proof that DF determines the DecompositionIntervals.
- If r is a (partial) order on facets, definition of what it means for r to be compatible with a decomposition: if s is a facet and t is a face of s, then DF(t) must be less than or equal to s (for the order r).
- If r is compatible with a decomposition, formula for the complex of old faces determined by r and a facet s (see OrderOnFacets): it is the complement in the boundary of s of the interval [R(s),s].
- As a consequence, the complex of old faces is either, or pure of dimension card(s)-1.
- Definition of a Pi0 facet: this is a facet s whose decomposition interval is the half-infinite inverval [<-,s]. It will contribute 1 to the Euler-Poincaré characteristic.
- Definition of a homology facet: this is a non-Pi0 facet s whose decomposition interval is equal to {s}. It will contribute (-1)^{card(s)-1} to the Euler-Poincaré characteristic.
- Characterization of Pi0 and hommology facets using the map R.
This contains a lemma about equivalences of categories: it proves that, if F:C->D is an equivalence of categories and E is a category, then composing by the (given) quasi-inverse of F gives an equivalence from Func(C,E) to Func(D,E).
Imports Decomposability.
- Definition of the Euler-Poincaré characteristic of a finite abstract simplicial complex (as the sum over all its faces t of (-1)^{card(t)-1}).
- Calculation of the Euler-Poincaré characteristic of a finite decomposable complex: it is equal to the cardinality of the set of Pi0 facets plus the sum over all homology facets s of (-1)^{card(s)-1}.
Imports AbstractSimplicialComplex.
General facts about the face poset of an abstract simplicial complex K.
Main definitions and results:
- Partial order instance on the set of faces of K.
- A simplicial map induces an OrderHom between face posets.
- The face poset of K is a LocallyFiniteOrder and a LocallyFiniteOrderBot.
- Every filter of the face poset is principal.
Results about ideals:
- Support of an order ideal I of the face poset: this is the union of all faces s in I.
- Every nonempty finset of the support of I is a face and an element of I.
- If I is principal generated by s, then its support is s.
- An ideal is equal to the set of faces of K contained in its support.
- An ideal is principal if and only if its support is finite.
- Any subideal of a principal ideal is principal.
- A face of K is a facet if and only the principal ideal that it generates is maximal.
- The set of all faces is an ideal if and only K is a (possibly infinite) simplex.
Results about Noetherian simplicial complexes (i.e. those with a Noetherian face poset):
- If K is Noetherian, then every face of K is contained in a facet.
- A finite or finite dimensional complex is Noetherian.
- If K is Noetherian and all its facets have the same dimension, then K is pure.
Some lemmas about preoders that I could not find in mathlib.
Main definitions and results:
- Total preorders satisfy trichotomy: if s is a total preorder, then for all a,b we have a<b, b<a or a and b are equivalent for the antisymmetrization of s.
- For a total preorder, we have \not(a \le b) if and only if b < a.
- Definition of a Noetherian preordered set: this means that the relation (a,b) |-> b < a is well-founded. (I.e. that there are no infinite strictly increasing sequences.)
- Definition of a "maximal nonproper" order ideal: this is an order ideal that is maximal among all (not necessarily proper) order ideals. This notion is only interesting for non-directed posets.
- Order ideals form an inductive set (every chain has an upper bound).
- Every order ideal is contained in a maximal nonproper order ideal.
- An order ideal that has a maximal element is principal generated by that element.
- An order filter that has a minimal element is principal generated by that element.
- A preordered set is Noetherian if and only if every order ideal is principal.
- The order embedding from a partially ordered set to the poset of its order ideals, given by sending an element to the principal ideal it generates.
- LocallyFiniteOrder and LocallyFiniteOrderBot instances on the type of finsets on a type.
Imports Decomposability.
Main definitions and results:
- Definition of a shelling order on the facets of a simplicial complex.
- Definition of the restriction map associated to a shelling order.
- Definition of the "distinguished facet" associated to a shelling order: it sends a face to the smallest facet containing it. We need the complex to be Noetherian for this to exist.
- Proof that a Noetherian complex with a shelling order is decomposable.
- Converse: if K is decomposable, if r is a well-order on its facets that is compatible with the decomposition, then r is a shelling order and the decomposition it defines is the original one.