Polyhedra in mathlib

Stream: maths

[ooovi]

Hi! We (me, Martin Winter and Georg Loho) are Berlin/Leipzig based discrete geometry enthusiasts interested in adding basics of polytope theory (including polyhedral cones, polyhedra and polytopes) to mathlib. That could mean figuring out good definitions and proving some standard results:

• the Minkowski-Weyl theorem
• faces + basic theorems (faces are polytopes, face of face is face, etc)
• face lattice + combinatorial equivalence + basic theorems (face lattice is graded, intervals are face lattices, etc)
• polar duality + basic theorems (polarity is an involution, flips face lattice)
• normals, normal fan, normal equivalence
• basic operations yield polytopes: product, direct sum, join, Minkowski sum, projections, sections, convex hull
• standard polytopes: simplex, cube, crosspolytope
• polytope classes: simple, simplicial, centrally symmetric, zonotope, lattice, etc
• edge graph + basic theorems (connected, degree >= d)
• trivial classification in dimensions 0,1,2

Since this topic has come up now and again (#Is there code for X? > Main Theorem of Polytope Theory, #mathlib4 > Minkowski-Weyl theorem and convexity), we'd like to discuss people's ideas and needs regarding this.

Some thoughts we had:

• We'd like the definition and theorems to be as general as possible and avoid inner products, norms or topologies as long as possible. It should be possible to talk about polyhedra over infinite dimensional spaces or spaces with unusual structure (Puiseux series, tropical semiring, hyperfields, lattices). Let us know if you have applications in mind that might be relevant to consider!
• Many interesting structural properties, like the existence of faces, face lattice and duality, can be proven for cones and then derived for polyhedra by projectivizing. This is usually done in the literature, because it makes the proofs much nicer. Since convex cones already exist in mathlib (and polyhedral cones apparently on the way? @Justus Springer), this seems like a reasonable approach. It might be possible to get some of the results in an even more general setting ("abstract" convexity with no useful notion of projectivization), but the cone approach should cover the generalizations mentioned above. We'd like to hear your opinions on this!
• It is useful for polytopes/polyhedra to live in affine space, e.g. since proofs from discrete geometry often consider subsets of polyhedra that are again polyhedra in some subspace of the original domain, without a natural way to assign an origin. However, convexity is not (yet) defined for affine spaces in mathlib, and @Yaël Dillies considers doing so to entail a significant amount of work to do properly. If we follow the cone approach above first, we will have some time to discuss and see what can be done about this.

[Justus Springer]

+1 for trying to avoid inner products and topology! That's what I've been trying to do for polyhedral cones in the Toric project. The main thing I did there was show that "finitely generated = polyhedral" in a completely algebraic setting, i.e. over linearly ordered fields. You need the order to speak about positivity and hence cones of course. You can find it here but I have not upstreamed it to mathlib. Also, some work on faces (face of face is a face, face lattice...) has been done by @Giacomo Maletto on a separate branch.

[Yaël Dillies]

@Matthew Johnson and I worked out a naïve version of polytopes in #23940 and proved that they were preserved under a few basic operations like the Minkowski sum. Feel free to review the PR! For example, I don't know whether we should have two predicates: IsVPolytope and IsHPolytope, that agree only in finite dimensions.

[Justus Springer]

By the way, do you have good references/books that treat cones and polytopes in the generality you're aiming for? I was struggling to find good ones, the ones I was looking at either omit proofs for the convex geometry stuff, or they do everything over the reals and start with hyperplane separation in euclidean space.

[Martin Winter]

@Justus Springer I don't, and my feeling is we won't find any because most of convex/polyheral geometry cares deeply about real numbers. I am somewhat confident that proofs in polyhedral geometry will transfer without much effort to general linearly ordered fields. Beyond that we first need to clarify what generality we are aiming for. I believe Georg Loho mentioned a proof of Minkowski-Weyl in some tropical context, which works over a linearly ordered semiring, so some generalization might be possible.

[Violeta Hernández]

Any chance we could get abstract polytopes somewhere along the line? That's actually the reason I started using Lean (before ordinals completely won me over...)

[Justus Springer]

@Martin Winter I agree most proofs should work for linearly odered fields. The best reference I could find was actually lecture notes by my supervisor (in German). There he sets up the basic theory of polyhedral cones over general fields and the proofs are all algebraic. But it's pretty limited in scope. Maybe I should ask him if he knows better references.

[Justus Springer]

I don't know what you mean by "abstract convexity with no useful notion of projectivization". Can you elaborate?

[Martin Winter]

@Violeta Hernández One could define abstract polytopes independently as special types of lattices and later show that face lattices of convex polytopes are instances of abstract polytopes.

[Martin Winter]

@Justus Springer That's a great reference! Can you say what "scope" it lacks in your opinion?

[Justus Springer]

I just mean it's not the most extensive reference depending on what your goals are, as it's basically an undergraduate course. But it does cover the basics quite well.

[Justus Springer]

One reason I'm pushing for this algebraic approach is that I believe convex geometry should be an area where one could use Lean not only for formal proofs but also as a programming language for actual computations. So the theory should at least work over the rationals, which is where computations tend to work in.

[Artie Khovanov]

Also if a result doesn't hold over all ordered fields, maybe it holds over all real closed fields :)

[Violeta Hernández]

Surreal polyhedra sound both incredibly cursed and incredibly mundane

[Violeta Hernández]

(in fact, is every convex polyhedron over a real-closed field isomorphic to one over ℝ?)

[Yaël Dillies]

Violeta and I wrote quite a fair bit of code about abstract polytopes in Lean 3. I could fetch that code when necessary.

[Martin Winter]

To get the ball rolling, let me formulate my stance on what generality we should be aiming for. I have not much experience with the standards of mathlib, so I am happy to be educated on this.

First, I do not insist in generality for its own sake. I think we should implement what is of obvious interest to the working mathematicians that uses polyhedra/polytopes, and then make it maximally general without the need to invent new mathematics. For example, polyhedral geometry over R is standard, and if it needs little effort to generalize to affine spaces over linearly ordered field without inner products or topoloy (which I believe is the case), then this is a lower bound of what we should go for. Some generality that is currently there and that bothers me a bit is that, say, the convex hull convexHull k S takes the field k as an explicit parameter. In my experience this generates friction, and I have never seen any use of this, either in mathlib or real life maths.

Now, I am aware already from inside my own community that people care about settings that go beyond the above generality, e.g. tropical polytopes. Moreover, I personally also care about polytopes in spherical/hyperbolic space, and I don't yet know what would be the right setup that allows us to include those. Perhaps some sort of synthestic geometry backbone would be useful, where one can talk about hyperplanes, halfspaces, angles etc abstractly, and show that affine/spherical/hyperbolic polytopes are instances thereof.

In any case, I think polyhedral cones are the first thing we should get right in the right generality. I hope we can collect here what is/can be interesting to the mathematician working with these concepts, and then figure out what is the right common generalization.

[Yaël Dillies]

Martin Winter said:

Some generality that is currently there and that bothers me a bit is that, say, the convex hull convexHull k S takes the field k as an explicit parameter. In my experience this generates friction, and I have never seen any use of this, either in mathlib or real life maths.

Interesting... I was the one to make that change several years. Isn't it necessary to consider ℚ-convex hulls sometimes? I also know that @Patrick Massot wanted to do convex geometry over a space of germs (IIRC?) in sphere-eversion.

[Martin Winter]

@Yaël Dillies I though about precisely this when I first encountered the implementation. I could not think of a good reason to consider a $\Bbb Q$-convex hull unless $S$ is already in $\Bbb Q^d$. I can imagine someone working with $\Bbb Q^d\cap \operatorname{conv}(S)$, but this is something different (unless $S\subseteq\Bbb Q^d$). Of course I cannot claim to have a complete overview of all potential usecases, but at least to me it feels unnatural to call this a convex hull since it has "holes" from the perspective of the ambient space.

[Yaël Dillies]

I think your surprise/confusion might come from the assumption that a space in Lean "knows" what scalars it is a module over. This is very false, as eg all abelian groups are ℤ-modules, even the ones that already are ℝ-modules.

[Yaël Dillies]

It isn't possible to write a convexHull function that somehow infers what scalars one should be talking about. The only option would be to fix the scalars once and for all, which was indeed the case before: scalars were fixed to be ℝ and one could not talk about the convex hull of $S \subseteq \mathbb Q^d$.

[Martin Winter]

But isn't this also just a design decision? For example, for my personal projects I defined a VectorSpace that "knows" its ground field and I defined convex hulls for sets in this VectorSpace which then did no longer need the explicit reference to the field. I guess I also always wondered why a modul does not "know" its ring, even though they seem to do in everyday math. But then again, I personally don't really work with modules - but I work with vector spaces, and there it's true ;)

[Yaël Dillies]

In commutative algebra, it is very often the case that one has $S$ an $R$-algebra, and $M$ an $S$-module, and then it is very useful/necessary to view $M$ as a $R$-module. This would be impossible with your design without jumping a few hoops.

[Martin Winter]

I can imagine that this was already discusse somewhere else: is it intended/necessary to carry this complexity over into parts of math that are increasingly distant from algebra? Would it be bad to define a VectorSpace (or some other bundled structure) and build geometry (convexity, polyhedra, etc) on that?

[Joël Riou]

The burden of typing ℚ or ℝ is very low. This is what we need in order to develop a consistent mathematical library for all purposes. (Note that in mathlib, we also have categories of modules over a given ring R, ModuleCat R, and each M : ModuleCat R "knows" that it is a module over R. However, most of the developments about these bundled objects are based on the corresponding unbundled API for types equipped with structures, using the typeclass system, as {M : Type*} [AddCommGroup M] [Module R M].)

[Michael Rothgang]

You can sometimes use custom or local notation to reduce cumbersome notation. "Under the hood", Lean still sees the extra argument, but you can avoid typing it.

[Martin Winter]

@Michael Rothgang Is there some place in mathlib that does it this way? I would like to see how to do this properly.

[Martin Winter]

@Joël Riou The burden might be low, but as far as my limited understanding goes right now, it might also be avoidable. Also, we want to have convexity on affine spaces next, and so I was hoping for bundled affine spaces as well, as otherwise we would need to write convexHull k V A I believe. And eventually all this complexity will be forwarded to polytopes, so we would need to write Polytope k V A rather than Polytope A.

So would it be possible to develop geometry on ModuleCat R? It does not seem to be a typeclass, so maybe not what I was hoping for.

[Aaron Liu]

I have at one point doing something polyhedron-related wanted to restrict scalars from ℝ-module to NNReal-module

[Patrick Massot]

Yaël Dillies said:

Martin Winter said:

Some generality that is currently there and that bothers me a bit is that, say, the convex hull convexHull k S takes the field k as an explicit parameter. In my experience this generates friction, and I have never seen any use of this, either in mathlib or real life maths.

Interesting... I was the one to make that change several years. Isn't it necessary to consider ℚ-convex hulls sometimes? I also know that Patrick Massot wanted to do convex geometry over a space of germs (IIRC?) in sphere-eversion.

Yes talking about convex hulls is very natural when using partitions of unity and the ring of scalars is either a ring of functions or germs of functions. In particular it is an ordered ring that is not linearly ordered and does not embed in a field.

[Patrick Massot]

More generally I hope it is obvious that the notion of convexity is useful in areas of mathematics that have nothing to do with polyedras, so we should keep this in mind here.

[Patrick Massot]

About the extra parameters, we can always use custom elaborators if they become too annoying.

[Martin Winter]

@Patrick Massot Thanks for the interesting use case. Since I don't understand the details I need to ask: do you use a convexHull k S where k is not the ground field of the module in which S lives?

[Patrick Massot]

As explained earlier in this thread, there is nothing like "the ground field of the module in which S lives". In my case it could be either real numbers or functions taking values in real numbers, or rational numbers or integers...

[Michael Rothgang]

I was about to mention custom elaborators: Patrick and I wrote one for differential geometry, in #27021. This allows shortening e.g. mfderiv I J f x to mfderiv f x --- as I and J can be inferred from the types of f and x and the local context (without invoking typeclass inference too hard, i.e. in a manner that's not too slow).

[Eric Wieser]

Though the ground field probably isn't going to be the integers!

[Martin Winter]

Okay, here is my understanding so far. We keep explicit scalars in convexHull k S because we actually want them and there is not really a feasible way around them anyway. By extension, we will likely have explicit scalars in PolyhedralCone k S (and explicit scalars and vector spaces in Polytope k V A etc.). I don't see a use for these explicit parameters at this point, so here the reason is mainly the lack of a good alternative implementation.

For ease of use one then provides a custom elaborator that makes the scalars (etc) implicit and infers them from the context somehow. Since this will need to be done for a lof of definitions, and since the usefulness is not specific to polyhedral/convex geometry, one should perhaps implement this more generally?

[Michael Rothgang]

I understand where you're coming from --- but the elaborator itself is necessarily domain-specific. To write the model with corners one, you need to know which ones can be inferred sensibly (and which ones cannot, i.e. some understanding of the domain), and which part of the local context to get this from.

There may be some common logic, but these data will be domain-specific.

[Michael Rothgang]

I'm all ears for more general conveniences for everybody. But I don't see how this can be done without any domain knowledge.

[Michael Rothgang]

(The diffgeo elaborators are also fairly short, so this is not a lot of code that would be duplicated.)

[ooovi]

Thanks for all the comments! :)

