Grassmannians

Stream: mathlib4

[Sophie Morel]

This is a sequel to #narrow/stream/287929-mathlib4/topic/Projective.20space
In that topics I announced that I had defined the smooth manifold structure on projective space, and was asked about grassmannians (for example by @Kevin Buzzard ). So grassmannians are now done too, see there: https://github.com/smorel394/Grassmannian

It is less polished than projective spaces so far, I haven't tried to optimize anything and I don't even have a readme. The definition of the ChartedSpace and SmoothManifoldWithCorners structures are in the file Manifold.lean.

The big problem I have for now is that I can't figure out how to make these instances, so there might be a lot of pain when I start working with smooth maps on grassmannians. I don't really understand instances but I think of them as "canonical structures", so the problem might be that my ChartedSpace structure is not canonical ? It depends on a model space $U$ and on a choice of isomorphism between $U$ and a codimension $r$ subspace of $E$ (the space of which I take the grassmannian). For projective spaces I solved that problem by using the axiom of choice to pick $U$ and the isomorphism, but then I got complaints because my model space was strange. But I really don't see what else I can do, if I want a ChartedSpace instance. Any advice ?

[Johan Commelin]

Let me try if this trick works one more time: If you've done $\mathbb{P}^n$ and Grassmanians, shouldn't you really actually do Quot schemes? :stuck_out_tongue_wink:

[Sophie Morel]

Johan Commelin said:

Let me try if this trick works one more time: If you've done $\mathbb{P}^n$ and Grassmanians, shouldn't you really actually do Quot schemes? :stuck_out_tongue_wink:

Do we have schemes in mathlib now ?

Can't you help with my instance problem instead of torturing me ? :pleading_face:

[Johan Commelin]

On a more serious note: @Sophie Morel can you please link to where the exact definition is that you would like to make an instance?

[Sophie Morel]

https://github.com/smorel394/Grassmannian/blob/master/Grassmannian/Manifold.lean line 103

[Johan Commelin]

Hmmz, so does that declaration depend on $\varepsilon$?

[Johan Commelin]

One trick (but a bit ugly) is to make $U$ and/or $\varepsilon$ explicit as argument to Grassmanian.

[Sophie Morel]

Yes, the ChartedSpace structure depends on $\varepsilon$, I suppose that's the problem.

[Sophie Morel]

Hm, interesting trick.

[Sophie Morel]

The other solution is to use choice to pick an $\varepsilon$. I would incline towards that, since in my experience the precise model is unimportant.

[Johan Commelin]

Yeah, it's a bit ugly from an informal maths POV. But it will certainly make typeclass inference happier (-;

[Sophie Morel]

So which do you think is less ugly: make $\varepsilon$ an explicit argument of Grassmannian, or use choice to pick an $\varepsilon$ ?

[Sophie Morel]

I suppose what I could do if I choose the first solution is make a copy of the Grassmannian type that will carry the ChartedSpace structure. I don't want Grassmannian as a topological space to have $\varepsilon$ as an argument, because it doesn't depend on $\varepsilon$ !

[Johan Commelin]

If you want to use choice to pick $\varepsilon$ then you need to add another hypothesis, roughly asserting that $\varepsilon$ exists, right?

[Johan Commelin]

Some Prop fact about the dimension of U and how it relates to r...

[Johan Commelin]

Or would you also pick U directly, as part of that choice?

[Sophie Morel]

Johan Commelin said:

If you want to use choice to pick $\varepsilon$ then you need to add another hypothesis, roughly asserting that $\varepsilon$ exists, right?

Yes, but if I want things to be canonical I would do a definition by cases: if $E$ has dimension at least $r$ then an $\varepsilon$ exists, otherwise the grasssmannian is empty hence has a trivial ChartedSpace structure.

[Sophie Morel]

Johan Commelin said:

Or would you also pick U directly, as part of that choice?

In fact I would pick a continuous linear surjection from E to Fin r → 𝕜. I already have a construction somewhere that deduces an U and an $\varepsilon$.

[Sophie Morel]

And to construct such a continuous linear surjection, I just need a SeparatingDual instance on $E$ and a suspace of $E$ of dimension $r$ (i.e. a point of the grassmannian). I also have code doing that.

