Simplicial complex

Stream: maths

[Yaël Dillies]

I am about to start pouring branch#sperner-again into mathlib and wanted your opinion on two things:

1. Does this definition look right to you? It definitely does to me, but I've worked on it day and night for a month so my eye is far from fresh.

import analysis.convex.hull
import linear_algebra.affine_space.independent

variables (𝕜 E : Type*) [ordered_ring 𝕜] [add_comm_group E] [module 𝕜 E]

/-- A simplicial complex in a `𝕜`-module. -/
@[ext] structure simplicial_complex :=
(faces : set (finset E))
(indep : ∀ {X}, X ∈ faces → affine_independent 𝕜 (λ p, p : (X : set E) → E))
(down_closed : ∀ {X Y}, X ∈ faces → Y ⊆ X → Y ∈ faces)
(disjoint : ∀ {X Y}, X ∈ faces → Y ∈ faces →
  convex_hull 𝕜 ↑X ∩ convex_hull 𝕜 ↑Y ⊆ convex_hull 𝕜 (X ∩ Y : set E))

2. Where should it live? Instinctively, I'd say analysis.convex. (yeah, I took permanent residence here), but linear_algebra.affine_space. is also a candidate.

[Adam Topaz]

Have you considered formalizing "abstract simplicial complexes" in the sense of
https://en.wikipedia.org/wiki/Simplicial_complex ?

[Heather Macbeth]

