Small and large categories in Type Theory

Stream: maths

[Stepan Nesterov]

As is well-known and almost always ignored in graduate textbooks and courses in anything involving homological algebra, a distinction between small and large categories has to be made in set theory. This is due to the fact that the set of all sets can not be formed due to Russel paradox.
However, Lean is not based on set theory, but rather in a version of type theory I do not yet understand very well. But it seems like a type of all types which are not its own members does not make sense in Lean. Does no Russel paradox mean it is ok to form the category of all types?
So I want to understand two things:
a) Where can I find a list of type theory axioms which Lean uses, preferably summarized in a mathematician’s notation.
b) Where can I find a summary of what difficulties in standard smallness-sensitive category-theoretic constructions (Freyd adjoint functor theorem, localization of categories, enough injectives in abelian categories, etc) disappear in type theory, and what are some new difficulties? A concrete example — how to define a derived category of R-mod not yet in Lean, but in Lean’s type theory informally? Are large Hom-sets allowed? Does a theorem that these Hom-sets are actually small makes any sense?

[Johan Commelin]

@Stepan Nesterov Everything has a type. The type of the natural numbers nat is called Type. This thing Type is the type of all types. And mathlib knows that it is a "large" category. But since everything has a type, Type also needs to have a type. In some systems, Type is it's own type, which leads to Russell-like paradoxes. In Lean Type the type turns out to be Type 1. And Type 1 has type Type 2. Etc...

[Stepan Nesterov]

@Johan Commelin Does it have any kind of a 'reduction axiom' as Russell was trying to have in the 1900's? Let's say, if we can prove that a 'Type 1' is a countable 'Type 1', then can it be regarded as a 'Type'?

[Johan Commelin]

Nope, not really. You can try to define an equivalence (aka isomorphism, aka bijection) between X : Type 1 and Y : Type, and for countable types that will always be possible.

[Johan Commelin]

But in general it's tricky to downsize your universe.

[Johan Commelin]

Bumping up is easy: there's a function ulift : Type u -> Type (max u v)

[Stepan Nesterov]

