Zulip Chat Archive

Stream: maths

Topic: Schemes in Isabelle/HOL


view this post on Zulip Oliver Nash (Apr 20 2021 at 10:25):

I haven't finished reading this yet but this is good food for thought: https://arxiv.org/abs/2104.09366

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 10:30):

It's great to see this stuff happening in the other theorem provers -- especially Isabelle/HOL with its weaker logic (I was not at all convinced that this was even possible, and in some sense they'll still have to do more to convince me that it's usable, but this is a fabulous start). I would be in some sense less interested in seeing a Coq formalisation, because Coq's type theory is very close to Lean's so I am very confident that defining schemes in Coq would be possible. But I would also be very interested to see a formalisation in a HoTT prover, because for a while the HoTT people had convinced me that the problems we ran into with our initial approach would all be solved by HoTT, and it is only more recently that I decided that I'd had the wool pulled over my eyes (details: in HoTT R[1/fg]=R[1/f][1/g] so the issues we had with our original 2018 approach in Lean (we only had an isomorphism) look like they might not be there -- however after rewriting along this equality I realised that one still has to do the diagram chase! You now have two maps from some localisation to another and HoTT doesn't say that they're equal, so one still has to do the work which Kenny, Chris and I did)

view this post on Zulip Oliver Nash (Apr 20 2021 at 10:42):

I too would be most interested to see this done in HoTT. The fact that R[1/fg] = R[1/f][1/g] (or depending on foundations) is, I guess, a minor mathematical result so I don't blame HoTT if I still have a diagram to chase. Maybe HoTT sets me up more conveniently to discharge this proof obligation, or maybe the opposite? I don't know!

view this post on Zulip Oliver Nash (Apr 20 2021 at 10:44):

Despite remaining convinced that Lean is the way forward, I salute this work in Isabelle. It will be very interesting to see how we both scale. I think we're lucky to have something against which we can compare.

view this post on Zulip Joachim Hauge (Apr 20 2021 at 10:48):

Kevin Buzzard said:

It's great to see this stuff happening in the other theorem provers -- especially Isabelle/HOL with its weaker logic (I was not at all convinced that this was even possible, and in some sense they'll still have to do more to convince me that it's usable, but this is a fabulous start). I would be in some sense less interested in seeing a Coq formalisation, because Coq's type theory is very close to Lean's so I am very confident that defining schemes in Coq would be possible. But I would also be very interested to see a formalisation in a HoTT prover, because for a while the HoTT people had convinced me that the problems we ran into with our initial approach would all be solved by HoTT, and it is only more recently that I decided that I'd had the wool pulled over my eyes (details: in HoTT R[1/fg]=R[1/f][1/g] so the issues we had with our original 2018 approach in Lean (we only had an isomorphism) look like they might not be there -- however after rewriting along this equality I realised that one still has to do the diagram chase! You now have two maps from some localisation to another and HoTT doesn't say that they're equal, so one still has to do the work which Kenny, Chris and I did)

That HoTT pitch kind of sounded suspicious because how could they have non-isomorphic line bundles for example if everything is equal?

view this post on Zulip Scott Morrison (Apr 20 2021 at 10:48):

Great to see that we provoked them into doing this in Isabelle/HOL! :-)

view this post on Zulip Scott Morrison (Apr 20 2021 at 10:55):

I'd love to hear any of our local experts who also know Isabelle/HOL give any comments they have on this paper.

view this post on Zulip Scott Morrison (Apr 20 2021 at 10:57):

One thing that struck me was

We seized the opportunity of formalizing schemes to build a new topology library
despite the two existing formalizations of topology in Isabelle/HOL

view this post on Zulip Scott Morrison (Apr 20 2021 at 11:00):

Similarly they built off an experimental algebra library. In both cases this was driven by their desire to use "locales".

view this post on Zulip Gabriel Ebner (Apr 20 2021 at 11:06):

AFAICT locale is as mundane in Isabelle/HOL as structure is in Lean.

view this post on Zulip Johan Commelin (Apr 20 2021 at 11:32):

@Gabriel Ebner I'm confused by that comment. I guess here "locale" is being used in the mathematical sense of the word, as some sort of variation on topological space. Not in the sense of open_locale and other keywords, etc...

view this post on Zulip Johan Commelin (Apr 20 2021 at 11:33):