(Adam, you mean https://en.wikipedia.org/wiki/Abstract_simplicial_complex ?)

[Adam Topaz]

Yes!

[Scott Morrison]

@Adam Topaz, what did you have in mind? Here's my abortive guess:

1. define SimplicialComplex (just as a Type bundled with a set of finsets in that Type, satisfying some axioms)
2. define maps of abstract simplicial complexes (and optionally define the category of abstract simplicial complexes)
3. then for any affine space E there is a SimplicialComplex consisting of the affine_independent finite sets in E
4. a map from some SimplicialComplex to the simplicial complex from (3) is then the same as @Yaël Dillies's definition, but without the disjoint axiom.
5. but I don't see how to set up the disjoint axiom without explicitly saying it!

[Adam Topaz]

TBH my thoughts about this are not completely organized.

I do think we shouuld have 1 and 2 (i.e. abstract simplicial complexes and morphisms and/or a category structure).

We could then think about defining something like a geometric realization constructed out of simplices in affine space (or any context where one can speak about convex combinations). I don't immediately see how to do this... maybe as some formal colimit or something?

And finally, we can consider embeddings of such geometric realizations into affine spaces, which should yield the above.

But as I said, I would have to digest this for a little longer...

[Scott Morrison]

Ah, yes, this is good. Scrap my point 3, and just ask for the pair (an-abstract-simplicial-complex, an-embedding-of-its-realization-into-E).

[Scott Morrison]

But I think that we shouldn't ask @Yaël Dillies to take this detour. This can be an equivalence proved after the fact once someone does abstract simplicial complexes.

[Scott Morrison]

@Yaël Dillies, what is the state of affine spaces in mathlib now? Can you make this definition in an affine space rather than a module yet?

[Adam Topaz]

For now, it should be easy enough to define abstract simplicial complexes and have the definition above extend it, right?

[Scott Morrison]

Yes, except that in an abstract simplicial complex you probably want to say that all singletons are faces, so you don't have an "ambient" type sitting around, being ignored by the morphisms.

[Scott Morrison]

(The wikipedia and nlab pages diverge on their treatment of this point.)

[Adam Topaz]

right, good point

[Yaël Dillies]

I have currently no use for abstract simplicial complexes. So my plan was to just ignore them hoping they would insert nicely later.

[Yaël Dillies]

Scott Morrison said:

Yes, except that in an abstract simplicial complex you probably want to say that all singletons are faces, so you don't have an "ambient" type sitting around, being ignored by the morphisms.

I agree on that precise point. It seems that we must separate the geometric embedding from the actual structure (which is just a downward-closed set of finsets). But then I don't know how to define a geometric embedding without... defining simplicial complexes.

[Yaël Dillies]

Scott Morrison said:

Yaël Dillies, what is the state of affine spaces in mathlib now? Can you make this definition in an affine space rather than a module yet?

No we can't.... I had to decide between generalizing to semimodules and generalizing to affine spaces, and I chose the forme (blame Yakov for wanting convexity over ℝ≥0 :stuck_out_tongue_closed_eyes:). Now we're stuck away from affine spaces until we define convex spaces. And, as Yury pointed out, we'll have a nondefeq diamond when going from vector spaces to convex spaces (either through semimodules or through affine spaces).

[Yaël Dillies]

Really, this is a whole second convexity refactor, that I foresee as being even more disruptive as the first one.

[Patrick Massot]

No we can't.... I had to decide between generalizing to semimodules and generalizing to affine spaces, and I chose the forme (blame Yakov for wanting convexity over ℝ≥0 :stuck_out_tongue_closed_eyes:).

This is really insane. Mathematically it makes no sense at all.

[Oliver Nash]

@Yakov Pechersky is there an easy way to explain the motivation for having convexity over a semiring?

[Yakov Pechersky]

Do you mean to ask about convexity without an underlying negation, or lack of commutativity?

[Oliver Nash]

I meant without negation, but the only context here I have is @Yaël Dillies remark so it's possible I'm asking the wrong question.

[Yakov Pechersky]

Screenshot_20211008-052524_Drive.jpg

[Oliver Nash]

IIUC, it sounds like you have a situation where convexity over ℝ was too restrictive and Yael has solved this for you. I'm wondering what that situation was because our affine space library requires negation so we have a blocker to stating convexity in that language.

[Yakov Pechersky]

Screenshot_20211008-052524_Drive.jpg

[Yakov Pechersky]

I'm having issues sending the screenshot (on a plane :small_airplane:️) so I don't know if it went through

[Oliver Nash]

I can't quite tell. What are the scalars in this :wait_one_second:️?

[Oliver Nash]

(arrived twice but I think if you're on a plane then this can wait :smile:)

[Yakov Pechersky]

T here is the tropical semiring, which in the paper is defined as over with_top real. But I don't think there is anything in the definition or theorem to preclude with_top nnreal from working (or nnrat or nat). This is for optimization theory, mixed integer programming, etc.

[Oliver Nash]

There is a definite cost to generalising to the case where we don't have negation. Is there a definite benefit?

[Oliver Nash]

Wait, nat scalars! I'm pretty sure a + b = 1 over nat doesn't have many solutions!

[Oliver Nash]

(incidentally I love that Mathlib is getting some optimization theory, integer programming)

[Yakov Pechersky]

If you want to say, okay, convex is solely on rings, I understand and won't push back. Of course one can state concavity without concave_on

[Yakov Pechersky]

I mean, concavity as the theorem above uses it, and "state" as solely in the context of the file that proves that theorem

[Yaël Dillies]

If the consensus is that getting rid of negation isn't the mathematical highway, we can make affine_space -> convex_space the instance and semimodule -> convex_space the def

[Yaël Dillies]

but I don't think we should push back the convexity refactor. I did a lot of work to eliminate negation where I could.

[Oliver Nash]

I'm not pushing in any direction for now. I just want to understand the various costs, benefits, motivations etc. I only ever think about convexity over the reals so I don't have good perspective yet.

[Yakov Pechersky]

I apologize for my misguided desire for generality, misplaced over pragmatic usage and results

[Yaël Dillies]

In my perspective, the cost of generalizing convexity to semimodules as it is is low as it is a matter of typeclasses (except for finset.center_mass that really needs some relooking). The cost of generalizing to affine spaces would have been higher, as it requires redefining the objects. The cost of generalizing to affine spaces now is still quite high, but I'd argue that this time it's splitable. First part is to define convex spaces and give their instances/defs given affine spaces/semimodules. Second part is generalizing the lemmas, which arguably will be quite hard but not harder than what generalizing to affine spaces would have been in the first place.

[Yaël Dillies]

(we should move to Convexity refactor)

[Oliver Nash]

Yakov Pechersky said:

I apologize for my misguided desire for generality, misplaced over pragmatic usage and results

Please don't apologize, and I certainly don't think it's fair to characterise any of your excellent work as misguided! I sincerely hope my inquiries here do not come across as critical, I'm really just trying to learn about motivations.

[Yaël Dillies]

One big question, should I use simplex?

[Yaël Dillies]

because currently I model simplices using finite independent sets, without ever mentioning simplex.

[Reid Barton]

This notion is definitely important and useful separately from (or alongside) the notion of an abstract simplicial complex. To avoid ambiguity, it can also be called a geometric simplicial complex.
Yaël Dillies said:

I am about to start pouring branch#sperner-again into mathlib and wanted your opinion on two things:

1. Does this definition look right to you? It definitely does to me, but I've worked on it day and night for a month so my eye is far from fresh.

There should be a condition that each X ∈ faces is nonempty, and down_closed needs a corresponding change also (Y should be assumed to be nonempty).

Usually one wants to assume either that the simplicial complex is finite or that it is at least locally finite--I'm not sure whether "locally finite" is meaningful in this level of generality. I guess these conditions can be added on separately.

2. Where should it live? Instinctively, I'd say analysis.convex. (yeah, I took permanent residence here), but linear_algebra.affine_space. is also a candidate.

I don't see any analysis here. How about geometry.convex?

[Reid Barton]

Yaël Dillies said:

One big question, should I use simplex?

It looks like simplex is ordered, so it doesn't really fit well, I think.

[Yaël Dillies]

Reid Barton said:

There should be a condition that each X ∈ faces is nonempty, and down_closed needs a corresponding change also (Y should be assumed to be nonempty).

What's your incentive? We found it to be quite convenient to allow the empty face.

[Yaël Dillies]

This does look like Bourbaki forbiding univ to be a filter.

[Reid Barton]

Well a simplicial complex is a set of simplices, and the empty set is not a simplex (e.g. it's not contractible). If you allow then you should say you have something like an "augmented simplicial complex". What's your motivation for allowing it?

[Reid Barton]

Another option would be to require the empty set to belong to faces--that's decidedly nonstandard but in a way that doesn't make any real difference, because we could always throw it out and get a simplicial complex in the usual sense.

[Reid Barton]

I think arguably the "correct" thing to do is perhaps to work with simplicial complexes modulo whether or not they contain the empty set, but in practice everyone implements this by forbidding it (because it isn't a simplex).

[Reid Barton]

If you don't have any condition relating to the empty set then you have two simplicial complexes that both "look empty", one which is genuinely empty and one which contains the empty set as a face. That's the whole difference we are talking about here

[Yaël Dillies]

Allowing this corner case just seems to let all the proofs flow more easily. For example, I can define the "closure" of set of faces by doing

/-- A constructor for simplicial complexes by specifying a set of faces to close downward. -/
@[simps] def simplicial_complex.of_faces (faces : set (finset E))
  (indep : ∀ {s}, s ∈ faces → affine_independent 𝕜 (λ p, p : (s : set E) → E))
  (disjoint : ∀ {s t}, s ∈ faces → t ∈ faces →
    convex_hull 𝕜 ↑s ∩ convex_hull 𝕜 ↑t ⊆ convex_hull 𝕜 (s ∩ t : set E)) :
  simplicial_complex 𝕜 E :=
{ faces := {s | ∃ t, t ∈ faces ∧ s ⊆ t},
  indep := λ s ⟨t, ht, hst⟩, (indep ht).mono hst,
  down_closed := λ s t ⟨u, hu, hsu⟩ hts, ⟨u, hu, hts.trans hsu⟩,
  disjoint := sorry}

[Reid Barton]

Well you just also require that s is nonempty, right? The proof gets a bit longer because the definition is a bit longer. Your argument would suggest that also in ordinary mathematics we should remove the nonempty condition, yet nobody actually does this.

[Reid Barton]

I think we need a really good reason to diverge from the standard meanings of words, and while I'm open to the idea that there could be one here, I don't know of any

[Yaël Dillies]

Is there any statement you can think of that requires the empty set not to be a face?

[Yaël Dillies]

Also, why isn't the empty set a simplex? Surely p : fin 0 → E is an independent family of points.

[Yaël Dillies]

Some more arguments to bring to the discussion: https://math.stackexchange.com/questions/855566/empty-set-in-a-simplicial-complex

[Yaël Dillies]

Yaël Dillies said:

Is there any statement you can think of that requires the empty set not to be a face?

I'm asking because we already wrote 4.2k lines (amounting to 35 files) on top of that definition, so it seems pretty correct to me.

[Reid Barton]

I don't know what it means for a definition to be "correct"... but I do know that this is not what people mean by the phrase "simplicial complex".

[Reid Barton]

Yaël Dillies said:

Is there any statement you can think of that requires the empty set not to be a face?

For example if $K$ is a finite simplicial complex then the Euler characteristic of $|K|$ is the sum over the simplices of $(-1)$ to the dimension of the simplex.

[Yaël Dillies]

Oh right. I'll have to study this.

[Reid Barton]

Yaël Dillies said:

Also, why isn't the empty set a simplex? Surely p : fin 0 → E is an independent family of points.

It's not a simplex because that's how "simplex" is defined (compare docs#affine.simplex) but ultimately, the reason is that a simplex is contractible and the empty set is not.

[Bhavik Mehta]

It's worth noting that in the SE thread above, and on wikipedia, the empty set is mentioned to be a useful simplex for certain applications, so there are at least some people who consider "simplex" to include the empty set

[Reid Barton]

The empty set is not a simplex. It is sometimes useful to consider it alongside simplices though.

[Reid Barton]

Then we talk about an augmented simplicial whatever

[Reid Barton]

This conversation is reminding me of "How many legs does a dog have if you call his tail a leg?"

[Reid Barton]

By the way, what are you using this for? Is there a branch somewhere I could take a look at?