And do all the definitions in Lean have 'Type 1' counterpart? Say, a Gromov-Hausdorff space (https://en.wikipedia.org/wiki/Gromov%E2%80%93Hausdorff_convergence) is a metric space whose points are isomorphism classes of compact metric spaces. A correct statement in Lean is than 'Gromov-Hausdorff space is a 'Metric Space 1' which is non-canonically isomorphic to a 'Metric Space'', is that right?

[Johan Commelin]

Yes, almost everything in mathlib is "universe polymorphic"

[Johan Commelin]

Note that mathlib knows about your example: docs#Gromov_Hausdorff.GH_space

[Johan Commelin]

But metric spaces (and almost all other definitions) are defined using a universe variable u, so that they make sense in Type u for arbitrary u.

[Stepan Nesterov]

I type #check Gromov_Hausdorff.GH_space and it says Type though.
While you just explained it should be Type 1. I'm confused

[Stepan Nesterov]

Johan Commelin said:

But metric spaces (and almost all other definitions) are defined using a universe variable u, so that they make sense in Type u for arbitrary u.

Is u here a natural number? Or is there a Type \omega and more?

[Johan Commelin]

It's not a natural number as in nat, but you can only construct them using zero, succ, and max.

[Johan Commelin]

So effectively there's countably many universes.

[Johan Commelin]

You cannot quantify explicitly over u.

[Johan Commelin]

I think docs#Gromov_Hausdorff.isometry_rel.setoid explains why this particular example is in Type. It's not defined (in mathlib) exactly in the way you described.

[Johan Commelin]

So maybe docs#cardinal is a better example.

[Stepan Nesterov]

Yes, Gromov-Hausdorff space is defined as a space of all subspaces of l^{\infty}(\R), and than it is a theorem that every compact metric space so arises.

[Stepan Nesterov]

Is there a list of axioms anywhere in mathlib docs, so that I can see full list of which consructions are possible? I can't find one in there.

[Johan Commelin]

What exactly do you mean by axioms? Things like how to construct new types from existing ones? Those are usually not called axioms, afaik.

[Stepan Nesterov]

I mean, in ZFC we have Axiom of Union, Axion of Comprehension, Axiom of Powerset, etc

[Stepan Nesterov]

What is Lean's analogue for that?

[Johan Commelin]

I don't know ZFC, but your questions are probably answered in Mario's thesis. (searching link for you)

[Johan Commelin]

https://github.com/digama0/lean-type-theory/releases/tag/v1.0

[Stepan Nesterov]

Looks like it, thanks!

[Mario Carneiro]

It is possible to resize types both up and down. The general mechanism for resizing up is ulift, so for example if you need a copy of the real numbers in a big universe you can use ulift real

[Mario Carneiro]

To resize down, you have to know some kind of smallness property of the type. For example if the type is countable, then by definition that means it is isomorphic to a subset of nat, and that subset lives in Type

[Scott Morrison]

We also have src#small, for working with types that you know are "smaller" than the universe that the typechecker knows they inhabit.

[Scott Morrison]

Also src#category_theory.essentially_small, for the corresponding categorical idea.

[Mario Carneiro]

If you want to think in terms of set theory, lean is fairly well approximated by thinking of it as ZFC + countably many inaccessible cardinals. The types Type, Type 1, Type 2 correspond to $V_{\kappa_i}$ where $\kappa_i$ is the i'th inaccessible

[Mario Carneiro]

In particular, Type can be used to construct a model of ZFC, Type 1 can be used to construct a model of ZFC with one inaccessible, and so on

[Stepan Nesterov]

Mario Carneiro said:

If you want to think in terms of set theory, lean is fairly well approximated by thinking of it as ZFC + countably many inaccessible cardinals. The types Type, Type 1, Type 2 correspond to $V_{\kappa_i}$ where $\kappa_i$ is the i'th inaccessible

So in particular, Axiom of Replacement is provable/has an analogue in Lean?
How do I define \aleph_\omega?

[Stepan Nesterov]

Another problem with set theory-based category theory is that the embeddings V_k into V are not necessary elementary. Can we prove an analogue of reflection principle for Type u universes in Lean?

[Kevin Buzzard]

The axiom schema of replacement is a set-theoretic concept really. Lean's dependent type theory is equiconsistent with ZFC + infinitely many inaccessibles in the sense that we can build a model of ZFC + inaccessibles in Lean, and conversely in ZFC one can build sets which correspond to Lean's dependent types. This doesn't mean however that there is some direct translation between the axioms of ZFC and what is happening in Lean.

[Kevin Buzzard]

Any function in Lean has a well-defined domain and codomain. The axiom of replacement talks about this more general concept of a mapping or whatever you want to call it; such a concept does not really exist in Lean's type theory.

[Kevin Buzzard]

Lean's maths library does have a model of ZFC in it, and within that model you can define stuff like its aleph_omega.

[Stepan Nesterov]

Here's a more math way of reformulating the Replacement issue: does Lean prove that the category of all types has all (small) limits and colimits?

[Johan Commelin]

Yup, that's in mathlib

[Scott Morrison]

https://leanprover-community.github.io/mathlib_docs/category_theory/limits/types.html#category_theory.limits.types.sort.category_theory.limits.has_limits

[Kevin Buzzard]

(deleted)

[Johan Commelin]

We should have a :wat: emoji

[Scott Morrison]

Gah, somehow the name is not what it should be, so it's hard to link to in the documentation.

[Stepan Nesterov]

And here's a math explanation of the problem with embeddings of V_k -> V:
Assume that we have proved that the category of all schemes inside Type has products. By definition, that means that for a small scheme Z one has Hom(Z,X \times Y) = Hom(Z,X) \times Hom(Z,Y). But what if we changed our mind and at some point needed a scheme in Type 1 or Type 2? Then for such a large scheme Z the universal property has no reason to hold.
Is this just as much pain in Lean as it is in set theory?

[Kevin Buzzard]

I :heart: instance names

[Kevin Buzzard]

Stepan Nesterov said:

And here's a math explanation of the problem with embeddings of V_k -> V:
Assume that we have proved that the category of all schemes inside Type has products. By definition, that means that for a small scheme Z one has Hom(Z,X \times Y) = Hom(Z,X) \times Hom(Z,Y). But what if we changed our mind and at some point needed a scheme in Type 1 or Type 2? Then for such a large scheme Z the universal property has no reason to hold.
Is this just as much pain in Lean as it is in set theory?

Yes. But it doesn't happen in "real math" so it hasn't really bitten us yet.

[Scott Morrison]

Also, that's not actually "the definition" of having products. :-)

[Scott Morrison]

Of course as a lemma one has that equivalence (not equality :-).

[Kevin Buzzard]

We do run into universe problems sometimes when trying to be uber-general (e.g. if we're proving theorems about two modules over a ring, the mathlib style is to have the ring in universe u, one module in universe v and the other in universe w, and then maybe the tensor product of them will be in universe max(u,v,w)). If universes get out of hand then we tend to roll back and start putting things in the same universe. But in the kind of maths which is happening in mathlib, if you just restrict everything to one universe then this in practice solves all your universe problems.

[Stepan Nesterov]

Kevin Buzzard said:

Stepan Nesterov said:

And here's a math explanation of the problem with embeddings of V_k -> V:
Assume that we have proved that the category of all schemes inside Type has products. By definition, that means that for a small scheme Z one has Hom(Z,X \times Y) = Hom(Z,X) \times Hom(Z,Y). But what if we changed our mind and at some point needed a scheme in Type 1 or Type 2? Then for such a large scheme Z the universal property has no reason to hold.
Is this just as much pain in Lean as it is in set theory?

Yes. But it doesn't happen in "real math" so it hasn't really bitten us yet.

I learned some etale cohomology recently and I believe that it present an example of such a 'real-math' universe juggling.
Let X be a scheme in Type. Then its etale site is Type 1, and therefore so is any etale sheaf and any of its injective resolution. Therefore the etale cohomology of X are a priori abelian groups in Type 1 until we prove otherwise in the cases we deem interesting.

[Kevin Buzzard]

Yes that's absolutely right.

[Stepan Nesterov]

But I understand that etale cohomology is not coming to Lean anytime soon sadly :(

[Kevin Buzzard]

That's not right!

[Stepan Nesterov]

I thought we didn't even have that the category of affine schemes is antiequivalent to commutative rings

[Kevin Buzzard]

It's on the horizon, like lots of other things, and indeed we will have to deal with your issue, either by doing the kind of thing de Jong does, or by not caring.

[Kevin Buzzard]

The only reason schemes are stagnating right now is that nobody is working hard on them because all of the algebraic geometers and category people and number theorists have been sucked into this Scholze formalisation project going on in #condensed mathematics

[Kevin Buzzard]

What is happening in practice is that those of us who care about these things have decided that getting homological algebra off the ground is a more important project, and here we run into a type theory issue which probably does not exist in set theory (although I'm not sure about this, I've never formalised mathematics in set theory).

[Kevin Buzzard]

As you can imagine, a solid homological algebra base is going to be necessary before we embark on a serious cohomology theory project. It is possible to get around it, e.g. I have had an MSc student formalising group cohomology, but they stopped before they proved the long exact sequence (they just defined $H^n(G,M)$ and proved they were functorial).

[Scott Morrison]

There's no reason etale cohomology can't be in mathlib a year after condensed sets are done. :-)

[Kevin Buzzard]

The problem we run into when formalising is that if we have abelian groups $A_i$ and maps $A_i\to A_{i+1}$ then we have maps $A_{i-1}\to A_{(i-1)+1}$, and $(i-1)+1$ is equal, but not definitionally equal, to $i$, which means that although there are canonical maps $A_{(i-1)+1}\to A_i$ and the other way, these are not in some sense "the identity function", and this causes an added layer of confusion which we're still learning how to tame.

[Scott Morrison]

(Or just a year from now if we keep finding new people at this rate. Or 6 months if someone is especially keen.)

[Scott Morrison]

(...I better get back to the homology2 branch. I got bored for a few days.)

[Stepan Nesterov]

Kevin Buzzard said:

The only reason schemes are stagnating right now is that nobody is working hard on them because all of the algebraic geometers and category people and number theorists have been sucked into this Scholze formalisation project going on in #condensed mathematics

Okay, makes sense, will check this out.
I'd love to join some work on schemes after I play with some easy theorems and get the hang of it, hopefully soon :)

[Kevin Buzzard]

Right -- group cohomology was sufficiently "easy" to do that an MSc student with no Lean experience at all could formalise the objects (which involved doing a lot of combinatorics with $d^2=0$ etc) in 9 months whilst working on his other masters courses.

[Kevin Buzzard]

@Stepan Nesterov you might also be interested in the "Schemes in Isabelle/HOL" thread in this #maths stream. In particular there is some recent activity due to Justus Springer.

[Scott Morrison]

@Justus Springer has recently been doing some great work improving our existing material on sheaf theory. Johan and I wrote much of the first version of this that made it into mathlib, and it wasn't uniformly lovely. @Bhavik Mehta has then done sheaves on sites, but we haven't unified the two developments yet. :-(