@Joachim Hauge Who said everything is equal in HoTT? Only isomorphic things are equal.

view this post on Zulip Sebastien Gouezel (Apr 20 2021 at 11:36):

Yes, a locale in Isabelle is a mechanism to put together a bunch of different assumptions/results in one framework. You can instantiate a locale in a proof, by showing that some objects satisfy the assumptions in this locale, and then all the results of the locale become available.

view this post on Zulip Johan Commelin (Apr 20 2021 at 11:37):

Aha, so I misunderstood what they are doing with locales. It's not the intuitionistic variant on topological spaces that they are talking about.

view this post on Zulip Sebastien Gouezel (Apr 20 2021 at 11:38):

Their desire to build a new topological space theory in Isabelle is certainly due to the fact that they can not use typeclasses. For instance, fibers of a topological vector bundle would not be types in Isabelle (as there are no dependent types), so instead you would see them as subsets of the total space of the fiber bundle, and then you want to talk about the topology on this subset. You can not use a typeclass here, so you have to rebuild everything from scratch in a different language. And locales probably give the right abstraction to be able to do this in a mildly convenient way.

view this post on Zulip Sebastien Gouezel (Apr 20 2021 at 11:40):

(I say mildly because, if you open the formalization, you will see that everything is very verbose since you can not rely on the system to infer the topology for you, so you have to provide it by hand in all statements).

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:06):

Now we need to raise the bar. In some sense we have less about schemes now than in 2019 because after Ramon's thesis Kenny did a bunch of stuff like gluing sheaves and Gamma Spec adjointness all of which needs to be redone because we changed the definition again (to something different -- we changed our definition of the structure sheaf from Stacks to Hartshorne which makes some things easier and some more difficult). There are plenty of interesting mini projects here but in some sense you can argue that Isabelle/HOL caught up with us right now.

Accessible future Lean projects:

1) isomorphism between R and global sections of Spec(R)
2) global sections (ideally on category of locally ringed spaces) are adjoint to Spec
3) Hartshorne exercise which glues sheaves on a top space
4) existence of pullback squares in the category of schemes
5) definition of affine morphisms, finite presentation morphisms, smooth morphisms, flat morphisms, étale morphisms... (all relatively easy in some sense because you just mindlessly copy the definition from a book), but...
6) basic API for these notions. Specific example: prove that if X->Y is affine in the weak sense that there's an open cover of Y by affines whose preimage is affine, then it's affine in the strong sense that the preimage of every open affine is affine.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:06):

Then we challenge mathematicians to do the same in Isabelle/HOL and see if we can get any more algebraic geometers involved

view this post on Zulip Joachim Hauge (Apr 20 2021 at 12:42):

Johan Commelin said:

Joachim Hauge Who said everything is equal in HoTT? Only isomorphic things are equal.

Sure but then the fibers of the line bundles are all equal but since it's possible to be equal in homotopically different ways this is not much better than any other type theory with decidable type checking. Thus bringing in question how it could help with Buzzard's complaint.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:49):

HoTT's concept of equality is very different to Lean's, and in my experience very different to that of the generic mathematician. I'm not saying that's a bad thing, but it's just something to remember. Nowadays my mental model of HoTT is that it's Lean but with a more powerful rewrite command that rewrites along isomorphisms, and they happen to use the notation = for what we call \cong.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:51):

So we know NZ\mathbb{N}\cong\mathbb{Z} and they write this as N=Z\mathbb{N}=\Z but big deal, they're not really equal in any useful sense, they just biject with each other. If you have a Diophantine equation about naturals then you can use their rw to turn it into what looks like a Diophantine equation over integers, but it's integers with a completely wacky + and * inherited from the naturals via the bijection you chose to rewrite along (different bijections give you different goals, of course, even though they all look identical)

view this post on Zulip Eric Rodriguez (Apr 20 2021 at 12:51):

why does that not cause problems with things that are unique up to isomorphism, but not up to unique isomorphism?

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:51):

Because = doesn't mean =

view this post on Zulip Eric Rodriguez (Apr 20 2021 at 12:52):

that's some insanity, the ℕ ℤ stuff

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:52):

We have things which are unique up to non-unique isomorphism and we're not bothered by this because for us \cong is data, it involves the choice of an isomorphism. In HoTT = is also data, things can be equal in more than one way, so it's just \cong in disguise.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:53):