Justus Springer said:

You can find it here but I have not upstreamed it to mathlib.

That looks like a great starting point for us! What is the course of action? Would it make sense to make it into a mathlib PR next, so we can use it in both our projects?

Also, some work on faces (face of face is a face, face lattice...) has been done by Giacomo Maletto on a separate branch.

I can't seem to find this. Could you point me there maybe?

[Martin Winter]

Olivia and me went through @Justus Springer's implementation of polyhedral cones. I collect here some thoughts and questions:

1. Currently the code defines IsPolyhedral p C. I would really like to also have a bundled structure PolyhedralCone R N p, e.g. defined as {C : PointedCone R N // IsPolyhedral p C}. This would enable us to later work with polyhedral cones very naturally. For example, we could have the lattice of polyhedral cones, or if C D : PolyhedralCone R N p then C ∩ D and C + D are automatically treated as polyhedral cones as well.

2. More generally, I was hoping to eventually have a very geometric language to work with. That is I would like to also have structures Halfspace, Hyperplane, Ray, etc rather than to always work with the underlying linear algebra. This would also help to unify concepts between Euclidean/spherical/hyperbolic space. One question is then how early one should start working with these structures. In my own implementation I first implemented Halfspace R M p and defined a polyhedral cone as the intersection of such.

3. @Yaël Dillies asked whether we eventually need both V and H polytopes as separate concepts. I tend to say no. Once V=H is established we know that we are dealing with a single notion of polytope and the V- and H-representations are only properties of them. There are people proving theorems about the relation and conversion between these representations, but I believe an interface that hides the implementation and allows access to both representations should still be totally sufficient. Problems may arise if one cares about cones/polytopes/polyhedra in settings where V=H does not hold. I don't, so I can't say much about this.

4. More tangential, but is there any plan or opposition to implement bilinear pairings using type classes? I am thinking of something like has_inner but for pairs of modules, that is has_bilinear_pairing or so. I see modules with a bilinear pairing as a precursor to inner product spaces and normed spaces, which are treated using type classes. I don't know what is already implemented, but I imagine we eventually want that an inner product space is considered (via type class inference) to have a bilinear pairing with itself, don't we?

[Justus Springer]

ooovi said:

I can't seem to find this. Could you point me there maybe?

This file can be a starting point. I have a feeling some of those proofs could be simplified though.

[Justus Springer]

@Martin Winter

1. Yes I think that makes sense.
2. Agree. Note that the current definition of IsPolyhedral basically says the same thing as being the intersection of finitely many halfspaces. After all, a halfspace is just the dual of singleton set, so most API for halfspaces should probably be phrased more generally for duals. If we still want Halfspace, maybe as an abbrev?
3. If I understand correctly, V=H is basically the polytope version of the statement that's already there for cones, namely that, finitely generated = polyhedral. The idea should be basically the same right? Namely some version of Fourier-Motzkin elimination. I agree an interface that hides the implementation would be sufficient for now. Down the line we could have a computational version of Fourier Motzkin that actually translates between V- and H-representations but that should be a different project from just getting the proof that there exists a way to translate between them.
4. Maybe Yael has more to say about this, I think there was some concern mentioned about a possibly problematic instance has_inner N M -> has_inner M N? Note that mathlib already has docs#PerfectPairing. This is a bit stronger as it already requires that the pairing is injective in both arguments.

[Justus Springer]

I'm sorry I have left things in a bit of messy state. I never properly incorporated Giacomo's work on faces and never finished the new blueprint for the convex geometry part of Toric. You can find fragments of my blueprint work on this branch, if you are interested. I'm in the middle of finishing my PhD thesis right now, so I won't be able to contribute much until that's done. After that, depending on my career position by then, I will either have very much time doing Lean, or no time at all. In the former case, I'd be very happy to do more on convex geometry.

[Yaël Dillies]

ooovi said:

That looks like a great starting point for us! What is the course of action? Would it make sense to make it into a mathlib PR next, so we can use it in both our projects?

As shown on https://yaeldillies.github.io/Toric/file_deps.pdf, there are some prerequisites before we can upstream IsPolyhedral. The current prerequisite PR is #28140; feel free to review!

[Yaël Dillies]

Martin Winter said:

is there any plan or opposition to implement bilinear pairings using type classes? I am thinking of something like has_inner but for pairs of modules, that is has_bilinear_pairing or so.

This is not exactly what you were looking for, but as of recently we have docs#LinearMap.IsPerfPair, and this is what you should be using. The difference with what you're asking for is that we are not assuming that there is a single canonical bilinear pairing between M and N, and instead you should declare that such an already-declared pairing is perfect.

[Martin Winter]

@Justus Springer

Agree. Note that the current definition of IsPolyhedral basically says the same thing as being the intersection of finitely many halfspaces.

Yes, mathematically it is equivalent, but ...
I do find it a bit awkward that isPolyhedral (and therefore a PolyhedralCone defined on it) takes a bilinear pairing as an argument. There is another way: we can define a Halfspace as the preimage of $[0,\infty)$ under a non-constant linear form (and I actually think there is a good reason to allow constant linear forms as well). This requires no pairing. And so a polyhedral cone defined as the intersection of such halfspaces also requires no pairing. We should then be able to prove all the things you proved, getting a pairings involved only when we explicitly say something about duality.

[Justus Springer]

Okay but the preimage of $[0,\infty)$ under a linear form $\varphi : N \to \mathbb{K}$ is by definition the same as the dual of $\{\varphi\}$, where we view $\varphi$ as an element of $N^*$ and take the canonical pairing $N^* \times N \to \mathbb{K}, (\varphi, v) \mapsto \varphi(v)$. Working with an arbitrary pairing is more flexible, as it also works in situations where the two vector spaces $N$ and $M$ are dual to each other, but $M$ is not defeq to $N^*$ for instance.

[Justus Springer]

Of course, it is true that the predicate IsPolyhedral does not depend on the pairing, which is evident by the fact that it's shown to be equivalent to Submodule.FG, which doesn't depend on it. So you could simply define your structure PolyhedralCone by using Submodule.FG and then there is no pairing any more.

[Justus Springer]

Now that I think about it, maybe for the predicate IsPolyhedral, it's okay to define it with respect to the canonical pairing $N^* \times N \to \mathbb{K}$ only. For the dual function (as well as Halfspace, being a special case), I still think we should allow more flexibility by having an arbitrary pairing as input.

[Martin Winter]

I tend to agree that dual should have this flexibility.

I am not so sure about Halfspace. Using linear forms, the statement whether a set $S\subseteq M$ is a halfspace is of the form "there exists a linear form $\phi:M\to\Bbb k$ so that $S=\phi^{-1}([0,\infty))$". If I want to express this using general pairings, the analogue would be "there exists a module $N$, a pairing between $\phi:N\to (M\to\Bbb k)$, and a point $x\in N$ so that $S=(\phi(x))^{-1}([0,\infty))$". So the pairing is still not a parameter of a halfspace, but the statement just became more complicated.

[Martin Winter]

I think I understand now that we may have different intentions for what Halfspace expresses. For me a halfspace is a particular kind of subset of space, whereas you seem to see it as a subset of the paired space bundled with the primal point it is constructed from. This would be in contrast to how you defined polyhedral cones, which don't "remember" the points that generate them. Or am I misunderstanding something?

[Martin Winter]

I am now wondering what we actually gain by letting dual depend on a pairing.
Let the canonical dual be the dual w.r.t. the canonical pairing $\tilde p:N\to (N^*\to\Bbb k)$. It is a cone in $N^*=N\to\Bbb k$. Now, if we take a different pairing $p:N\to (M\to\Bbb k)$, then I think I just conviced myself that the dual w.r.t. $p$ (which is a cone in $M$) is just the preimage of the canonical dual under the flipped pairing $p^*:M\to (N\to\Bbb k)$. So we don't gain any extra generality by including the pairing, but we now have to carry around this extra parameter.

[Yaël Dillies]

Justus Springer said:

Now that I think about it, maybe for the predicate IsPolyhedral, it's okay to define it with respect to the canonical pairing $N^* \times N \to \mathbb{K}$ only. For the dual function (as well as Halfspace, being a special case), I still think we should allow more flexibility by having an arbitrary pairing as input.

Perfectly agreed :100:

[Yaël Dillies]

Martin Winter said:

Let the canonical dual be the dual w.r.t. the canonical pairing $\tilde p:N\to (N^*\to\Bbb k)$. It is a cone in $N^*=N\to\Bbb k$. Now, if we take a different pairing $p:N\to (M\to\Bbb k)$, then I think I just conviced myself that the dual w.r.t. $p$ (which is a cone in $M$) is just the preimage of the canonical dual under the flipped pairing $p^*:M\to (N\to\Bbb k)$. So we don't gain any extra generality by including the pairing, but we now have to carry around this extra parameter.

The point is that for example you can now talk about the double dual cone as a subset of the original space, while the double canonical dual cone would live in the double dual.

[Justus Springer]

It's true we don't gain any generality in a mathematical sense. After all, for any pair of vector spaces $N$ and $M$ with a perfect pairing, we have $M \cong N^*$. But we gain flexibility in Lean, as it might happen that $M$ is not definitionally equal to $N^*$. If we only allow the "canonical" dual, we would then have to carry around the isomorphism all the time, as in the example with the double dual Yael mentions.

[Justus Springer]

Another example comes from toric geometry: To an algebraic torus $T$, one associates the lattices $T \to \mathbb{K}^*$ and $\mathbb{K}^* \to T$ (characters and one-parameter subgroups). These are dual to each other, but one is not definitionally equal to the dual of the other. But we still would like to be able to say that the dual of a cone in the characters lattice lives in the lattice of one-parameter subgroups, without carrying around an isomorphism.

[Martin Winter]

@Yaël Dillies In my understanding the double-dual cone should really live in the double-dual space $N^{**}$. Considering it as a cone in $N$ is a trick we can pull if $N\cong N^{**}$. So yes, by default the dual is not an involution, but why should it be if duality on the space itself is not an involution. And if there is a perfect pairing we get the double-dual in $N$ by post-composing with the canonical isomorphism p.
So for example, if you want to express

dual p.flip (dual p C) = C

you now instead write:

dual (dual C) = p C

[Martin Winter]

@Justus Springer Regarding carriying around additional isomorphisms: yes, if you want your cone to live not in the canonical dual $N^*$ but a space $M$ that is (non-canonically) isomorphic to it, you have to carry around this isomorphism $N^*\cong M$. But you have to do this anyway in the form of a pairing. And the only difference is that now we also have to state the pairing explicitly even if we only care about the canonical dual.

[Martin Winter]

I might be missing the real usecase here, but so far I am not conviced. My feeling is that by including the pairing in dual we incorporate functionality that is really external to it for the cost of convoluting the interface.

Let me stress my point by compare it to something obviously ridiculous: the inverse of a bijection $f:A\to B$ lives (canonically) in $B\to A$. But maybe we want to work instead with a space $M$ non-canonically isomorphic to $B\to A$ via an isomorphism $p: M\simeq (B\to A)$. To me the current situation reads like you want to include $p$ as a parameter to Function.invFun because it is useful sometimes and more convenient than just post-composing with $p$.

[Antoine Chambert-Loir]

Probably an useless remark, but I wish to mention that duality can work in both directions: a subset of $M^*$ both an orthogonal in the bidual $M^{**}$ and a pre-orthogonal in $M$.

[Kevin Buzzard]

@Martin Winter it's kind of a "formalisation philosophy" that one should have as many types as possible, and predicates relating them, rather than sticking to concrete constructions. For example we had Localization R S in commutative algebra to localise a commutative ring R by a multiplicative subset S (a concrete construction) and then when we tried to prove that an affine scheme was a scheme (i.e. that O_X was a sheaf on Spec(R)) we ran into all sorts of unexpected problems, documented in the Schemes in Lean paper. The fix was to introduce another type A and a predicate IsLocalization R S A saying that A was isomorphic to R[1/S] and then things were much better. In formalization in general, more general seems to be more helpful. Although I haven't read this thread carefully, it seems to be another instance of the same phenomenon.

[Justus Springer]

To your ridiculous example, let me counter that with a non-ridiculous one: In commutative algebra, Mathlib uses a predicate IsLocalization (M : Submonoid R) S to express the fact that S is isomorphic to the localization of R at M. Of course, one could instead just work with the "canonical model" of localization, which can be constructed explicitly as a subring of the field of fractions etc... So you might say, why do we need the predicate since it doesn't add any generality and we could just work with the canonical model instead. It turned out that with the way IsLocalization is defined (it's three very explicit properties of the algebra map) makes it a lot more convenient to work with, as you don't have to worry about composing with the correct isomorphisms everywhere. Instead, you apply all the localization API directly to any user-provided R-algebra, provided you show it satisfies the IsLocalization property. Kevin likes to tell this story a lot.

