Zulip Chat Archive

Stream: toric

Topic: Weekly meetings

Yaël Dillies (Mar 16 2025 at 21:34):

Dear all, from now on @Michał Mrugała and I will meet weekly to discuss the project. If contributors want to hop in to talk about their current task, find their next task or get help, this is the perfect occasion to do so. :smile:

Yaël Dillies (Mar 16 2025 at 21:37):

The tentative details are:

Date and time: 2025-03-18T10:00:00Z, 2025-03-25T10:00:00Z, 2025-04-01T09:00:00Z, ...
Duration: 45min
Location: https://meet.google.com/ert-ueaa-cxy

Yaël Dillies (Mar 18 2025 at 11:01):

Thank you everyone who came! This was very productive :smiley:

Yaël Dillies (Mar 25 2025 at 08:00):

Weekly meeting in two hours!

Yaël Dillies (Mar 25 2025 at 10:05):

Now!

Yaël Dillies (Apr 01 2025 at 08:06):

Next meeting will be in one hour

Yaël Dillies (Apr 08 2025 at 08:01):

Next meeting at 2025-04-08T10:00:00+01:00. @Sophie Morel, if you are available, we would love to hear from you

Sophie Morel (Apr 08 2025 at 08:06):

Oh, okay! I'm home waiting for a delivery, so I can join.

Yaël Dillies (Apr 08 2025 at 10:07):

Conclusions of this meeting:

@Justus Springer keeps on working with $ℝ$ -inner products, but could simultaneously think about to generalise to a more general exact pairing.
See https://github.com/ImperialCollegeLondon/FLT/compare/main...CrazyAffine and https://link.springer.com/chapter/10.1007/978-3-031-64529-7_9 for the version of the Hopf algebra - affine group scheme that Edison Xie, Jujian Zhang and co formalised.
The blueprint should be expanded a lot more to avoid series of disappointments like @Sophie Morel experienced.
Let's stop trusting Milne.

Sophie Morel (Apr 08 2025 at 11:23):

I like to think of them as "fun surprises".

3bis. I should update the blueprint to reflect the prerequisites I added, and do some PRs.

Kevin Buzzard (Apr 08 2025 at 12:06):

Let's stop trusting Milne.

Some of us did this a long time ago...

Kevin Buzzard (Apr 08 2025 at 12:07):

In fact I was slightly worried that the only reference for Poitou-Tate duality (needed for FLT) which I knew, for many years, was Milne's "arithmetic duality theorems" (which experts tell me has mistakes, some serious) but now we have Neukirch-Wingberg-Schmidt "Cohomology of number fields" which hopefully will be more accurate...

Yaël Dillies (Apr 22 2025 at 05:53):

We will meet in three hours and a bit. Michał and I will be travelling, so no guarantee on how present we can be, but Andrew will be there animating the meeting.

Yaël Dillies (Apr 22 2025 at 05:53):

I personally want to talk about the convex geometry side of things

Yaël Dillies (Apr 22 2025 at 09:04):

This is the PR we're talking about #24149

Yaël Dillies (Apr 22 2025 at 10:36):

Conclusion of the meeting: The PR Andrew and I wrote over the weekend (#24149) is great for the infinite dimensional case, but won't apply to eg rational cones

Yaël Dillies (Apr 22 2025 at 10:37):

Justus instead suggests to develop the theory of cones in finite dimensional spaces purely algebraically

Yaël Dillies (Apr 22 2025 at 10:41):

This means mathlib might eventually have two theories of cones:

One purely algebraic, namely docs#ConvexCone + docs#PointedCone, with the dual cone defined along a bilinear pairing, mostly developed in the finite dimensional case.
One topological/analytic, namely docs#ProperCone, with the dual cone defined under a continuous bilinear pairing, developed in arbitrary dimensions

Yaël Dillies (Apr 22 2025 at 10:51):

Some points we will need to care about:

Closed cones in the topological setting correspond to polyhedral cones in the algebraic setting
The start of the algebraic theory does not need to restrict to finite dimensional spaces, so we can reuse some of it for the topological theory
If we want to reuse the algebraic dual cone to define the topological dual cone we need to be careful not to assume the pairing is perfect. Indeed, a pairing M → N → R cannot be perfect both as a map M →ₗ[R] N →ₗ[R] R and a map M →L[R] N →L[R] R (that would mean all linear maps M →ₗ[R] R and N →ₗ[R] R are actually continuous). That's the current status of #24149.
Inner dual cones can be obtained straightforwardly from topological dual cones by setting the continuous bilinear pairing to be the inner product. I am planning to do this refactor in #24149 too.

Yaël Dillies (Apr 22 2025 at 10:58):

Here are a few things I didn't have time to mention before I was rudely interrupted by the train change:

Andrew and I do not know what a continuous perfect pairing should be. It's certainly at least a map M →ₗ[R] N →ₗ[R] R, but we probably want it to be continuous in both arguments simultaneously, ie as a map M × N → R, otherwise it wouldn't induce a map N → M →L[R] R. We probably also want the fact that a continuous perfect pairing between M and N implies that M is the dual of N and vice-versa. That means we would need the two maps M → N →[L] R and N → M →L[R] R to be homeorphisms. In #24149, we are currently only assuming that they are bijective, which is enough to show that the double dual of a proper cone is itself.

Justus Springer (Apr 22 2025 at 11:42):

Very nice writeup! For the "algebraic theory", there is a nice stackexchange answer explaining the crucial lemma for proving that the double dual of a polyhedral cone is itself: https://math.stackexchange.com/a/638026. Notably, it does not use any functional analysis (no hahn-banach) hence should work over any linearly ordered field. However it only works in finite dimensions.

Andrew Yang (Apr 22 2025 at 17:40):

They say "all except perhaps property (2) can be proved" where "2. $\sigma^{\wedge\wedge} = \sigma$ " though. Or am I missing something.

Yaël Dillies (Apr 23 2025 at 08:12):

Have you checked the book by Ziegler Lectures on Polytope that was linked?

Justus Springer (Apr 23 2025 at 16:21):

Andrew Yang said:

They say "all except perhaps property (2) can be proved" where "2. $\sigma^{\wedge\wedge} = \sigma$ " though. Or am I missing something.

The statement $\sigma^{\vee\vee} = \sigma$ is trivial for polyhedral cones, when polyhedral is defined as "is the dual of a finite set" (i.e. intersection of finitely many halfspaces). Indeed, one can show $S^{\vee\vee\vee} = S^{\vee}$ holds for any set $S$ completely elementary. The hard part is to see that this definition of polyhedral is the same as "is generated by a finite set", which they use in the stackexchange question.

Justus Springer (Apr 23 2025 at 16:29):

Just to emphasize how trivial it is: $S \subseteq S^{\vee\vee}$ is immediately obvious. Now apply the dual on both sides and get $S^{\vee\vee\vee} \subseteq S^\vee$ . Now apply the same fact to $S^\vee$ to get $S^{\vee} \subseteq S^{\vee\vee\vee}$ .