Schemes in Isabelle/HOL

Stream: maths

[Oliver Nash]

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

[Kevin Buzzard]

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)

[Oliver Nash]

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!

[Oliver Nash]

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.

[Joachim Hauge]

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?

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Gabriel Ebner]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Sebastien Gouezel]

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.

[Johan Commelin]

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

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Joachim Hauge]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

So we know $\mathbb{N}\cong\mathbb{Z}$ and they write this as $\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)

[Eric Rodriguez]

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

[Kevin Buzzard]

Because = doesn't mean =

[Eric Rodriguez]

that's some insanity, the ℕ ℤ stuff

[Kevin Buzzard]

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.

[Kevin Buzzard]

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:X\cong Y$ and $j:X\cong Y$ with $i\not=j$ as well.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Gabriel Ebner]

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

[Johan Commelin]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

[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]

[Kevin Buzzard]

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.

[Kevin Buzzard]

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:

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Sebastien Gouezel]

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.

[Johan Commelin]

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.

[Bhavik Mehta]

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?

[Markus Himmel]

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/

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Kevin Buzzard]

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 $R$, like the polynomial ring $\mathbb{C}[T]$, and spits out a topological space $Spec(R)$ which is basically $\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 $\mathbb{C}-\{0,37\}$ the function $(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 $\mathbb{C}$ with another one along their common $\mathbb{C}-\{0\}$ via the map $z\mapsto 1/z$ then you've just made the Riemann sphere $\mathbb{C}\cup\{\infty\}$.

[Bhavik Mehta]

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?

[Adam Topaz]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Bhavik Mehta]

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

[Kevin Buzzard]

The pasting lemma is gluing sheaves

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Bhavik Mehta]

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

[Kevin Buzzard]

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})

[Kevin Buzzard]

and one direction of the universal property is the pasting lemma

[Damiano Testa]

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.

[Adam Topaz]

Pullbacks are constructed by gluing pullbacks of affine schemes

[Damiano Testa]

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

[Damiano Testa]

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

[Kevin Buzzard]

pushouts don't exist in general though :-(

[Damiano Testa]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Damiano Testa]

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

[Kevin Buzzard]

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 $U_{ij}$ which you want to consider as an element of $U_{ji}$ and then of $X_k$ and then of $X_i$ and then of $X$...

[Damiano Testa]

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!

[Damiano Testa]

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

[Adam Topaz]

Do schemes even have elements!? :wink:

[Kevin Buzzard]

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?]

[Damiano Testa]

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!

[Adam Topaz]

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

[Adam Topaz]

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

[David Wärn]

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)

[Adam Topaz]

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

[Kevin Buzzard]

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

[Wenda Li]

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.

[Kevin Buzzard]

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)$ attached to each open set $U$ (and satisfying some axioms). A sheaf of modules for this sheaf of rings is an abelian group $M(U)$ attached to each open set $U$, plus an action of $R(U)$ on $M(U)$ for each $U$, 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).

[Johan Commelin]

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

[Justus Springer]

Currently I'm proving the isomorphism $\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

[Johan Commelin]

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

[Johan Commelin]

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.

[Justus Springer]

Okay, but as soon as the sheaf theory has been set up, you essentially define $\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 :)

[Justus Springer]

Personally I find Hartshorne's definition more comprehensible

[Johan Commelin]

@Justus Springer No, I mean that "and extend" doesn't preserve the definition of $\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.

[Justus Springer]

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

[Johan Commelin]

There will be some colimit thrown in the mix

[Wenda Li]

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)$ attached to each open set $U$ (and satisfying some axioms). A sheaf of modules for this sheaf of rings is an abelian group $M(U)$ attached to each open set $U$, plus an action of $R(U)$ on $M(U)$ for each $U$, 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)$ 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 :-)

[Johan Commelin]

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

[Mario Carneiro]

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.