[Johan Commelin]

Hmm, I very much agree that the topology doesn't depend on any of this, so it also shouldn't be made visible in the type of Grassmanian. But I don't know what the best way is to deal with the ChartedSpace instance.

[Sophie Morel]

I cannot find the definition of a ChartedSpace structure on an empty type in mathlib, which disappoints me deeply. :grinning_face_with_smiling_eyes: Still, I think I can manage to construct it.

[Johan Commelin]

The problem is possibly again: what is the model? There is no canonical choice in this case, right?

[Johan Commelin]

You probably can't find an instance for a 1-pt space either...

[Sophie Morel]

Nope. If $E$ is finite-dimensional of dimension $n+r$ then you could argue that $\mathrm{Fin}\ n \to \mathbb{k}$ is the canonical model.

[Sophie Morel]

But I wrote everything for a possibly infinite-dimensional space $E$...

[Johan Commelin]

For the Grassmanian, yes. But for Empty...

[Sophie Morel]

Ah, for Empty, I don't know...

[Sophie Morel]

You can just use $\mathbb{k}$, I suppose. Since there will be no charts, it doesn't matter, and $\mathbb{k}$ is already part of the data. (If you are working with grassmannians at least.)

[Sophie Morel]

Or maybe it would make more sense to use $\{0\}$. I'm not sure it matters all that much.

[Yaël Dillies]

"What is the model of the empty manifold?" is truly a mathlib question :rofl:

[Damiano Testa]

I would say that it is not entirely devoid of content. Especially if you use the model to determine its dimension.

[Sophie Morel]

What is the dimension of the empty space in mathlib ? Is it $0$ or $-\infty$ ?

[Johan Commelin]

Well, you first need to give a definition of dimension, I fear

[Damiano Testa]

For polynomials, there are degree and natDegree and in natDegree you would get 0, while with degree you would get $-\infty$.

[Damiano Testa]

I imagine that there will be a natDim and a dim...

[Johan Commelin]

Or maybe dim will be a locally constant function to Nat?

[Damiano Testa]

So, sheafDim, dim, natDim, ...

[Anatole Dedecker]

I assume this question was discussed a long time ago (probably before I even learned what a manifold was), but both this thread and the last one on projective spaces make me wonder wether we really want to choose a fixed model space for the whole manifold. One could imagine a definition of manifolds where structure groupoids are replaced by any sub-groupoid (in the categoretical sense) of Top. But I feel like this must have been ruled out for technical reasons that I don't immediately see...

[Kevin Buzzard]

Sophie Morel said:

I cannot find the definition of a ChartedSpace structure on an empty type in mathlib, which disappoints me deeply. :grinning_face_with_smiling_eyes: Still, I think I can manage to construct it.

To prove that the empty set had a perfectoid space structure we had to prove that the trivial topological ring was an arbitrary product of trivial topological rings in the category of topological rings (becuase you can cover the empty set by arbitrarily many empty sets...)

[Anatole Dedecker]

Isn't the model space explicit in docs#ChartedSpace? Which means that we could put a manifold structure on the empty set for any topological vector space?

[Kevin Buzzard]

Damiano Testa said:

For polynomials, there are degree and natDegree and in natDegree you would get 0, while with degree you would get $-\infty$.

Two of my PhD students are thinking about dimension, and indeed they are considering the same set-up, this time with WithBot (WithTop Nat) and Nat.

[Anatole Dedecker]

(Sorry if I'm saying nonsense, I've never actually touched the manifold library)

[Damiano Testa]

Honestly, I think that the more "aesthetic" definition is degree/dim, even though it only really started making sense with formalization for me. However, the automation around Nat is so much better than around WithBot Nat, that I prefer to use natDegree. I would really like this to change, though.

[Sophie Morel]

Anatole Dedecker said:

Isn't the model space explicit in docs#ChartedSpace? Which means that we could put a manifold structure on the empty set for any topological vector space?

Yes, I think so.

[Sophie Morel]

Anatole Dedecker said:

I assume this question was discussed a long time ago (probably before I even learned what a manifold was), but both this thread and the last one on projective spaces make me wonder wether we really want to choose a fixed model space for the whole manifold. One could imagine a definition of manifolds where structure groupoids are replaced by any sub-groupoid (in the categoretical sense) of Top. But I feel like this must have been ruled out for technical reasons that I don't immediately see...

