Proj construction

Stream: maths

[Jujian Zhang]

I am working on Proj construction at https://github.com/leanprover-community/mathlib/pull/9964. When try to prove

def stalk_iso (x : projective_spectrum.Top 𝒜) :
  (structure_sheaf 𝒜).1.stalk x ≃+* CommRing.of (hartshorne_localisation 𝒜 x)  :=

-- 𝒜 is grading

by following hartshorne, the definition I ended up with is full of classical.some so not very useful. Does any body know a cleaner way to do this?

Because hartshorne_localisation 𝒜 x is a subring of a localisation ring, so I couldn't directly use localization.lift.

I also wasn't able to follow the method in prime_spectrum because there is a lot of degree of homogeneous elements involved.

[Johan Commelin]

I don't have Hartshorne hear next to me. Did you also look at the Stacks Project? Do they do the same thing?

[Jujian Zhang]

Stack project defined structure sheaf on basic open sets and lift it up.

[Kevin Buzzard]

Can you say something about the mathematics behind the question you're asking? I just looked at the diff for the branch and it's really long and terrifying

[Kevin Buzzard]

Hartshorne's definition of the structure sheaf is completely different to stacks.

[Jujian Zhang]

So the problem is the following:

From my understanding In Hartshorne $O(U)$ is defined to be $s: U \to \coprod S_{(\mathfrak p)}$ where $S_{(\mathfrak p)}$ is subring of $S_{\mathfrak p}$ such that numerator and denominator are homogeneous with same degree.

[Jujian Zhang]

So I defined $S_{(\mathfrak p)}$ to be a long existentially quantified thing

{y : (localization.at_prime x.as_homogeneous_ideal.1) |
    ∃ (a b : A) (i : ι) (a_hom : a ∈ 𝒜 i) (b_hom : b ∈ 𝒜 i) (b_nin : b ∉ x.as_homogeneous_ideal),
    y = (localization.mk a ⟨b, b_nin⟩ : (localization.at_prime x.as_homogeneous_ideal.1))}

[Kevin Buzzard]

So S is some nat-graded ring and you're localising at a homogeneous prime ideal I guess.

[Kevin Buzzard]

My guess is that the localisation is Z-graded and S_(p) is just the degree 0 piece. Possibly.

[Jujian Zhang]

Then when I define functions from this ring, because I need to use choose ... using .... Then to prove things about the definition, there is always classical.some

[Kevin Buzzard]

If your functions don't actually depend on the choice of a and b then you could avoid classical.some . But if you don't want to avoid it then the trick I usually use is to define the basic functions you need, i.e. numerator and denominator using classical.some (giving you a and b from y), and then immediately make an API for these things (i.e. prove a \in A i and b \in A i and y = mk a b) using classical.some_spec and then never use classical.some any more but only use these wrappers for which you have all the API you need right there.

[Jujian Zhang]

I was trying to be as general as possible: so A is an R-algebra graded by 𝒜 : \iota \to submodule R A

[Jujian Zhang]

Kevin Buzzard said:

If your functions don't actually depend on the choice of a and b then you could avoid classical.some . But if you don't want to avoid it then the trick I usually use is to define the basic functions you need, i.e. numerator and denominator using classical.some (giving you a and b from y), and then immediately make an API for these things (i.e. prove a \in A i and b \in A i and y = mk a b) using classical.some_spec and then never use classical.some any more but only use these wrappers for which you have all the API you need right there.

Let me try this.

[Kevin Buzzard]

The idea is that a = numerator y and b = denominator y and you immediately prove all the things you need relating a and b to y using classical.some_spec and then just stick to numerator and denominator from then on.

[Adam Topaz]

I think we need to think carefully about the proj construction, and my first inclination is that this approach is not necessarily the right way to go herre...

[Adam Topaz]

I would guess that we would be in better shape if we glued affine schemes..

[Kevin Buzzard]

You mean to define projective n-space or to define Proj of a graded ring?

[Adam Topaz]

proj of a graded ring.

[Kevin Buzzard]

So you mean look at the proof in Hartshorne that projective schemes are schemes, and then implement this as the definition

[Adam Topaz]

yeah essentially.

[Adam Topaz]

Do we have a gluing construction for sheaves @Andrew Yang ? I mean, if we have a topological space $X$, and an open cover $U_i$ with sheaves $\mathcal{F}_i$ on $U_i$ which are compatible on the intersections, can we glue to get a sheaf on $X$?

[Adam Topaz]

I.e. stacks#00AL

[Kevin Buzzard]