It's a theorem in Lean that if h1 : a = b and h2 : a = b then h1 = h2 because "all proofs are equal". In HoTT this can fail. But in Lean we can have i:XYi:X\cong Y and j:XYj:X\cong Y with iji\not=j as well.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:54):

We just have a cool extra thing which they don't have, called proof-irrelevant equality.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:54):

And they have a cool extra thing which we don't have, called rewriting along isomorphisms.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:54):

And they can probably make our thing in some way, and we can make their thing in some way using tactics

view this post on Zulip Gabriel Ebner (Apr 20 2021 at 12:55):

Is rewriting along isomorphisms any better than equiv_rw + suitable simp lemmas for the equivs?

view this post on Zulip Johan Commelin (Apr 20 2021 at 12:56):

Well yes, because to make equiv_rw work, you need to do quite a lot of things. In HoTT it's "for free".

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:56):

I would be interested to hear from people who actually know what they're talking about (oh there's someone now) if they could say anything which my "model" of HoTT is missing, i.e. some extra useful functionality they have which my model doesn't make clear.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:58):

My feeling right now is that it's a bit like these "axiom schemes" they have in ZFC. You get something which isn't an axiom, but in fact a family of axioms, one for e.g. each mathematical statement which has some property. In another system you could imagine that this would be one axiom, but in ZFC it's an infinite family of axioms. It feels like the same here -- we have to prove infinitely many theorems, but they're of a similar form so ultimately if we need them we'll write a tactic to do it (and right now we've not really needed them, and have proved special cases by hand ourselves like "if X and Y are isomorphic topological spaces and X is compact then Y is compact", an example which is subject to the Mario counter anyway).

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 12:59):

[Mario observes that in an API for compact top spaces you want the result that if X surjects onto Y and X is compact then Y is compact, and the fact that compactness travels along isomorphisms is an easy consequence]

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 13:01):

My counter to the Mario counter was local rings. If A and B are isomorphic commutative rings and A is local, then B is local, and we will have to prove that as a lemma because it is not true that if A surjects onto B and A is local then B is local; indeed being local means "has a unique maximal ideal" so if B is the zero ring then it has too few maximal ideals so it's not local. However recently I discovered a fix for this! Say a ring is prelocal if it has at most 1 maximal ideal. Then a homomorphic image of a prelocal ring is prelocal, so you can get the result that locality travels along isomorphisms from the fact that nonzeroness travels along isomorphisms, which is easy.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 13:15):

The above arguments are perhaps an indication that for the kind of maths we're doing, you can see that we can get away with not rewriting along isomorphisms and still go a long way. Anyway, back to Isabelle:

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 13:20):

The reason that my mental model of Isabelle said "schemes is impossible" is the following, and perhaps an Isabelle whizz can explain to me my mistake. The sheaf of rings on X, X a scheme, is the data of, for each U, a ring O(U). So it's a function from the open subsets of X to...something which Isabelle doesn't have (the category of rings). I can believe that one can use trickery to make some kind of object in HOL which in some way corresponds to this gadget, in the sense that it contains the same data as the gadget, perhaps packaged up in a clever way. However what was not at all clear to me was that one could now use Isabelle's type class system to say "O(U) is a ring for every U".

Oh -- a really important thing to add to my list of future work is sheaves of O-modules. This is again a fundamental construction in algebraic geometry -- a "continuously varying" family of modules M(U), with M(U) a module for O(U). We don't have these so I can't crow about it on Twitter, and the last time we talked about it we ended up in some category theory rabbithole from which I never emerged. Here is the definition of Picard group of a scheme which I want to give: take the monoid whose objects are isomorphism classes of sheaves of O-modules, with monoid law tensor product; the Picard group is the units of this monoid. In Lean if we define it like this we'll have universe issues. What issues will they have in Isabelle/HOL?

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 13:20):

If X : Type u then we'll get Pic X : Type (u+1) :-)

view this post on Zulip Sebastien Gouezel (Apr 20 2021 at 14:22):

Kevin Buzzard said:

However what was not at all clear to me was that one could now use Isabelle's type class system to say "O(U) is a ring for every U".

