## Stream: maths

### Topic: locally ringed spaces in Isabelle

#### Kevin Buzzard (Apr 01 2019 at 11:03):

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 (Apr 01 2019 at 11:04):

@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 (Apr 01 2019 at 11:05):

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

#### Mario Carneiro (Apr 01 2019 at 11:07):

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 (Apr 01 2019 at 11:07):

Does metamath use type theory?

no

ZFC set theory

#### Mario Carneiro (Apr 01 2019 at 11:08):

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 (Apr 01 2019 at 11:08):

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

#### Mario Carneiro (Apr 01 2019 at 11:09):

you would want the rings to be a small category too

#### Kevin Buzzard (Apr 01 2019 at 11:09):

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

#### Mario Carneiro (Apr 01 2019 at 11:09):

just so that you can apply general category machinery

#### Mario Carneiro (Apr 01 2019 at 11:10):

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

#### Mario Carneiro (Apr 01 2019 at 11:11):

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 (Apr 01 2019 at 11:11):

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 (Apr 01 2019 at 11:12):

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 (Apr 01 2019 at 11:13):

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 (Apr 01 2019 at 11:13):

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


no

#### Mario Carneiro (Apr 01 2019 at 11:14):

vector is a dependent type

#### Kevin Buzzard (Apr 01 2019 at 11:14):

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

yes

#### Kevin Buzzard (Apr 01 2019 at 11:14):

Can I then make presheaves of types?

#### Mario Carneiro (Apr 01 2019 at 11:15):

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

this is trouble

#### Kevin Buzzard (Apr 01 2019 at 11:15):

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.

[in Isabelle]

#### Mario Carneiro (Apr 01 2019 at 11:16):

that's not a type in isabelle

Oh!

#### Mario Carneiro (Apr 01 2019 at 11:16):

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

#### Kevin Buzzard (Apr 01 2019 at 11:17):

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

#### Mario Carneiro (Apr 01 2019 at 11:17):

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 (Apr 01 2019 at 11:17):

What's a statement? A Prop?

#### Mario Carneiro (Apr 01 2019 at 11:17):

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

Thanks.

#### Mario Carneiro (Apr 01 2019 at 11:17):

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

#### Mario Carneiro (Apr 01 2019 at 11:18):

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

#### Mario Carneiro (Apr 01 2019 at 11:20):

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 (Apr 01 2019 at 11:22):

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 (Apr 01 2019 at 12:05):

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 (Apr 01 2019 at 12:07):

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 (Apr 01 2019 at 14:00):

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 (Apr 01 2019 at 14:05):

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

#### Chris Hughes (Apr 01 2019 at 14:15):

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

#### Mario Carneiro (Apr 01 2019 at 16:13):

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 (Apr 01 2019 at 16:16):

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

#### Kevin Buzzard (Apr 01 2019 at 16:29):

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?

Last updated: May 18 2021 at 07:19 UTC