Zulip Chat Archive

Stream: maths

Topic: affine schemes are schemes


view this post on Zulip Kevin Buzzard (May 23 2018 at 07:01):

I just reached a milestone:

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:01):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:02):

This was a very surprising process.

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:02):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:02):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:03):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:04):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:05):

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.

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:05):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:05):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:06):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:07):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:07):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:08):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:08):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:10):

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"

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:11):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:11):

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.

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:11):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:12):

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

view this post on Zulip Kenny Lau (May 23 2018 at 07:12):

but there is only countably many terms!

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:13):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:13):

I don't care

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:13):

I don't think I care

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:13):

Maybe I haven't got the language right

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:14):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:14):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:14):

and that pretty much covers everything

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:14):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:15):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:15):

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_

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:15):

because to a mathematician they are equal

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:16):

but in dependent type theory they are just canonically isomorphic

view this post on Zulip Johan Commelin (May 23 2018 at 07:16):

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

view this post on Zulip Chris Hughes (May 23 2018 at 07:16):

No they're equal?

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:16):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:17):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:17):

Johan -- in this case I am suggesting another approach

view this post on Zulip Johan Commelin (May 23 2018 at 07:17):

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

view this post on Zulip Mario Carneiro (May 23 2018 at 07:17):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:17):

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

view this post on Zulip Johan Commelin (May 23 2018 at 07:18):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:18):

The eq.rec remark is true, however

view this post on Zulip Mario Carneiro (May 23 2018 at 07:18):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:18):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:19):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:19):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:19):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:19):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:19):

or it would be a PITA to formulate

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:19):

because the naively written rewrite was not type correct

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:20):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:20):

and congr was not good enough at this sort of thing

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:20):

and subst was not either

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:20):

sorry, subst, not congr

view this post on Zulip Kenny Lau (May 23 2018 at 07:21):

@Kevin Buzzard have you pushed?

view this post on Zulip Mario Carneiro (May 23 2018 at 07:21):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:21):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:22):

Kenny, I just pushed

view this post on Zulip Mario Carneiro (May 23 2018 at 07:22):

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

view this post on Zulip Mario Carneiro (May 23 2018 at 07:22):

this is what HoTT people deal with

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:22):

Mario -- I'm sure you're right

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:22):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:22):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:23):

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

view this post on Zulip Mario Carneiro (May 23 2018 at 07:23):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:23):

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

view this post on Zulip Mario Carneiro (May 23 2018 at 07:23):

the choice is obvious

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:23):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:23):

the choice is obvious

To you

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:24):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:24):

and in some sense this is a problem

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:24):

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

view this post on Zulip Mario Carneiro (May 23 2018 at 07:24):

The important part is to recognize the issue itself

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:25):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:25):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 07:26):

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

view this post on Zulip Andrew Ashworth (May 23 2018 at 07:26):

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

view this post on Zulip Kenny Lau (May 23 2018 at 09:11):

I reached another milestone:

view this post on Zulip Kenny Lau (May 23 2018 at 09:11):

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

view this post on Zulip Kenny Lau (May 23 2018 at 09:13):

@Kevin Buzzard

view this post on Zulip Kenny Lau (May 23 2018 at 09:37):

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

view this post on Zulip Kenny Lau (May 23 2018 at 09:37):

my question is: how important is that ring A?

view this post on Zulip Johan Commelin (May 23 2018 at 09:42):

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

view this post on Zulip Johan Commelin (May 23 2018 at 09:42):

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

view this post on Zulip Kenny Lau (May 23 2018 at 09:43):

I see

view this post on Zulip Patrick Massot (May 23 2018 at 09:43):

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

view this post on Zulip Kenny Lau (May 23 2018 at 09:43):

oh really

view this post on Zulip Kenny Lau (May 23 2018 at 09:43):

is it just the global section?

view this post on Zulip Kenny Lau (May 23 2018 at 09:45):

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

view this post on Zulip Johan Commelin (May 23 2018 at 09:46):

Nope

view this post on Zulip Johan Commelin (May 23 2018 at 09:46):

Only the existence

view this post on Zulip Kenny Lau (May 23 2018 at 09:46):

interesting

view this post on Zulip Johan Commelin (May 23 2018 at 09:46):

is it just the global section?

Yes, up to isomorphism

view this post on Zulip Patrick Massot (May 23 2018 at 09:46):

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

view this post on Zulip Patrick Massot (May 23 2018 at 09:46):

Too late

view this post on Zulip Johan Commelin (May 23 2018 at 09:47):

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

view this post on Zulip Johan Commelin (May 23 2018 at 09:47):

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

view this post on Zulip Johan Commelin (May 23 2018 at 09:47):

That is what would be the first challenge

view this post on Zulip Patrick Massot (May 23 2018 at 09:48):

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

view this post on Zulip Patrick Massot (May 23 2018 at 09:49):

Oh! The new Stacks project website went live!

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:53):

indeed

view this post on Zulip Patrick Massot (May 23 2018 at 10:04):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 10:07):

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

view this post on Zulip Kenny Lau (May 28 2018 at 11:24):

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

view this post on Zulip Kenny Lau (May 28 2018 at 11:35):

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,

view this post on Zulip Kenny Lau (May 28 2018 at 11:35):

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

view this post on Zulip Kenny Lau (May 28 2018 at 11:35):

oh no, we can't

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:56):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:57):

I proved several results under two additional hypotheses:

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:57):

1) intersection of two basis elements was a basis element

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:57):

2) intersection of no basis elemnts was a basis element

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:57):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:57):

So in some cases I actually cut corners

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:58):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:58):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:58):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:59):

I just couldn't be bothered

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:03):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:04):

That's the tag I did

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:04):

not the one before


Last updated: May 12 2021 at 07:17 UTC