status of schemes

Stream: general

[Kevin Buzzard]

And this uses category theory

[Kevin Buzzard]

And I'm pretty sure that they're not at the point where we can start doing this

[Scott Morrison]

Surely there is lots of work on schemes that can come to mathlib now, before anyone runs into needing sheaves of modules over a sheaf of rings...

[Kevin Buzzard]

We can't even define a scheme I don't think Scott

[Scott Morrison]

You're saying that checking the sheaf condition on a basis is the blocker?

[Damiano Testa]

ok, so i can

code [anything i want]

and if i import a file it will be from the version of mathlib that i have in my lean directory?

[Kevin Buzzard]

Damiano read how to install projects on the community website

[Scott Morrison]

That's good to know, I'll try to make that happen. I didn't realise anyone was yet waiting on that.

[Kevin Buzzard]

Scott here's the issue

[Kevin Buzzard]

A scheme is a ringed space locally isomorphic to Spec R

[Kevin Buzzard]

The isomorphism takes place in the category of spaces equipped with a presheaf of rings

[Kevin Buzzard]

But putting the presheaf of rings on Spec R is not as easy as it sounds because of non affine opens

[Kevin Buzzard]

In Lean-scheme we put the presheaf on a basis

[Kevin Buzzard]

Then proved it was a sheaf (although sheafifying would also work)

[Kevin Buzzard]

And then proved that sheaves on X were the same as sheaves on a basis

[Kevin Buzzard]

By hand

[Kevin Buzzard]

In our particular case

[Kevin Buzzard]

My understanding is that @Bhavik Mehta has a bunch of this stuff in the topos repo but he also has a thesis to write

[Scott Morrison]

I wish I knew whether we should be doing this with sites. Or just presheaves on opens X.

[Kevin Buzzard]

The construction I sketched needs the concept of sheaf on something more general than opens X

[Kevin Buzzard]

One could make the construction in a completely different way of course

[Kevin Buzzard]

I think Hartshorne does it totally differently

[Scott Morrison]

Are you just saying you want to check the sheaf condition only for covers consisting of opens in the basis?

[Scott Morrison]

That's easy to do in the current setup.

[Kevin Buzzard]

@Damiano Testa IIRC Hartshorne defines the sheaf of rings on Spec R directly by looking at functions on U taking values in some crazy disjoint union of rings

[Kevin Buzzard]

This might be a way to proceed

[Patrick Massot]

I think Harshorne basically defined the stalks first, and then recover the sheaf using "continuous" sections of the stalks;

[Kevin Buzzard]

Scott I'm just saying that the way we did it pre category followed the stacks project approach which needed the concept of a presheaf and sheaf on a basis

[Kevin Buzzard]

And my understanding is that these are not yet in mathlib

[Damiano Testa]

Kevin Buzzard said:

This might be a way to proceed

I think that he mentions espaces étalés somewhere, but it might be only in an exercise

[Kevin Buzzard]

We should move this thread to #maths and call it current status of schemes

[Scott Morrison]

https://stacks.math.columbia.edu/tag/009H

[Kevin Buzzard]

Damiano I'm talking about the definition Hartshorne gives of the sheaf of rings on Spec R

[Notification Bot]

This topic was moved here from #new members > invalid import by Scott Morrison

[Kevin Buzzard]

Yes Scott we formalised stuff like that.

[Kevin Buzzard]

In a hands on way

[Kevin Buzzard]

With sheaves modelled as dependent functions taking values in Type

[Damiano Testa]

Kevin Buzzard said:

Damiano I'm talking about the definition Hartshorne gives of the sheaf of rings on Spec R

Yes, he uses "continuous sections" by mapping to the disjoint union over all primes of the localizations

[Kevin Buzzard]

One way to proceed here would be to deviate from the stacks project and use Hartshorne's definition, which is essentially applying the sheafification functor by hand

[Damiano Testa]

I suspect that, in the long run, using sites might be a more robust approach

[Kevin Buzzard]

Right Damiano. One could work in current mathlib and define this presheaf of rings

[Kevin Buzzard]

If one went this way then there would be no need for sites

[Damiano Testa]

after all, all this discussion is heavily founded on the notion of open sets and covers, which sites already contain in their definitions

[Kevin Buzzard]

Sure, but you see in this game you always have to decide where to stop

[Damiano Testa]

ok, I see!

[Kevin Buzzard]

I could just as easily argue that schemes should not be formalised because they're a special case of stacks

[Kevin Buzzard]

Or that we should just concentrate on making the topos

[Damiano Testa]

which indeed is where i was going! ahahaha

[Kevin Buzzard]

:-)

[Kevin Buzzard]

I think that there's no obstruction to just making the sheaf directly a la Hartshorne

[Damiano Testa]

Kevin Buzzard said:

Damiano read how to install projects on the community website

(In the meantime, I have managed to create my own version of the current version of mathlib! thanks!)

[Kevin Buzzard]

leanproject get mathlib

[Kevin Buzzard]

In there there's an algebraic geometry directory

[Kevin Buzzard]

You could make a new file called spec

[Damiano Testa]

Kevin Buzzard said:

I think that there's no obstruction to just making the sheaf directly a la Hartshorne

I just wanted to point out that, defining schemes à la Hartshorne also seems a great goal!

[Kevin Buzzard]

.lean

[Kevin Buzzard]

And then try to define the sheaf of rings on Spec R, following Hartshorne

[Damiano Testa]

Kevin Buzzard said:

You could make a new file called spec

(ok, i did something similar and, hopefully, equivalent: i typed

leanproject new Chevalley

and now i am working in there)

[Kevin Buzzard]

Now you have a new project

[Kevin Buzzard]

The issue is not making schemes

[Kevin Buzzard]

The issue is getting schemes into mathlib

[Kevin Buzzard]

So really the work defining the presheaf of rings should be done in a clone of mathlib, not in a new repo

[Kevin Buzzard]

Once we have the presheaf of rings on Spec R it will be easy to make schemes

[Kevin Buzzard]

I have a little time, maybe I can just start this now

[Kevin Buzzard]

After all, I'm only working on three other projects

[Damiano Testa]

@Kevin Buzzard I think that if I could shadow your progress, then I would be asking many fewer silly questions here on the chat: is there a way for me to "peek" what it is that you are doing?

[Johan Commelin]

@Damiano Testa you could do a screen share with someone

[Johan Commelin]

Kenny regularly streams what he is doing

[Kenny Lau]

someone is streaming at this very moment!

[Damiano Testa]

ah, where are the streams?

[Kenny Lau]

the same channel where we talked last time

[Kenny Lau]

in discord, to be clear

[Damiano Testa]

Ah, ok! i was looking here...

[Kenny Lau]

it seems they have stopped streaming now

[Scott Morrison]

hmm... thinking about it, I fear we want prop_limits to land before we define sites...

[Kevin Buzzard]

I'll stream in discord

[Kenny Lau]

limits of propositions?

[Patrick Massot]

limits as propositions.

[Scott Morrison]

(The has_limit typeclass should be in Prop, rather than carrying non-subsingleton data.)

[Kevin Buzzard]

