Convex geometry in mathlib

Stream: toric

[Yaël Dillies]

Heads up about this. #24149 is a first PR to clean things up in mathlib, currently still focusing the case of a real inner product space. The hope is that the new definition will be easier to adapt to the perfect pairing setting once it is figured out

[Yaël Dillies]

@Justus Springer, feel free to help fixing the build if you have time! Otherwise I'll do it slowly over the next few days

[Notification Bot]

2 messages were moved here from #toric > Correct setting for convex geometry by Yaël Dillies.

[Yaël Dillies]

Here are a few pain points I am currently identifying with mathlib's cones:

1. There are three types of cones (namely ConvexCone R E, PointedCone R E, ProperCone R E), and the file layout doesn't really show whether they should all be considered simultaneously, or each separately. They have one file each, and there is also roughly one file per concept, but the boundary between the two kinds of files is unclear. Furthermore, files are not clearly split according to typeclass assumptions.

2. The dual cone is defined as three functions:

   • Set.innerDualCone : Set E → ConvexCone R E
   • PointedCone.dual : PointedCone R E → PointedCone R E
   • ProperCone.dual : ProperCone R E → ProperCone R E

   but the dual of a set is always a proper cone! If anything, we should have a function Set E → ProperCone R E and the other ones would just be convenience. Here are the three functions I think we should have:

   • ConvexCone.innerDual : Set E → ConvexCone R E
   • PointedCone.innerDual : Set E → PointedCone R E
   • ProperCone.innerDual : Set E → ProperCone R E

   It would mean we lose dot notation on cones, but I doubt it hugely matters?

3. Nothing works for perfect pairings yet :smiling_face_with_tear:

[Yaël Dillies]

@Justus Springer, do you have thoughts on point 2, by any chance?

[Yaël Dillies]

@Andrew Yang and I have been thinking very hard today :thinking: https://en.wikipedia.org/wiki/A_Perfect_Pairing

[Kevin Buzzard]

You know about docs#RootDatum right? This is a perfect pairing over $\Z$ related to the character and cocharacter group of a maximal torus in a connected reductive group. We don't have the group scheme theory yet but the basic algebra is there.

[Yaël Dillies]

We know about it, although I don't really see how it is related (except for the fact that it's a pairing)

[Justus Springer]

Yaël Dillies said:

Justus Springer, do you have thoughts on point 2, by any chance?

I completely agree. Basically the dual : Set E -> ConvexCone R E should behave very similar to Submodule.span : Set E -> ConvexCone R E. In the latter, you describe a convex cone by giving a generator set, in the former, you describe it as the intersection of halfspaces.

[Yaël Dillies]

Just FYI ConvexCone R E is not defined as Submodule ?? E, although it almost could be!

[Justus Springer]

Right, but PointedCone R E is? I'm not sure whether this naming convention is standard.

[Yaël Dillies]

I have gathered that there is not really a standard :sad:

[Yaël Dillies]

Yaël Dillies said:

Just FYI ConvexCone R E is not defined as Submodule ?? E, although it almost could be!

Here's a thread about making it be defined as Submodule {r : R // 0 < r} E: #maths > G-submodules

[Yaël Dillies]

I've just updated #24149 to draw the line between the two theories of convex cones at algebra vs topology, rather than topology vs analysis.