Stream: maths

Topic: affine schemes are schemes

Kevin Buzzard (May 23 2018 at 07:01):

I just reached a milestone:

Kevin Buzzard (May 23 2018 at 07:01):

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

Kevin Buzzard (May 23 2018 at 07:02):

This was a very surprising process.

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

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

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)

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

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.

Kevin Buzzard (May 23 2018 at 07:05):

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

Kevin Buzzard (May 23 2018 at 07:05):

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

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

Kevin Buzzard (May 23 2018 at 07:07):

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

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]

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

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

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"

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

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.

Kevin Buzzard (May 23 2018 at 07:11):

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

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

Kenny Lau (May 23 2018 at 07:12):

but there is only countably many terms!

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

I don't care

Kevin Buzzard (May 23 2018 at 07:13):

I don't think I care

Kevin Buzzard (May 23 2018 at 07:13):

Maybe I haven't got the language right

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

Kevin Buzzard (May 23 2018 at 07:14):

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

Kevin Buzzard (May 23 2018 at 07:14):

and that pretty much covers everything

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

Kevin Buzzard (May 23 2018 at 07:15):

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

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_

Kevin Buzzard (May 23 2018 at 07:15):

because to a mathematician they are equal

Kevin Buzzard (May 23 2018 at 07:16):

but in dependent type theory they are just canonically isomorphic

Johan Commelin (May 23 2018 at 07:16):

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

Chris Hughes (May 23 2018 at 07:16):

No they're equal?

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

Kevin Buzzard (May 23 2018 at 07:17):

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

Kevin Buzzard (May 23 2018 at 07:17):

Johan -- in this case I am suggesting another approach

Johan Commelin (May 23 2018 at 07:17):

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

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

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

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

Kevin Buzzard (May 23 2018 at 07:18):

The eq.rec remark is true, however

Mario Carneiro (May 23 2018 at 07:18):

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

Kevin Buzzard (May 23 2018 at 07:18):

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

Kevin Buzzard (May 23 2018 at 07:19):

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

Kevin Buzzard (May 23 2018 at 07:19):

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

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

Kevin Buzzard (May 23 2018 at 07:19):

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

Kevin Buzzard (May 23 2018 at 07:19):

or it would be a PITA to formulate

Kevin Buzzard (May 23 2018 at 07:19):

because the naively written rewrite was not type correct

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

Kevin Buzzard (May 23 2018 at 07:20):

and congr was not good enough at this sort of thing

Kevin Buzzard (May 23 2018 at 07:20):

and subst was not either

Kevin Buzzard (May 23 2018 at 07:20):

sorry, subst, not congr

Kenny Lau (May 23 2018 at 07:21):

@Kevin Buzzard have you pushed?

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

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

Kevin Buzzard (May 23 2018 at 07:22):

Kenny, I just pushed

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...

Mario Carneiro (May 23 2018 at 07:22):

this is what HoTT people deal with

Kevin Buzzard (May 23 2018 at 07:22):

Mario -- I'm sure you're right

Kevin Buzzard (May 23 2018 at 07:22):

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

Kevin Buzzard (May 23 2018 at 07:22):

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

Kevin Buzzard (May 23 2018 at 07:23):

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

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

Kevin Buzzard (May 23 2018 at 07:23):

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

Mario Carneiro (May 23 2018 at 07:23):

the choice is obvious

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

Kevin Buzzard (May 23 2018 at 07:23):

the choice is obvious

To you

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

Kevin Buzzard (May 23 2018 at 07:24):

and in some sense this is a problem

Kevin Buzzard (May 23 2018 at 07:24):

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

Mario Carneiro (May 23 2018 at 07:24):

The important part is to recognize the issue itself

Kevin Buzzard (May 23 2018 at 07:25):

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

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

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

Andrew Ashworth (May 23 2018 at 07:26):

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

Kenny Lau (May 23 2018 at 09:11):

I reached another milestone:

Kenny Lau (May 23 2018 at 09:11):

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

@Kevin Buzzard

Kenny Lau (May 23 2018 at 09:37):

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

Kenny Lau (May 23 2018 at 09:37):

my question is: how important is that ring A?

Johan Commelin (May 23 2018 at 09:42):

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

Johan Commelin (May 23 2018 at 09:42):

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

I see

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?

oh really

Kenny Lau (May 23 2018 at 09:43):

is it just the global section?

Kenny Lau (May 23 2018 at 09:45):

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

Nope

Johan Commelin (May 23 2018 at 09:46):

Only the existence

interesting

Johan Commelin (May 23 2018 at 09:46):

is it just the global section?

Yes, up to isomorphism

Patrick Massot (May 23 2018 at 09:46):

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

Too late

Johan Commelin (May 23 2018 at 09:47):

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

Johan Commelin (May 23 2018 at 09:47):

That is what would be the first challenge

Patrick Massot (May 23 2018 at 09:48):

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

Patrick Massot (May 23 2018 at 09:49):

Oh! The new Stacks project website went live!

indeed

Patrick Massot (May 23 2018 at 10:04):

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

Kevin Buzzard (May 23 2018 at 10:07):

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

Kenny Lau (May 28 2018 at 11:24):

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

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,
`

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?

oh no, we can't

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

Kevin Buzzard (May 28 2018 at 11:57):

I proved several results under two additional hypotheses:

Kevin Buzzard (May 28 2018 at 11:57):

1) intersection of two basis elements was a basis element

Kevin Buzzard (May 28 2018 at 11:57):

2) intersection of no basis elemnts was a basis element

Kevin Buzzard (May 28 2018 at 11:57):

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

Kevin Buzzard (May 28 2018 at 11:57):

So in some cases I actually cut corners

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

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

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

Kevin Buzzard (May 28 2018 at 11:59):

I just couldn't be bothered

Kevin Buzzard (May 28 2018 at 12:04):

That's the tag I did

Kevin Buzzard (May 28 2018 at 12:04):

not the one before

Last updated: May 12 2021 at 07:17 UTC