# Zulip Chat Archive

## Stream: new members

### Topic: typechecking error with linear_algebra.dimension

#### Heather Macbeth (Jun 09 2020 at 18:52):

I have two vector spaces and can take their dimensions successfully, but the statement that their dimensions are equal does not seem to parse. Any idea what I am doing wrong?

```
import linear_algebra.dimension
noncomputable theory
variables (π : Type*) [field π]
variables (E : Type*) [add_comm_group E] [vector_space π E]
-- these both work
example : cardinal := vector_space.dim π π
example (x : E) (h : x β 0) : cardinal := vector_space.dim π (submodule.span π ({x} : set E))
-- "don't know how to synthesize placeholder"
example (x : E) (h : x β 0) : vector_space.dim π π = vector_space.dim π (submodule.span π ({x} : set E))
:= sorry
```

#### Johan Commelin (Jun 09 2020 at 18:53):

They live in different universes

#### Sebastien Gouezel (Jun 09 2020 at 18:53):

Does it work if you replace `Type*`

with `Type u`

?

#### Johan Commelin (Jun 09 2020 at 18:53):

If you really want that, then `cardinal.lift`

(I think) will allow you to lift the cardinal to a higher universe.

#### Heather Macbeth (Jun 09 2020 at 18:54):

Aha, today is the day I find out what a universe is.

#### Heather Macbeth (Jun 09 2020 at 18:55):

SΓ©bastien, which should have `Type u`

? `π`

or `E`

?

#### Johan Commelin (Jun 09 2020 at 18:55):

Both

#### Johan Commelin (Jun 09 2020 at 18:55):

So that they are in the same universe :wink:

#### Johan Commelin (Jun 09 2020 at 18:55):

`u`

is a universe variable

#### Johan Commelin (Jun 09 2020 at 18:55):

And `*`

creates a fresh one.

#### Heather Macbeth (Jun 09 2020 at 18:56):

Great! Yes, it works now. Thank you!

#### Johan Commelin (Jun 09 2020 at 18:58):

@Heather Macbeth Does that mean that you found out what a universe is ? (-;

#### Heather Macbeth (Jun 09 2020 at 18:59):

Well, maybe not. There must be one or two more subtleties, right? :)

#### Johan Commelin (Jun 09 2020 at 18:59):

Lol, not that many, I think

#### Johan Commelin (Jun 09 2020 at 18:59):

It's just that `Type = Type 0`

and `Type n : Type (n+1)`

.

#### Kevin Buzzard (Jun 09 2020 at 18:59):

$u$ is in some weird set that you can't reason about, I guess that's an interesting thing

#### Johan Commelin (Jun 09 2020 at 18:59):

This circumvents Russel's paradox

#### Sebastien Gouezel (Jun 09 2020 at 19:00):

Rule number 17 in Lean: if something doesn't work and you don't understand why, try replacing all `Type*`

by `Type`

