abstract polytopes

Stream: maths

[Grayson Burton]

A friend (GH: vihdzp) and I (GH: ocornoc) are formalizing abstract polytopes and thought it would be nice to have in mathlib. Can we get non-master write access for a branch regarding this?

[Alex J. Best]

@maintainers

[Scott Morrison]

Great! I will send an invite shortly.

[Scott Morrison]

Have you seen the recent discussion about abstract and concrete simplicial complexes?

[Scott Morrison]

Invitations sent!

[Grayson Burton]

Scott Morrison said:

Have you seen the recent discussion about abstract and concrete simplicial complexes?

I haven't but I'll look it over. Thank you very much :)

[Scott Morrison]

There may have also be a separate discussion about associahedra; I forget if that was in the same thread or not.

[Grayson Burton]

So, just exactly how limited in scope should the branch be? In order to aid in formalizing abstract polytopes, for example, it would be nice to have a bounded_order simply being the combination of order_top and order_bot, along with some theorems about it. should this be added into order/ (say, adding it near the top of order/bounded_lattice.lean with a few theorems)? or should this be in a polytopes/ folder? thanks

[Scott Morrison]

Just a word of warning re: order_top and order_bot: see #9891 which is making some changes.

[Scott Morrison]

PRs should basically be as small as possible, but no smaller. :-) Essentially, if there is a bundle of changes that makes sense without the "main" part of the PR, please do those as an initial PR.

[Scott Morrison]

It's fine to make multiple PRs at once, and indicate dependencies between them. Sometimes this is helpful so reviews can understand the motivation for the initial PRs.

[Grayson Burton]

Scott Morrison said:

Just a word of warning re: order_top and order_bot: see #9891 which is making some changes.

Oh right, this got linked in the Xena discord. I think I'll block on that.

[Scott Morrison]

So for example, if you have some theorems that hold when both order_top and order_bot are available, that can probably be a PR by itself, and those lemmas should certainly not be in polytopes/.

[Violeta Hernández]

Oh, hi! Just found this thread