Definition of Simplicial Complex

Stream: mathlib4

[Bolton Bailey]

I'm working on #33364 where I am refactoring the definition of docs#SimplicialComplex , which is currently

structure SimplicialComplex where
  /-- the faces of this simplicial complex: currently, given by their spanning vertices -/
  faces : Set (Finset E)
  /-- the empty set is not a face: hence, all faces are non-empty -/
  empty_notMem : ∅ ∉ faces
  /-- the vertices in each face are affine independent: this is an implementation detail -/
  indep : ∀ {s}, s ∈ faces → AffineIndependent 𝕜 ((↑) : s → E)
  /-- faces are downward closed: a non-empty subset of its spanning vertices spans another face -/
  down_closed : ∀ {s t}, s ∈ faces → t ⊆ s → t.Nonempty → t ∈ faces
  inter_subset_convexHull : ∀ {s t}, s ∈ faces → t ∈ faces →
    convexHull 𝕜 ↑s ∩ convexHull 𝕜 ↑t ⊆ convexHull 𝕜 (s ∩ t : Set E)

@Eric Wieser points out that we could drop the empty_notMem condition, then simplify the down_closed condition to IsLowerSet faces. We might even be able to refactor the definition as an extension of docs#LowerSet (or an extension of a new AbstractSimplicialComplex type extending LowerSet).

There are a couple ways I could see to do this.

• Do this without any other changes. This means that now the emptyset is considered to be included in all Simplicial Complexes, except for a new complex which is empty.
• Do this but add a requirement that emptyset is in the set of faces. This means hat now the emptyset is considered to be included in all Simplicial Complexes, which are in bijection with how it was defined before.

Is it a problem, mathematically, to have simplicial complexes defined this way? The drawback I know of for sure is that Wikipedia does not seem to define it with emptyset allowed, so possibly this is a well known convention that will confuse people to see.

[Eric Wieser]

If you haven't already done so, I'll try a refactor to see what in mathlib breaks

[Bolton Bailey]

Go for it, but I think SimplicialComplex is currently a leaf file so I am thinking more about the future.

[Eric Wieser]

#35115 has an initial cleanup

[Eric Wieser]

#35116 is another orthogonal cleanup to the same file

[Eric Wieser]

Good point about it being a leaf file, and so this not being a very valuable experiment

[Eric Wieser]

cc @Bhavik Mehta and @Yaël Dillies, as authors of docs#Geometry.SimplicialComplex

[Eric Wieser]

Bolton Bailey said:

• This means that now the emptyset is considered to be included in all Simplicial Complexes, except for a new complex which is empty.

My take is that we should do this, for the same reason that we do for docs#Filter. In the rare case where this extra complex is annoying, we can use NeBot just as we do for filters.

[Vlad Tsyrklevich]

These trivial complexes have names btw, the void and irrelevant complexes for the complexes that do not even include emptyset as a face and the one that only includes emptyset as a face. The suspension of the irrelevant complex is two points, e.g. an S^0, so in a sense the irrelevant complex is an S^{-1}.

[Kevin Buzzard]

Right -- if we allow the empty set then all of a sudden we have simplices with dimension -1 which might cause more pain elsewhere.

[Edward van de Meent]

something something WithBot Nat

[Ben Eltschig]

Vlad Tsyrklevich said:

These trivial complexes have names btw, the void and irrelevant complexes for the complexes that do not even include emptyset as a face and the one that only includes emptyset as a face. The suspension of the irrelevant complex is two points, e.g. an S^0, so in a sense the irrelevant complex is an S^{-1}.

Just to make sure I understand that right - this void complex would be the only new complex we're gaining, right? And it has a unique map to every other complex, but no other complex has a map to it - so categorically, what this would do is freely adjoin an initial object to a category that already has one?

[Violeta Hernández]

Kevin Buzzard said:

Right -- if we allow the empty set then all of a sudden we have simplices with dimension -1 which might cause more pain elsewhere.

The theory of abstract polytopes requires that every abstract polytope has a top and bottom; the bottom element is traditionally considered to have rank/dimension -1. So there is precedent to this!

[Ben Eltschig]

This feels very related to the distinction between simplicial sets as presheaves on docs#SimplexCategory and augmented simplicial sets as presheaves on docs#AugmentedSimplexCategory, but I must say I've never quite understood the advantages of the latter - I've just always worked with plain simplicial sets instead. I think one advantage in that context is that the empty simplex functions as the unit of a monoidal structure you otherwise wouldn't have, but is that all or is there more to the distinction that would also apply to simplicial complexes?

[Ben Eltschig]

(I'm just asking this out of curiosity by the way - I think I've already seen enough to be convinced that removing the empty_notMem condition is at the very least not a bad idea)

[Vlad Tsyrklevich]

Ben Eltschig said:

Vlad Tsyrklevich said:

These trivial complexes have names btw, the void and irrelevant complexes for the complexes that do not even include emptyset as a face and the one that only includes emptyset as a face. The suspension of the irrelevant complex is two points, e.g. an S^0, so in a sense the irrelevant complex is an S^{-1}.

