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?

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

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.

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