Formalization of Grassmannians

Stream: Lean Together 2024

[Sophie Morel]

Slides for the talk: https://quatramaran.salle-s.org/~smorel/grassmannians.pdf
Code: https://github.com/smorel394/ExteriorPowers

[Florent Schaffhauser]

Is it insufficient for your purposes to assume that $E$ is a (real or complex) Hilbert space and to take the orthogonal of the $r$-dimensional subspace $W \subset E$ for your complement? So basically, set $U = W^{\perp}$.

[Kevin Buzzard]

This theory all works over the $p$-adic numbers, where there is no concept of $\leq$.

[Johan Commelin]

@Sophie Morel when working on some of the applications that you mentioned, did you run into trouble with the "choicy" parts of the construction?

[Sophie Morel]

No, there was no trouble at all, except the psychological problem that things are not canonical.

[Johan Commelin]

Ok, that's good news!

[Sophie Morel]

As continuous linear maps are smooth, adding some continuous linear equivalences in the charts was not a problem.

[Sophie Morel]

Kevin Buzzard said:

This theory all works over the $p$-adic numbers, where there is no concept of $\leq$.

Also, I was thinking about the algebraic variety situation, where we cannot take orthogonals.

[Florent Schaffhauser]

Right! So, in finite dimension you can everything in coordinates if you want. And for real or complex Hilbert spaces you can use a canonical complement. But if you want a unified approach, you need to make a choice of a complement in the coordinate-free version. Cool.

[Sophie Morel]

That's right. But I don't think it's a good idea to do things in coordinates, even in finite dimension. You don't want the manifold structure to depend on a choice of basis of your vector space.

[Florent Schaffhauser]

Presumably, a different basis would give an equivalent atlas, though. So it also depends what is meant by manifold structure.

[Sophie Morel]

Yes, all bases give the same manifold structure from the point of view of math. I meant the manifold structure in the sense of mathlib, so the data of a chart around each point.

[Florent Schaffhauser]

Is there talk of defining compatible atlases in mathlib?

[Eric Wieser]

I note that your repository defines ContinuousAlternatingMap , but docs#ContinuousAlternatingMap already exists in mathlib (as of #5678)! Perhaps it wasn't there when you first looked for it? Or is there something inconvenient about the mathlib definition that meant you needed your own?

[Eric Wieser]

(looking forward to seeing the talk when the recording get uploaded :) )

[Sophie Morel]

I think it didn't exist when I started, so I'll have to start using the mathlib definition. I don't see the operator norm for ContinuousAlternatingMapss in mathlib and I do need that too, did I miss something ?

[Eric Wieser]

I think the norm may indeed be missing; though @Yury G. Kudryashov may have a branch with it if so

[Yury G. Kudryashov]

#8691

[Yury G. Kudryashov]

I want to have topology on ContinuousAlternatingMaps independent of the norm.

[Yury G. Kudryashov]

But I need to make some changes in supporting lemmas to prove equivalence of 2 topologies.

[Yury G. Kudryashov]

I'll try to get back to it soon.

[Sophie Morel]

There is an obvious norm coming from the one ContinuousMultilinearMaps, and it's the one I was using in my Grassmannian project. (For the rest of the project, I need a norm and not just a topology.) But this is very easy to do anyway.

[Yury G. Kudryashov]

This is the norm added in #8691. Probably, we should update&merge it now, change the definition of topology later.

[Eric Wieser]

Is the desired topology not just the one induced by the multilinear maps? If so, does that not come for free with the induced norm?

[Yury G. Kudryashov]

We have topology on continuous linear maps defined based on TVS structures. I want to do the same for multilinear maps.

[Eric Wieser]

Right; I guess my question is what makes inducing that topology nontrivial

[Yury G. Kudryashov]

Inducing from ... to ...?

[Eric Wieser]

TopologicalSpace.induced AlternatingMap.toMultilinearMap

[Yury G. Kudryashov]

This step is trivial. Defining a topology on ContinuousMultilinearMap without asking for a norm is not.

[Eric Wieser]

Oh, I thought we already had that bit

[Yury G. Kudryashov]

No, we only have it for continuous linear maps, not for multilinear maps.

[Eric Wieser]

Yury G. Kudryashov said:

This is the norm added in #8691. Probably, we should update&merge it now, change the definition of topology later.

In that case we should definitely do this

[Eric Wieser]

(where between update and merge there is a "label as awaiting-review" step!)

[Yury G. Kudryashov]

Sure, I meant that I should update it and label as awaiting-review.

[Yury G. Kudryashov]

I merged master and removed commented section. I'll fix variables and docs tomorrow.

[Sophie Morel]

Yury G. Kudryashov said:

Sure, I meant that I should update it and label as awaiting-review.

Maybe wait a little, I am preparing a PR to generalize the construction of the operator norm on ContinuousMultilinearMap to the case where the spaces are only seminormed (and not necessarily normed), which will affect this too. I actually use the seminormed case in another project.

[Eric Wieser]

I think I tried that in Lean 3, and ran into typeclass timeouts (edit: !3#13566)

[Sophie Morel]

I don't have that problem now, but when generalizing the stuff of Mathlib.Analysis.NormedSpace.Multilinear.Basic to seminormed spaces, I needed to add a DecidableEq instance on ι for some things (in particular the existence of the operator norm); here ι is the type indexed the entries of the multilinear maps, so it's a Fintype. Is that kind of thing problematic ? As a mathematician, I don't have any problem making equality decidable (especially on a Fintype !), and many things about multilinear maps already require this, but maybe there is a reason I didn't see not to add the instance?

[Eric Wieser]

The fact that you need to add that sounds slightly suspicious, but it's hard to say for sure without seeing a PR

[Sophie Morel]

No PR, but I have a branch of mathlib.

[Eric Wieser]

I think you should be able to remove [DecidableEq ι] from the theorem statement and add classical to the proof?

[Eric Wieser]

Or if that fails, add letI := Classical.decEq ι to the proof, which is a bit more precise

[Sophie Morel]

Oh dear, I didn't think about that ! Thanks, I will try !

[Eric Wieser]

We used to have CI that would tell you this, but I think it was lost to lean3

[Ruben Van de Velde]

I think @Yury G. Kudryashov was working on restoring that one

[Yury G. Kudryashov]

I am not working on that yet. I asked for advice here, got no replies, and don't know how to start.

[Yury G. Kudryashov]

Sophie Morel said:

Yury G. Kudryashov said:

Sure, I meant that I should update it and label as awaiting-review.

Maybe wait a little, I am preparing a PR to generalize the construction of the operator norm on ContinuousMultilinearMap to the case where the spaces are only seminormed (and not necessarily normed), which will affect this too. I actually use the seminormed case in another project.

#8691 is almost ready anyway. We can generalize in any order.

[Sophie Morel]

As you wish. I made my PR, it is #9700. There is really very little that needs to change.

[Yury G. Kudryashov]

Assigned to myself. I'll review it over the weekend.

[Sophie Morel]

Thank you!

[Eric Wieser]

Yury G. Kudryashov said:

We have topology on continuous linear maps defined based on TVS structures. I want to do the same for multilinear maps.

Is there a tracking issue for this anywhere? I feel like TopologicalSpace (ContinuousMultilinearMap _ _ _) has been discussed before elsewhere, but I can't find the previous Zulip thread

[Eric Wieser]

Maybe

Yury G. Kudryashov said:

BTW, we can redefine topology on multilinear forms in a similar way.

is what I was thinking of

[Anatole Dedecker]

I think Yury has an open PR about that which I’m going to have a look at

[Yury G. Kudryashov]

#10777