Now, the situation for us is of course a bit different: First, our pairing is data and not a predicate (I don't know how much of a difference that makes, but it's a difference). Second, having a perfect pairing $p : N \times M \to \mathbb{K}$ is much closer to having the actual isomorphisms $N \cong M^*$ and $M \cong N^*$ already (it's just a matter of currying and swapping the arguments of $p$). This was different to the IsLocalization predicate, where the three axioms do imply the existence of such an isomorphism, but the way to get there is arguably a bit more complicated. In particular, checking the axioms tend to be easier than constructing the isomorphism, hence reduces complexity for the user.

But I would still argue that there is some difference between having a pairing and having an isomorphism $M \cong N^*$. Namely, a pairing feels a lot more symmetric than the isomorphism. With a pairing, you don't have a bias towards one lattice or the other. With an isomorphism, you tend to view one lattice as your "actual" lattice whose elements are points, and the other one as its dual, whose elements are linear maps. I would like to have a world where we treat them both equally. And this is indeed what a lot of informal references tend to do as well when they say "Let $N$ and $M$ be mutually dual lattices/vector spaces". Specifically in toric geometry, some people prefer to view certain concepts in the $N$-lattice, and others in the $M$-lattice.

Of course, once you leave finite dimension, duality is no longer an involution as you say, and some people will still want to do convex geometry in this setting. I'm under the impression that these people are more likely to come from an analysis/functional analysis background, where they work over the reals again and do Hahn-Banach hyperplane separation and what not. So in a sense, I think this should be a different theory and there has been some discussion over how to provide a common interface for both. Right now, this is also the theory that's predominant in Mathlib. In my world, I only care about polyhedral cones and polytopes in finite dimensional vector spaces and this is the setting I would like to have an algebraic theory for, which would then be amenable for computations.

[Justus Springer]

I was literally just about to post this and Kevin posted a second earlier :rolling_on_the_floor_laughing:

[Ruben Van de Velde]

Justus Springer said:

Kevin likes to tell this story a lot.

You're not wrong!

[Edward van de Meent]

(it's a good story)

[Artie Khovanov]

Justus Springer said:

Now, the situation for us is of course a bit different: First, our pairing is data and not a predicate (I don't know how much of a difference that makes, but it's a difference).

For another analogy: IsAdjoinRoot S (f : R[X]), which just means $S\cong_RR[X]/(f)$, is data and not just a predicate -- it contains the data of where $X$ goes.

[Yaël Dillies]

Justus Springer said:

Now that I think about it, maybe for the predicate IsPolyhedral, it's okay to define it with respect to the canonical pairing $N^* \times N \to \mathbb{K}$ only.

I have just changed IsPolyhedral accordingly in Toric: https://github.com/YaelDillies/Toric/commit/3f53c491fce2b6f0651f46653ecd2ea17e53d706

[Martin Winter]

Since our last messages here Olivia and me made significant progress on polyhedral cones. A particular problem came up that I hope someone can help with.

Our current theory is developed explicitly without the assumumption of finite dimension. The reason is that there are many interesting things that can (and should) be said in this generality. Consider for example the statements (C ⊓ D).FG or dual p.flip (dual p C)) = C for when C and D are finitely generated cones. Previously this was proven under the assumption Module.Finite, which felt off. This is now no longer necessary.

Now the problem: for dual p.flip (dual p C)) = C we currently assume p.IsPerfPair. But this defies the purpose, since it implies that we are in finite dimensions after all. If you look closely, the proof only needs Surjective p.flip. This is especially problematic for (C ⊓ D).FG which does not even mention a bilinear pairing; yet, the proof works via duality, hence needs to choose one. This particular proof (and also the rest of the theory) works fine with choosing p := Dual.eval R M, for which p.flip is indeed surjective, but not a perfect pairing in general.

