affine schemes are schemes

Stream: maths

[Kevin Buzzard]

I just reached a milestone:

[Kevin Buzzard]

noncomputable definition scheme_of_affine_scheme (R : Type u) [comm_ring R] : scheme := [definition which typechecks]

[Kevin Buzzard]

This was a very surprising process.

[Kevin Buzzard]

Several times over the last few months I have confidently felt that I was "just a few hours' work away" from this result

[Kevin Buzzard]

and then I would run into a "trivial to a mathematician, not so trivial in dependent type theory" type issue

[Kevin Buzzard]

The most recent was last night, where I had to write down a map F U -> F (id '' U) (here U : set X)

[Kevin Buzzard]

and I foolishly rewrote id '' U to U and used the identity map and ran into all sorts of problems

[Kevin Buzzard]

but this time I was ready for it -- I changed it to a more general construction which gave a map F U -> F V for any V \sub U and applied it in this case.

[Kevin Buzzard]

There is a subtlety happening here which I am not entirely sure I 100% understand.

[Kevin Buzzard]

I think it might be to do with an equivalence of categories

[Kevin Buzzard]

A mathematician takes a topological space X and then defines a presheaf of abelian groups on X to be, for every open set U in X an abelian group F U

[Kevin Buzzard]

and for every pair of opens V in U, a restriction map F U -> F V

[Kevin Buzzard]

[the model is that F U is the set of "functions on U", so this restriction map is restriction of functions]

[Kevin Buzzard]

and this pair F,res has to satisfy two axioms: res : F U -> F U is the identity

[Kevin Buzzard]

and if W in V in U the two maps F U -> F W (res, and res circ res) are the same

[Kevin Buzzard]

And then an algebraic geometry textbook might then say "here's a cool way of looking at this: let's make the set of open subsets of X into a category -- the objects are the opens and there's one morphism from U to V iff V is a subset of U, and then the axioms for a presheaf are just the statement that F is a functor"

[Kevin Buzzard]

but somehow this is just a language, this particular fact that something is a functor is never really used in any deep way

[Kevin Buzzard]

there are plenty of functors around like global sections functors which really do play a role, with derived functors etc etc, but this is not one of them.

[Kevin Buzzard]

In dependent type theory, I think there is something deeper going on.

[Kevin Buzzard]

The "category of open sets" is somehow replaced by a much more complex category, the category of terms each of which can be proved to be an open set

[Kenny Lau]

but there is only countably many terms!

[Kevin Buzzard]

and there's a morphism t1 -> t2 precisely when there's a proof that the open set corresponding to t2 is a subset of the open set corresponding to t1

[Kevin Buzzard]

I don't care

[Kevin Buzzard]

I don't think I care

[Kevin Buzzard]

Maybe I haven't got the language right

[Kevin Buzzard]

I am happy that if I have a term and a proof that it is an open set then it's in

[Kevin Buzzard]

and the term might be U and the proof might be sorry

[Kevin Buzzard]

and that pretty much covers everything

[Kevin Buzzard]

So in some sense I did not even realise when I defined a presheaf that I was defining it on this much bigger category

[Kevin Buzzard]

but because the two categories are equivalent it doesn't matter mathematically

[Kevin Buzzard]

but a consequence of this incorrect mindset was that I often wanted to identify things like F ((U cap V) cap W) and F(U cap (V cap W)) as _equal_

[Kevin Buzzard]

because to a mathematician they are equal

[Kevin Buzzard]

but in dependent type theory they are just canonically isomorphic

[Johan Commelin]

Isn't this another instance of "we really need transport of structure"?

[Chris Hughes]

No they're equal?

[Kevin Buzzard]

and the correct way to move between them is via the restriction map associated to the proof that the sets are equal

[Kevin Buzzard]

Chris, perhaps they really are equal, but by equal here I think I mean defeq

[Kevin Buzzard]

Johan -- in this case I am suggesting another approach

[Johan Commelin]

I know, but it means that you are becoming more of a CS guy...

[Mario Carneiro]

Here you actually have transport of structure, because eq.rec asserts that everything you can express commutes with equality

[Kevin Buzzard]

"transport of structure" in this situation seems to be some sort of brute force collapsing of the bigger category into the equivalent smaller one

[Johan Commelin]

That brute force is exactly what we need, if we ever hope to get up to speed with formalising maths

[Kevin Buzzard]

The eq.rec remark is true, however

[Mario Carneiro]

but that doesn't mean the transport is easy to use without a lot of lemmas

[Kevin Buzzard]

in practice, because I was dealing with complicated things on top of all this

[Kevin Buzzard]

eq.rec did not suffice to solve all my problems.

[Kevin Buzzard]

If I had some complex term with id '' U in

[Kevin Buzzard]

and all of a sudden I thought "crap, my life would be much easier if that term was just U`

[Kevin Buzzard]

then sometimes I would try and rewrite and the rewrite would fail

[Kevin Buzzard]

or it would be a PITA to formulate

[Kevin Buzzard]

because the naively written rewrite was not type correct

[Kevin Buzzard]

because H used to be proof of V subset (id '' U) and that needed rewriting as swell

[Kevin Buzzard]

and congr was not good enough at this sort of thing

[Kevin Buzzard]

and subst was not either

[Kevin Buzzard]

sorry, subst, not congr

[Kenny Lau]

@Kevin Buzzard have you pushed?

[Mario Carneiro]