You can't. So the scheme formalization does not use Isabelle's type class system. There are two coexisting algebraic hierarchies in Isabelle, one in terms of type classes, and the other one in terms of locale. The second one is: we have a subset of some big type, and a ring structure on this subset (with its own 1, its own 0, its own multiplication, and so on). This subset can not be interpreted as a type (for lack of dependent type), so you can not use a typeclass to express this ring structure. Indeed, in your big types, you have a lot of rings (one above each open set in the basis), while a typeclass should talk about a unique ring structure. So, to formalize schemes, you give up on type classes, and provide all the data about the ring every time you speak about the ring, because Isabelle can not infer it from you. Maybe I am oversimplifying, but if I understand correctly this is how they are doing things.

view this post on Zulip Johan Commelin (Apr 20 2021 at 14:34):

But it seems that this locale thing allows you to bundle it together in some sense? I see some long-winded explicit passing-arounds of ringstructures, but other parts are quite concise.

view this post on Zulip Bhavik Mehta (Apr 20 2021 at 15:08):

Kevin Buzzard said:

Now we need to raise the bar. In some sense we have less about schemes now than in 2019 because after Ramon's thesis Kenny did a bunch of stuff like gluing sheaves and Gamma Spec adjointness all of which needs to be redone because we changed the definition again (to something different -- we changed our definition of the structure sheaf from Stacks to Hartshorne which makes some things easier and some more difficult). There are plenty of interesting mini projects here but in some sense you can argue that Isabelle/HOL caught up with us right now.

Accessible future Lean projects:

1) isomorphism between R and global sections of Spec(R)
2) global sections (ideally on category of locally ringed spaces) are adjoint to Spec
3) Hartshorne exercise which glues sheaves on a top space
4) existence of pullback squares in the category of schemes
5) definition of affine morphisms, finite presentation morphisms, smooth morphisms, flat morphisms, étale morphisms... (all relatively easy in some sense because you just mindlessly copy the definition from a book), but...
6) basic API for these notions. Specific example: prove that if X->Y is affine in the weak sense that there's an open cover of Y by affines whose preimage is affine, then it's affine in the strong sense that the preimage of every open affine is affine.

In my eyes 3 and 4 could be pretty doable - what's the maths proof of 4?

view this post on Zulip Markus Himmel (Apr 20 2021 at 15:14):

I think that the usual argument is to perform a series of reductions to reduce to the affine case. See for example https://rohilprasad.wordpress.com/2015/12/21/29/

view this post on Zulip Adam Topaz (Apr 20 2021 at 15:18):

That's right -- do it in the affine case and glue (same with every proof from EGA)

view this post on Zulip Adam Topaz (Apr 20 2021 at 15:25):

IMO the most pressing thing for schemes in mathlib is some sort of gluing construction

view this post on Zulip Adam Topaz (Apr 20 2021 at 15:26):

@Bhavik Mehta do you have something resembling "descent data" in your topos project?

view this post on Zulip Bhavik Mehta (Apr 20 2021 at 15:28):

I don't really understand what descent data means, so the answer is either no, or yes but indirectly

view this post on Zulip Bhavik Mehta (Apr 20 2021 at 15:31):

Looking through the nlab page, I have that the sheaves are a reflective subcategory, and iirc I almost have that any reflective subcategory of the presheaves is equivalent to the sheaves on some topology

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:32):

Bhavik: schemes are some weird way of gluing rings together to make a geometric rather than an algebraic object. This "Spec" construction starts with a ring RR, like the polynomial ring C[T]\mathbb{C}[T], and spits out a topological space Spec(R)Spec(R) which is basically C\mathbb{C} with a weird topology (the cofinite one) and for each open subset the data of what a "polynomial function" is on that open set (so for example on the open set C{0,37}\mathbb{C}-\{0,37\} the function (T2+3)/T(T37)2(T^2+3)/T(T-37)^2 is a "polynomial function". You can glue schemes together on open subsets: for example if you glue one C\mathbb{C} with another one along their common C{0}\mathbb{C}-\{0\} via the map z1/zz\mapsto 1/z then you've just made the Riemann sphere C{}\mathbb{C}\cup\{\infty\}.

view this post on Zulip Bhavik Mehta (Apr 20 2021 at 15:33):

If descent has anything to do with this then Beck's monadicity theorem was in the topos project and is now in mathlib; though you might need to dualise to get cases which are useful for geometry?

view this post on Zulip Adam Topaz (Apr 20 2021 at 15:33):

There is a general notion of descent, but the concrete version for schemes is described nicely here
https://en.m.wikipedia.org/wiki/Gluing_schemes

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:33):

