Correct setting for convex geometry

Stream: toric

[Justus Springer]

I'm currently looking at the convex geometry side of things, trying to prove that the dual of a polyhedral cone is again polyhedral. I have some code on my branch justus/dual_cone in case someone wants to take a look. Basically, the approach I'm choosing has three steps:

1) Show that $\mathbb{R}^d$ is a polyhedral cone (indeed, it's generated as a cone by $\{\pm e_1, \dots, \pm e_d\}$)
2) Show that if $\sigma$ is polyhedral, then so is $\sigma \cap H_w$ for one halfspace $H_w = \{v \in \mathbb{R}^d | \langle v,w\rangle \geq 0 \}$.
3) Conclude inductively that for $\sigma = cone(v_1, \dots, v_n)$, its dual $\sigma^\vee = H_{v_1} \cap ... \cap H_{v_n}$ is polyhedral.

So far, I've formalized steps 1) and 3). Step 2) will probably by a bit annoying, but I don't think there are any real hurdles, as it should be very explicit computations (the generators of $\sigma \cap H_w$ can be explicitly written down, this is basically a version of Fourier-Motzkin elimination).

All of this made me wonder however, what truly is the "correct" setting for us to do convex geometry in for the purposes of toric geometry. So far, everything is stated for a NormedAddCommGroup E with an InnerProductSpace ℝ E instance. I want to raise two points:

• In my undestanding, there isn't really a good reason to work over the reals and I know lecture notes on toric geometry that never mention $\mathbb{R}$ but do everything over $\mathbb{Q}$. In a sense, I don't think one should ever use the euclidian topology of $\mathbb{R}^d$ when doing convex geometry, but state everything in terms of the lattice that's embedded in your space (For example, one shouldn't speak about euclidian distances, as these aren't invariant under unimodular transformations. Instead, the correct distance measure is lattice distance, i.e. the number of lattice points on the line segment between your two points).
• In mathlib, PointedCone.dual and Set.innerDualCone give back cones that live in the same space E that one has started with. On the other hand, toric geometry textbooks like CLS place emphasis on working with two mutually dual lattices $N$ and $M$, which give rise two mutually dual vector spaces $N \otimes \mathbb{K}$ and $M \otimes \mathbb{K}$ (where $\mathbb{K}$ is either $\mathbb{Q}$ or $\mathbb{R}$). Dual cones of cones in $N$ live in $M$ and vice versa. I have a feeling this is going to be important when building the bridge from toric varieties back to cones and fans, as then the two lattices will be the character lattice and the lattice of one-parameter subgroups, which are truly different (but dual) lattices. I don't know mathlib well enough, is there a way in which one could express this concept of two mutually dual lattices or vector spaces, linked by a scalar product?

(I just started looking into the Toric project seriously a few days ago and I don't know mathlib's library on convex stuff well, so these two points might not be well informed. Please correct me if you think I misunderstand something)

[Kevin Buzzard]

I agree with this. I remember Michal stressing that it was important to use $\R$ in LLL in Feb and I was thinking "I don't think that's true at all". Is there a misunderstanding here?

[Yaël Dillies]

I have thought about this a bit myself (this is why the blueprint is stated with a pairing, rather than a module and its dual. I believe the correct thing to use here would be docs#PerfectPairing, except that I do not know how to make it practical:

• If it stays a non-class, then we need to carry it around always
• If it becomes a class, then we will need to make it explicit in a bunch of places, because Lean won't be able to guess N from M and [PerfectPairing M N] alone, and I do not know whether complications will arise from a potential PerfectPairing M N → PerfectPairing N M instance.

[Yaël Dillies]

I agree that it is very important to have things more generally than $\R$. Eg in the blueprint right now we have mentions of duals of rational convex cones, and I believe that the best way to formalise this would be to talk about cones in $\mathbb Q^n$.

[Justus Springer]

I didn't know about docs#PerfectPairing, but yeah that looks correct.

[Justus Springer]

Right, it would be annoying to carry N and M around explicitly all the time. On the other hand, when I want to speak about the dual of a cone $\sigma$ which lives in N, maybe I should explicitly say where I want that dual to live, otherwise it's not clear what I'm talking about.

[Yaël Dillies]

I believe it would be fine so long as N is a one-letter free variable :grinning: Maybe we could do some trickery where, if N isn't provided, then it is set to be dual M. Something similar happens in measure theory with measures and volume

[Michał Mrugała]

Kevin Buzzard said:

I agree with this. I remember Michal stressing that it was important to use $\R$ in LLL in Feb and I was thinking "I don't think that's true at all". Is there a misunderstanding here?

This is most likely a misunderstanding on my part

[Michał Mrugała]

This project is in part an excuse to motivate myself to learn about toric varieties

[Michał Mrugała]

After talking to some people: I was dead wrong with the reals mattering. I’ll look for sources which develop the theory in a more general setting.

[Justus Springer]

I just PR'd my proposed refactor of our convex geometry in Toric#23 . Everything is now done over a pair of modules over an arbitrary linearly ordered field with a bilinear pairing (the modules should be finite-dimensional though). The main statement is that polyhedral cones (defined to be duals of finite sets) are precisely the finitely generated ones. In particular, this implies that the dual of a polyhedral cone is again polyhedral (which was formalized previously, but only over the reals).

[Justus Springer]

@Yaël Dillies @Andrew Yang I think this "algebraic" cone theory is mostly independent from your mathlib PR #24149, though to make things compatible (hopefully), I've copied some of the basic API for dual cones from your PR (In particular, the dual should be sending sets to cones, not cones to cones). That way, we can keep working on convex geometry in the toric project without having to wait for that PR to be merged.

[Yaël Dillies]

Okay great, that's roughly what I expected, except for the fact that #24149 does define the algebraic dual of a cone. Do you not need that?

[Justus Springer]

Yes I do, it's part of the stuff I copied from your PR. Except I had to name it PointedCone.dual' to avoid collision with the existing PointedCone.dual that is defined only for cones and not sets.

[Justus Springer]

Once your PR is merged we can rename it back to dual. Or is there another way to maybe redefine an existing definition with the same name?

[Yaël Dillies]

Ah right! No, you did everything correctly. You just had me confused

[Yaël Dillies]

Here's an existing formalisation of Gordan's lemma in Lean 3 by @Bhavik Mehta: https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/Gordan.lean

[Yaël Dillies]

#24149 is finally being merged (thanks Bhavik) :tada:

[Yaël Dillies]

@Justus Springer, polyhedral cones are finally ready to be upstreamed, cf YaelDillies/Toric#42