Projective Space

Stream: maths

[Kenny Lau]

@Andrew Yang @David Ang @Kevin Buzzard I’m currently thinking about defining the following mathematical object:

Given a (comm semi)ring R and a module M, and also an indexing set n, form the following subquotient:

1. The full space is n -> M, i.e. M^n.
2. The subobject is n -> M whose image spans M.
3. Then quotient by the action defined by (Units R).

And I have a few questions / statements:

1. If we consider M across Pic R, we will recover P^n(R), so there is no generality that is lost here.
2. I intentionally left out any invertibility assumption on M, or anything close to that.
3. I propose to call this object ProjCoords R M n in mathlib4.
4. We might want to do the quotient first and then prove that the condition respects the setoid; though on second thought maybe there is no difference.
5. David, I think in the recent future I would want to refactor your current projective elliptic curve in mathlib using this new object. Maybe we will start with ProjCoords R R (Fin 3) first, before relaxing the second R to be M.

What are your thoughts?

[Kenny Lau]

(I basically invented this object, so I don’t know if anyone else has done it before, and if it already has a name in the literature.)

[Calle Sönne]

Kenny Lau said:

Andrew Yang David Ang Kevin Buzzard I’m currently thinking about defining the following mathematical object:

Given a (comm semi)ring R and a module M, and also an indexing set n, form the following subquotient:

1. The full space is n -> M, i.e. M^n.
2. The subobject is n -> M whose image spans M.
3. Then quotient by the action defined by (Units R).

And I have a few questions / statements:

1. If we consider M across Pic R, we will recover P^n(R), so there is no generality that is lost here.
2. I intentionally left out any invertibility assumption on M, or anything close to that.
3. I propose to call this object ProjCoords R M n in mathlib4.
4. We might want to do the quotient first and then prove that the condition respects the setoid; though on second thought maybe there is no difference.
5. David, I think in the recent future I would want to refactor your current projective elliptic curve in mathlib using this new object. Maybe we will start with ProjCoords R R (Fin 3) first, before relaxing the second R to be M.

What are your thoughts?

@Kevin Buzzard had/has an M4R student working on Grasmannians, maybe projective space should be obtained as a specialization of this. But I don't know how close that code is to PR-ready (or what the eventual conclusion of this project was).

[Eric Wieser]

I assume docs#Projectivization is the wrong thing here?

[Kevin Buzzard]

Yes that only works for division rings

[Kevin Buzzard]

To be honest it could probably be beefed up for general rings but then it will be harder to use for fields

[Kevin Buzzard]

I would hesitate to start refactoring elliptic curves though. Our definition is already wrong and changes that you suggest won't make it right, they'll just make it less wrong. Our current definition is fine for fields (less general than rings) and what we really want is a definition which works for schemes (more general than rings), so it's not clear to me who you're actually helping if you tinker with the definition which we essentially accidentally have for rings (I say accidentally because in some sense it's an accident that it type checks, it's the wrong definition in general as I explain in great detail in docstrings)

[David Ang]

Note that there was a similar proposal here about two years ago

[David Ang]

Personally I don't like the current API for projective coordinates in elliptic curves in terms of Fin 3 -> R + nonsingular condition, and I proposed #24593 to change this into R x R x R + nonsingular condition so that more things are defeq. What you're proposing is to change this into Fin n -> R + image spans R + nonsingular condition, which is going to revert that PR. Unless you have a way of maintaining the defeqs from R x R x R without adding a tonne of extra rewrites, I would much rather have something like R x R x R + image spans R + nonsingular condition.

Note that the nonsingular condition implies that the image spans R, but I'm happy for this to be added (e.g. it allows Jacobian.comp_equiv_comp to be written without the nonsingular condition, since this is true for any weighted projective coordinates). Note that I am strongly inclined to keep the Jacobian and projective coordinates API essentially identical (which helps with maintenance immensely), so you'd need to define a weighted version of ProjCoords if you want to do the refactor.

[David Ang]

But otherwise I'm all for your proposal - why don't you redefine Projectivization to be this rather than calling it ProjCoords?

[Kenny Lau]

@Calle Sönne When Kevin Buzzard mentioned it to me, I thought that we could have both and then some relation between them. I don’t know what the general philosophy here, I thought that having a more special thing vs a more general thing generally shouldn’t be a conflict because different degrees of generalisation could have different uses. For example, a mathematician would see Fin 2 -> R and R x R to be the same object, but for mathlib I think we definitely want to be able to write both Fin n -> R and also R x R.

@Kevin Buzzard what I’m proposing here would seem to me to be “one more step in the right direction”. For example, as I’ve mentioned, the functor represented by P^n(R) could be seen as the disjoint union of my objects ProjCoords R M n across M : Pic (R). So, similarly, given a cubic for a ring (I know it doesn’t always exist), the correct E(R) would also be a disjoint union of the refactored points.

Taking a step back, would you agree that it would be a good idea to have my proposed object even if I don’t refactor elliptic curves using it?

@David Ang there might be a general point to be made on how much we rely on defeq, but perhaps that’s a discussion for another day. I’ll look into your linked PR later to get more information.

What if we made a “power type” so that R ^ 3 is defeq to R x R x R? This might be useful to have in general, and I think this might even be a good step in general and we could develop this a lot to be used in way larger generality? I feel like we haven’t paid enough attention to the low dimensional cases and we’ve just taken Fin n -> R as axiom.

As another alternative, what if both versions coexist? Then you would keep your Projective folder, and I would have a new folder ProjCoords?

@Eric Wieser You might be in a better position to answer my question above. This is also related to Projectivisation. In general, do you think it’s a better idea to have different degrees of generality coexisting, or to define just the most general thing and then keep specialising?

[Eric Wieser]

I don't understand why you want R ^n at all here rather that a general vector space / free module

[Eric Wieser]

Kevin Buzzard said:

To be honest it could probably be beefed up for general rings but then it will be harder to use for fields

Should I take it that this means that simply replacing Field with Ring gives the wrong generalization?

[Kevin Buzzard]

Yeah, you have to replace "vector isn't zero" with "ideal generated by the coefficients of the vector is the entire ring" which is more annoying to deal with

[Eric Wieser]

I don't think the definition uses "vector isn't zero?

[David Ang]

Does it not?

variable (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V]

