typechecking error with linear_algebra.dimension

Stream: new members

[Heather Macbeth]

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]

They live in different universes

[Sebastien Gouezel]

Does it work if you replace Type* with Type u?

[Johan Commelin]

If you really want that, then cardinal.lift (I think) will allow you to lift the cardinal to a higher universe.

[Heather Macbeth]

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

[Heather Macbeth]

Sébastien, which should have Type u? 𝕜 or E?

[Johan Commelin]

Both

[Johan Commelin]

So that they are in the same universe :wink:

[Johan Commelin]

u is a universe variable

[Johan Commelin]

And * creates a fresh one.

[Heather Macbeth]

Great! Yes, it works now. Thank you!

[Johan Commelin]

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

[Heather Macbeth]

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

[Johan Commelin]

Lol, not that many, I think

[Johan Commelin]

It's just that Type = Type 0 and Type n : Type (n+1).

[Kevin Buzzard]

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

[Johan Commelin]

This circumvents Russel's paradox

[Sebastien Gouezel]

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]

You can't have Type : Type. (Although some theorem provers act as if you can.)

[Heather Macbeth]

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

[Kevin Buzzard]

Type?? You mean just do normal mathematics??

[Sebastien Gouezel]

Yes, Type, the one we know and like so much.

[Heather Macbeth]

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]

Johan Commelin said:

It's just that Type = Type 0 and Type n : Type (n+1).

Oh, I see, it's this.

[Kevin Buzzard]

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]

@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]

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]

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]

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]

You don't know which one is larger.

[Heather Macbeth]

Ah!

[Sebastien Gouezel]

If you can avoid dim and work with findim, you should definitely do it!

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

Here's an example: ordinal.{u} is an additive monoid

[Mario Carneiro]

surreal.{u} is a field

[Mario Carneiro]

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]

(at least, before the recent changes to enable Type : Type in meta land)

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

I was waiting for you to say that ;)

[Mario Carneiro]

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

[Kevin Buzzard]

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]

That's what I was getting at with the presheaves

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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

[Heather Macbeth]

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]

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]

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]

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]

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]

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]

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]

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