In these examples, it is clear that the "natural" model depends on the point at which you take a chart. On the other hands, there are ContinuousLinearEquiv's between all these models, and these are diffeomorphisms, and so in practice it has not made a difference for me what model I chose (so far).

[Damiano Testa]

Maybe the correct answer is that you should use a torsor under a topological vector space as model and then you use the empty torsor for the empty manifold, at which point maybe the actual vector space is irrelevant!

[Sophie Morel]

Okay, but say I want to finish formalizing the manifold structure on grassmannians in finite time...

[Damiano Testa]

So many requirements...

[Sophie Morel]

I already have to rewrite part of the normed space library if I want to get quaternionic grassmannians...

[Yaël Dillies]

What parts? I'm interested to know.

[Sophie Morel]

The parts of the automatic continuity of linear maps whose source is finite-dimensional. (RIght now we require the base ring to be a NontriviallyNormedField, but NontriviallyNormedDivisionRing would be sufficient.)
I did some of it there: https://github.com/leanprover-community/mathlib4/tree/NontriviallNormedDivisionRing
But it's not enough.

[Anatole Dedecker]

I think it would be nice to discuss that in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/NormedModule.20.3F, the fact that we have twenty different threads with twenty different plans is not making it easy to agree on a plan :sweat_smile:

[Anatole Dedecker]

And I'd be happy to help once we've agreed on what's needed and a general plan!

[Sophie Morel]

My plan was less ambitious. I just noticed that some mathlib results still compiled if you made the base field into a base division ring. But yes, it would be nice to have NormedModule.

[Anatole Dedecker]

Oh yes for that part there's no real need to wait

[Sophie Morel]

Well, I did have to define a NontriviallyNormedDivisionRing class, but it's exactly what you would expect.

[Eric Wieser]

Even if it's not enough, it might be nice to start merging the generalization into mathlib!

[Anatole Dedecker]

Sophie Morel said:

Well, I did have to define a NontriviallyNormedDivisionRing class, but it's exactly what you would expect.

This name triggers my un-bundling instinct. Do we really hate [Field F] [NormedRing F] that much?

[Sophie Morel]

We already have NontriviallyNormedField. Attack that one first.

[Yaël Dillies]

This is really a question for another thread, Anatole!

[Sophie Morel]

It's not just a normed field, there's also a condition that the norm is not trivial.

[Anatole Dedecker]

Sophie Morel said:

It's not just a normed field, there's also a condition that the norm is not trivial.

I know, but I was suggesting un-bundling the algebra and normed structures in general to reduce the amount of boilerplate necessary. But this would be a huge refactor and, as Yaël said, it's mostly orthogonal to the current discussion.

[Sebastien Gouezel]

The model space in ChartedSpace is indeed explicit to allow for different charted space structure on the same type. So the empty type can be a charted space on everything simultaneously. At the start of the library, the model space was an outparam (i.e., meant to be unique), but this created nasty diamonds with products, so that's why we switched to an explicit one. In the same way, when you speak of smooth functions on a manifold M, there is always an explicit gadget (typically called I) saying which model space you're using (and also how the model space embeds in a given vector space).

[Sophie Morel]

Okay, so I tried a little bit to handle the case of empty grassmannian, it got nasty and I said "screw all this". So now we get ChartedSpace and SmoothManifoldWithCorners instances on the grassmannian (with a model space picked by Classical.choice), given you put a Nonempty instance on the grassmannian first.
I also kept the code defining the ChartedSpace etc structures from an explicit choice of model, so anybody can choose their favorite model in a given situation.

[Sophie Morel]

I'll write a couple of helper lemmas to prove non-emptiness of the grassmannian (like "if the finrank is at least $r$ then the grassmannian is not empty").

[Antoine Chambert-Loir]

(deleted)

[Alena Gusakov]

Out of curiosity, is there any work for the cardinality of a Grassmannian (or more specifically, q-deformed binomial coefficients)? I have some work for that in Lean 3 that I'd like to port over, but if it's been done already then I won't worry about it. I couldn't find it in the Grassmannian.lean file so I figured I'd ask.