To fix this I could replace [p.IsPerfPair] by (hp : Surjective p.flip) everywhere. But my impression was that IsPerfPair was introduced as a typeclass precisely for the reason so that we do not have to carry around the bijectivity assumotions explicitly all the time.

My question: can we have surjectivity (in the case for bilinear pairing) as a typeclass as well, or how else would you resolve the situation above?

[Kenny Lau]

what is the type of p.flip?

[Martin Winter]

p : N →ₗ[R] M →ₗ[R] R for some modules M and N over R.

[Kenny Lau]

Martin Winter said:

can we have surjectivity (in the case for bilinear pairing) as a typeclass as well

[Fact (Function.Surjective p.flip)] if you really need it

[Kenny Lau]

don't use Fact for everything, that's the only warning label that comes with it

[Martin Winter]

Interesting! I have to ask: is this a good longer-term solution or should I see this as a temporary fix?

I also need this "Fact" to be inferred from certain assumptions automatically. For example, from IsPerfPair, or from p := Dual R M. I will then go on to implement the corresponding instances with it, alright?

[Kenny Lau]

yeah

[Kenny Lau]

Martin Winter said:

is this a good longer-term solution or should I see this as a temporary fix?

as long as that is the only thing you put inside Fact and you don't expand its scope then it's fine