the eq.rec term itself acts as a function F U -> F (id '' U), and then you need to know this is functorial for later stuff

[Kevin Buzzard]

In this particular case all my problems went away when I started thinking about the equivalent category

[Kevin Buzzard]

Kenny, I just pushed

[Mario Carneiro]

and this is true, but more complicated to prove; and you may need that proof to be functorial and it gets yet more complicated...

[Mario Carneiro]

this is what HoTT people deal with

[Kevin Buzzard]

Mario -- I'm sure you're right

[Kevin Buzzard]

This certainly sounds like the sort of issue which we have to deal with here

[Kevin Buzzard]

And to be quite frank I did feel like I had dodged a bullet

[Kevin Buzzard]

When I realised I couldn't use id, I knew things might be bad

[Mario Carneiro]

At the same time, you have already a robust language of restriction maps that you already know are functorial, because they are the object of study

[Kevin Buzzard]

when I realised I could use res, I had some hope

[Mario Carneiro]

the choice is obvious

[Kevin Buzzard]

and then when gigantic one-page-long goals started yielding to refl I realised I'd had the right insight

[Kevin Buzzard]

the choice is obvious

To you

[Kevin Buzzard]

I would argue that the choice is not at all obvious to a practicing algebraic geometer trained in ZFC

[Kevin Buzzard]

and in some sense this is a problem

[Kevin Buzzard]

because it means that we are teaching people in slightly the wrong way

[Mario Carneiro]

The important part is to recognize the issue itself

[Kevin Buzzard]

As is so often the case (I have seen this time and time again in mathematics)

[Kevin Buzzard]

the insight came to me ten minutes after I'd spent an hour being stuck and whining here about how stupid Lean was, and then turned off my laptop and thought about something else

[Kevin Buzzard]

but I could _envisage_ situations where that bullet cannot be dodged and you have to take the hit and transport your structures

[Andrew Ashworth]

Did you get any insights with the ALEXANDRIA / Peter Koepke lecture person today?

[Kenny Lau]

I reached another milestone:

[Kenny Lau]

definition scheme_of_affine_scheme (R : Type u) [comm_ring R] : scheme := [definition which typechecks]

[Kenny Lau]

@Kevin Buzzard

[Kenny Lau]

So an affine scheme is one that is isomorphic to Spec(A) for some ring A

[Kenny Lau]

my question is: how important is that ring A?

[Johan Commelin]

What do you mean? Whether you should carry A around?

[Johan Commelin]

In maths it is not important at all. Only the fact that it exists

[Kenny Lau]

I see

[Patrick Massot]

I don't understand that question. You can recover A from its affine scheme, is that what you want to know?

[Kenny Lau]

oh really

[Kenny Lau]

is it just the global section?

[Kenny Lau]

now a scheme is covered by affine schemes. Are the affine schemes important?

[Johan Commelin]

Nope

[Johan Commelin]

Only the existence

[Kenny Lau]

interesting

[Johan Commelin]

is it just the global section?

Yes, up to isomorphism

[Patrick Massot]

Sure, global sections of the structure sheaf gives you back A

[Patrick Massot]

Too late

[Johan Commelin]

@Kenny Lau This what the Gamma-Spec adjunction is all about

[Johan Commelin]

So, if you feel like writing an interface for schemes (-;

[Johan Commelin]

That is what would be the first challenge

[Patrick Massot]

https://stacks.math.columbia.edu/tag/01I2

[Patrick Massot]

Oh! The new Stacks project website went live!

[Kevin Buzzard]

indeed

[Patrick Massot]

Kevin, will you come to http://www.ihes.fr/~abbes/Gabber/gabber60-programme.html?

[Kevin Buzzard]

I wasn't planning on it. I just have too much on at the minute.

[Kenny Lau]

@Kevin Buzzard why are you using the broken definition of basis in 009I?

[Kenny Lau]

instance presheaf_on_basis_stalk.setoid  :
   setoid (presheaf_on_basis_stalk.aux) :=
{ r := λ Us Vt, ∃ (W : set X) (Hx : x ∈ W) (BW : W ∈ B) (HWU : W ⊆ Us.U) (HWV : W ⊆ Vt.U),
   FPTB.res Us.BU BW HWU Us.s = FPTB.res Vt.BU BW HWV Vt.s,

[Kenny Lau]

@Kevin Buzzard do you think we can change this definition to saying that they agree in the intersection?

[Kenny Lau]

oh no, we can't

[Kevin Buzzard]

It was a real annoyance that the intersection of two basis elements was not a basis element

[Kevin Buzzard]

I proved several results under two additional hypotheses:

[Kevin Buzzard]

1) intersection of two basis elements was a basis element

[Kevin Buzzard]

2) intersection of no basis elemnts was a basis element

[Kevin Buzzard]

Both of these are true for the D_f basis of Spec(R)

[Kevin Buzzard]

So in some cases I actually cut corners

[Kevin Buzzard]

Kenny if you are sufficiently fanatical to go through those proofs and actually prove the correct statements then feel free

[Kevin Buzzard]

Even the definition of a sheaf got so much more complicated when working with a basis not closed under intersection

[Kevin Buzzard]

You have to check that the two functions are equal on the intersection by covering each intersection with new basis elements and checking that the res's coincide

[Kevin Buzzard]

I just couldn't be bothered

[Kevin Buzzard]

cf https://stacks.math.columbia.edu/tag/009L

[Kevin Buzzard]

That's the tag I did

[Kevin Buzzard]

not the one before