/-- The setoid whose quotient is the projectivization of `V`. -/
def projectivizationSetoid : Setoid { v : V // v ≠ 0 } :=
  (MulAction.orbitRel Kˣ V).comap (↑)

/-- The projectivization of the `K`-vector space `V`.
The notation `ℙ K V` is preferred. -/
def Projectivization := Quotient (projectivizationSetoid K V)

[David Ang]

I think it's a bad idea to have two (equally weighted) projective coordinates for elliptic curves! Why would we ever need two?

[Kenny Lau]

Eric Wieser said:

I don't understand why you want R ^n at all here rather that a general vector space / free module

when you unfold all of the definitions etc. then the object actually has very little do with M^n (in the notation of my original exposition); it's really to do with "n elements in M" that satisfy certain properties etc.

[Kenny Lau]

(yes, in the case of M := R, then it does have to do with R^n, but that's the wrong generalisation)

[Kenny Lau]

Eric Wieser said:

I don't understand why you want R ^n at all here rather that a general vector space / free module

I do want to explicitly control the "dimension" here as well. As I've mentioned above, the correct model for P^n(R) is Σ M : Pic (R), ProjCoords R M n. Note how n is explicit there and corresponds to the subscript n in P^n.

[Kenny Lau]

and yeah I also want to control the module M explicitly.

[Kenny Lau]

so I'm not advocating to "projectivise" an arbitrary (free or not) module, that's the wrong generalisation

[Kenny Lau]

It's a bit hard in general to gauge the consensus of the community because people don't tend to reply in concrete terms. Without the consensus, then I can't make sure that after I spend time working on this new object, people won't just say "but like why would you make this object?", and we all know how long PR's can take.

To summarise, I propose to define the object ProjCoords R M n where R is a (comm semi)ring, M is a module over R, and n is an arbitrary indexing type. It will be a subquotient of n -> M, namely take { f : n -> M | image of f spans M }, and then quotient by the natural action by Units R.

So, with that in mind, could people react to this message with an indication of their opinion?

• :thumbs_up: I would be happy to see this object in Mathlib4.
• :thumbs_down: I would not want to see this object in Mathlib4.
• :hammer_and_wrench: I would propose some modifications (please specify, including change of name).

[David Ang]

I would be happy to see this object in Mathlib4 if it replaces Projectivization

[Calle Sönne]

What is the point of fixing M? If I've understood correctly, when Pic(R) is non-trivial, and M is in Pic(R) then ProjCoords R M n will be a subset of P^n(R). Why are we interested in this subset for say M non-isomorphic to R?

[Kenny Lau]

@David Ang Earlier I expressed hesitation of replacing Projectivization with the reason of "maybe we want general things and specialised cases to co-exist". Now I actually come with a very strong reason of why these two objects are not compatible.

Firstly, Projectivization K V works with an arbitrary module over a division ring. The lack of commutativity might be a concern, I haven't really thought about it, maybe we can make my object work without commutativity as well.

Secondly, V is not given a basis. To say that it is equivalent to an instance of my ProjCoords R R n (I'm assuming you want M := R here), you're essentially choosing a basis. While there might be a short convenient idiom to do so, this transformation is highly non-canonical. I searched Projectivization on Loogle, and there are certainly some results that can be transformed this way, such as those that involve Fin 3, but there are also results that cannot. The strongest example here is Projectivization.Subspace, which just does not have an (easy) equivalent. (you could probably cook up an equivalent definition such as maybe ProjCoords R R m injecting into ProjCoords R R n, but that feels "different" and is not actually a more general definition).

(The same reason is why we can't just teach linear algebra using matrices, because you'll naturally run into subspaces like { (x,y,z) | x+y+z=0 } which is not canonically isomorphic to K^2.)

And thirdly, I've kept the strongest reason to the last: it actually breaks if dim V is aleph-0! My ProjCoords K K n corresponds to Projectivization K (n -> K), and it's actually a theorem that direct products of K never have dimension aleph-0. This means that if V has dimension aleph-0, then there is no n such that ProjCoords K K n is equivalent to Projectivization K V!

(This is also making me wonder about what scheme would naturally correspond to ℕ →₀ K. Maybe we can build an "affine space with finite support"? Anyway, this is a topic for another discussion.)

[Calle Sönne]

(continuing my comment above). Wouldn't you want to treat all M (in Pic(R) for now) at the same time, so that you get ProjCoords R n consisting of tuples (M, n->M) where the second factor satisfied your condition from before.

[Kenny Lau]

Calle Sönne said:

What is the point of fixing M? If I've understood correctly, when Pic(R) is non-trivial, and M is in Pic(R) then ProjCoords R M n will be a subset of P^n(R). Why are we interested in this subset for say M non-isomorphic to R?

I suppose there is a bigger point here to be made. Let's say we want to talk about the scheme GL_n, and I give you an explicit definition right now (it's Spec ℤ[a11, ..., ann, 1/Det(aij)]). Are we done here? In my personal philosophy (I don't know if this aligns with Mathlib's philosophy), I would say that we are not done, and we would actually want to construct GL_n(R) separately first (functor CommRing ⥤ Grp), and then prove that the scheme GL_n represents the functor GL_n(R).

(There's actually an extra bonus point that comes with first defining the functor, because we get a cogroup structure for free on that big explicit ring.)

So in the same vein, I would also want to construct the functor explicitly first, and then prove that P^n represents the functor. In this case, the functor is just the disjoint union of ProjCoords R M n across M : Pic R.

Calle Sönne said:

(continuing my comment above). Wouldn't you want to treat all M (in Pic(R) for now) at the same time, so that you get ProjCoords R n consisting of tuples (M, n->M) where the second factor satisfied your condition from before.

Then we can't talk about other invertible modules that happen to not be (definitionally) equal to terms of Pic R. My personal philosophy here is that I would want to split things into more steps, with smaller objects in each step, and also in greater generality.

[Calle Sönne]

Okay I think your second point is good :)

[Calle Sönne]

Although could you not just rephrase it in a more general way? Like as pairs (M, n->M) such that we have [IsInvertible M] (I dont know if this class exists)?

[Kenny Lau]

Calle Sönne said:

[IsInvertible M] (I dont know if this class exists)?

All part of the ongoing PR #25337 (please review!)

[Kenny Lau]

Calle Sönne said:

Although could you not just rephrase it in a more general way? Like as pairs (M, n->M) such that we have [IsInvertible M] (I dont know if this class exists)?

Then that statement you're implicitly referring to is false. You must take isomorphism classes to produce the correct functor represented by P^n.

[Calle Sönne]

Okay good point. But let me ask: what do you expect to gain from this definition for rings with non-trivial picard group which can't be achieved with the more general notion of surjective maps from some fixed free module V of rank n to an invertible module M (all up to isomorphism)

[Scott Carnahan]

Just adding my voice to say I don't see any benefit of specifying the invertible quotient module explicitly.

[Kenny Lau]

Calle Sönne said:

Okay good point. But let me ask: what do you expect to gain from this definition for rings with non-trivial picard group which can't be achieved with the more general notion of surjective maps from some fixed free module V of rank n to an invertible module M (all up to isomorphism)

I'm not sure what the domain of you "all up to isomoprhism" is. I'll assume that it's the correct one, i.e. isomorphism on M. I'm not sure if your definition is more general, because in mine I did not even assume M is invertible (or in fact any condition at all), M is an arbitrary module.

I'm also not sure what you gain by letting the indexing n -> M be replaced with free module of rank n. (Let's also repeat that you'd have to be more careful if n is infinite)

[Kenny Lau]

and I've basically made it more explicit. I've implicitly used the result that End(M,M) = R for any invertible module M, so I've skipped directly to Units R as the group acting on the subset.

[Kenny Lau]

I consider Units R to be more explicit and user-friendly than "up to isomorphism"

[Kenny Lau]

Scott Carnahan said:

Just adding my voice to say I don't see any benefit of specifying the invertible quotient module explicitly.

which point are you replying to?

[Scott Carnahan]

Sorry I was unclear. I don't know how things work in the noncommutative or semiring settings, but for commutative rings R, EGA II Prop 4.2.3 says that if you have an R-module N, the A-points of its projectivization are equivalence classes of A-linear surjections N ⊗ A → L where L is locally A-free of rank 1, and equivalence is by isomorphisms of invertible modules commuting with the surjections. When we want the usual P^n, we set N to be free of rank n+1.

The definition of ProjCoords given here doesn't directly correspond with this: we are varying both the source module (taking M^(n+1) instead of fixing R^(n+1)) and the target. Also, I haven't seen any situations in the literature where people use a stratification of points by choosing a particular invertible quotient (but this may just be my own ignorance since it is far from my main research focus).

[Kevin Buzzard]

Yes projective space is a special case of Grassmannians and the underlying functor for these can all definitely be done in the way Scott suggests without ever taking a disjoint union over isomorphism classes of modules. The latter feels unnatural to me and it will be much easier to prove that the former is representable.

[Kevin Buzzard]

It's all very elegantly explained in FGA (will try and remember to add link later) (edit: it's not FGA but @Ivan Farabella and me found https://www.numdam.org/item/SHC_1960-1961__13_1_A8_0/ very nice.

[Calle Sönne]

Yes I think that my point is the following: it's nice to have a simpler description for projective space e.g. by quotienting by units instead of some more general automorphisms, but I have only ever seen these descriptions being used for local ring-valued points (and I think rarely outside the case of fields, which we already have). In the generality you are working in, I feel that one should just work with the object one actually wants (which is the Grassmannian). Also, it's definitely very useful to be in the case of a general vector space (and not just k^n) as sometimes you are interested in parametrizing rank 1 quotients of a certain vector space which might not come with a canonical basis.

[Antoine Chambert-Loir]

@Scott Carnahan I know two or three places of proofs where one stratifies the projective space by the invertible ideal generated by a set projective coordinates. In all theses cases, the goal is to compute something associated to that projective space, number of points of bounded height, or description of the Kapranov zeta function, things like that, via a more concrete expression. This is how the class number appears in the computation for the residue of Dedekind's zeta function, at least in the classic, non-adelic, approach.

[Antoine Chambert-Loir]

There is a design question here. I can feel that people who use projective spaces of fields only wouldn't even want to thinks about invertible modules, and Mathlib could have ProjectiveSpace and Scheme.ProjectiveSpace, with an equality that would hold in particular cases only. Then it would be useful to have TwistedProjectiveSpace J where the projective coordinates generate a fixed ideal J, so that ProjectiveSpace R corresponds to TwistedProjectiveSpace R.

[Jeremy Ravenel]

It could make some sense to put more focus on complex numbers. Critically, nobody has done ℂP-∞ or complex grassmanians, and these classify vector bundles.

In higher math, this analytic situation can 'stick to its guns' because of how GLₙ(ℂ) is the hub of characteristic class theory, in the integral cohomology
of which the Chern classes reside.

The Thom class of the complex Grassmanian and its universal vector bundle, which classifies vector bundles of a fixed rank, is the universal characteristic class up to splitting.

So it could be good to try complex Grassmanians.

[Antoine Chambert-Loir]

It certainly wouldn't hurt to have ComplexProjectiveSpace and RealProjectiveSpace, whatever initial definition they could be based on.

[Kenny Lau]

Scott Carnahan said:

for commutative rings R, EGA II Prop 4.2.3 says that if you have an R-module N, the A-points of its projectivization are equivalence classes of A-linear surjections N ⊗ A → L where L is locally A-free of rank 1, and equivalence is by isomorphisms of invertible modules commuting with the surjections. When we want the usual P^n, we set N to be free of rank n+1.

The definition of ProjCoords given here doesn't directly correspond with this: we are varying both the source module (taking M^(n+1) instead of fixing R^(n+1)) and the target.

@Scott Carnahan I think there is some misunderstanding here. M^(n+1) does not show up anywhere, or maybe, these two are equivalent. In the case of P^n(R) (so A := R), you set N to be R^(n+1), and I fixed L here to be M, so your formula N ⊗ A → L becomes R^(n+1) ⊗ R → M, which is equivalent to the choice of n+1 elements of M, which I am arguing here to be a much more explicit and much more usable definition.

Kevin Buzzard said:

Yes projective space is a special case of Grassmannians and the underlying functor for these can all definitely be done in the way Scott suggests without ever taking a disjoint union over isomorphism classes of modules. The latter feels unnatural to me and it will be much easier to prove that the former is representable.

I understand that if you look at the statement "isomorphism classes of surjections" literally, it does not mention a disjoint union. But if you actually examine it, and if you want to make the object usable, isn't it the same as first taking isomorphism classes of the target, and then taking a disjoint union of surjections?

Calle Sönne said:

Yes I think that my point is the following: it's nice to have a simpler description for projective space e.g. by quotienting by units instead of some more general automorphisms, but I have only ever seen these descriptions being used for local ring-valued points (and I think rarely outside the case of fields, which we already have). In the generality you are working in, I feel that one should just work with the object one actually wants (which is the Grassmannian). Also, it's definitely very useful to be in the case of a general vector space (and not just k^n) as sometimes you are interested in parametrizing rank 1 quotients of a certain vector space which might not come with a canonical basis.

That description is also used for Z because Z has trivialclass group.

The Grassmannian is certainly nice, but I don't think it completely overshadows the usefulness of a separate P^n functor. In fact, if you read Grassmannians in Stacks Project, the last lemma they proved is that G(n, n+1) = P^n, which means that in terms of "formalisation" (in their case, not using a computer), it might be useful to do both generalities, i.e. P^n and G(k, n), separately?

After all, I don't think you would deny that P^n is by itself a very useful functor apart from being G(n, n+1)? (For example, P^2 itself is very useful as well, and elliptic curve is (locally) a closed subscheme of P^2). What I'm saying is, let's say I did do Grassmannians and it was in Mathlib4 right now. Then it would also be a goal to specialise that to P^n, right? So my point here is that the functor P^n is separately useful and should definitely be done, instead of saying "it's just a special case of G(k,n) so it doesn't need to be done". I hope I'm making sense here.

[Kenny Lau]

This situation is basically identical to the situation of Polynomial vs. MvPolynomial. The fact that MvPolynomial exists does not suddenly mean that Polynomial is useless (it's "just" MvPolynomial but indexed by PUnit), which I feel like is unfortunately an attitude that I'm getting from the discussion here...

[Kevin Buzzard]

I believe that P°n is important independent of Grassmannians. What I'm not at all clear about is your claim that introducing the disjoint union is a step in the right direction. I have been through the proof this year when supervising a lean MSc and I would say that in fact it's a step in the wrong direction because in the proof of representabity you never focus on the global isomorphism class of the module, you just use that it's locally free. So you are introducing what looks to be to be a spurious extra global stratification in your definition. In fact we never say "isomorphism classes of surjections" in the proof, we just say "submodules such that the quotient has these properties" so never get into isomorphism class hell at all. You're introducing the hell in a fundamental way with your proposal and it's not needed in the construction of the functor or the proof that it's representable.

[Kenny Lau]

Thanks for the clarification.

So, if I ask you what "is" P^n(Spec R) as a set, the correct answer would be the following?

1. P^n(Spec R) is the following subquotient:
2. The total space is Submodule (R^n). (There is some unfortunate indexing issues here, which I will ignore for now)
3. The sub-space is { S // _ ⧸ S is locally free of rank 1 }.
4. The quotient is by the equivalence relation Nonempty (_ ⧸S₁ ≃ₗ[R] _ ⧸S₂).

If you think this is the right direction, I'm very happy to do this. But I would still want to ask a question in my original direction: I think my more explicit construction, this time crucially I will not use M at all, is still useful for the case Cl(R)=1, specialised to the case of local rings, and also specialised to the case of fields. Would you agree that we should still build my original object but this time without mention of M? i.e. I propose ProjCoords R n this time, without the M.

I'm still a bit torn here, I've accepted your point that we should not mention M at all, but I know that Projectivization exists in the library and is useful in its own right (again, different degrees of generality is useful), even though it's only correct for fields. I would argue that a wrong definition that happens to be correct for local rings, is also useful: for local rings the condition would say that one of the coordinates is a unit. For example, this could be useful for a DVR.

[Kenny Lau]

@Kevin Buzzard (forgot to ping you in the original message)

[Calle Sönne]

I think ProjCoords R n seems reasonable!

[Calle Sönne]

Also i definitely agree that it is useful to have a specialized notation for P^n, I was only mentioning the Grassmannian since I thought your original definition would apply to give coordinates for that as well (since you could take M to be a vector bundle in particular), but now I realize that you specialize to only quotient by the units.

[Kenny Lau]

Calle Sönne said:

I think ProjCoords R n seems reasonable!

There's still a huge implementation question here, in all cases the quotient will be by Units R, this will never change. However, the definition of the subspace will change a lot:

• If R is a field, then the condition is just x ≠ 0. This is how Projectivization is defined in Mathlib4.
• If R is a local ring, then the condition is ∃ i, IsUnit (x i). This is useful for example in a DVR.
• If R is a general ring with Pic(R)=1, then we get the most general definition, which is the one I proposed, where the condition says that the elements generate the whole ring.

[Kenny Lau]

so maybe the correct thing to do is to build the function .mk, .mk', and .mk'' for the three cases...

[Kenny Lau]

We won't have defeqs, and I can't predict the ramification of this. I believed that defeqs are overrated, but David Ang has a strong reason to believe otherwise.

[Kevin Buzzard]

Kenny Lau said:

So, if I ask you what "is" P^n(Spec R) as a set, the correct answer would be the following?

1. P^n(Spec R) is the following subquotient:
2. The total space is Submodule (R^n). (There is some unfortunate indexing issues here, which I will ignore for now)
3. The sub-space is { S // _ ⧸ S is locally free of rank 1 }.
4. The quotient is by the equivalence relation Nonempty (_ ⧸S₁ ≃ₗ[R] _ ⧸S₂).

No, there is no quotient at all. This is why it's much simpler. It's just the subspace. In fact your suggestion is just Pic again; over a field the quotients are all isomorphic, for example.

[Kevin Buzzard]

cf P^1 over a field K is lines in K^2 = submodules of K^2 such that the quotient is 1-dimensional , no "up to isomorphism" needed.

[Kenny Lau]

it would indeed be quite neat if we don't need quotients! (i said "would" here because i don't see why yet)

[Kenny Lau]

aha, i see where i went wrong, i forgot that the isomorphism has to commute with the surjection as well. now I see why we don't need quotient. this is very nice and neat!

[Kenny Lau]

@Kevin Buzzard now I see why this is a nice object. It's very satisfying to not need to quotient. So what should the Mathlib4 name of this object be?

[Kenny Lau]

I suppose this construction can be immediately generalised to the grassmannians by replacing "1" with "n-k" (i really don't like this indexing)

[Kenny Lau]

can we do Grassmannian k n with docstring saying that this corresponds to n-k n lol

[Kevin Buzzard]

Aren't they isomorphic? ;-) (maybe not canonically though?)

[Kenny Lau]

@Kevin Buzzard there's no n-1 if n is infinite

[Kevin Buzzard]

GrassmannianFunctor? ProjectiveSpaceFunctor? The correct generality is probably a base scheme and a quasicoherent sheaf rather than an n.

[Kenny Lau]

yes, the correct functor is probably typed Scheme^op => Set rather than Ring => Set...

[Kenny Lau]

i don't know what the philosophy should be

[Kenny Lau]

the correct generality is probably some machinery that takes in a functor Ring => Set that satisfies certain axioms, and outputs a smooth scheme :melt:

[Calle Sönne]

We should probably have both anyway (referring to Scheme^op => Set vs Ring => Set)

[Kevin Buzzard]

Note that Calle has done some of the key gluing machinery here IIRC

[Kenny Lau]

What's the correct generalisation of the n that Kevin is referring to? As in, are we saying that given a quasi-coherent sheaf M on a scheme X, we can construct Grassmannian(M, k) as { N subsheaf M | M/N locally free rank k }?

[Kenny Lau]

so i currently count 7 objects now... lol

[Calle Sönne]

Yes although I don't know the conditions for when this is representable (you might have to force M to be a vector bundle?)

[Kenny Lau]

that's fine, it doesn't have to be representable to be a functor

[Kenny Lau]

actually, i skipped some steps, let me try again

[Calle Sönne]

Kenny Lau said:

so i currently count 7 objects now... lol

Yeah to me it seems we should have the Grassmannian on both the ring side and the scheme side (in this case maybe ProjectiveSpace could even be an abbrev). Then we should have something like you suggest ProjectiveCoords for explicit descriptions over fields/local rings/pic=1 rings.

[Kenny Lau]

S : Scheme, M : quasi-coherent sheaf on S and k : ℕ , then we define the functor Grassmannians {S} M k with type (Scheme/S)ᵒᵖ ⥤ Set that sends the scheme f : X ⟶ S to the set { N subsheaf f⁻¹M | f⁻¹M ⧸ N locally free of rank k }.

[Kenny Lau]

is this correct?

[Kenny Lau]

Calle Sönne said:

Kenny Lau said:

so i currently count 7 objects now... lol

Yeah to me it seems we should have the Grassmannian on both the ring side and the scheme side (in this case maybe ProjectiveSpace could even be an abbrev). Then we should have something like you suggest ProjectiveCoords for explicit descriptions over fields/local rings/pic=1 rings.

to be clear, when you said it's an abbrev, you're referring to ProjectiveSpaceFunctor : Schemeᵒᵖ ⥤ Set right? it's because I also made ProjectiveSpace : Scheme

[Kenny Lau]

i'm also thinking about whether we want:

• HomogeneousCoords
• HomogeneousCoordinatess
• HomogCoords
• HomoCoords
• ProjCoords
• ProjectiveCoords
• ProjectiveCoordinates

[Calle Sönne]

Kevin Buzzard said:

Note that Calle has done some of the key gluing machinery here IIRC

This is what Kevin is referring to (and Joël also wrote it). Although I think it needs to be refactored at some point since now you can't immediately apply it if you're working on Sch/S for a base scheme S.

[Kenny Lau]

well... if the whole functor over Spec Z is representable then surely i can just take the product with S right

[Kenny Lau]

@Calle Sönne @Kevin Buzzard so, in summary:

1. We want to build the functor GrassmannianFunctorScheme that has type (Scheme/S)ᵒᵖ ⥤ Set, given a quasi-coherent sheaf on S and k : ℕ. (perhaps a later goal)
2. We want to build the functor GrassmannianFunctorRing with type R ↓ CommRing ⥤ Set, given an R-module M and k : ℕ. Concretely, given f : R ⟶ A, the corresponding set is { N ≤ A ⊗[R] M | _ ⧸ N is locally free of rank k }.
3. Specialise 1 to projective (see 4).
4. Specialise (with abbrev) 2 to ProjectiveSpaceFunctorRing with M := (n → R) and k := 1.
5. Separately, build ProjCoords R n to be { f : n → R | range of f spans R } / Rˣ, which mathematically is isomorphic to ProjectiveSpaceFunctorRing R n when Pic(R) = 1.
6. Make a constructor for local rings, where the condition becomes ∃ i, IsUnit (f i).
7. Make a constructor for fields, where the condition becomes f ≠ 0. And refactor Projectivization to use this whenever possible?

And please suggest shorter names :melt:

[Kenny Lau]

what's the advantage of using an arbitrary module in 2 instead of n -> R?

[Calle Sönne]

Kenny Lau said:

what's the advantage of using an arbitrary module in 2 instead of n -> R?

Because what if you are interested in parametrizing rank k quotients of something with no canonical basis?

Here is a very convoluted example: infinitesimal subgroups of an abelian scheme corresponds to submodules of the Lie algebra of the abelian scheme (or something like this). I am personally interested in parametrizing these, so now I want to consider the projectivization of this lie algebra (but it would be much more convoluted if I was forced to choose a basis here!). Maybe someone else has a very clever simple example.

[Calle Sönne]

Maybe with some choice of namespaces your names could become shorter (so the first 3 should just be Grassmannian and ProjectiveSpace). And also there should be notation in these namespaces anyways.

[Calle Sönne]

And in 3 there should be a version where you are able to choose which M to use. Maybe some nice notation could make both of these possible at once (so that P^n picks R^n for you, but you can also write P(V)).

[Kenny Lau]

ℙ^(n; R) vs. ℙ(V; R)? I mean, whatever notation we choose, we'll also have to deal with namespace conflict, because the scheme ProjectiveSpace : Scheme should also use ℙ^(n; R)?

[Kenny Lau]

maybe ; vs. ,? this feels very evil

[Kevin Buzzard]

I think that the correct definition of "projective morphism" (ie the EGA one not the Hartshorne one) uses this generality (X->S is projective if it factors through P(M)->S where M is some general qc O_S-module or something?)

[Calle Sönne]

Kenny Lau said:

ℙ^(n; R) vs. ℙ(V; R)? I mean, whatever notation we choose, we'll also have to deal with namespace conflict, because the scheme ProjectiveSpace : Scheme should also use ℙ^(n; R)?

I have sadly not kept up to date with all the recent AG developments, so someone else has a better reply here. But I'm not sure if we have figured out how to deal with the whole scheme vs functor of points situation. There might be a world where one wants to define something like Scheme.HasFunctor which contains a given functor that is naturally isomorphic to the functor obtained by yoneda. Then the notation could be Scheme.functor to access it or something like this. Then maybe the functor will be ℙ(V; R).functor but at the same time the notation ℙ(V; R) might mean only the functor in some other namespace(s) where its clear we only ever want to talk about the functor.

[Kenny Lau]

This sounds nice, we can just have that notation today

[Kevin Buzzard]

My impression is that in the toric project they have some equivalence between affine group schemes and Hopf algebras so maybe they have some ideas? @Andrew Yang ?

[Yaël Dillies]

Yes, we definitely have some ideas here. It's a bit of a hectic for us three, but soon there will be some detailed explanation on what we've done

[Andrew Yang]

About the notation thing: My default answer would be just scope both and don't open them at the same time.

[Andrew Yang]

Scheme.HasFunctor is a fun idea, but I would be inclined to pass around Functor.RepresentableBy for now unless this proves to be tedious and repetitive.

[Kenny Lau]

There's a subtle point here about infinite modules. Let's just consider $R^{\oplus \mathbb{N}} = \bigoplus_{n \in \mathbb{N}} R$.

We currently have $\mathbb{A}^\mathbb{N}$ whose $R$-points are $\prod_{n \in \mathbb{N}} R$, which is perhaps $\mathrm{Hom}(R^{\oplus \mathbb{N}}, R)$?

Then the grassmannian discussed above, $\mathbb{P}^\mathbb{N}(R) = \mathbb{G}(R^{\oplus \mathbb{N}}, 1)$ is the "hyperplanes" of the module $R^{\oplus \mathbb{N}}$.

The subtle point here is that sometimes it comes up as a direct sum, and sometimes it comes up as a direct product. For example, the "lines" and the "hyperplanes" of the module $R^{\oplus \mathbb{N}}$ are not equivalent!

[Kenny Lau]

On the point of taking dual: let $M$ be an $R$-module, and let $A(M) = \oplus_{n \in \mathbb{N}} M^{\otimes n}$ be its... I tried to find the name but could not.

Then $\mathrm{Spec}(A(M))(\mathrm{Spec}(R)) = \mathrm{Mor}(\mathrm{Spec}(R), \mathrm{Spec}(A(M)) = \mathrm{Hom}(A(M), R) = \mathrm{Hom}(M,R)$ which indeed takes duals, a subtle point that is not clear when we only focused on free modules of finite rank.

[Kenny Lau]

@Andrew Yang should we generalise AffineSpace to take a module?

[Kenny Lau]

Update: A(M) above should be Sym(M), we need to take symmetric quotient to make it commutative

[Antoine Chambert-Loir]

Kenny Lau said:

This situation is basically identical to the situation of Polynomial vs. MvPolynomial. The fact that MvPolynomial exists does not suddenly mean that Polynomial is useless (it's "just" MvPolynomial but indexed by PUnit)

Actually, it's not that…

[Michał Mrugała]

Kenny Lau said:

Calle Sönne said:

What is the point of fixing M? If I've understood correctly, when Pic(R) is non-trivial, and M is in Pic(R) then ProjCoords R M n will be a subset of P^n(R). Why are we interested in this subset for say M non-isomorphic to R?

I suppose there is a bigger point here to be made. Let's say we want to talk about the scheme GL_n, and I give you an explicit definition right now (it's Spec ℤ[a11, ..., ann, 1/Det(aij)]). Are we done here? In my personal philosophy (I don't know if this aligns with Mathlib's philosophy), I would say that we are not done, and we would actually want to construct GL_n(R) separately first (functor CommRing ⥤ Grp), and then prove that the scheme GL_n represents the functor GL_n(R).

(There's actually an extra bonus point that comes with first defining the functor, because we get a cogroup structure for free on that big explicit ring.)

So in the same vein, I would also want to construct the functor explicitly first, and then prove that P^n represents the functor. In this case, the functor is just the disjoint union of ProjCoords R M n across M : Pic R.

Calle Sönne said:

(continuing my comment above). Wouldn't you want to treat all M (in Pic(R) for now) at the same time, so that you get ProjCoords R n consisting of tuples (M, n->M) where the second factor satisfied your condition from before.

Then we can't talk about other invertible modules that happen to not be (definitionally) equal to terms of Pic R. My personal philosophy here is that I would want to split things into more steps, with smaller objects in each step, and also in greater generality.

For the GL_n example I object to saying that you get the group structure for free. We currently have 2 APIs for getting group object instances on affine schemes: through a Hopf algebra structure or through Yoneda. If you do identify these two things as schemes you would also need to identify them as group schemes. This does not come for free.

[Kenny Lau]

@Michał Mrugała Does the Hopf algebra structure not come from Yoneda?

[Michał Mrugała]

You can recover a Hopf algebra structure from Yoneda, but you also want to be able to do computations with the Hopf algebra structrure. The instance you'll get with Yoneda won't have a nice form and you will need to show that it is the Hopf algebra structure you expect regardless.

[Kenny Lau]

Michał Mrugała said:

you also want to be able to do computations with the Hopf algebra structrure. The instance you'll get with Yoneda won't have a nice form

@Michał Mrugała I object to this claim. In fact, I have no idea how to compute any of the Hopf algebra structure (by hand), except via Yoneda.

[Michał Mrugała]

On paper I agree, but from my experience working with this in Lean I don't think what you get from just unfolding the definitions will be useable. Right now the way you get an instance through Yoneda is quite hacky. Me and @Andrew Yang are currently working on formalizing SO2, so we can try and see if I'm wrong about this.

[Michał Mrugała]

Also note that you can compute the Hopf algebra morphisms using the classical theory of linear algebraic groups without needing to go through Yoneda.

[Kenny Lau]

Michał Mrugała said:

On paper I agree, but from my experience working with this in Lean I don't think what you get from just unfolding the definitions will be useable.

unfold is not the only way to solve a problem, it's sometimes also the worst way

[Andrew Yang]

I don't think the concrete description of the comultiplication map is a bad thing to have, so we should have it anyways.

[Michał Mrugała]

Concretely: let's say you define GL_n(R) and show that it represents a group functor. This gives you a group scheme instance and recovers a Hopf algebra instance on its global sections. How do I write down the comultiplication or antipode of an element?

[Andrew Yang]

And then we should give the description of multiplication on the yoneda presheaf so that people can do the calculations in yoneda if they prefer.

[Kenny Lau]

Michał Mrugała said:

Concretely: let's say you define GL_n(R) and show that it represents a group functor. This gives you a group scheme instance and recovers a Hopf algebra instance on its global sections. How do I write down the comultiplication or antipode of an element?

You do the computation you would on paper, and hope that Yoneda has enough API to translate that paper computation directly into Lean

[Michał Mrugała]

I don't know what else to say than: until you can give me a proof of concept I remain very skeptical this works out. I don't believe the current API supports this and I don't know how you'd design one that does this. Maybe @Andrew Yang can see how this would work?

[Andrew Yang]

I think you basically write some thing analogous to docs#Grp_Class.ofRepresentableBy and things will work out fine.

[Kenny Lau]

Also could I say that this does not feel very relevant to Projective Space, mainly because the Grassmannian basically has no structure (it's just a set)

[Michał Mrugała]

Do I understand correctly that you'd want to have a representability statement when you turn it into a functor on algebras? I guess this would work, although you still need a compatibility API between schemes and algebras.

[Kenny Lau]

#26060: define Grassmannians G(M; R, k) of module over ring

[Kenny Lau]

#26061: define ProjectiveSpace ℙ(n; S) as a scheme over a given scheme S with an arbitrary indexing type n

[Kenny Lau]

so i'm now returning to projective space and i have forgotten all of the previous conversation 4 months ago

[Kenny Lau]

@Andrew Yang what would we want in projective space? should we copy the approach in affine space? or should we ignore that file?

[Kenny Lau]

do we want S x Proj Z[n]? do we want Proj R[n]? (R[n] means MvPolynomial n R)

[Kenny Lau]

do we want Proj R[Fin n]?

[Kenny Lau]

do we want to describe the functor? do we want the open cover by n charts?

[Kenny Lau]

Kenny Lau said:

so i'm now returning to projective space and i have forgotten all of the previous conversation 4 months ago

so I read through the conversation and they didn't seem very relevant so let's just start again

[Kenny Lau]

note that in #26061 I used S x Proj Z[n] just because AffineSpace did it that way, and @Andrew Yang commented that he would want the isomorphism to Proj R[n] when S = Spec R, so now I'm thinking that we would want Proj R[n] anyway so why not do that first

[Kenny Lau]

I think in private communications @Andrew Yang also noted that n and S should be in the same universe, so that's another point on which I should not blindly copy AffineSpace

[Andrew Yang]

I don't think we want much API on Proj R[n], and only the ones necessary to establish the isomorphism (which I assume is none if it the iso is done in the generality of base changes of graded rings)

[Kenny Lau]

@Andrew Yang how do you get the charts?

[Andrew Yang]

docs#AlgebraicGeometry.Proj.affineOpenCover

[Kenny Lau]

@Andrew Yang yes, but you still need the fact that R[n]_(X i)_0 is isomorphic to R[n without i]

[Andrew Yang]

I don't get what you are trying to say. The fact you are describing is useful and we need it, but I don't see how it is related to the discussion about not needing API for Proj R[n].

[Kenny Lau]

@Andrew Yang firstly i'm asking about whether we want S x Proj Z[n] in the first place (which is the approach in #26061), or if we just want to focus on Proj R[n].

Secondly, in any case, we would want an open cover of P^n by A^n (replace one n by n+1 or n-1), which means that after using your linked result, we would still need to make the isomorphism bewteen the homogeneous localization and the concrete mvpolynomial ring

[Kenny Lau]

your linked result is a cover by "homogeneous localizations", but I think we want a cover by "spec of mvpolynomial"

[Andrew Yang]

1. We want ProjectiveSpace n R := S x Proj Z[n] and not Proj R[n].
2. We want an open cover of ProjectiveSpace n R by AffineSpace _ R (Still no Proj R[n]).

[Kenny Lau]

@Andrew Yang ok, but 2 still requires my isomorphism for Z

[Kenny Lau]

for 1, might I ask why? to be clear, the alternative definition I'm proposing is:

def ProjectiveSpaceAffine (R : CommRing) (n : Type) := Proj R[n]

[Kenny Lau]

i.e. i propose that we don't talk about P^n/S

[Kenny Lau]

https://github.com/kckennylau/EllipticCurve/blob/007f6b58a9b563ca74eb5441a66d87b610261a07/EllipticCurve/ProjectiveSpace/TensorProduct/GradedAlgebra.lean#L363

[Kenny Lau]

@Andrew Yang I now have a graded algebra structure on the base change

[Kenny Lau]

summary:

1. we want to show that P^n(Spec R) = Proj R[n], which requires
2. in general a theorem Spec S x[Spec R] Proj A = Proj (S ⊗[R] A), which requires
3. firstly a graded algebra structure on Proj (S ⊗[R] A), which is the result linked above

[Kenny Lau]

so now i'm in step 2, and the only reference i could find is https://math.arizona.edu/~cais/CourseNotes/AlgGeom04/notes216.pdf , which already implicitly uses a "by cover" construction

[Kenny Lau]

image.png

(the highlighted part is the "by cover")

[Kenny Lau]

oh and also this uses S0 instead of R

[Kenny Lau]

actually now that I think about it, I don't know why in mathlib Proj takes a GradedAlgebra instead of a GradedRing...

[Kenny Lau]

the base ring plays no part

[Kenny Lau]

so i'm still doing this and i strongly suspect that this will produce at least 5 PR's

[Kenny Lau]

for example we don't even know that the docs#HomogeneousLocalization.Away.mk of 0 is 0

[Kenny Lau]

@loogle HomogeneousLocalization.Away.mk

[loogle]

:search: HomogeneousLocalization.Away.mk, HomogeneousLocalization.Away.mk_surjective, and 5 more

[Kenny Lau]

since there are only 7 declarations i would also suggest to make this instead an add hom from A i?

[Kenny Lau]

so now i have an isomorphism of each component but not yet the proof that they agree on intersection

[Kenny Lau]

(each component of Spec R x Proj A vs. Proj (R tensor A))

[Andrew Yang]

I think the right theorem is that the canonical map Spec R x Proj A -> Proj (R tensor A) is an isomorphism?

[Kenny Lau]

aha that might be better, thanks

[Kenny Lau]

and we don't have functoriality of Proj...

[Kenny Lau]

(i don't think we even have "morphism of graded algebra", i've been inputting the definition manually)

[Kenny Lau]

I now have 5 erws in my project :melt:

[Antoine Chambert-Loir]

@María Inés de Frutos Fernández and I have written a fair number of lines about graded algebras for our divided powers project. Especially, base change and quotients by homogeneous ideals. In case this helps…
https://github.com/AntoineChambert-Loir/DividedPowers4

[Kenny Lau]

@Antoine Chambert-Loir aha, thanks for the pointer, but i'm afraid i've already done (and duplicated) base change for graded algebra

[Kenny Lau]

here: https://github.com/kckennylau/EllipticCurve/blob/master/EllipticCurve/ProjectiveSpace/TensorProduct/GradedAlgebra.lean#L366

[Kenny Lau]

corresponding to your file here: https://github.com/AntoineChambert-Loir/DividedPowers4/blob/8ac87135ef7b23afe47748073c19e8e16b2a44ec/DividedPowers/ForMathlib/GradedBaseChange.lean#L172

[Kenny Lau]

Proj is now functorial (in my project): https://github.com/kckennylau/EllipticCurve/blob/74075515ae23812b74a38e6bcae8b351842aebaf/EllipticCurve/ProjectiveSpace/TensorProduct/ProjMap.lean#L262

[Kenny Lau]

@Andrew Yang using your suggestion I've tried to come up with the details on paper:

1. I assume you meant the opposite direction, i.e. we get a map e : Proj(R ⊗ 𝒜) ⟶ Spec(R) × Proj(𝒜) using UMP of pullback and the functoriality result I just proved.
2. the away map Spec((𝒜_f)₀) ⟶ Proj(𝒜) is an open immersion (in mathlib), so pullback gives us an open immersion V := Spec(R) × Spec((𝒜_f)₀) ⟶ Spec(R) × Proj(𝒜) (I hope).
3. Similarly we have open immersion U := Spec(((R ⊗ 𝒜)_(1 ⊗ₜ f))₀) ⟶ Proj(R ⊗ 𝒜).
4. I hope we can prove that on the level of points, e maps U to V.
5. By the UMP of open immersion, we can restrict e to e|UV : U ⟶ V.
6. I hope we can prove that e|UV is exacly (the forward direction of) the isomorphism I talked about before your message (the isomorphism of components).
7. Therefore e is locally invertible (f is a cover), therefore e is iso.

[Kenny Lau]

Is this what you have in mind?

[Andrew Yang]

Instead of 4, you show that e commutes with the (R ox A)_(1 ox f) = R ox A_(f) iso you had earlier and then you should be done.

[Kenny Lau]

That makes sense, but I suspect it might still involve the same work, because in the (to be proved commutative) square you're referring to, I need to compare two maps from Spec S to scheme X, and I don't know how to do that

[Kenny Lau]

quiver

image.png

[Andrew Yang]

I’m not sure what X is, but what it boils down to is that the map between Projs commutes with the affine open cover, which should be true by construction.

[Kenny Lau]

aha yes i forgot it's a map to a pullback so it has UMP

[Kenny Lau]

thanks!

[Kenny Lau]

it's amazing how much you can prove with no input (i.e. just category theory)

[Kenny Lau]

the square that commutes "by construction" is now proven in my project: https://github.com/kckennylau/EllipticCurve/blob/4437ba885487cb04532d918900772075f5c0ce7a/EllipticCurve/ProjectiveSpace/TensorProduct/ProjMap.lean#L451

[Kenny Lau]

/--
The following square commutes:
```
Proj 𝒜₂         ⟶ Proj 𝒜₁
    ^                   ^
    |                   |
Spec A₂[f(s)⁻¹]₀ ⟶ Spec A₁[s⁻¹]₀
```
-/
theorem awayι_comp_map {i : ℕ} (hi : 0 < i) (s : A₁) (hs : s ∈ 𝒜₁ i) :
    awayι 𝒜₂ (f s) (f.2 hs) hi ≫ map f hf =
    Spec.map (CommRingCat.ofHom (Away.mapₐ f f.2 (by rfl)).toRingHom) ≫ awayι 𝒜₁ s hs hi

[Kenny Lau]

also the total line count for the code relating to this part is definitely more than 1000

[Kenny Lau]

I would not be surprised if I produced 10 PR's this week

[Kenny Lau]

Andrew Yang said:

Instead of 4, you show that e commutes with the (R ox A)_(1 ox f) = R ox A_(f) iso you had earlier and then you should be done.

I now have this result locally! :tada: so I "should be done" with one more step

[Kenny Lau]

I suspect we won't have a lemma that "is an isomorphism" can be checked locally

[Kenny Lau]

but i can prove that easily

[Christian Merten]

Kenny Lau said:

I suspect we won't have a lemma that "is an isomorphism" can be checked locally

docs#AlgebraicGeometry.instIsLocalAtTargetIsomorphismsScheme

[Kenny Lau]

nice

[Kenny Lau]

@Christian Merten the version I'm stating in my file is this:

/-- To check if `f : X ⟶ Y` is an isomorphism, one can supply an open cover of `X` and an open
cover of `Y` (indexed by the same set `S`), and then maps `f_i : U_i ⟶ V_i` for `i : S` that are
iso such that the squares commute. -/
theorem isIso_of_cover {X Y : Scheme.{v}} (f : X ⟶ Y)
    (U : X.OpenCover) (V : Y.OpenCover)
    {ι : Type*} (iU : ι → U.I₀) (hu : iU.Surjective) (iV : ι → V.I₀) (hv : iV.Surjective)
    (φ : ∀ i, U.X (iU i) ⟶ V.X (iV i)) [∀ i, IsIso (φ i)]
    (hfφ : ∀ i, U.f (iU i) ≫ f = φ i ≫ V.f (iV i)) :
    IsIso f :=

[Kenny Lau]

I wonder if you have the intermediate steps

[Kenny Lau]

(I suspect in actual applications we will have U.I0 = V.I0 so we can perhaps strengthen the assumption to an equiv

[Kenny Lau]

oh wow this generalisation is not true... lol

[Kenny Lau]

I need to control each preimage

[Kenny Lau]

counter-example: take X = disjoint union of two copies of Y, call them X1 and X2, then the cover is {X1, X2} on X and {Y, Y} on Y

[Kenny Lau]

Proj of tensor product!

[Kenny Lau]

I have finally completed the "fundamental theorem" of projective space, i.e. the characterisation when S is affine

/-- `ℙ(n; Spec(R))` is isomorphic to `Proj R[n]`. -/
def SpecIso (R : Type u) [CommRing R] : ℙ(n; Spec(R)) ≅ Proj (homogeneousSubmodule n R)

[Kenny Lau]

I propose we define a class of rings with a canonical graded structure, and then a function Graded.of to retrieve the structure, and then define the notation Proj(R) to mean Proj (Graded.of R)

[Kenny Lau]

import Mathlib

namespace AlgebraicGeometry

class CanonicalGradedStructure (A : Type*) [CommRing A]
    (R : outParam Type*) [CommRing R] [Algebra R A] where
  grading (A) : ℕ → Submodule R A -- to be replaced with `AddSubmonoidClass`
  gradedAlgebra : GradedAlgebra grading := by infer_instance

attribute [instance] CanonicalGradedStructure.gradedAlgebra

scoped notation "Proj(" R ")" => Proj (CanonicalGradedStructure.grading R)

noncomputable instance (R σ : Type*) [CommRing R] :
    CanonicalGradedStructure (MvPolynomial σ R) R where
  grading := MvPolynomial.homogeneousSubmodule σ R
  gradedAlgebra := MvPolynomial.gradedAlgebra

variable (R σ : Type*) [CommRing R]
#check Proj(MvPolynomial σ R)

end AlgebraicGeometry

[Andrew Yang]

The fact that Proj (R) and Proj(R) have different meaning is very confusing (so is Spec(R) and Spec (R) so we are getting rid of the former).

[Kenny Lau]

oh no, i liked Spec(R)

[Christian Merten]

I don't like Spec(R) at all. The only use case I see for this is for propaganda purposes, but in this case one can easily locally create the notation.

[Kenny Lau]

like, they might be confusing, but i don't think anyone can read Proj (fun n ↦ (𝒜 n).baseChange S))

[Kenny Lau]

Christian Merten said:

locally create the notation

isn't that the point of a scoped notation; also this one I proposed for Proj is not as easy, since it requires a class of canonically graded rings

[Christian Merten]

Kenny Lau said:

like, they might be confusing, but i don't think anyone can read Proj (fun n ↦ (𝒜 n).baseChange S))

But this would already be fixed by your first suggestion of introducing CanonicalGradedStructure, which I think is worth considering.

[Kenny Lau]

Christian Merten said:

propaganda purposes

well I do want to make lean notation as close to maths as possible... if you count that as "propaganda purposes" then I guess we just have different aims

[Andrew Yang]

I thought the point was that MvPolynomial _ R has no canonical graded structure because you often want different variables to have different weights.

[Kenny Lau]

actually i didn't quite understand that point; the input in GradedAlgebra already tells you which family of submodules you're considering, so i don't really see why we shouldn't make it an instance

[Kenny Lau]

taking a step back, even if I accept that, we can just copy the same thing, and make MvPolynomial.instCanonicallyGradedHomogeneousSubmodule a definition and a local instance when we need it

[Christian Merten]

Kenny Lau said:

Christian Merten said:

propaganda purposes

well I do want to make lean notation as close to maths as possible... if you count that as "propaganda purposes" then I guess we just have different aims

By propaganda purposes I mean Lean demos for non-Lean people, where I don't want to spend time on explaining the .of R in Spec (.of R).

We should of course try to make mathlib close to paper notation, but we also need to make sure it is not confusing for the people that actually work in it.

[Kenny Lau]

I think people working in it know that ident( is special notation...

[Andrew Yang]

Kenny Lau said:

actually i didn't quite understand that point; the input in GradedAlgebra already tells you which family of submodules you're considering, so i don't really see why we shouldn't make it an instance

I'm saying that homogeneousSubmodule shouldn't be automatic. docs#MvPolynomial.gradedAlgebra could be. I don't know why it's not.

[Kenny Lau]

yes, so we'll make that a local instance

[Kenny Lau]

Christian Merten said:

locally create the notation

taking a step back, would it be acceptable to scope the notation in its own scope? so Spec(R) should live in the scope AlgebraicGeometry.Spec.Notation and Proj(R) should live in the scope AlgebraicGeometry.Proj.Notation; I think this is as good as making it a local notation each time we want it, and this also makes it more maintainable (since the notation is only defined once)

[Kenny Lau]

for accessibility we should also mention the scopes in the docstrings of Spec and Proj

[Andrew Yang]

I am keeping the Spec() notation for now but removing its usage in mathlib.

[Christian Merten]

We should ban it from being used in mathlib though.

[Kenny Lau]

I respectfully disagree.

[Yaël Dillies]

Andrew Yang said:

The fact that Proj (R) and Proj(R) have different meaning is very confusing (so is Spec(R) and Spec (R) so we are getting rid of the former).

Wait, what? I thought we had won that battle!

[Yaël Dillies]

Christian Merten said:

We should of course try to make mathlib close to paper notation, but we also need to make sure it is not confusing for the people that actually work in it.

I claimed in the past and claim again now that goals full of things of the form Spec (CommRingCat.of R) are in fact confusing for the people that work on them

[Kenny Lau]

@Yaël Dillies this conversation has been moved to #mathlib4 > Remove `Spec()` notation

[Kenny Lau]

here's the (future) PR graph i drew:
image.png

[Kenny Lau]

update:
image.png