Weekly meetings

Stream: toric

[Yaël Dillies]

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]

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]

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

[Yaël Dillies]

Weekly meeting in two hours!

[Yaël Dillies]

Now!

[Yaël Dillies]

Next meeting will be in one hour

[Yaël Dillies]

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]

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

[Yaël Dillies]

Conclusions of this meeting:

1. @Justus Springer keeps on working with $ℝ$-inner products, but could simultaneously think about to generalise to a more general exact pairing.
2. 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.
3. The blueprint should be expanded a lot more to avoid series of disappointments like @Sophie Morel experienced.
4. Let's stop trusting Milne.

[Sophie Morel]

3. 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]

4. Let's stop trusting Milne.

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

[Kevin Buzzard]

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]

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]

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

[Yaël Dillies]

This is the PR we're talking about #24149

[Yaël Dillies]

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]

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

[Yaël Dillies]

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]

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]

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]

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]

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]

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

[Justus Springer]

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]

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}$.

[Kevin Buzzard]

docs#GaloisConnection.u_l_u_eq_u

[Yaël Dillies]

I will be on a hike during the next meeting in a bit under two hours, so Michał will be leading it

[Justus Springer]

Is it just me or has the meeting not been started yet?

[Michał Mrugała]

Sorry had a slight delay

[Michał Mrugała]

Starting in a few mins

[Michał Mrugała]

Started now!

[Justus Springer]

I'm still "asking to be let in"

[Andrew Yang]

We are here:
https://meet.google.com/ert-ueaa-cxy

[Michał Mrugała]

Hmm I didn't get any notifs

[Justus Springer]

Strange...

[Michał Mrugała]

It might only be Yael who can let people in...

[Michał Mrugała]

Setting new one up

[Andrew Yang]

Let's move here for today:
https://meet.google.com/vpj-jiyw-rbk

[Justus Springer]

Do we have a meeting today?

[Justus Springer]

Making a new link for today in case someone wants to talk:
https://meet.google.com/sdt-bbpn-rmw

[Yaël Dillies]

Aah apologies. I am still hiking and the meeting fell off my radar :national_park:

[Michał Mrugała]

I had an interview at the time, sorry

[Yaël Dillies]

Meetings will be back properly next week

[Justus Springer]

No problem! Me and @Giacomo Maletto talked a bit about convex geometry.

[Yaël Dillies]

Any chance you can brief us on what you both concluded?

[Justus Springer]

Not much, we just talked about what the current state is for convex geometry. Giacomo might look into defining faces of polyhedral cones.

[Justus Springer]

I probably won't work on Lean this week as I'm on vacation for a few days now. Should be back for the next "proper" meeting next week though.

[Yaël Dillies]

Great! No problem. Andrew and I will keep on writing the schemes paper

[Yaël Dillies]

Next meeting in 40min! Neither Andrew nor Michał can make it, so it's a prime time to discuss the convex geometry

[Justus Springer]

Will there be a meeting today?

[Michał Mrugała]

I’ll be there

[Yaël Dillies]

Can't attend. I have been roped into listening to some dynamics talks.

[Justus Springer]

Then we need a different link

[Michał Mrugała]

I think the same link should work, I'm in the call

[Justus Springer]

But I think only Yael can let people in?

[Michał Mrugała]

Ah maybe yeah

[Justus Springer]

I'm currently waiting to be let in

[Michał Mrugała]

New link for today: https://meet.google.com/idb-xtyf-muh

[Yaël Dillies]

Next meeting in one hour!

[Yaël Dillies]

Next meeting in 10min! I might not be there on the clock

[Yaël Dillies]

Now that the perfect pairing between characters and cocharacters is sorry-free, here's what we will spend the next three weeks doing, in rough order of priority:

1. Write a blogpost summarising what was done, what we learned, and announcing that the second phase of the project is open to contribution.

2. Write the blueprint for that second phase. The two big components are:
   a. The equivalence between affine toric varieties and affine monoids, following Cox-Little-Schenck 1.1. This is mostly done already, but @Andrew Yang, @Michał Mrugała and I will split up a few items to make sure each of them is self-contained.
   b. The equivalence between convex polyhedral cones and affine monoids. @Justus Springer is handling this. We will want to coordinate with the people in Berlin for how to formalise convex cones optimally in synergy with polytopes.

3. Give examples using the definitions in the project to show that they are not bonkers. We identified the following, in increasing order of difficulty:
   a. $𝔾ₐ$ is not a torus. Can be done by showing that it's invariant under base change and not isomorphic as a scheme to $𝔾ₘⁿ$ for any $n$.
   b. Compute the char-cochar pairing of an explicit torus with an explicit identification of its chars and cochars with $ℤⁿ$
   c. Product of (split) tori is a (split) torus, as a structural property of (split) tori
   d. Base change of a torus is a torus
   e. $U(1)$ is a non-split torus over $ℝ$. It is a torus because it is isomorphic to $𝔾ₘ$ over $ℂ$, and it is non-split because its real points are the circle, which is torsion while the real points of $𝔾ₘⁿ$ lie inside $ℝⁿ$ and are non-torsion.

4. Cleaning up the project. A few files need to be moved around and also build time nearly tripled yesterday, with GroupScheme.Diagonalizable now taking a whopping six minutes to build (!!)

5. Writing the paper about Hopf algebras, affine group schemes and tori. @Andrew Yang, @Michał Mrugała and I are doing that.
6. Printing :donut: shirts to wear at Kevin's summer school in Oxford.

[Yaël Dillies]

A lot of us are attending Tao's talk in Cambridge until 2025-06-10T10:15:00+01:00. Don't expect the meeting to start until then

[Yaël Dillies]

Actually I am not sure the meeting will happen at all today, sorry!

[Yaël Dillies]

Running slightly late from the previous meeting. Might be 5-10min late

[Michał Mrugała]

For the record, it's been 11 minutes and they're still not here, curious

[Yaël Dillies]

Next meeting in one hour! We'll talk about the project's next steps

[Yaël Dillies]

Michał says Alexander Esterov (aes@lims.ac.uk) has ideas of papers we could formalise once the basic theory of toric varieties has been laid out

[Yaël Dillies]

From now on we will use https://github.com/users/YaelDillies/projects/4 to handle tasks

[Yaël Dillies]

In a few days I will bump to v4.22.0-rc1 which includes the new grind tactic: #mathlib4 > `grind` is available. What should Mathlib users expect?

[Yaël Dillies]

I might be 5-10min late to the meeting today

[Yaël Dillies]

We won't be meeting today as four of us are attending Kevin's CFT workshop

[Yaël Dillies]

Are people wanting to meet today?

[Michał Mrugała]

I’m on holiday, so skipping today

[Yaël Dillies]

Let's put the weekly meetings on hold. No one is available, and the work that needs to be done has already been coordinated