Abstract Simplicial Complex

Stream: maths

[Archie Browne]

Hello - I have a full formalisation of the "Stanley-Reisner Correspondence" as described here. This relies on a structure which I have defined as follows:

/-- An `AbstractSimplicialComplex X` is a collection of finite sets of `X` which is downward closed
with respect to set inclusion. -/
structure AbstractSimplicialComplex (X : Type) where
  /-- The `faces` are represented as Finsets -/
  faces : Set (Finset X)
  /-- The empty face is contained in the complex -/
  empty_mem : ∅ ∈ faces
  /-- Any subset of a face is also a face -/
  down_closed : ∀ {s t}, s ∈ faces → t ⊆ s → t ∈ faces

Whilst there is a geometric interpretation of such an object, it is really just a set of sets. I wondered wether I should push this to Mathlib (with some basic API) or if there is anything similar already in Mathlib.

I have already looked at the SimplicialComplex object but the problem is that it has not_empty_mem which is the exact opposite of AbstractSimplicialComplex's empty_mem.

Thanks

[Yaël Dillies]

If you want to talk about down-closed nonempty families of sets, maybe use LowerSet (Finset X)

[Joël Riou]

See this other thread #mathlib4 > AbstractSimplicialComplex. It seems nothing is in mathlib yet. In the other formalizations, it was assumed that faces were not empty, while you assume that the empty set is a face. Then, there should be some design discussion about what would be the best choice.

[Yaël Dillies]

For me, the entire point of simplicial complexes compared to lower sets is that convention difference on whether the empty set is included or not

[Archie Browne]

Thanks! I'll give both of these a look

[Archie Browne]

Yaël Dillies said:

If you want to talk about down-closed nonempty families of sets, maybe use LowerSet (Finset X)

LowerSet (Finset X)seems like a good suggestion - although they too are not by default non-empty. To rewrite my results in terms of LowerSets would require adding non-empty-ness as a hypothesis, which seems a bit clunky. Am I missing something?

[Yaël Dillies]

No, what you understood is exactly what I am suggesting

[Archie Browne]

Okay great thanks! Where abouts do you think it would be appropriate to push this result?

[Johan Commelin]

@Archie Browne Do you mean "where in mathlib"? I guess abstract simplicial complexes could start a new file or folder in AlgebraicTopology?

[Yaël Dillies]

@Sophie Morel has a great start on ASCs which I really want to see in Mathlib

[Archie Browne]

Johan Commelin said:

Archie Browne Do you mean "where in mathlib"? I guess abstract simplicial complexes could start a new file or folder in AlgebraicTopology?

Yes - this is what I meant, thanks :)

[Sophie Morel]

Yaël Dillies said:

Sophie Morel has a great start on ASCs which I really want to see in Mathlib

I'm not going to PR it, but if anybody wants to take the code, improve it (or not) and then PR it, feel free.

[Yaël Dillies]

What's the repository?

[Sophie Morel]

There's this and that, I can't remember why I created two branches... (One has the stuff about the category of abstract simplicial complexes and the other doesn't, so maybe I was planning to PR the smaller one, but it's still pretty big for a PR.)

[Yaël Dillies]

Okay great! Will put everything in LeanCamCombi and start PRing from there

[Berber]

Any progress on this branch? I see no activity in this branch. I want abstract simplicial complexes in lean and considered contributing my own implementation of abstract simplicial complexes. But since there are existing efforts, I would love to have the existing code make progress!

[Yaël Dillies]

We're needing fans for Toric, so there will be movement soon, yes :smile: