Grassmannians

Stream: maths

[Kenny Lau]

#PR reviews > #26060 Grassmannians #26060 is Grassmannians. One issue is that the convention is to take F-submodules of V of dimension k, but this cannot be generalised, and is only valid for fields with finite dimensional subspaces. So, in EGA, Grothendieck used instead the quotients of M that are locally free with rank k.

[Kenny Lau]

if you follow the submodule definition, you get two problems:

1. over a field F, if V is a countably infinite direct sum of F, then the submodules with dimension 1 would also look like V (after taking a chart), but (R => infinite direct sum of R) is actually not a representable functor.
2. over a ring R with trivial class group, if you take R itself, then the set becomes { non-zero-divisors of R } / Rˣ, which also doesn't look really representable to me.

[Calle Sönne]

I think that when talking about the Grassmannian as a scheme you always interpret it to mean quotients of a certain rank. I looked quickly in both Vakil and Görtz-Wedhorn now and they both do it this way, however the numbering is different, where the quotients are of rank "k" and "n-k" respectively.

[Calle Sönne]

So within AG you are definitely following the convention (I mean Grothendieck did it), and when it comes to numbering I'm not sure if there exists an established convention that everyone uses. But maybe someone else knows more about this than me.

[Matthew Ballard]

Correctly - quotients. Informally - subspaces. Seems like there are two types here.

[Kenny Lau]

The previous iteration of the #mathlib4 > Grassmannians thread (2 years ago) was focused on manifolds, so naturally they followed the subspace indexing :melt:

[Kenny Lau]

Let me also add that if you agree with the quotient definition, then you have to use quotient indexing, because n-k makes no sense if n is infinite.

[Calle Sönne]

Are you just concerned about the indexing? Because then I think it just varies in the literature. But when it comes to which one you demand to be locally free (the quotient or the subspace), then only one of them gives you the right answer for schemes.

[Kenny Lau]

I'm not concerned about anything, I know that only the quotient definition and indexing are correct.

[Kenny Lau]

I just apparently have to convince everyone else as well that this is the case, despite a different convention existing when specialising in fields and finite dimensional vector spaces.

[Calle Sönne]

Okay but what I'm saying is that you are not even challenging the conventions, because only one of the options is correct (the one you have chosen).

[Kenny Lau]

The subspace convention does unfortunately exist in a lot of places

[Kenny Lau]

(and it is correct if you restrict to finite dimensional vector spaces over fields, which is why it is so persistent)

[Calle Sönne]

Yes but surely not in AG (which is where you plan to apply this anyways right)?

[Kenny Lau]

yes, but I still need to convince other people (e.g. @Eric Wieser )

[Calle Sönne]

I think your original phrasing in that docstring was confusing, because it seemed to imply that there was an existing convention that you chose to go against.

[Kenny Lau]

yes, there was an existing convention when people were talking about grassmannians over f.d.vec.s./field

[Kenny Lau]

Notice how Stacks hilariously starts with

loosely speaking parametrize k-dimensional subspaces of n-space

and then immediately follows it with

for technical reasons it is more convenient to parametrize (n−k)-dimensional quotients

(oh and yeah they only did it for the free module of rank n)

[Kenny Lau]

it's not "technical" or "convenient", it's just wrong to do it the other way :melt:

[Calle Sönne]

Okay sure but you are defining it in a more general setting, and in this setting there is only one correct option (and that is the convention).

[Calle Sönne]

I think no one defines the grassmannian over anything other than fields to parametrize locally free submodules.

[Kenny Lau]

yes, but it's also rarer to generalise grassmannians unless you're really deep into AG

[Kenny Lau]

people usually just stop at f.d.vec.s./field

[Kenny Lau]

@Calle Sönne maybe i should put something in the docstring like:?

this is different from a convention used for finite dimensional vector spaces over fields, where the k-th Grassmannian parameterises k-dimensional subspaces instead of quotients

[Mario Carneiro]

I don't see why this is about a battle of definitions, I just see two different definitions here

[Mario Carneiro]

it sounds like you want grassmannians and cograssmannians

[Mario Carneiro]

over an infinite dimensional vector space, wouldn't you still have 2 dimensional subspaces in it?

[Kenny Lau]

yes, but it's no longer representable, so it isn't a scheme

[Mario Carneiro]

okay?

[Mario Carneiro]

I have to admit I don't know what that entails

[Mario Carneiro]

I'm just thinking about it from a linear algebra perspective

[Kenny Lau]

hmm...

[Kenny Lau]

Mario Carneiro said:

it sounds like you want grassmannians and cograssmannians

which one are you naming the cograssmannian?

[Calle Sönne]

I think if someone really wants the other convention they can think about the implementation of that later. But most likely all the statements they want to prove will need to assume the ring is a field. And furthermore they can probably transfer a lot of theorems that Kenny will prove by identifying it with the AG grassmannian of the dual of the vector space they were working with.

[Kenny Lau]

yes, either G(k;V*), or G(n-k;V) (both are canonical)

[Mario Carneiro]

Kenny Lau said:

Mario Carneiro said:

it sounds like you want grassmannians and cograssmannians

which one are you naming the cograssmannian?

heh

[Mario Carneiro]

I think the one you are advocating for looks more co- to me

[Mario Carneiro]

but I am not at all an authoritative source on this, ask someone who actually works with this thing

[Mario Carneiro]

I do think it is telling that baby's first grassmannian is usually presented with subspaces of a vector space, not quotients

[Kenny Lau]

Mario Carneiro said:

but I am not at all an authoritative source on this, ask someone who actually works with this thing

An algebraic geometer would tell you the quotient, and a differential geometer would tell you the subspace

[Kenny Lau]

Mario Carneiro said:

I do think it is telling that baby's first grassmannian is usually presented with subspaces of a vector space, not quotients

A baby usually doesn't learn algebraic geometry

[Kevin Buzzard]

babies learn differential geometry first :-)

[Eric Wieser]

Kenny Lau said:

yes, but I still need to convince other people (e.g. Eric Wieser )

I don't want to be convinced, I wanted you to write stuff down and convince other people. Consider my opinion irrelevant now.

[Andrew Yang]

Some data points:

• EGA I 9.7 (2nd edition) defined $\mathbf{G}^n(E)$ to be the rank $n$ subspaces of $E$, and $\mathrm{Grass}_n(\mathcal{E})$ to be the locally free rank $n$ quotients of $\mathcal{E}$ (and remarked that the fiber of the scheme representing $\mathrm{Grass}_n(\mathcal{E})$ is isomorphic to $\mathbf{G}^n(\check{\mathcal{E}_s})$
• Stacks defined (in stacks#089R) $G(k, n)$ to be the locally free rank $n-k$ quotients of $\mathcal{O}_S^n$.
• The rising sea defines $G(k, n)$ to be the locally free rank $k$ quotients of $\mathcal{O}_S^n$, and $\mathbb{G}(k, n)$ be the functor sending a scheme $B$ to the set of finitely presented, flat, closed subschemes of $\mathbb{P}^n_B$ whose fibers look like $\mathbb{P}^k$. The claim (in 25.3.3) is $G(k, n)$ represents $\mathbb{G}(k-1, n-1)$

[Kevin Buzzard]

Thanks Andrew. I'm tempted to conclude that the literature is a mess and that we should do whatever is best for mathlib and then document it clearly.

Note that to make matters worse, in the classical case (finite-dimensional vector space over a field) the space of rank n subspaces is isomorphic (noncanonically in general) to the space of rank n quotients.

[Kenny Lau]

Ok, so let's say I write something like:

In the literature, two conventions exist:

1. The k-th Grassmannian parametrises k-dimensional subspaces of a given finite dimensional vector space over a field.
2. The k-th Grassmannian parametrises quotients that are locally free of rank k, of a given module over a ring.

We note that the first definition cannot be generalised beyond the stated setting, but the second definition can be generalised to arbitrary rings, and then to schemes as well, so this is the definition that we have chosen.

Note that one can recover the first definition by noting that for a finite dimensional vector space V over a field, k-dimensional subspaces of V are canonically equivalent to (n-k)-dimensional quotients of V, and also to k-dimensional quotients of V*, the dual of V.

[Kenny Lau]

@Kevin Buzzard would you edit anything from this description?

[Kevin Buzzard]

That looks great to me

[Mario Carneiro]

k-dimensional subspaces of V are canonically equivalent to (n-k)-dimensional quotients of V

is this true? I thought the equivalence was not canonical

[Mario Carneiro]

part of the reason I think there should be two definitions is because it's not really the case that one is a special case of the other

[Mario Carneiro]

they are equivalent only in a very high level mathematician's = sense, mathlib generally wants better defeqs than you get from this kind of embedding

[Kenny Lau]

Mario Carneiro said:

k-dimensional subspaces of V are canonically equivalent to (n-k)-dimensional quotients of V

is this true? I thought the equivalence was not canonical

The map in -> direction is "take the quotient", and in <- direction is "take the kernel"

[Kenny Lau]

Mario Carneiro said:

part of the reason I think there should be two definitions is because it's not really the case that one is a special case of the other

We're put in a bit of a difficult situation then... we can't name both Grassmannian, so one of them will have to give way for the other

[Eric Wieser]

AlgebraicGeometry.Grassmannian vs Module.Grassmannian?

[Oliver Nash]

I might also observe that differential geometers consider Grassmannians over non-commutative scalars, such as the quaternions. For example quaternionic projective space is an important model geometry exhibiting one of Berger's irreducible holonomy groups.

[Kenny Lau]

Eric Wieser said:

AlgebraicGeometry.Grassmannian vs Module.Grassmannian?

I would reserve both for quotient indexing, and then maybe DifferentialGeometry.Grassmannian for the subspace indexing

[Kenny Lau]

Mario Carneiro said:

they are equivalent only in a very high level mathematician's = sense, mathlib generally wants better defeqs than you get from this kind of embedding

actually... they might be defeq

[Kenny Lau]

when people see the words "k-dimensional quotients", they think the definition is some equivalence class of surjections to R^k, but Kevin has discovered that it's way better to just record the submodule, so actually in the file, the k-th grassmannian is defined as:

@[stacks 089R] structure Grassmannian extends Submodule R M where
  finite_quotient : Module.Finite R (M ⧸ toSubmodule)
  projective_quotient : Projective R (M ⧸ toSubmodule)
  rankAtStalk_eq : ∀ p, rankAtStalk (R := R) (M ⧸ toSubmodule) p = k

[Kenny Lau]

so when M is now a vector space over field F with dimension n, then abbrev DG.Grassmannian := Grassmannian F M (n-k) is now recording k-dimensional subspaces!

[Kenny Lau]

once you have the correct API, then nobody can even tell the difference!

def DG.Grassmannian.mk (N : Submodule F V) (hn : dim N = k) :=

theorem DG.Grassmannian.dim_eq (N : DG.Grassmannian F V k) : dim N.toSubmodul = k :=

[Kenny Lau]

@Mario Carneiro if you think this path is worth pursuing, I can (try to) produce a MWE to let you see what the code would actually look like

[Kenny Lau]

Andrew Yang said:

• EGA I 9.7 (2nd edition) defined $\mathbf{G}^n(E)$ to be the rank $n$ subspaces of $E$, and $\mathrm{Grass}_n(\mathcal{E})$ to be the locally free rank $n$ quotients of $\mathcal{E}$ (and remarked that the fiber of the scheme representing $\mathrm{Grass}_n(\mathcal{E})$ is isomorphic to $\mathbf{G}^n(\check{\mathcal{E}_s})$

uh... should i introduce the notations as G^ and G_ then? :melt:

[Kenny Lau]

i.e. G_(k, M; R)

[Kenny Lau]

I have updated the docstring in #26060 and renamed it to Module.Grassmannian

[Mario Carneiro]

Kenny Lau said:

Andrew Yang said:

• EGA I 9.7 (2nd edition) defined $\mathbf{G}^n(E)$ to be the rank $n$ subspaces of $E$, and $\mathrm{Grass}_n(\mathcal{E})$ to be the locally free rank $n$ quotients of $\mathcal{E}$ (and remarked that the fiber of the scheme representing $\mathrm{Grass}_n(\mathcal{E})$ is isomorphic to $\mathbf{G}^n(\check{\mathcal{E}_s})$

uh... should i introduce the notations as G^ and G_ then? :melt:

G(n, E) and ⅁(n, E)

[Kenny Lau]

I'm not sure if that was a serious suggestion.

[Oliver Nash]

Kenny Lau said:

I have updated the docstring in #26060 and renamed it to Module.Grassmannian

This still won't cover the quaternionic coefficients though, right?

[Kenny Lau]

@Oliver Nash the proposal is to define Geometry.Grassmannian in some other generality

[Oliver Nash]

Ah OK, so two definitions. Indeed that seemed necessary to me.

[Kenny Lau]

presumably in this case, I'll define it for modules over division rings (no finite dimension hypothesis)

[Kenny Lau]

that's why I asked about two notations too

[Oliver Nash]

I see. Somewhat independently, it seems a shame to need two notations. Presumably it will be very, very rare to have an argument dealing with both notions at once so I'd prefer to be able to tie the notation to whichever definition I was working on locally.

[Junyan Xu]

Kenny Lau said:

yes, either G(k;V*), or G(n-k;V) (both are canonical)

Let me remark there's Subspace.orderIsoFiniteCodimDim in mathlib (I added it) but we should restrict it to an Equiv between subspaces of fixed (co)dimension.

[Junyan Xu]

In #14686 there's also a comment

We consider the Grassmannian parametrizing r-dimensional quotients of V instead of
r-dimensional subspaces of V, because this is more natural when working over a general
ring (or scheme).

The Zulip thread is #AIM24: alg geom formalization > Grassmannians (probably not publicly accessible)

Kenny Lau said:

The previous iteration of the #mathlib4 > Grassmannians thread (2 years ago) was focused on manifolds, so naturally they followed the subspace indexing :melt:

There were also discussions at #Lean Together 2024 > Formalization of Grassmannians (recording of talk)

[Michał Mrugała]

@Kevin Buzzard I seem to recall there being a student at Imperial who did Grassmannians as a project this year, did anything come of it?

[Kevin Buzzard]

They wrote a nice project and some code which Kenny is aware of

[Kevin Buzzard]

They used the quotient convention btw

[Antoine Chambert-Loir]

Kenny Lau said:

Mario Carneiro said:

it sounds like you want grassmannians and cograssmannians

which one are you naming the cograssmannian?

The other one.

[Andrew Yang]

Andrew Yang said:

• The rising sea defines $G(k, n)$ to be the locally free rank $k$ quotients of $\mathcal{O}_S^n$, and $\mathbb{G}(k, n)$ be the functor sending a scheme $B$ to the set of finitely presented, flat, closed subschemes of $\mathbb{P}^n_B$ whose fibers look like $\mathbb{P}^k$. The claim (in 25.3.3) is $G(k, n)$ represents $\mathbb{G}(k-1, n-1)$

I Am Not a Algebraic Geometer (nor differential) but this seems to suggest rank $k$ locally free quotient sheaves correspond to $k$ dimensional subspaces geometrically? So maybe it is the same thing all along?

[Kenny Lau]

"geometrically" means evaluating at fields