Just to make sure I understand that right - this void complex would be the only new complex we're gaining, right? And it has a unique map to every other complex, but no other complex has a map to it - so categorically, what this would do is freely adjoin an initial object to a category that already has one?

My reading was the other way around. I believe the definition in the original message allows void but not irrelevant. Irrelevant seems useful to have (you want a bottom element/closure under intersection) and void I have no idea if it’s ever useful

[Ben Eltschig]

Oh, right - void is the initial object in both categories then I guess, and irrelevant a postinitial object with unique maps to everything but void. Looks like the category you get is still isomorphic to the usual category of simplicial complexes with an initial object adjoined though, what I got wrong is just which object is called what

[Bolton Bailey]

Dimension for simplicial complexes seems complicated. We already have the irrelevant complex which has, I think, dimension -1, and the question is whether to allow the void complex (with an even lower dimension?). But also we can have complexes with no bound on the size of their faces, so I guess it is not even possible to define dimension as a function at all currently, perhaps this is something else we want to change.

[Weiyi Wang]

WithBot (WithBot Nat) incoming

[Ben Eltschig]

WithBot (WithBot ENat) in order to cover complexes without an dimension bound as well :)

[Vlad Tsyrklevich]

I’m not sure we need void. For example, https://en.wikipedia.org/wiki/Independence_system explicitly disallows it. Is there some natural construction by which you get a void complex back?

[Vlad Tsyrklevich]

Void just feels very odd to me, defining a simplicial cone operator for example doesn’t behave very well with it, the normal construction would force you to define the cone of void as a point and then you’ve gone up 2 in dimension and it’s equal to the cone of the irrelevant complex. You could define it to be the irrelevant complex but this feels arbitrary

[Ben Eltschig]

I guess I don't quite understand the join of simplicial complexes (cones are just joins with a point, right?) well enough yet: without (-1)-dimensional faces I would've defined it as "a set is a face of the join of K and L iff it is a face of K, a face of L or the disjoint union of a face of K with a face of L", and I briefly thought that if you include the (-1)-dimensional face this simplifies to "the faces of the join of K and L are precisely the disjoint unions of faces of K with faces of L", but then due to void having no faces any join with void would have no faces either, which I feel would be bad because then the set of vertices of a join is suddenly no longer the disjoint union of the two vertex sets

[Ben Eltschig]

At least abstractly, I feel like void is very natural to include though. Simplicial complexes without empty faces can be viewed (up to equivalence of categories) as concrete presheaves on the category of nonempty finite sets, and simplicial complexes with potentially empty faces as concrete presheaves on the full category of finite sets: in both cases the initial object is the constant presheaf on the empty set, i.e. a complex with no faces at all. Since such a concrete presheaf exists on any concrete site, I don't think it's possible to maintain this view of simplicial complexes as concrete presheaves while disallowing void

[Damiano Testa]

In my experience, the void and the irrelevant simplicial complex are very different.

The void complex, the one that does not even contain the empty face, is "contractible", while the irrelevant complex is "the -1-dimensional sphere".

You can also tell the difference between them by computing the Euler characteristic of their face complexes.

However, I am not sure why there would have to be two nested WithBots. Maybe it is enough to have -1, and above. Whether or not you want to add an infinity is a different matter.

[Aaron Liu]

clearly the void complex is -2 dimensional

[Damiano Testa]

I would have said that since its suspension is the 0-dimensional sphere and suspension increases dimension by 1, that its dimension would be -1.

[Damiano Testa]

Ah, sorry, void, not irrelevant!

[Aaron Liu]

Damiano Testa said:

The void complex, the one that does not even contain the empty face, is "contractible", while the irrelevant complex is "the -1-dimensional sphere".

What is "contractible"?

[Damiano Testa]

A space is contractible is the identity map is homotopic to a constant map.

[Damiano Testa]

However, in the case of abstract simplicial complexes, you can read off a lot of topological information from the face complex and that normally works well also for the "degenerate" cases, giving you ways into getting induction arguments for instance starting at the void or irrelevant complex and yielding meaningful information for all complexes/

[Aaron Liu]

I don't think the void complex would be docs#ContractibleSpace

[Aaron Liu]

because it has no vertices

[Damiano Testa]

I think that it would be according to the wikipedia definition of contractible:

https://en.wikipedia.org/wiki/Contractible_space

[Ben Eltschig]

Mathlib uses the definition "homotopy-equivalent to a point", so every contractible space is in particular nonempty

[Aaron Liu]

I think it is standard to require contractible spaces to be nonempty

[Kim Morrison]

The empty space is only "precontractible".

[Bhavik Mehta]

Let me mention that the choice of allowing empty in simplicial complexes has come up a few times in the past:

• #maths > Simplicial complex @ 💬
• #PR reviews > #9762 simplicial complex @ 💬
• #maths > Abstract Simplicial Complex @ 💬