. (I'll let someone else invent the first 16 rules).

#### Johan Commelin (Jun 09 2020 at 19:00):

You can't have `Type : Type`

. (Although some theorem provers act as if you can.)

#### Heather Macbeth (Jun 09 2020 at 19:00):

Johan, could you give me the full code snippet using `cardinal.lift`

?

#### Kevin Buzzard (Jun 09 2020 at 19:00):

`Type`

?? You mean just do normal mathematics??

#### Sebastien Gouezel (Jun 09 2020 at 19:01):

Yes, `Type`

, the one we know and like so much.

#### Heather Macbeth (Jun 09 2020 at 19:05):

Sebastien Gouezel said:

Rule number 17 in Lean: if something doesn't work and you don't understand why, try replacing all

`Type*`

by`Type`

. (I'll let someone else invent the first 16 rules).

I did not realise that `Type`

can be used without an argument! Why does `mathlib`

always give it an argument (`*`

or `u`

), then?

#### Heather Macbeth (Jun 09 2020 at 19:05):

Johan Commelin said:

It's just that

`Type = Type 0`

and`Type n : Type (n+1)`

.

Oh, I see, it's this.

#### Kevin Buzzard (Jun 09 2020 at 19:07):

Mathlib style is to make all statements universe-polymorphic. This actually hurts them sometimes, because concrete types like $\mathbb{R}$ have type `Type`

and you just saw what happened if different vector spaces live in different universes. I have still not remotely understood the point of this design decision, and my personal take on it is that `Type u`

and `Type*`

look more intimidating to beginners. I often just use `Type`

when giving demos to undergrads.

#### Johan Commelin (Jun 09 2020 at 19:11):

@Heather Macbeth

```
universe variables u v
variables (π : Type u) [field π]
variables (E : Type v) [add_comm_group E] [vector_space π E]
set_option pp.universes true
example (x : E) (h : x β 0) :
cardinal.lift.{v u} (vector_space.dim π (submodule.span π ({x} : set E))) =
cardinal.lift.{u v} (vector_space.dim π π)
:= sorry
```

#### Johan Commelin (Jun 09 2020 at 19:13):

Of course this also typechecks:

```
example (x : E) (h : x β 0) :
vector_space.dim π (submodule.span π ({x} : set E)) = 1
:= sorry
```

But you have to remember that this `1`

on the RHS lives in universe `v`

(-;

#### Johan Commelin (Jun 09 2020 at 19:14):

Note that, if you have an instance of `finite_dimensional`

hanging around, then you can use `findim`

to get a good old `nat`

instead of these weird cardinals.

#### Heather Macbeth (Jun 09 2020 at 19:17):

Thank you, this is very instructive. Why do I need to lift both cardinals? Naively I would have thought it was enough to lift one to the other.

#### Sebastien Gouezel (Jun 09 2020 at 19:21):

You don't know which one is larger.

#### Heather Macbeth (Jun 09 2020 at 19:21):

Ah!

#### Sebastien Gouezel (Jun 09 2020 at 19:21):

If you can avoid `dim`

and work with `findim`

, you should definitely do it!

#### Mario Carneiro (Jun 09 2020 at 19:46):

Kevin Buzzard said:

Mathlib style is to make all statements universe-polymorphic. This actually hurts them sometimes, because concrete types like $\mathbb{R}$ have type

`Type`

and you just saw what happened if different vector spaces live in different universes. I have still not remotely understood the point of this design decision, and my personal take on it is that`Type u`

and`Type*`

look more intimidating to beginners. I often just use`Type`

when giving demos to undergrads.

I believe that when you say that everything you ever use is in `Type`

, this is selective memory in the same sense as "all rings are commutative". Sure most of the things you use are in `Type`

, but you also make use of certain constructions that cannot fit in `Type`

, especially in category theory, for example presheaves and everything built thereupon. And if the library doesn't support these objects it's really a hard cut - nothing is available and you have to rewrite the entire theory. So we end up refactoring it to be polymorphic in the end anyway. (I still dread the day when we have to face a similar incompatibility / complete rewrite problem when it comes to 2-categories.)

#### Mario Carneiro (Jun 09 2020 at 19:46):

That said, for demos to undergrads you should *absolutely* use only `Type`

#### Mario Carneiro (Jun 09 2020 at 19:52):

Now, that's not to say I wouldn't prefer a universe-less ambient logic. I've been a quite vocal supporter of ZFC here in the past and I stand by it in this case as well: you don't need this hierarchy of universes to infect everything, you can have just one "universe" called V and all categories are formally "small", with largeness itself being relativized to certain very large sets that get the proper designation of "universe". (The interesting thing is that for most purposes these don't actually need to be Grothendieck universes and so they exist in plenty in straight ZFC; but you can always pull out a weak large cardinal axiom if you want some Grothendieck universes.)

#### Kevin Buzzard (Jun 09 2020 at 19:53):

I am not convinced by this argument. I sometimes use sets, and I sometimes use categories, and the sets are in Type and the categories are in Type 1 and I don't do typey things with them

#### Mario Carneiro (Jun 09 2020 at 19:54):

Here's an example: `ordinal.{u}`

is an additive monoid

#### Mario Carneiro (Jun 09 2020 at 19:54):

`surreal.{u}`

is a field

#### Mario Carneiro (Jun 09 2020 at 19:59):

In a quite different area, I know I have struggled on at least one occasion with the fact that `tactic A`

only works for `A : Type`

#### Mario Carneiro (Jun 09 2020 at 20:00):

(at least, before the recent changes to enable `Type : Type`

in meta land)

#### Mario Carneiro (Jun 09 2020 at 20:01):

You wouldn't think that large types come up in programming, but they do, when you have certain higher order functions

#### Mario Carneiro (Jun 09 2020 at 20:02):

It's quite common to have an object in maths defined by a universal property that could be written down but would bump the universe, and then we have to find some way to write it without the universe bump

#### Kevin Buzzard (Jun 09 2020 at 20:02):

Ordinals and surreal numbers aren't proper maths really, but I do appreciate that one day this attitude of mine might lead to a disaster

#### Mario Carneiro (Jun 09 2020 at 20:02):

I was waiting for you to say that ;)

#### Mario Carneiro (Jun 09 2020 at 20:03):

I think mathlib shouldn't take a stand on such matters

#### Kevin Buzzard (Jun 09 2020 at 20:04):

Here's perhaps an example. If we are lazy and don't do all the universe controlling when defining etale cohomology, we might end up with etale cohomology groups of a concrete scheme being in Type 1

#### Mario Carneiro (Jun 09 2020 at 20:04):

That's what I was getting at with the presheaves

#### Mario Carneiro (Jun 09 2020 at 20:04):

I don't understand all the definitions but it seems like schemes and such are heading right into that territory

#### Kevin Buzzard (Jun 09 2020 at 20:04):

I think the sheaves are ok. But it's the cohomology of the sheaves which is worrying me now

#### Mario Carneiro (Jun 09 2020 at 20:05):

I point at presheaves because they are in a sense the source of the problem, being functions out of Type by definition

#### Kevin Buzzard (Jun 09 2020 at 20:06):

The sooner you do all the ZFC nonsense which convinces you that the limits you're taking are not too big, the sooner you'll be able to use facts about groups proved only for Type. But I bet that this is exactly how it's done in the books, because in the books people won't dare to take the limit at all before it's proved to be a set

#### Mario Carneiro (Jun 09 2020 at 20:07):

On its face this seems like a silly thing in the same way that anything uncountable must lead to navel gazing questions like CH that miss the point because there is some more "arithmetic" structure underlying it that we are actually interested in

#### Mario Carneiro (Jun 09 2020 at 20:08):

In the case of sheaves I think this manifests in "representable objects" or some such

#### Heather Macbeth (Jun 10 2020 at 15:04):

Could one use `Type 1`

for the Gromov-Hausdorff metric space structure on the set of compact metric spaces? (If I understand correctly, SΓ©bastien did not do this, but instead kept it as `Type`

by realizing all compact metric space, up to isometry, as subsets of $L^\infty$.)

#### Kevin Buzzard (Jun 10 2020 at 15:06):

I guess there isn't a set of compact metric spaces so this sounds like pretty much the same phenomenon occurring in a different branch of mathematics.

#### Kevin Buzzard (Jun 10 2020 at 15:08):

The simplest situation where this shows up in etale cohomology would be where the base is a point Spec(K), K a field, where you want to do calculations with all algebraic extensions of K, but they're not a set either, so (slightly vaguely speaking) you just take an algebraic closure and work with the algebraic extensions in there.

#### Heather Macbeth (Jun 10 2020 at 15:10):

In both cases, one is actually working with a quotient of "the set of all the objects" -- metric spaces / isometry for the one, algebraic extensions / isomorphism for the other.

#### Sebastien Gouezel (Jun 10 2020 at 15:17):

Yes, you could absolutely use `Type 1`

by considering all compact metric spaces in `Type`

up to isometry. But it means you would get a notion that could not compare a compact set in `Type`

and a compact set in `Type 1`

. You would get another Gromov-Hausdorff space by taking all the compact metric spaces in `Type 1`

, modulo isometry, and this one would live in `Type 2`

. I definitely prefer the approach where you are careful to stay in `Type`

.

#### Kevin Buzzard (Jun 10 2020 at 15:20):

The problem with just naively working with things up to isomorphism is that some of these objects have non-trivial automorphisms, so if you work with objects up to isomorphism then you lose the correct definition of a morphism. This was why I said "vaguely speaking". There is some careful dance you have to do in algebraic geometry involving cardinalities, but if you don't do it then your answers end up one universe higher than your questions and you'll see the issues Sebastien is pointing out (those which started this conversation basically).

#### Kevin Buzzard (Jun 10 2020 at 15:21):

Another alternative would be simply to declare that `Type : Type`

and promise not to do anything stupid -- i.e. allow Russell's paradox but promise not to use it to prove theorems. It sounds ridiculous in a mathematical setting but apparently in program verification this technique is sometimes used.

#### Heather Macbeth (Jun 10 2020 at 15:25):

This makes sense, I had not thought of the issue that SΓ©bastien raises.

Last updated: May 12 2021 at 05:19 UTC