[Martin Winter]

What do people think about renaming PointedCone.span to PointedCone.hull (or something like this) to distinguish from Submodule.span which is still very important in the theory of cones and can get confusing if both are used.

[Yaël Dillies]

I am not against it

[Martin Winter]

I should note: we still want to use lemmas named with span for statements about hull, which we can but is harder to look up. Is this a concern?

[Martin Winter]

As a quick update: we now have a working definition of polyhedral cone in vector spaces over general fields, with no assumption of topology, and in potentially infinite dimensional space. Some non-trivial results that are already proven include that polyhedral cones are closed under intersection and duality.

[Martin Winter]

We also built some theory of faces of general pointed cones (see also here), and one of the next tasks is to show that polyhedral cones have finitely many faces and that their faces are again polyhedral and form a lattice with nice properties. This will likely also involve proving some Krein-Milman version for polyhedral cones.

[Martin Winter]

This means it is also time to check in how far our code works well with the abstract polytopes code by @Yaël Dillies and @Violeta Hernández. That is, the goal would be to show that our face lattice is an abstract polytope in this sense.

[Violeta Hernández]

I don't believe we ever really finished that much code? I'd be willing to come back to this project, but it has been quite a long while since I last worked with this.

[Yaël Dillies]

I replied in DMs with Martin that the abstract polytope stuff that was high enough quality for mathlib has already been PRed, and that the rest should probably be redone