@Damiano Testa and whoever else is interested (because I know that at least one other person was talking about schemes -- I forget who :-( ) -- if people want to do scheme stuff right now then probably the way to proceed is to define the sheaf on Spec(R) following Hartshorne (i.e. building it explicitly as functions from U to disjoint union of R_P for P in U) rather than following the stacks project. I have started a branch of mathlib called spec-of-a-ring which starts on this. I have filled in a lot of the data, but I have sorried all the theorems.

[Kevin Buzzard]

You can see the file online here . To get it on your computer, just go into your local copy of mathlib in a terminal and type

git pull
git checkout spec-of-a-ring

and you should be able to now find the file in the algebraic_geometry directory. Feel free to start filling in the sorrys! You can do them all in begin/end blocks; other people can tidy up later.

[Scott Morrison]

If you ignore is_locally_allowable for a second, then we've already got the presheaf of dependent functions (sections of the bundle with fibres $R_p$), and indeed the fact that this forms a sheaf.

We don't have the general machinery for this yet, but I think the right thing to do is next notice that is_locally_allowable is a local condition, and the sub-presheaf consisting of dependent functions satisfying some local condition is always a sub-sheaf.

[Scott Morrison]

i.e. I think we should define a suitable T : prime_spectrum R -> Type, and obtain a presheaf of all dependent functions as presheaf.to_Types T and the sheaf condition as sheaf_condition.to_Types T. Then do some abstract nonsense about "local conditions".

[Kevin Buzzard]

Kenny was really focused on the idea that the sheaf of dependent functions was the important idea -- the big sheaf

[Scott Morrison]

Something like:

import topology.sheaves.sheaf_of_functions

variables {X : Top}
variables (T : X → Type)

open topological_space

def condition_restricts (P : Π {U : opens X}, (Π x : U, T x) → Prop) : Prop :=
∀ (U V : opens X) (i : U ⟶ V) (f : Π x : V, T x) (h : P f), P (λ x : U, f (i x))

def condition_is_local (P : Π {U : opens X}, (Π x : U, T x) → Prop) : Prop :=
∀ (U : opens X) (f : Π x : U, T x) (w : ∀ x : U, ∃ (V : opens X) (i : V ⟶ U), P (λ x : V, f (i x : U))), P f

[Scott Morrison]

hopefully if P satisfies both condition_restricts and condition_is_local then the dependent functions satisfying the predicate P form a presheaf and a sheaf, respectively.

[Scott Morrison]

Then it's just a matter of verifying these for is_locally_allowable.

[Scott Morrison]

(but I have very low confidence in any of this... please shoot it down!)

[Scott Morrison]

So the presheaf part is easy:

import topology.sheaves.sheaf_of_functions

universe v

variables {X : Top.{v}}
variables {T : X → Type}

open topological_space
open opposite

def condition_restricts (P : Π {U : opens X}, (Π x : U, T x) → Prop) : Prop :=
∀ {U V : opens X} (i : U ⟶ V) (f : Π x : V, T x) (h : P f), P (λ x : U, f (i x))

def condition_is_local (P : Π {U : opens X}, (Π x : U, T x) → Prop) : Prop :=
∀ {U : opens X} (f : Π x : U, T x) (w : ∀ x : U, ∃ (V : opens X) (i : V ⟶ U), P (λ x : V, f (i x : U))), P f

def presheaf_of_dependent_functions_satisfying_condition
  (P : Π {U : opens X}, (Π x : U, T x) → Prop)
  (w : condition_restricts @P) :
  (opens X)ᵒᵖ ⥤ Type v :=
{ obj := λ U, { f : Π x : unop U, T x // P f },
  map := λ U V i f, ⟨λ x, f.1 (i.unop x), w i.unop f.1 f.2⟩ }

[Scott Morrison]

I think I'm going to go to bed before attempting the sheaf condition (wimping out!), but it hopefully is just an abstraction of the existing src#Top.sheaf_condition.to_Top that Johan and I wrote.

[Kevin Buzzard]

I might have to go to the beach but hopefully I can get to this later when sanity has been restored

[Bhavik Mehta]

/-- We enforce here that the open cover is actually contained in the given set. -/
def down_closed_open_cover (U : opens X) (S : set (opens X)) := (∀ V ∈ S, V ≤ U) ∧ (∀ x ∈ U, ∃ V, V ∈ S ∧ x ∈ V)

variable (P : (opens X)ᵒᵖ ⥤ Type u)

def restrict_presheaf {U V : opens X} (h : V ≤ U) (s : P.obj (opposite.op U)) :
  P.obj (opposite.op V) := P.map (hom_of_le h).op s

def locality : Prop :=
  ∀ (U : opens X) (S) (c : down_closed_open_cover U S) (s t : P.obj (opposite.op U)),
    (∀ Ui ∈ S, restrict_presheaf P (c.1 Ui H) s = restrict_presheaf P (c.1 Ui H) t) → s = t

def gluing : Type u :=
  Π (U : opens X) (S) (c : down_closed_open_cover U S) (s' : Π (Ui ∈ S), P.obj (opposite.op Ui))
    (hs : ∀ (Ui Uj ∈ S), restrict_presheaf P (lattice.inf_le_left _ Uj) (s' _ ‹_›) = restrict_presheaf P (lattice.inf_le_right Ui Uj) (s' _ ‹_›)),
    {s : P.obj (opposite.op U) // ∀ (Ui ∈ S), restrict_presheaf P (c.1 _ H) s = s' _ H}

I'd put together this, which might be useful - a sheaf is then just a presheaf with locality and gluing axioms

[Bhavik Mehta]

(I only made this to make sure my abstract sheaf axioms were the same thing as the ones on wikipedia, I'm not claiming these are the best for mathlib)

[Damiano Testa]

Johan Commelin said:

algebraic_geometry/prime_spectrum

Dear Johan,

I am trying to use your prime_spectrum file, and I believe that the following should be true, but I am having lots of trouble proving it: am I misunderstanding something? Is this already proved in your file? I tried searching for something along these lines, but was unable to find anything

Thank you very much!

import data.polynomial.induction
import algebraic_geometry.prime_spectrum

open prime_spectrum

universes u


variables {R : Type u} [comm_ring R] (I : prime_spectrum (polynomial R))

noncomputable def Cstar := prime_spectrum.comap (polynomial.C : R →+* polynomial R)

lemma incl {R : Type u} [comm_ring R] (I : prime_spectrum (polynomial R))
 : ∀ p ∈ (Cstar I).1 , polynomial.C p ∈ I.1 :=
begin

    sorry,
end

[Damiano Testa]

(Although I do not need this at the moment, basically what I am interested in is that if the ring map A --> B is an inclusion, then, in terms of sets rather than types, the induced map on spectra is simply the intersection of an ideal in the larger ring B with the smaller ring A.)

[Johan Commelin]

Tell me try

[Damiano Testa]

sure! and no rush: I will have to leave soon, and I am not sure that I will have time to seriously look at this over the weekend. I will be definitely looking at it on Monday, though!

[Johan Commelin]

lemma incl {R : Type u} [comm_ring R] (I : prime_spectrum (polynomial R))
 : ∀ p ∈ (Cstar I).as_ideal , polynomial.C p ∈ I.as_ideal :=
begin
    intros p hp,
    dsimp [Cstar] at hp,
    simp at hp,
    exact hp,
end

[Johan Commelin]

lemma incl {R : Type u} [comm_ring R] (I : prime_spectrum (polynomial R))
 : ∀ p ∈ (Cstar I).as_ideal , polynomial.C p ∈ I.as_ideal :=
begin
    intros p hp, exact hp,
end

[Damiano Testa]

really?! this quick?

Let me use it! Ahaah

[Damiano Testa]

Thank you very much!

[Johan Commelin]

In other words, hp is by definition the thing that you wanted to prove (-;

[Damiano Testa]

Yes, I can see that, although it was not clear to me that this was the case... Lean is very good at understanding its own code! And so are you!

[Damiano Testa]

Thank you very much!

[Damiano Testa]

I need to go now, but I will continue on Monday!

[Johan Commelin]

Ciao!

[Scott Morrison]

@Kevin Buzzard, I pushed the "local predicate" construction as #3906.

[Scott Morrison]

Now I think all that is required to build the sheaf on prime_spectrum R is to package is_locally_allowable as a local_predicate. Hopefully that is easy from the definition.

[Scott Morrison]

(Putting the ring structure on is orthogonal --- because of #3609, we can ignore the ring structure while checking the sheaf condition.)

[Johan Commelin]

Nice!

[Johan Commelin]

Scott Morrison said:

Now I think all that is required to build the sheaf on prime_spectrum R is to package is_locally_allowable as a local_predicate. Hopefully that is easy from the definition.

We also need a presheaf to start with, right?

[Johan Commelin]

Scott Morrison said:

(Putting the ring structure on is orthogonal --- because of #3609, we can ignore the ring structure while checking the sheaf condition.)

Looks good! I left a review with some typos I found.

[Scott Morrison]

I was starting to look at @Kevin Buzzard's spec-of-a-ring branch, and getting worried because his definition of is_locally_allowable isn't obviously local in the sense of #3906.

However when I go look at Hartshorne (p.70) File-Aug-22-15-28-25.jpeg I get happier, because the definition there is obviously local in my sense, but also sadder, because it's not obvious to me that this is equivalent to the definition Kevin gave. If anyone wants to help me sort this out that would be great. :-)

[Johan Commelin]

@Scott Morrison Sure! Let's try to figure this out.

[Johan Commelin]

Let me grab a copy of Kevin's branch

[Scott Morrison]

(I'm happy to do a screen share if that's the easiest way --- just let me know when you've had a look)

[Johan Commelin]

Ok, I have the branch open

[Johan Commelin]

I guess we'll have breakfast in 15 a 30 minutes, but we can try a quick screenshare

[Scott Morrison]

I did some more work after we finished, @Johan Commelin, and it seems to work well.

[Scott Morrison]

I have the structure sheaf on Spec R (although not the ring structure).

[Johan Commelin]

That shouldn't be too hard, right?

[Scott Morrison]

#3907, if anyone wants to look at it.

[Scott Morrison]

No, the ring structure is hopefully straightforward, but it is going to be a little messy because we need to check that the ring operations interact properly with locally_quotient.

[Johan Commelin]

Let's define schemes today (-;

[Scott Morrison]

Okay, so what comes next? Should we just do the ring structure?

[Kevin Buzzard]

Morning. If my definition is not the same as Hartshorne then I messed up because it was supposed to be

[Scott Morrison]

@Kevin Buzzard, notice your condition never talks about any smaller open sets inside U.

[Scott Morrison]

You've just asked for functions on U which are, on U, a quotient.

[Johan Commelin]

@Scott Morrison I left a minor review

[Johan Commelin]

Next steps:

0. ring structure
1. compute stalks
2. define LRS
3. show that comap is a hom of LRS

[Scott Morrison]

How does the computation of stalks go?

[Johan Commelin]

Clearly there is a map from the stalk to stalks x

[Johan Commelin]

Show that it is bijective

[Scott Morrison]

We are definitely exceeding my level of studiousness when reading Hartshorne 20 years ago. :-)

[Johan Commelin]

@Scott Morrison Want to screenshare again?

[Scott Morrison]

Sure!

[Johan Commelin]

Same room?

[Scott Morrison]

Finished the ring structure, but not yet that the restriction maps are ring_homs

[Scott Morrison]

Okay, that was trivial, all worked by rfl.

[Scott Morrison]

We have the structure sheaf on Spec R, as a sheaf of commutative rings!

[Johan Commelin]

Awesome!

[Johan Commelin]

@Scott Morrison did you push?

[Johan Commelin]

up next is the iso to stalks?

[Johan Commelin]

@Scott Morrison I pushed a tiny tweak

[Johan Commelin]

(Most of what I did was duplicate)

[Kevin Buzzard]

I am spending the day travelling so might not be much help. Remember that the local isomorphism in the definition of schemes is only an isomorphism of spaces equipped with a presheaf of rings and because affine schemes are locally ringed spaces you only need to say that a scheme is a ringed space which is locally affine

[Kevin Buzzard]

Can we pull back a presheaf of rings on a space to an open subspace?

[Scott Morrison]

No, we don't have pullback to an open yet.

[Kenny Lau]

I'm thinking of a reform. I want a definition (i.e. implementation) that is best suited for Lean. Here is what I have come up with:

import algebraic_geometry.prime_spectrum
import ring_theory.localization

universes u v

noncomputable theory
open_locale classical

variables (R : Type u) [comm_ring R]

-- How far can I go avoiding partial functions and sigma types?

/-- set (Σ x, S x) = Π x, set (S x)  -/
structure stalk_topology (X : Type u) (S : X → Type v) :=
(is_open : (Π x, set (S x)) → Prop)
-- TODO : univ, inter, sUnion

-- TODO : add the hypothesis of them forming a basis
def stalk_topology.generate_from_basis {X : Type u} {S : X → Type v}
  (B : set (Π x, set (S x))) : stalk_topology X S :=
{ is_open := λ s, ∀ (f : Π x, S x), (∀ x, f x ∈ s x) →
    ∃ b ∈ B, ∀ x, by exact f x ∈ b x ∧ b x ⊆ s x }


def espace_etale (P : prime_spectrum R) : Type u :=
localization.at_prime P.1

-- I claim that this contains exactly the same information.
def structure_sheaf : stalk_topology (prime_spectrum R) (espace_etale R) :=
stalk_topology.generate_from_basis
  { s | ∃ f a : R, ∃ n : ℕ, ∀ x : prime_spectrum R,
      (if H : f ∈ x.1 then ∅ else {localization.mk a ⟨f ^ n,
        show f ^ n ∈ x.val.prime_compl.carrier,
        from mt (x.2.mem_of_pow_mem n) H⟩})
    = s x }

[Bhavik Mehta]

Kevin Buzzard said:

My understanding is that Bhavik Mehta has a bunch of this stuff in the topos repo but he also has a thesis to write

Yeah, I'm in the process of slowly PR-ing the preliminary stuff though

[Scott Morrison]

@Johan Commelin, I'm done for the day I think, but I just pushed LRS, which includes a definition of Scheme. There are no sorries in that file, but there are sorries elsewhere!

[Scott Morrison]

At least to get to the definition, all we need now is restricting a PresheafedSpace / SheafedSpace / LocallyRingedSpace to an open subset.

[Scott Morrison]

Those restrictions are stubbed out in their respective files, but the actual content is not there.

[Johan Commelin]

Ok, thanks for all you've done!

[Kenny Lau]

@Kevin Buzzard @Johan Commelin what do you think of my idea?

[Johan Commelin]

My intuition :stuck_out_tongue_wink: likes the categorical approach

[Johan Commelin]

But maybe Lean doesn't...

[Johan Commelin]

I'm trying to find it out

[Johan Commelin]

I guess your idea would also work, but then we shift the problem to next year, when we want to discuss etale sheaves.

[Adam Topaz]

I'm not saying this is the right approach, but the etale topos does have enough points, so the espace etale approach "could" work in the etale topology as well.

[Kevin Buzzard]

@Kenny Lau when the dust has settled it will be interesting to see which approach can glue schemes together. Making projective 1 space by glueing two affine 1 spaces will be a key exercise

[Scott Morrison]

So I think that at least one of the remaining sorries on the way to the definition of Scheme deserves to wait until we get prop_limits right. When definining LocallyRingedSpace.restrict, we need to check that a stalk of the restriction to some U is the stalk of the original LRS. The right way to do this is to show that neighbourhoods inside U are cofinal in all neighbourhoods.

But I don't really want to define cofinal until I know how we're fixing has_limit and friends.

[Heather Macbeth]

@Scott Morrison, naive question -- is the definition local_predicatein #3906 equivalent to the 1st + 3rd axioms in docs#structure_groupoid.local_invariant_prop?

[Scott Morrison]

I can't quite understand what local_invariant_prop is saying, but I don't think so. For one, in local_predicate there is only a single topological space anywhere in the picture, but local_invariant_prop has two.

[Heather Macbeth]

Certainly local_predicate is more general -- I guess I'm asking if local_invariant_prop could be rewritten to extend it.

[Heather Macbeth]

Easier question, perhaps -- is the first axiom of local_invariant_prop the same as #3906 's prelocal_predicate?

[Scott Morrison]

No, I still don't think so. local_invariant_prop.local seems much more specific. It says that it suffices to check the property on any open neighbourhood of the point x.

[Scott Morrison]

prelocal_predicate only says that it's necessary that the property also hold on a smaller nbhd, if it holds on a big nbhd.

[Heather Macbeth]

Ah -- so in fact, it is more akin to local_predicate than prelocal_predicate?

[Scott Morrison]

well, but local_predicate still doesn't care about any particular point

[Scott Morrison]

it says that if at every point in the U of definition you can find a nbhd V where the property holds, the property holds for the function on all of U.

[Scott Morrison]

so still I think there's an incompatible order of quantifiers difference between the two

[Scott Morrison]

(I still haven't got my head around a canonical example of local_invariant_prop, however, so I may just be wrong.)

[Heather Macbeth]

Scott Morrison said:

(I still haven't got my head around a canonical example of local_invariant_prop, however, so I may just be wrong.)

(local_invariant_prop is for classes of functions between manifolds which are (1) characterized locally and (2) are basically expressed in terms of the model space, for example smoothness)

[Scott Morrison]

Regardless of the logical relation between them, a big mismatch between them is going to be that local_invariant_prop uses total functions, while local_predicate is all in terms of functions defined only on some U : opens X. (Possibly this is a bad idea, but it seems to work.)

[Scott Morrison]

I can have a look later to see if I can reformulate local_predicate more like this... The first step would be to change the predicate to take a third argument, a particular point. This is making an assumption about the form the predicates take, but I think in all examples this holds.

[Scott Morrison]

But I'm not certain this is a good idea --- the current design is meant to be "exactly what you need to check so that a subset of dependent functions forms a presheaf / sheaf".

[Scott Morrison]

Certainly I think if it is possible to provide some glue going from local_invariant_prop to local_predicate that would be great.

[Heather Macbeth]

Scott Morrison said:

Certainly I think if it is possible to provide some glue going from local_invariant_prop to local_predicate that would be great.

Yep, that's exactly what I would hope for, I don't think it matters if the definitional organizations differ.

[Scott Morrison]

We do want to be able to effortlessly say "the rings of smooth functions on open sets form a sheaf, because smoothness is a local property"

[Scott Morrison]

(not, in case Patrick is watching, that I have any desire to infect differential geometry with sheaves --- just for the sake of the exercise :-)

[Scott Morrison]

@Heather Macbeth could you point me to the instance of local_invariant_prop for C^\infty smoothness? I can try to add this as an example.

[Heather Macbeth]

I would be very interested to see this! docs#times_cont_diff_within_at_local_invariant_prop

[Adam Topaz]

@Scott Morrison sorry if I missed this in the discussion above and/or the code... do you have a way of restricting a (pre)local_predicate to an open set?

[Scott Morrison]

That's the res field.

[Adam Topaz]

I mean taking, say, a prelocal_predicate T where T is a dependent function on X, and and open set U in X, and obtaining a prelocal_predicate T' where T' is the restriction of T to U.

[Adam Topaz]

I'm thinking about how to make the sheafification with this approach

[Scott Morrison]

No, I don't have that.

[Adam Topaz]

I.e. the left adjoint of the forgetful functor from local_predicate to prelocal_predicate

[Scott Morrison]

Do you mean define the sheafification as the subsheaf of dependent functions into the stalks, given by the local_predicate of being locally induced by something from the presheaf? (i.e. Proposition-Definition II.1.2 of Hartshorne)

[Adam Topaz]

Exactly

[Adam Topaz]

(I assume, I don't have Hartshorne in front of me)

[Scott Morrison]

But I don't see how that relates to restricting?

[Scott Morrison]

Proposition-Definition II.1.2 of Hartshorne

[Scott Morrison]

I'd be happy to give this a go, it does sounds like a good test of local_predicate. Let me know if you're already doing it!

[Adam Topaz]

You're right this should be easy to write down. I was thinking of using covers of U

[Adam Topaz]

I was planning on trying it out, but I won't be able to do much until a few hours from now

[Scott Morrison]

great, okay!

[Scott Morrison]

I pushed a start on this to sheafification:

import topology.sheaves.local_predicate
import topology.sheaves.stalks

universes v

noncomputable theory

open Top
open topological_space
open opposite
open category_theory.limits

variables {X : Top.{v}}
variables (F : presheaf (Type v) X)

namespace sheafification

def stalks : Π x : X, Type v := λ x : X, F.stalk x

-- TODO it seems all `local_predicate`s have `pred` starting with:
-- `λ U f, ∀ x : U, ∃ (V : opens X) (m : x.1 ∈ V) (i : V ⟶ U) ...`
-- Make a definition of this shape, and make it easier to prove `res` and `locality`?

def predicate : local_predicate (stalks F) :=
{ pred := λ U f, ∀ x : U, ∃ (V : opens X) (m : x.1 ∈ V) (i : V ⟶ U) (g : F.obj (op V)),
    f x = colimit.ι ((open_nhds.inclusion x.1).op ⋙ F) (op ⟨V, m⟩) g, -- TODO define `germ`!
  res := sorry,
  locality := sorry, }

end sheafification

def sheafification : sheaf (Type v) X :=
subsheaf_to_Types (sheafification.predicate F)

-- TODO check the stalks are correct
-- TODO functoriality

[Adam Topaz]

Nice! I was thinking even more low-level... something like this:

def sheafify (P : prelocal_predicate T) : local_predicate T :=
{ pred := λ U f, ∀ (x : U), ∃ (V : opens X) (mem : x.1 ∈ V) (i : V ⟶ U),
    P.pred (λ x : V, f (i x : U)),
  res := sorry,
  locality := sorry }

[Scott Morrison]

oh!

[Scott Morrison]

Neat!

def sheafify {T : X → Type v} (P : prelocal_predicate T) : local_predicate T :=
{ pred := λ U f, ∀ x : U, ∃ (V : opens X) (m : x.1 ∈ V) (i : V ⟶ U), P.pred (λ x : V, f (i x : U)),
  res := λ V U i f w x,
  begin
    specialize w (i x),
    rcases w with ⟨V', m', i', p⟩,
    use V ⊓ V',
    use ⟨x.2, m'⟩,
    use opens.inf_le_left _ _,
    convert P.res (opens.inf_le_right V V') _ p,
  end,
  locality := λ U f w x,
  begin
    specialize w x,
    rcases w with ⟨V, m, i, p⟩,
    specialize p ⟨x.1, m⟩,
    rcases p with ⟨V', m', i', p'⟩,
    use V',
    use m',
    use i' ≫ i,
    exact p',
  end, }

[Adam Topaz]

Golfed a little bit:

def sheafify {T : X → Type v} (P : prelocal_predicate T) : local_predicate T :=
{ pred := λ U f, ∀ x : U, ∃ (V : opens X) (m : x.1 ∈ V) (i : V ⟶ U), P.pred (λ x : V, f (i x : U)),
  res := λ V U i f w x,
  begin
    specialize w (i x),
    rcases w with ⟨V', m', i', p⟩,
    refine ⟨V ⊓ V',⟨x.2,m'⟩,opens.inf_le_left _ _,_⟩,
    convert P.res (opens.inf_le_right V V') _ p,
  end,
  locality := λ U f w x,
  begin
    specialize w x,
    rcases w with ⟨V, m, i, p⟩,
    specialize p ⟨x.1, m⟩,
    rcases p with ⟨V', m', i', p'⟩,
    exact ⟨V',m',i' ≫ i,p'⟩,
  end }

[Adam Topaz]

I don't know if this is worth doing, but there is a natural category structure on "dependent functions", and it's possible to build a category of local_predicates on top of that. Sheaves (of sets on a topological space) as a category should be essentially this.

Here's a little sketch of the category of dependent functions:

import tactic
import category_theory.category

open category_theory

variable (X : Type*)

def depfun := (Σ {G : X → Type*}, Π (x : X), G x)

namespace depfun

variable {X}
def hom (T1 T2 : depfun X) :=
  { g : Π {x : X}, T1.fst x → T2.fst x // ∀ x, g (T1.snd x) = T2.snd x }

namespace hom

def id (T : depfun X) : depfun.hom T T :=
{ val := λ x, id,
  property := by tauto }

def comp (T1 T2 T3 : depfun X) (F : hom T1 T2) (G : hom T2 T3) : hom T1 T3 :=
{ val := λ x y, G.val $ F.val y,
  property := λ x, by rw [F.2,G.2] }

end hom

instance : category (depfun X) :=
{ hom := depfun.hom,
  id := depfun.hom.id,
  comp := depfun.hom.comp }
end depfun

[Scott Morrison]

@Adam Topaz, I've refactored the spec branch (#3907) to use prelocal_predicate.sheafify. It's nice!

[Johan Commelin]

Note that Bhavik already did sheafification in an arbitrary topos

[Kevin Buzzard]

Right but it's not in mathlib

[Scott Morrison]

Actually defining the sheafification is now delightfully easy --- just a couple of lines:

def is_germ : prelocal_predicate (λ x, F.stalk x) :=
{ pred := λ U f, ∃ (g : F.obj (op U)), ∀ x : U, f x = F.germ x g,
  res := λ V U i f ⟨g, p⟩, ⟨F.map i.op g, λ x, (p (i x)).trans (F.germ_res _ _ _).symm⟩, }

def is_locally_germ : local_predicate (λ x, F.stalk x) := (is_germ F).sheafify

def sheafify : sheaf (Type v) X :=
subsheaf_to_Types (sheafify.is_locally_germ F)

I'm trying to prove that the stalks are the original stalks, and I can do the constructions, but checking well-definedness I'm in classical.some hell.

[Bhavik Mehta]

Yeah I'm in the process of putting it in mathlib though

[Scott Morrison]

The sheafification I was playing with today is not that important. It was just a spin-off of what we've been doing on Spec R in the last few days.

[Bhavik Mehta]

I don't know if it would be worth investigating other constructions of sheafification though - for instance if there's a particular construction which gives nice defeq properties for geometers then it could be worthwhile to use that version as the definition, and since it should be isomorphic to my version (once the sheafify-forget adjunction is done for some other version) properties like being a geometric morphism of topoi would drop out: this is a question for the geometers really

[Kevin Buzzard]

We should experiment!

[Adam Topaz]

Regardless what the definition is, we would need the theorem that the stalks of the sheafification agree with those of the presheaf, and an "extensionality" principle that a map of sheaves is an iso iff it is an iso on all stalks. This makes me think that the disjoint union of stalks definition has a good chance of being useful in practice.

[Kevin Buzzard]

I'm just trying to catch up on all this stuff today

[Kevin Buzzard]

How far are we from sheaves of modules on a ringed space? From bundled locally ringed spaces?

[Kevin Buzzard]

Have we isolated some kind of concept of a "concrete sheaf" on a topological space, as being a subsheaf of the sections of a dependent pi type? And the theory of sheafification is nice and straightforward here. Is this what has happened?

[Scott Morrison]

@Kevin Buzzard, there is a branch branch#LRS that Johan and I have been working on that defines a bundled LocallyRingedSpace, as well as a bundled Scheme.

[Scott Morrison]

It has two major sorries:

1. checking that when you pull back a presheaf along an open embedding, you don't change the stalks
2. checking that the stalks of Spec R are the localizations

[Scott Morrison]

For 1., the thorough way to do this would be to set up the theory of cofinal functors. (Because the inclusion of "nbhds of x within U" into "nbhds of x" is cofinal, so colimits are the same.)

[Scott Morrison]

We're pretty well set up to do this, because @Bhavik Mehta made a nice API for connected categories. I thought about this a little, but struggled getting my head around doing the construction without ever inducting on zigzags... I think instead you want to use the characterisation "functors out of a connected category to a discrete category are constant" directly.

[Scott Morrison]

For 2. as far as I can see it is just a matter of copying and pasting the relevant page of Hartshorne. I haven't started this yet, but would be happy to either do it, or screen share with someone and see if we can hack it out. I don't see any particular obstruction.

[Scott Morrison]

How far are we from sheaves of modules on a ringed space?

I haven't made any progress on this. One thing I would like to try is modelling a sheaf of rings as an internal ring object in sheaves, and then talking about a sheaf of modules as an internal module object. However, the "internal objects" development that exists so far is largely incompatible with the changes we really ought to make to get prop_limits (making the currently evil has_limit typeclass into a Prop) merged.

So I've stopped working on / thinking about internal objects, until we get that done.

[Scott Morrison]

The two main blockers on the prop_limits branch are now:

1. fixing the construction of a monoidal category from a category with binary products, so it's possible to specify which binary products you want to use,
2. the file src#Top.sheaf_condition.to_Types uses an "it's obvious" step that relied on Lean knowing the definition of limits in Type, and this is currently broken on the prop_limits branch, and every time I look at it my head hurts.

[Scott Morrison]

That said, it may be that @Reid Barton has other ideas besides the prop_limits branch about how to resolve the has_limit issue, but I'm not sure where his thinking is on this.

[Scott Morrison]

The PR #3873, already merged into prop_limits takes care of one of the other obstructions, namely getting all the constructions of limits in concrete categories working compatibly with a propositional has_limit typeclass. (I think this obstruction is where @Markus Himmel originally paused when he started the prop_limits branch.)

[Bhavik Mehta]

Scott Morrison said:

How far are we from sheaves of modules on a ringed space?

modelling a sheaf of rings as an internal ring object in sheaves

I think this is a useful thing to have as well

[Bhavik Mehta]

I think one thing which will help the has_limit issue yet also be useful for prop_limits would be to have basically everything stated in terms of is_limit rather than "the" limit

[Scott Morrison]

Yes. I understand that this is better, but it's also usually really painful. :-)

[Adam Topaz]

I'm still playing around with these local predicates: here's an idea for sheaves of modules using local_predicate:

import algebra
import topology.sheaves.local_predicate

open Top
open topological_space
universe v
variables {X : Top.{v}}
variables (T : X → Type v) (S : X → Type v)

structure local_ring_predicate extends local_predicate T :=
(fibre_ring (x  : X) : ring (T x))
(is_subring : ∀ {U : opens X}, is_subring (pred : set (Π (x : U), T x)))

structure local_module_predicate (A : local_ring_predicate T) extends local_predicate S :=
(fibre_add_comm_group (x : X) : add_comm_group (S x))
(fibre_module (x : X) : by letI := A.fibre_ring x; exact module (T x) (S x))
(is_submodule : sorry) -- is_submodule doesn't exist in mathlib, but you get the idea.

Of course, this is different from the categorical approach that @Scott Morrison and @Johan Commelin have used.

[Adam Topaz]

Yes, I know that I shouldn't use is_subring :)

[Scott Morrison]

Wouldn't it make more sense to parametrise by fibre_ring, rather than bundle it?

[Adam Topaz]

Oh yeah, good point. I guess that way the instance will be found in the second definition.

[Scott Morrison]

one way to deal with the deprecation of is_subring would be to rename local_predicate.pred to local_predicate.carrier, and have local_ring_predicate extend subring... not sure if this actually makes sense.

[Scott Morrison]

(the idea being to force .pred and .carrier to agree by having them be the same thing)

[Adam Topaz]

import algebra
import topology.sheaves.local_predicate

open Top
open topological_space
universe v
variables {X : Top.{v}}
variables (T : X → Type v) (S : X → Type v)

structure local_ring_predicate [Π (x : X), ring (T x)] extends local_predicate T :=
(is_subring : ∀ {U : opens X}, is_subring (pred : set (Π (x : U), T x)))

structure local_module_predicate [Π (x : X), ring (T x)] (A : local_ring_predicate T)
  [Π (x : X), add_comm_group (S x)] [Π (x : X), module (T x) (S x)] extends local_predicate S :=
(is_submodule : sorry) -- is_submodule doesn't exist in mathlib, but you get the idea.

[Scott Morrison]

In another direction, @Adam Topaz, do you know of an abstract condition on prelocal_predicate that ensures that the stalk of its sheafification is the original fibre?

[Scott Morrison]

I was trying to do this in the sheafification branch, where the prelocal_predicate is just is_germ. I ran into trouble with classical.some.

[Scott Morrison]

I think finishing off that isomorphism in the sheafification branch is a good test of this local_predicate setup.

[Adam Topaz]

Scott Morrison said:

In another direction, Adam Topaz, do you know of an abstract condition on prelocal_predicate that ensures that the stalk of its sheafification is the original fibre?

Yes, you can just say that for every element z of T x, there is some neighborhood U of x, and some section w over U, where Z and w agree over x.

[Scott Morrison]

Doesn't that only give a (presumably surjective) map from the fibre to the stalk?

[Adam Topaz]

I don't think so... The union of the sections over the neighborhoods is the colimit in the category of sets, and the sections over the open sets are already defined as subsets of the union of the fibres.

[Adam Topaz]

Oh actually I think you're right.

[Adam Topaz]

E.g. think about SpecZ, and put the fibre over a prime of Z to be the residue field of that point.

[Adam Topaz]

But I think we can get around this by imposing some injectivity

[Adam Topaz]

Ah but even that is too restrictive in general!

[Adam Topaz]

Yeah I don't see how to make it work in general :frown:

[Adam Topaz]

The only way I see how to do it is by saying that the canonical map from the union to the fibre is a bijection.

[Scott Morrison]

Do you have any idea how to proceed at https://github.com/leanprover-community/mathlib/blob/sheafification/src/topology/sheaves/sheafify.lean#L55?

[Adam Topaz]

Ok so you can take the condition i mentioned above (which is equiv to surjectivity) and add another condition saying that whenever z is in T x and wi is a section over Ui, i=1,2, mapping to z, there is a neighborhood V contained in the intersection of U1 and U2, such that w1 and w2 agree everywhere over V. This is an ugly condition, but still elementary

[Adam Topaz]

Hmm I'm on mobile now, but I'll try to look at that file a little later if I have time (tomorrow for sure)

[Adam Topaz]

Even with this approach, classical.some will still be used to pass from a bijection to an isomorphism :oh_no:

[Adam Topaz]

Okay, I think something like this should work:

structure compat_local_predicate extends prelocal_predicate T :=
(surj (x : X) (z : T x) : ∃ (U : opens X) (m : x ∈ U) (w : Π (u : U), T u), pred w ∧ (z = w ⟨x,m⟩))
(inj (x : X) (z : T x) (U₁ U₂ : opens X) (m₁ : x ∈ U₁) (m₂ : x ∈ U₂)
  (w₁ : Π (u₁ : U₁), T u₁) (w₂ : Π (u₂ : U₂), T u₂) (h₁ : pred w₁) (h₂ : pred w₂)
  (e₁ : w₁ ⟨x,m₁⟩ = z) (e₂ : w₂ ⟨x,m₂⟩ = z) :
  ∃ (V : opens X) (i₁ : V ⟶ U₁) (i₂ : V ⟶ U₂) (w : Π (v : V), T v),
  ∀ (v : V), w₁ (i₁ v) = w v ∧ w₂ (i₂ v) = w v)

[Scott Morrison]

almost there with the proof that this give injectivity...

[Adam Topaz]

@Scott Morrison Concerning sheafify.foo, I think the (pen-and-paper) correct way to define this is using the universal property of the colimit. I'm not sure how to phrase this using the colimits from mathlib though.

[Scott Morrison]

Okay, injectivity and surjectivity from these condition are now proved in #3906.

[Scott Morrison]

Hopefully this will be useful both for sheafify, and for calculating the stalks of Spec R.

[Scott Morrison]

Oh ... hmm, maybe I'm not sure if the injectivity condition applies for Spec R.

[Scott Morrison]

I guess it does... this is exactly Hartshorne's argument, just factored out a bit strangely.

[Scott Morrison]

with a bit of work to construct the V in Adam's language.

[Scott Morrison]

sheafify.foo on the sheafification branch is now just stalk_to_fiber, defined in #3906 (and constructed, as you said, Adam, using colimit.desc.)

[Adam Topaz]

Yeah it should all be fine for $Spec R$. Here's the "pen-and-paper" proof I would give in a commutative algebra class :)

If $\mathfrak{p}$ is a prime and $a/f \in R_{\mathfrak{p}}$, then just think of $a/f$ as a section over the standard open set $U_f$, and this gives surjectivity. And if $U_1,U_2$ are neighborhoods of $\mathfrak{p}$ and $w_i$ are sections which agree in $R_\mathfrak{p}$, then first make $U_1$ and $U_2$ a bit smaller to assume they're standard opens $U_{f_1}$ and $U_{f_2}$ (this is fine since the standard opens form a basis for the topology), so WLOG $w_i = a_i/f_i$ (really, I should say $a_i/(f_i)^{n_i}$, but then just replace $f_i$ with $(f_i)^{n_i}$). Saying they're equal in the localization at $\mathfrak{p}$ means that there is some $s \notin \mathfrak{p}$ such that $a_1 \cdot f_2 \cdot s = a_2 \cdot f_1 \cdot s$. Take $V$ to be the intersection $U_{f_1} \cap U_{f_2} \cap U_{s} = U_{f_1 \cdot f_2 \cdot s}$, etc.

[Adam Topaz]

Of course, I'm assuming you take $R_\mathfrak{p}$ to be the fibre over $\mathfrak{p}$.

It's actually quite interesting that in some cases (I guess reduced schemes would be enough?) you can take the residue field as the fibre, and define the structure sheaf using a local_predicate. This should satisfy the surjectivity condition but not injectivity, but should yield the same sheaf!

[Johan Commelin]

@Scott Morrison What's up next?

[Scott Morrison]

So, in the sheafification branch (which is a bit of a sideshow, but I think an excellent exercise of the machinery), we now have that the stalks are correct, except that there's a sorry:

lemma germ_eq (F : X.presheaf (Type v)) {U V : opens X} (x : X) (mU : x ∈ U) (mV : x ∈ V)
  (s : F.obj (op U)) (t : F.obj (op V))
  (h : germ F ⟨x, mU⟩ s = germ F ⟨x, mV⟩ t) :
  ∃ (W : opens X) (m : x ∈ W) (iU : W ⟶ U) (iV : W ⟶ V), F.map iU.op s = F.map iV.op t :=
begin
  sorry,
end

[Scott Morrison]

Now that we have good machinery for checking that stalk_to_fiber is a bijection, we should sit down and write the proof that the stalks of Spec R are correct. (e.g. following Hartshorne, or close to isomorphically the proof Adam wrote above).

[Scott Morrison]

I would like to do germ_eq, but it's hard to get at!

[Scott Morrison]

The problem is just that we don't have much machinery for filtered / directed colimits.

[Johan Commelin]

I just pushed a proof of local_ring.of_ring_equiv

[Scott Morrison]

The maths proof would say "If two points in a colimit are equal, they are related by some zigzag of morphisms in the indexing diagram. Since we're looking at open sets (which form a directed set), we can just take the intersection of all the open sets appearing in that zigzag, and in fact the two points are related by a single V shape in the indexing diagram. That's the W in the goal."

[Scott Morrison]

But I don't want to actually have a zigzag appear, and I don't think we have the right induction principle to hand. :-(

[Johan Commelin]

Right

[Scott Morrison]

We could leave that for now, and just do the stalks in Spec R calculation. Starting in about 90 minutes I'd be happy to screenshare that. (What's the verb for pair-programming remotely?)

[Johan Commelin]

remogramming?

[Kevin Buzzard]

These are filtered colimits -- surely this makes things easier. We surely don't need zigzags.

[Reid Barton]

If it helps, I think this is an old proof of what you're looking for

[Scott Morrison]

Reid Barton said:

If it helps, I think this is an old proof of what you're looking for

Perfect! I had seen this before, but forgotten it. I've just taken the liberty of merging master into branch#filtered-colimits-2, and making the necessary changes.

Could you make a PR out of it? I only made small changes, so on the assumption I didn't botch anything it looks straightforward to me. I can make the PR if you'd prefer, too.

[Kevin Buzzard]

All you need to be able to do to make schemes, are

• the definition of a sheaf of rings on a topological space,
• ability to pull back a presheaf of rings along an open immersion,
• ability to talk about an isomorphism of presheaves of rings on a fixed space, and
• The definition of the canonical presheaf of rings on Spec(R).

How close are we to these four things?

[Kevin Buzzard]

Other things are interesting for the API but not needed for the definition.

[Johan Commelin]

We have all those 4 things

[Kevin Buzzard]

so we can define schemes in mathlib, right?

[Johan Commelin]

Yup, everything is already PR'd

[Johan Commelin]

But we want to know that Spec(R) is a functor to schemes.

[Kevin Buzzard]

we want to know all sorts of things, but it would be wonderful actually get the definition of a scheme into mathlib

[Kevin Buzzard]

this is the milestone

[Kevin Buzzard]

not that some map is a functor

[Kevin Buzzard]

Johan Commelin said:

We have all those 4 things

How do I pull back a presheaf of rings along an open immersion?

[Adam Topaz]

I was under the impression that restriction of sheaves to open sets was not done yet.

[Johan Commelin]

Sure, but presheaves is easier

[Adam Topaz]

Is it done for preseheaves?

[Johan Commelin]

@Kevin Buzzard one of the PRs contains a way to turn an h : open_embedding f into a functor opens U \func opens X.

[Johan Commelin]

And then you simply compose with the \op of that.

[Kevin Buzzard]

How do I search for this? I want to see a recent PR which contained a commit which mentions open_embedding. How do I look for this?

[Kevin Buzzard]

I haven't been looking at the PR's

[Patrick Massot]

https://github.com/leanprover-community/mathlib/search?q=open_embedding&type=Issues

[Kevin Buzzard]

I can't find it. I need precisely what you said Johan.

[Johan Commelin]

1 sec, finding the link

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/LRS/src/topology/category/Top/opens.lean#L172

[Johan Commelin]

@Kevin Buzzard :up:

[Scott Morrison]

Note that branch#LRS which Johan just linked to is not yet a PR!

[Scott Morrison]

Sorry, maybe I'm missing something, but I don't we need more than what Kevin has said?

[Scott Morrison]

In particular, in the definition of Scheme we want a cover by opens on each of which our sheaf of local rings is isomorphic as a locally ringed space to some Spec R.

[Scott Morrison]

(That is, it's not good enough to just say that the presheaf of local rings on U is isomorphic as a presheaf to the presheaf on some Spec R.)

[Scott Morrison]

The point being that locally ringed spaces are not a full subcategory of SheafedSpace, but rather have an extra condition about the maximal ideals.

[Scott Morrison]

So we're still missing

1. that Spec R is a locally ringed space
2. that the restriction of a locally ringed space along an open embedding is a locally ringed space.

[Scott Morrison]

So far we have only Spec R as a SheafedSpace.

[Scott Morrison]

We know that the underlying type of the stalk at a point x : prime_spectrum R is isomorphic to the localization of R at x. But we don't yet have that this isomorphism is an isomorphism of rings.

[Scott Morrison]

This is the sorry at https://github.com/leanprover-community/mathlib/blob/LRS/src/algebraic_geometry/structure_sheaf.lean#L311

[Scott Morrison]

To prove this, I would like to first prove that the forget CommRing preserves filtered colimits, and hence that the stalk (as a CommRing) at x is the same as the stalk (as a Type) at x, and so the isomorphism of rings can use the existing isomorphism of types.

We'll then need to check that it is actually a morphism of rings, but I think this part will not be hard.

[Scott Morrison]

There is a WIP branch preserves_filtered_colimits that is doing this, but I having got into the woods a bit, I think I would like to redo this branch, and actually prove that filtered colimits commute with finite limits, and then use this framework when showing forgetful functors preserve filtered colimits. It's more work if we're just racing to Scheme, but I think it will be nicer in the long run, and you basically do most of the work along the way in any case. If anyone wants a category-theoretic task to work on, I know how to chop up this goal into some separate subunits and would be happy to have help / have someone do it!

[Scott Morrison]

For 2. (restricting a locally ringed space along an open embedding to get another LRS), what we already have is that you can restrict a PresheafedSpace or a SheafedSpace.

[Scott Morrison]

See in particular https://github.com/leanprover-community/mathlib/blob/LRS/src/algebraic_geometry/sheafed_space.lean#L97, with no sorries.

[Scott Morrison]

However what we don't have yet is

def restrict_stalk_iso {U : Top} (X : PresheafedSpace C)
  (f : U ⟶ (X : Top.{v})) (h : open_embedding f) (x : U) :
  (X.restrict f h).stalk x ≅ X.stalk (f x) :=

[Scott Morrison]

This should not be hard: the correct way to do this is to define cofinal functors (easy), show that "open neighbourhoods of x within U" is cofinal inside "open neighbourhoods of x" (easy), and show that precomposing with a cofinal functor doesn't change the colimit (should not be hard, but hasn't been done yet, and requires looking at from the right angle before it's easy!)

[Scott Morrison]

This is also on my agenda, but I haven't made any start on it, so again if anyone would like to jump in and do any of those three steps (obviously the definition of cofinal functor comes first, but it's just a one-liner, in terms of src#category_theory.connected and src#category_theory.over) please do so!

[Adam Topaz]

I think the point is that an isomorphism of ringed spaces induces isomorphisms on stalks, and an isomorphism of local rings is a local morphism (since the unique maximal ideals are preserved). But schemes are not interesting. What is interesting are morphisms of schemes, and everything that Scott has said is necessary for this.

[Scott Morrison]

Hmm --- but maybe we should do this later?

[Adam Topaz]

So yes, a scheme is "just" a ringed space which is locally isomorphic to Spec, but you really do want an isomorphism of locally ringed spaces for all the actually interesting properties of schemes :smiling_face:️

[Scott Morrison]

So give the definition just asking for an isomorphism on each U to Spec R as a PresheafedSpace

[Scott Morrison]

and then give a theorem later that these isomorphisms are in fact automatically isomorphisms as LocallyRingedSpace?

[Adam Topaz]

That sounds reasonable!

[Scott Morrison]

This has the advantage also of slicing into smaller PRs. And I can get the one up to the definition of Scheme out the door quite quickly if I make this change.

[Scott Morrison]

and I guess it is what Kevin had in mind all along.

[Scott Morrison]

Actually, even for morphisms of schemes, why is what I've been talking about necessary?

[Adam Topaz]

For this you really do need to know that the maps on stalks are local morphisms.

[Adam Topaz]

E.g. it's necessary to prove the spec gamma adjunction

[Scott Morrison]

Yes, but that's in the definition of LocallyRingedSpace

[Scott Morrison]

there's nothing in the definition of morphisms that asks for compatibility with the cover by affines?

[Adam Topaz]

Could you link the definition of LocallyRingedSpace?

[Adam Topaz]

Yeah the category of schemes is a full subcategory of locally ringed spaces

[Scott Morrison]

https://github.com/leanprover-community/mathlib/blob/LRS/src/algebraic_geometry/locally_ringed_space.lean

[Adam Topaz]

Thanks :grinning_face_with_smiling_eyes:

[Scott Morrison]

The key line is https://github.com/leanprover-community/mathlib/blob/LRS/src/algebraic_geometry/locally_ringed_space.lean#L109

[Adam Topaz]

So yeah, as long as we can get schemes to be an object in this category, we should be fine

[Scott Morrison]

Okay, I'll rip out the sorries and make the PR, in that case!

[Adam Topaz]

And this boils down to proving the map we were discussing before is a ring isomorphism, and that is_local_ring is preserved under isomorphisms

[Adam Topaz]

The compatibility with affines for morphisms of schemes is "just" the statement that the global sections of the structure sheaf of Spec R is "just" R.

[Adam Topaz]

Oh, and the fact that the basic opens for affine schemes are a basis for the topology, which is just some simple commutative algebra

[Adam Topaz]

There's a notion of an affine morphism of schemes, which says additionally that the preimage of any affine open is again an affine open, but this is an additional property.

[Scott Morrison]

Okay! The branch#LRS has no sorries, and a definition of Scheme that I think is correct. :-)

[Scott Morrison]

I'll polish things a bit, but will make it a PR shortly.

[Adam Topaz]

Wait... is the isomorphism here https://github.com/leanprover-community/mathlib/blob/93f74f255d8788c7bfb9b714f5be76a8fb4cd1ce/src/algebraic_geometry/Scheme.lean#L27 an isomorphism of ringed spaces?

[Scott Morrison]

yes

[Scott Morrison]

an isomorphism in SheafedSpace CommRing.

[Adam Topaz]

Ah ok.

[Scott Morrison]

I will make that more obvious by replacing one of the _ with CommRing :-)

[Scott Morrison]

and add a comment while I'm at it!

[Scott Morrison]

added

/--
We define `Scheme` as a `X : LocallyRingedSpace`,
along with a proof that every point has an open neighbourhood `U`
so that that the restriction of `X` to `U` is isomorphic, as a space with a sheaf of commutative rings,
to `Spec.SheafedSpace R` for some `R : CommRing`.

(Note we're not asking in the definition that this is an isomorphism as locally ringed spaces,
although that is a consequence.)
-/

[Scott Morrison]

@Kevin Buzzard, #3961!

[Johan Commelin]

@Scott Morrison Thanks a lot!

[Johan Commelin]

We could even check the iso in *Pre*SheafedSpace CommRing

[Johan Commelin]

That's mathematically easier, but you might need to jump throught extra projections in Lean

[Scott Morrison]

it's not actually any easier, because SheafedSpace CommRing is a full subcategory of PresheafedSpace CommRing.

[Scott Morrison]

so in fact it's even definitionally the same

[Scott Morrison]

but I agree that it still might be conceptually easier :-)

[Scott Morrison]

it costs one additional projection

[Johan Commelin]

@Scott Morrison It is easier, because it means that to build a scheme you don't need to check any sheaf condition

[Scott Morrison]

oh...

[Scott Morrison]

but then we would not want to extend LocallyRingedSpace

[Scott Morrison]

perhaps it is better to leave the definition as is (perhaps in future make it even stronger!) but provide an alternative constructor that starts with just a PresheafedSpace CommRing, and the data for affine

[Johan Commelin]

Right... so my initial idea was to just build an extra constructor.

[Scott Morrison]

we need gluing of sheaves first! :-)

[Adam Topaz]

You do need to check the sheaf condition on the whole space X.

[Scott Morrison]

@Adam Topaz but the point is you know the sheaf condition on each affine (because it's Spec R, which satisfies the sheaf condition)

[Adam Topaz]

No, that doesn't follow.

[Scott Morrison]

oh...

[Scott Morrison]

indeed

[Adam Topaz]

E.g. take a disjoint union of specs

[Scott Morrison]

because we have nothing in the definition about the overlaps, which you would need for gluing

[Scott Morrison]

I see, so the best you could hope for is a constructor that takes a PresheafedSpace CommRing, and the data for affine, and some extra data about compatibility between the affines?

[Johan Commelin]

Ooops, I guess I messed up.

[Adam Topaz]

@Johan Commelin what you said originally is fine, it's the isomorphisms between the specs and the members of the open cover that can be iso's of presheaved spaces.

[Scott Morrison]

in any case, if anyone wants to pair-program attempt gluing of sheaves at some point, let me know :-)

[Johan Commelin]

I guess I should first review a bunch of PRs

[Johan Commelin]

@Scott Morrison could you have a look at #3907? The diff is way too large

[Scott Morrison]

Fixed

[Scott Morrison]

The linter report on #3961:

/- TYPES ARE MISSING INHABITED INSTANCES: -/
-- algebraic_geometry/Scheme.lean
#print algebraic_geometry.Scheme /- inhabited instance missing -/

-- algebraic_geometry/locally_ringed_space.lean
#print algebraic_geometry.LocallyRingedSpace /- inhabited instance missing -/

-- algebraic_geometry/sheafed_space.lean
#print algebraic_geometry.SheafedSpace /- inhabited instance missing -/

[Patrick Massot]

It has a point. You can't really say you defined Scheme if you don't have a single example.

[Scott Morrison]

I can make a stupid instance of SheafedSpace easily enough.

[Adam Topaz]

The empty scheme?

[Adam Topaz]

Aka Spec 0

[Patrick Massot]

I can't say we didn't use this trick for perfectoid spaces...

[Adam Topaz]

The default CommRing is the trivial ring right? So this actually "makes sense".

[Johan Commelin]

Does CommRing have a default instance? TIL

[Adam Topaz]

I mean inhabited.

[Scott Morrison]

Well, we don't yet know that Spec R is a scheme...

[Patrick Massot]

The real message is you can put @[nolint ...] but getting Spec R has a scheme will be really urgent.

[Adam Topaz]

The empty scheme should be fine, since the scheme condition is for all x in X, blah blah.

[Scott Morrison]

checking the sheaf condition is not as easy as it should be :-)

[Johan Commelin]

@Scott Morrison We have Spec_as_LRS (CommRing.of pempty)

[Johan Commelin]

@Adam Topaz @Damiano Testa If you are interested, Kevin seems to be live streaming a review of these PRs on Discord...

[Scott Morrison]

no, that relies on sorries, we only have Spec.SheafedSpace. But that will do!

[Johan Commelin]

@Scott Morrison So you can use that LRS, and check it is a scheme.

[Damiano Testa]

Johan Commelin said:

Scott Morrison We have Spec_as_LRS (CommRing.of pempty)

Thanks for the heads up!

[Johan Commelin]

Ooh, you are right!

[Scott Morrison]

so I just need prime_spectrum punit \equiv pempty

[Adam Topaz]

I just realized that I don't know how to use discord...

[Johan Commelin]

Oooh, that's just because you're too old :grinning_face_with_smiling_eyes: :rofl:

[Johan Commelin]

It's designed for 14 year old kids that are addicted to video gaming

[Adam Topaz]

Sounds about right.... and I think I've aged 20 years over the last 5 months...

[Johan Commelin]

But since Lean is just as addictive as a video game...

[Johan Commelin]

Adam Topaz said:

Sounds about right.... and I think I've aged 20 years over the last 5 months...

Ooof, you shouldn't do that too often

[Patrick Massot]

It is a video game. But we have progress to make on graphics.

[Scott Morrison]

yay, I have inhabited Scheme.

[Adam Topaz]

Is there a $\varnothing$ emoji? :wink:

[Patrick Massot]

Now you can make one, we are allowed custom emojis.

[Kevin Buzzard]

Johan Commelin said:

Adam Topaz Damiano Testa If you are interested, Kevin seems to be live streaming a review of these PRs on Discord...

Sorry, I got distracted by Sylow's theorems...

[Kevin Buzzard]

We shouldn't need that Spec(zero ring) = empty to prove that the empty scheme is a scheme, right?

[Reid Barton]

no, but you do need to do some work (even the empty space has a nontrivial covering family, namely the empty cover of the empty set)

[Johan Commelin]

The structure sheaf is now in mathlib

[Johan Commelin]

We should have the category of schemes this weekend!

[Patrick Massot]

That would be a really nice milestone!

[Patrick Massot]

Next step will be to port our definition of perfectoid spaces to mathlib...

[Kevin Buzzard]

This is certainly looking much closer to being feasible than a few weeks ago.

[Johan Commelin]

#3961 ... LGTM

[Scott Morrison]

Bryan had a few more comments, which I've just addressed.

[Bryan Gin-ge Chen]

Thanks! I just added one more tiny comment.

[Johan Commelin]

I hit the commit button on that tiny comment (-;

[Patrick Massot]

And I told bors what I think about all this.

[Johan Commelin]

https://github.com/leanprover-community/leanprover-community.github.io/pull/122
Please feel free to make this PR to the overview page more complete

[Bryan Gin-ge Chen]

(The build should pass after #3961 lands.)

[Patrick Massot]

I would prefer a top-level "Geometry" with bot the affine stuff, manifolds and algebraic geometry.

[Patrick Massot]

"Differentiable manifolds" in analysis is already very weird, putting schemes in general algebra may be even worse.

[Johan Commelin]

Ok, let's reorganise a bit

[Patrick Massot]

Could you do it Johan?

[Johan Commelin]

Yup, I just did @Patrick Massot

[Patrick Massot]

Could you fix it somehow ?

[Johan Commelin]

@Patrick Massot I think we should just rerun. Because schemes are now in mathlib

[Patrick Massot]

"Pull requests that have a failing status can’t be merged on a phone. "

[Bryan Gin-ge Chen]

Ah, I think we have to wait for the docs to build again since the site build uses the exported JSON from there.

[Johan Commelin]

@Bryan Gin-ge Chen Can we cheat and make it build faster on this day?

[Johan Commelin]

Or do we have to wait until the bot thinks it is time?

[Johan Commelin]

If we can have this go live in 15 minutes, then @Patrick Massot can demo this in his talk (-;

[Johan Commelin]

No pressure :stuck_out_tongue_wink:

[Bryan Gin-ge Chen]

Let me try re-running one of the doc build actions here: https://github.com/leanprover-community/doc-gen/actions

[Bryan Gin-ge Chen]

The docs seem to take a random amount of time between 5 and 20 minutes to build, so I'm not sure if we'll make it :sweat:

[Gabriel Ebner]

It sometimes also takes 10-20 minutes for github to update the docs website.

[Johan Commelin]

Well, I guess Patrick will have to see halfway his talk whether it's done or not (-;

[Gabriel Ebner]

You are too fast with restarting the CI.

[Bryan Gin-ge Chen]

Yeah, the doc build finished, but the website hasn't updated yet.

[Bryan Gin-ge Chen]

Oh, it looks like it should work now.

[Gabriel Ebner]

Yeah it built!!!

[Bryan Gin-ge Chen]

The new overview is live!

[Gabriel Ebner]

We did all the effort for... two words on this page?

[Bryan Gin-ge Chen]

It was reorganized so that there's a new section "Geometry", I think.

[Johan Commelin]

@Bryan Gin-ge Chen @Gabriel Ebner Thanks a lot!

[Johan Commelin]

@Patrick Massot good luck with your talk

[Patrick Massot]

You know what? I was running out of time and didn't have time to show the overview page... :blushing:

[Johan Commelin]

...

[Patrick Massot]

The order in the new section is a bit surprising, maybe we should go up and list things as "Affine and Euclidean geometry", "Algebraic geometry" and "Differential geometry".

[Kenny Lau]

rss-bot said:

feat(algebraic_geometry/*): Gamma the global sections functor (#4126)
feat(algebraic_geometry/*): Gamma the global sections functor (#4126)
https://github.com/leanprover-community/mathlib/commit/5d35e626086c4e1639e49cd7cf574bc48592f554

[Ramon Fernandez Mir]

Hey, it's been a while. So happy to see that schemes are finally in mathlib and done properly, using the category theory library.

[Ramon Fernandez Mir]

Is anyone working on making Spec a functor? Was thinking of giving it a go

[Johan Commelin]

I don't think anyone is actively working on it atm

[Johan Commelin]

@Ramon Fernandez Mir Also, welcome back!

[Scott Morrison]

Fantastic!

[Scott Morrison]

I've been gearing up to prove that morphisms of sheaves are epi/mono/iso iff they are stalkwise, on the way to doing sheafification properly, but there's been a bit of hiatus in the progress.

[Scott Morrison]

I also proved a while back that filtered colimits commute with finite limits, and wanted to use this to show that the forgetful functors (in particular, from CommRing to Type) preserved stalks, but again I have stalled on this for a while.

[Scott Morrison]

We do now have cofinal functors, although I don't think I got around to stating that open neighbourhoods of x within U were cofinal in open nhds of x.

[Scott Morrison]

This is probably essential somewhere soon. :-)

[Kevin Buzzard]

I might try some of the exercises in chapter 2 of Hartshorne when my course is done (1 week to go) but we need sheafification of presheaves of abelian groups to state a lot of them

[Justus Springer]

I take the liberty to revive this thread: I'm currently working on the adjunction between Spec and Gamma, following the approach in the stacks project here. I realized that in order to prove this lemma, I need a version of docs#Top.presheaf.germ_exist for CommRing-valued sheaves. For that, it would suffice to know that the forgetful functor of CommRing preserves stalks (or more generally, filtered colimits). Have you ever gotten around to prove this @Scott Morrison ? If not, I could try to adopt this project if that's okay. Is the code on branch#preserves_filtered_colimits the latest attempt? Any advice on how to continue from here would be helpful!

[Scott Morrison]

Sorry, I didn't make further progress.