The way products work is that in the affine case you show that the tensor product works, and this is not purely ring-theoretic because you need to understand what a map from a random scheme to an affine scheme looks like. Once you've done this, then you can start gluing general schemes together by doing tensor producting on an affine cover and then checking it all glues together. It's quite an ordeal! In Hartshorne's alg geom book it's presented as an 8 step process.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:35):

For that gluing schemes Wikipedia page, if you want to understand it, just pretend "scheme" = "topological space", because already you see the key idea.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:36):

I suspect that doing that "simple" construction for topological spaces would be a challenge in dependent type theory. I say "simple" because if you were to explain that in class for top spaces you'd just say the proof was obvious, you just let X be the quotient of the disjoint union via the gluing phi_{ij} and you'd then claim that everything was obvious.

view this post on Zulip Bhavik Mehta (Apr 20 2021 at 15:36):

Is it reasonable to view this as like a pasting lemma but for schemes rather than spaces?

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:37):

The pasting lemma is gluing sheaves

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:37):

the difference between the descent and the pasting lemma is that with the pasting lemma you already have the top space -- it's just the union of X and Y.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:38):

With gluing schemes the X_i are arbitrary independent things so you have to make the type, not just the function on the type.

view this post on Zulip Bhavik Mehta (Apr 20 2021 at 15:39):

I see - so the summary is that I was very wrong to think 4 is more doable than the others!

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:39):

Once you've done the gluing to make the space, you can then prove the universal property, which is that to give a function on X it suffices to give functions on the X_i which agree on the U_{ij} in the obvious sense (via the phi_{ij})

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:41):

and one direction of the universal property is the pasting lemma

view this post on Zulip Damiano Testa (Apr 20 2021 at 15:46):

I got a bit lost in the discussion: I thought that 4 was pull-backs in the category of schemes. Aren't those fibered products? The discussion seems to be talking about gluing schemes along something, which seems more closely related to push-out diagrams, which are indeed harder.

view this post on Zulip Adam Topaz (Apr 20 2021 at 15:46):

Pullbacks are constructed by gluing pullbacks of affine schemes

view this post on Zulip Damiano Testa (Apr 20 2021 at 15:47):

Oh, I see: you are talking about how to define pull-backs, once you have pull-backs for affines!

view this post on Zulip Damiano Testa (Apr 20 2021 at 15:47):

Ok, I agree: then you do have to glue affine schemes together and you have push-outs!

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:48):

pushouts don't exist in general though :-(

view this post on Zulip Damiano Testa (Apr 20 2021 at 15:48):

No, but these kinds of push-outs are [several thousands of lines of code] obvious.

view this post on Zulip Damiano Testa (Apr 20 2021 at 15:48):

which is exactly why I had missed the point of talking about them! :wink:

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:49):

Can you see the problem? To actually make the underlying type you take the disjoint union of the UiU_i and then quotient out by the relation coming from the ϕij\phi_{ij}, but then the UiU_i are not actually subsets, they're just injective maps into the quotient

view this post on Zulip Damiano Testa (Apr 20 2021 at 15:49):

It is quite amazing how much "functoriality" buys you for free.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:50):

and when I tried this once (admittedly when I was a lot more Lean-naive) I got in a real mess with things, because you constantly have an element of UijU_{ij} which you want to consider as an element of UjiU_{ji} and then of XkX_k and then of XiX_i and then of XX...

view this post on Zulip Damiano Testa (Apr 20 2021 at 15:50):

Yes, and I was horrified when I realized that constructing the integers as equivalence classes of naturals did not "simply contain" the naturals. This is a whole different level!

view this post on Zulip Damiano Testa (Apr 20 2021 at 15:51):

I am slowly starting to appreciate how much more detailed proof have to be, in order to be formalized.

view this post on Zulip Adam Topaz (Apr 20 2021 at 15:54):

Do schemes even have elements!? :wink:

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 15:55):

