locally ringed spaces in Isabelle

Stream: maths

[Kevin Buzzard]

An MSc student of mine, Ramon Fernandez Mir, is refactoring my poorly-written definition of a scheme, and is doing a much better job of it than I did the first time round. He now has schemes, and is working on the construction of the scheme Spec(R) attached to a ring. He has also formalised locally ringed spaces. In talking to him about locally ringed spaces, I got interested in how much we were actually using dependent types.

A locally ringed space is a topological space $X$ equipped with a sheaf $\mathcal{O}_X$ of rings, such that the stalks are local. A sheaf of rings is a presheaf of rings plus an axiom. A presheaf of rings $\mathcal{R}$ is a way to associate a ring $\mathcal{R}(U)$ to each open set $U\subseteq X$ plus a way to associate a morphism of rings $\mathcal{R}(U)\to\mathcal{R}(V)$ to each inclusion $V\subseteq U$ of open sets, plus some axioms (it's a functor). The stalk of a presheaf of rings $\mathcal{R}$ at a point $x\in X$ is the direct limit of $\mathcal{R}(U)$ as $U$ runs over the open sets containing $x$ (this is a directed set). The direct limit of rings is a ring; the underlying type is the quotient of the disjoint union of all the rings by the smallest equivalence relation identifying an element of $\mathcal{R}(U)$ with its image in $\mathcal{R}(V)$, for every inclusion $x\in V\subseteq U$.

I know very little about the formalization world outside Lean but it seems to me that the three other major players are Coq, Isabelle HOL and HOTT. Larry Paulson has assured me that everything I can do in Lean can be done in Isabelle HOL, but my understanding is that not everyone agrees. I will be hanging out in Austria at AITP next week with a bunch of people who know a lot about formal proof verification but perhaps less about Lean itself; I would like to bone up a bit on other theorem provers. @Johannes Hölzl you understand this definition and you understand Isabelle. What are the problems in practice with getting this definition into Isabelle HOL?

[Kevin Buzzard]

@Mario Carneiro could you make this definition in metamath? I've given the "data" part of the story but skipped the axioms, however I'd be happy to fill in axiom details if they're relevant.

[Kevin Buzzard]

Ramon just wrote down this definition in Lean and it was essentially painless.

[Mario Carneiro]

axiom-wise, there wouldn't really be any problems formalizing all that in metamath, except that some of the categories may need to be restricted to some subset of the universe rather than dealing with the proper class Set

[Kevin Buzzard]

Does metamath use type theory?

[Mario Carneiro]

no

[Mario Carneiro]

ZFC set theory

[Mario Carneiro]

the tarski-grothendieck axiom is available because some people claim it's important for category theory, but it hasn't really been used

[Kevin Buzzard]

So there's an issue with defining a functor from the small category of open sets to the larger category of rings?

[Mario Carneiro]

you would want the rings to be a small category too

[Kevin Buzzard]

It's only the data of a ring for each open set; this is "small"

[Mario Carneiro]

just so that you can apply general category machinery

[Mario Carneiro]

More precisely, all categories would be sets, and "small" and "large" refer to what universes things live in

[Mario Carneiro]

formalizing actual large categories is a royal pain because it's not really a category so you can't apply the general machinery

[Kevin Buzzard]

I see -- so you have lying around some universe which is a model of ZFC and you could restrict to rings in that universe.

[Mario Carneiro]

yes; you can weaken the restrictions on the universe though for almost all purposes to something that doesn't satisfy replacement, say, and then you can prove existence of the universes even in vanilla ZFC

[Kevin Buzzard]

OK so I'm sure there is no problem doing it in metamath. What I am confused by is this claim "Isabelle doesn't have dependent types" and how this affects the kind of inductive types which one is allowed to have.

[Kevin Buzzard]

structure am_i_dependent (X : Type) :=
(Y : set X)

[Mario Carneiro]

no

[Mario Carneiro]

vector is a dependent type

[Kevin Buzzard]

But that structure above -- I can make it in Isabelle?

[Mario Carneiro]

yes

[Kevin Buzzard]

Can I then make presheaves of types?

[Mario Carneiro]

a ring $\mathcal{R}(U)$

this is trouble

[Kevin Buzzard]

Can I make the statement of FLT? "forall n, some statement that depends on n is true". That looks like a dependent type to me.

[Kevin Buzzard]

[in Isabelle]

[Mario Carneiro]

that's not a type in isabelle

[Kevin Buzzard]

Oh!

[Mario Carneiro]

you've been smoking the curry howard pipe for too long

[Kevin Buzzard]

Where can I read about Isabelle's type theory? This FLT thing was not what I was expecting.

[Mario Carneiro]

statements are not types. Statements can depend on terms, and terms can depend on statements; terms have types, and types can depend only on types

[Kevin Buzzard]

What's a statement? A Prop?

[Mario Carneiro]

You should read about "higher order logic" or "simply typed lambda calculus"

[Kevin Buzzard]

Thanks.

[Mario Carneiro]

yes, in set theory it's called a wff or formula

[Mario Carneiro]

it's an element of a type called "bool" or "o" in the STLC

[Mario Carneiro]

the types are "o" (propositions) and "i" (individuals, a basic infinite type) and you can form the type "A -> B" where "A" and "B" are types, and you can define type constructors "foo A B C" where A,B,C are types. That's all the types

[Mario Carneiro]

there is no dependent pi constructor for types. You can quantify over a type variable with the capital lambda, this allows polymorphic functions, and you can quantify over a type with little lambda

[Kevin Buzzard]

so Prop is relegated to a type, not a universe, and what I think of as a proposition, i.e. a term of type Prop but a type in its own right, is relegated to a term. So the whole concept of proving a proposition is now different to the concept of defining a term of a type and this is what you mean by the Curry Howard comment above.

[Chris Hughes]

Is there a distinction between propositions that quantify over types and those that don't in Isabelle? For example, could I define something like {x : α // Π {β : Type}, P β x}

[Sebastien Gouezel]

No, you can't define this.

And to come back to the initial question, having a ring depending in an open set (i.e., a type depending on a term) is not possible in Isabelle. The usual solution is to work in a big type, and to define disjoint subsets of this big type, depending on the open set, say R U. Together with maps on the big type that you could call add and mult, that would satisfy all the ring axioms when applied to elements in R U, for any U. In other words, you are imitating ZFC, inside one fixed type, and then everything becomes possible.

The main drawback of this approach is that you don't have genuine types depending on U, so you can't use typeclasses and all the nice already existing theory of rings defined using type classes. You need to reconstruct everything in parallel. This means that you will have two versions of rings in Isabelle, one with typeclasses, and one for subsets of a given type.

[Kevin Buzzard]

And if I want to do tensor products of presheaves of rings?

[Chris Hughes]

Just to be clear, Can I define this as a set rather than a subtype? {x : α | ∀ {β : Type}, P β x}

[Mario Carneiro]

I don't think you can do even that. Forall here has type Lambda A, (A -> bool) -> bool, so you have to put in some type for A, and Type is not a type

[Sebastien Gouezel]

Indeed it is not possible to quantify over types in Isabelle.

[Kevin Buzzard]

This sheaf of rings thing is kind of horrible. I see that in ZFC something similar is going on under the hood -- you would have a function from the set of open sets into some set of rings. Can I make some structure Ring in Isabelle so that to give a term of this structure I give a carrier type plus the ring structure and axioms on that carrier?