You want it for sheaves of types?

[Adam Topaz]

Well, in this case for sheaves of rings, but the same argument works.

[Kevin Buzzard]

Does it work for sheaves of topological spaces?

[Adam Topaz]

no ;)

[Kevin Buzzard]

I thought so ;-)

[Adam Topaz]

I'm looking at how stacks describes the proj construction now, and I think that would be a much better way to go:
https://stacks.math.columbia.edu/tag/00JM

[Jujian Zhang]

The underlying topological space of Proj is already defined.

https://stacks.math.columbia.edu/tag/01M3 defines structure sheaf on a basis of this topology. I think following stack project, the hard work would be proving sheaf condition. Following Hartshorne, the work would be proving that isomorphic to affine scheme on basic open set

[Adam Topaz]

The point is that the hard work should be done in the gluing construction for sheaves. You would then use assertion (6) from https://stacks.math.columbia.edu/tag/00JP to transfer the structure sheaf of the affine scheme along a homeomorphism, and the gluing construction should give you the structure sheaf on proj.

[Adam Topaz]

As for the issue about degrees of numerators and denominators, we should probably develop some API for the degree zero subring of a graded ring, and the grading on a localization by a homogeneous element.

[Andrew Yang]

The current way of gluing sheaves might be gluing sheafed spaces altogether, then transfer the sheaf onto the original space via some homeomorphism.

[Adam Topaz]

Hmmm... we should do something for descent data.

[Jujian Zhang]

@Andrew Yang Can you point me out to the gluing sheaf api please, I couldn't find the localtion of the api in mathlib, I would like to try to do proj construction by gluing affine scheme on basic open sets.

[Andrew Yang]

It is stuck in branch#open_subfunctor.
Hopefully this is going to make it into mathib in this month or the next.
The main stuff is in src/algebraic_geometry/presheafed_space/gluing.lean.
It's not yet well-documented, but examples can be found in src/algebraic_geometry/open_subfunctor.lean.
If you plan on using it, I'll try to make it compile later today or tomorrow.
I think the definitions are relatively stable now, and the proof of the lemmas might be tidied up in the future but that should not matter as much.

[Jujian Zhang]

Thank you! Let me try to understand the construction!

[Andrew Yang]

The stuff in the branch should be good to use except some errors in src/topology/gluing.lean. But that should be fixed once #9864 is merged today or tomorrow.
In the mean time, it should be fine to browse the branch using the current mathlib cache (c391512ee).

[Jujian Zhang]

I downloaded c391512ee cache, but didn't get any error in topology/gluing.lean. I guess this is good news.

Turns out it is vs code being frozen.

[Jujian Zhang]

I couldn't get this working, it seems there is category_theory/concrete_category/elementwise. I am getting this error.
file 'category_theory/concrete_category/elementwise' not found in the search path

[Will Sawin]

Really cool to see progress on this IMO!

[Andrew Yang]

I think it's fine to ignore that error. Lean should still work in src/algebraic_geometry/presheafed_space/gluing.lean.
If you really want to solve this error, you can merge the branch glue_spaces, but that branch touched some very basic files, so the cache might be un-usable.

[Andrew Yang]

The branch should now compile without errors again.

[Jujian Zhang]

The Proj construction is now sorry free

[Jujian Zhang]

EF1A7EB2-EDD2-4640-970E-1340A19206C3.png

[Johan Commelin]

@Jujian Zhang Congratulations! That's a milestone.

[Johan Commelin]

Out of curiousity: Can you give an estimate of the size of the diff between mathlib-master and your development?

[Jujian Zhang]

I merged a branch from Andrew Yang (but ended up not using it), the scheme.lean file is 5k lines and zariski topology and structure sheaf combined is about 1k. So everything together is about 6k lines.

[Jujian Zhang]

There are currently some heavy refls going on, so GitHub cannot compile it. I am working on fixing on heavy refls and try to get GitHub compile this branch.

[Johan Commelin]

Ok, thanks!

[Johan Commelin]

That's quite a size. Impressive work!

[Jujian Zhang]

Thank you for the kind word!

[Johan Commelin]

Would you mind pasting the full signature of Proj.to_Scheme? Because there's a bunch of variables in your screenshot, I guess that have been introduced by variables lines that aren't in the picture.

[Jujian Zhang]

A62B364B-362F-4F71-A734-A3F98DFB1E6C.png

[Jujian Zhang]

Sorry about this, but I am current out having lunch. So I have to take a screenshot of variables line

[Johan Commelin]

No worries, thanks a lot!