In fact @Bhavik Mehta this reminds me of the conversation we were having the other day about those pentagon/hexagon axioms. This is another situation where you constantly want to move between a bunch of things which are "all the same thing" but actually doing the moving just piles up maps on top of maps. It would be interesting to prove the gluing lemma statement for topological spaces (you just literally replace "scheme" by "topological space" in the statement on the Wikipedia page, and "isomorphism" by "homeomorphism" if you like). In fact the Wikipedia page is already a bit unclear -- am I allowed i=j? If so, does U_{ii} have to be X_i? Does phi_{ii} have to be the identity map? [YES! But it doesn't say this?]

view this post on Zulip Damiano Testa (Apr 20 2021 at 15:58):

There are funny examples in schemes, where you glue a projective scheme to itself along isomorphic proper closed subsets and the result is not projective anymore. Producing such examples would be a great addition to the counterexample branch!

view this post on Zulip Adam Topaz (Apr 20 2021 at 16:00):

I'm not sure that topological spaces is a good test, because Top has all colimits

view this post on Zulip Adam Topaz (Apr 20 2021 at 16:01):

The hard part is proving that for these diagrams, the colimit on the level of topological spaces is again a scheme

view this post on Zulip David Wärn (Apr 20 2021 at 16:08):

Kevin Buzzard said:

The way products work is that in the affine case you show that the tensor product works, and this is not purely ring-theoretic because you need to understand what a map from a random scheme to an affine scheme looks like. Once you've done this, then you can start gluing general schemes together by doing tensor producting on an affine cover and then checking it all glues together. It's quite an ordeal! In Hartshorne's alg geom book it's presented as an 8 step process.

This is basically docs#category_theory.adjunction.right_adjoint_preserves_limits for the gamma-spec adjunction, right? (spec turns colimits into limits, hence tensor product into pullback)

view this post on Zulip Adam Topaz (Apr 20 2021 at 16:13):

@David Wärn I think that's step 1 of the 8 :)

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 16:22):

Yeah, I cunningly mentioned Gamma-Spec adjunction before pullback squares :-)

view this post on Zulip Wenda Li (Apr 20 2021 at 16:49):

Sebastien Gouezel said:

Kevin Buzzard said:

However what was not at all clear to me was that one could now use Isabelle's type class system to say "O(U) is a ring for every U".

You can't. So the scheme formalization does not use Isabelle's type class system. There are two coexisting algebraic hierarchies in Isabelle, one in terms of type classes, and the other one in terms of locale. The second one is: we have a subset of some big type, and a ring structure on this subset (with its own 1, its own 0, its own multiplication, and so on). This subset can not be interpreted as a type (for lack of dependent type), so you can not use a typeclass to express this ring structure. Indeed, in your big types, you have a lot of rings (one above each open set in the basis), while a typeclass should talk about a unique ring structure. So, to formalize schemes, you give up on type classes, and provide all the data about the ring every time you speak about the ring, because Isabelle can not infer it from you. Maybe I am oversimplifying, but if I understand correctly this is how they are doing things.

Thanks a lot for your detailed explanation of the difference between type classes and locales, Sebastien :-) To me, locales are more flexible/general than type classes, and we can freely switch from locales to type classes by instantiating some carrier sets. In this project, we avoided type classes to gain the flexibility from locales. It is true that with locales we need to do some instance proofs manually, but Sledgehammer turns out fairly capable with such obligations. One issue with locale is that we cannot introduce a type within a locale structure, but I guess in the future there could be some resolutions from Andrei Popescu's Types-to-Sets framework.

view this post on Zulip Kevin Buzzard (Apr 20 2021 at 17:02):

Hi Wenda! I was just plotting about how to pull ahead of you guys again :-) Do you think you could do "sheaves of modules" in Isabelle? As you will know, a sheaf of rings on a topological space is a ring R(U)R(U) attached to each open set UU (and satisfying some axioms). A sheaf of modules for this sheaf of rings is an abelian group M(U)M(U) attached to each open set UU, plus an action of R(U)R(U) on M(U)M(U) for each UU, satisfying some axioms (the axioms for a sheaf of abelian groups, the axioms for modules over a ring, and an axiom saying that the actions are compatible with restriction maps).

view this post on Zulip Johan Commelin (Apr 20 2021 at 18:21):

@Justus Springer is working on turning Spec into a functor. So that would be (1.a) :smiley:

view this post on Zulip Justus Springer (Apr 20 2021 at 18:52):

Currently I'm proving the isomorphism OX(D(f))=Rf\mathcal{O}_X(D(f))=R_f, of which (1) is a special case. This is not strictly necessary to define Spec as a functor but it will be needed when proving adjointness of Spec. I think this exactly the part that's difficult in Hartshorns approach, because in Stacks, this is basically the definition of the structure sheaf. The proof is about one page in Hartshorne, which I've come to realize, is quite a lot when formlizing :sweat_smile:
I'm more than halfway through though

view this post on Zulip Johan Commelin (Apr 20 2021 at 18:53):

(Ooh, I mean (2.a) instead of (1.a)...)

view this post on Zulip Johan Commelin (Apr 20 2021 at 18:54):

Note that for the Stacks definition it is also not "by definition". You need to show that extending a sheaf from a basis doesn't "change" the values of the sheaf on the basis. Still seems to be a gory computation if you actually need to formalize it.

view this post on Zulip Justus Springer (Apr 20 2021 at 19:03):

Okay, but as soon as the sheaf theory has been set up, you essentially define OX(D(f)):=Rf\mathcal{O}_X(D(f)):=R_f and extend, don't you?
I didn't mean to imply that the other approach would be easier of course. Since I wasn't around for the earlier iterations of Schemes in Lean, I'm happy to take your word that you had good reasons to switch :)

view this post on Zulip Justus Springer (Apr 20 2021 at 19:03):

Personally I find Hartshorne's definition more comprehensible

view this post on Zulip Johan Commelin (Apr 20 2021 at 19:06):

@Justus Springer No, I mean that "and extend" doesn't preserve the definition of OX(D(f))\mathcal O_X(D(f)). So you will have to do a computation showing that some colimit preserves the thing up to isom. I'm sure it will be quite a bit shorter in Lean (at the expense of setting up sheaves over a basis). But you still need to do it. It's not defeq.

view this post on Zulip Justus Springer (Apr 20 2021 at 19:09):

Ah I think I see what you mean. I was using "by definition" more loosely in an informal way, not as defeq in Lean :)

view this post on Zulip Johan Commelin (Apr 20 2021 at 19:12):

There will be some colimit thrown in the mix

view this post on Zulip Wenda Li (Apr 20 2021 at 19:39):

Kevin Buzzard said:

Hi Wenda! I was just plotting about how to pull ahead of you guys again :-) Do you think you could do "sheaves of modules" in Isabelle? As you will know, a sheaf of rings on a topological space is a ring R(U)R(U) attached to each open set UU (and satisfying some axioms). A sheaf of modules for this sheaf of rings is an abelian group M(U)M(U) attached to each open set UU, plus an action of R(U)R(U) on M(U)M(U) for each UU, satisfying some axioms (the axioms for a sheaf of abelian groups, the axioms for modules over a ring, and an axiom saying that the actions are compatible with restriction maps).

I cannot give an affirmative answer yet, as subtleties often arise when going through the actual formalisation. But, in general, I don't think there is any major obstacle here: M(U)M(U) is essentially a bunch of extra functions (i.e., from an open set to the carrier set of M, from an open set to the group operation). I am not quite sure what an action of $$R(U)$$ on $$M(U)$$ looks like, but as long as it can be encoded into some sorts of functions we should be good. After that, axioms are just some predicates on those operations/functions. I will check this with our math expert Anthony, and see if we can have the exact definition in Isabelle :-)

view this post on Zulip Johan Commelin (Apr 20 2021 at 19:41):

an action of $$R(U)$$ on $$M(U)$$: just the "vector space axioms" but without assuming that R(U)R(U) is a field.

view this post on Zulip Mario Carneiro (Apr 20 2021 at 20:29):

Kevin Buzzard said:

My counter to the Mario counter was local rings. If A and B are isomorphic commutative rings and A is local, then B is local, and we will have to prove that as a lemma because it is not true that if A surjects onto B and A is local then B is local; indeed being local means "has a unique maximal ideal" so if B is the zero ring then it has too few maximal ideals so it's not local. However recently I discovered a fix for this! Say a ring is prelocal if it has at most 1 maximal ideal. Then a homomorphic image of a prelocal ring is prelocal, so you can get the result that locality travels along isomorphisms from the fact that nonzeroness travels along isomorphisms, which is easy.

By the way, another way to think of this is that most mathematical notations have some kind of variance, and you only get an invariant notion if you combine operators with different variance. Being prelocal is covariant, and being nonzero is contravariant (because being zero is covariant), so being local is invariant.


Last updated: Jun 17 2021 at 18:14 UTC