Stream: new members

Topic: universe levels

Fabian Glöckle (Apr 01 2019 at 16:01):

Hello, can you help me understanding universe levels?
I am working on the lemma

lemma dual_dim_eq [fintype B] : dim K V = dim K (dual K V) :=


(B being a basis of the finite dimensional K-vectorspace V)
which produces the error

type mismatch at application
dim K (dual K V)
term
dual K V
has type
Type (max u_2 u_1) : Type (max (u_2+1) (u_1+1))
but is expected to have type
Type u_2 : Type (u_2+1)


The problem is that dual := V →ₗ[K] K produces a type necessarily over the universe levels of K and V, whereas vector_space.dim works with a universe level of the vector space which is independent of the one of K.
How does Lean deal with such situations?
And can I read up on universe levels anywhere more thoroughly?

Kevin Buzzard (Apr 01 2019 at 16:06):

I'm not sure this should be happening. Hmm.

Kevin Buzzard (Apr 01 2019 at 16:07):

Can you post a minimum working example -- something which compiles and which I can just cut and paste? All imports included etc.

Fabian Glöckle (Apr 01 2019 at 16:08):

Is there a coercion to higher universe levels? If I change the two sides of the equality statement of the lemma, I get

type mismatch at application
dim K V
term
V
has type
Type u_2 : Type (u_2+1)
but is expected to have type
Type (max u_2 u_1) : Type ((max u_2 u_1)+1)


Kevin Buzzard (Apr 01 2019 at 16:08):

Can you point me to the definition of dim?

Fabian Glöckle (Apr 01 2019 at 16:09):

vector_space.dim in linear_algebra.dimension

Kevin Buzzard (Apr 01 2019 at 16:10):

dim :
Π (α : Type u_1) (β : Type u_2) [_inst_1 : discrete_field α] [_inst_2 : add_comm_group β]
[_inst_3 : vector_space α β], cardinal


This looks fine to me -- there's no reason K and V have to be in the same universe.

Kevin Buzzard (Apr 01 2019 at 16:11):

The issue is I guess the cardinals being in different universes.

Reid Barton (Apr 01 2019 at 16:12):

You could use cardinal.lift

Kevin Buzzard (Apr 01 2019 at 16:12):

Or you could turn the cardinal into a natural number before you ask about the equality.

Kevin Buzzard (Apr 01 2019 at 16:12):

I've never used cardinals in Lean, I am not much help.

Fabian Glöckle (Apr 01 2019 at 16:18):

The cardinal lift was what I was looking for (I did not know they depended on universes, but of course that makes much sense). Thank you all for the quick help!

Kenny Lau (Jul 12 2019 at 06:45):

structure B := (C : Type u)
#check B.{u} -- B : Type (u+1)


Kenny Lau (Jul 12 2019 at 06:46):

Why isn't it B : Type u?

Ken Lee (Jul 12 2019 at 06:50):

what does the projection looking '.{u}' mean?

Kenny Lau (Jul 12 2019 at 06:51):

it's specifying the universe parameters

Ken Lee (Jul 12 2019 at 06:54):

Uh... so the universe that C is supposed to be in?

right

Chris Hughes (Jul 12 2019 at 07:09):

This is why.

import set_theory.schroeder_bernstein

universe u

structure B := (C : Type u)

lemma eq.mpr_injective {α β : Sort u} (h : α = β) :
function.injective (eq.mpr h) := λ _ _, by cases h; exact id

instance : inhabited B := ⟨⟨pempty⟩⟩

open function

example {α : Type u} (f : B.{u} ↪ α) : false :=
let g := B.C ∘ inv_fun f in
have hg : surjective g, from
surjective_comp (λ x, ⟨B.mk x, rfl⟩) (inv_fun_surjective f.2),
let X : Type u := sigma g in
let a : α := classical.some (hg (X → Prop)) in
have ha : g a = (X → Prop), from classical.some_spec (hg (set X)),
cantor_injective (show set X → X, from λ s, ⟨a, by rw ha; exact s⟩)
(λ x y h, by simp at *; exact eq.mpr_injective _ h)


thanks

Chris Hughes (Jul 12 2019 at 07:15):

You can prove the well ordering theorem using this idea, provided you already know cardinals are well ordered.

parameter {σ : Type u}
open function

noncomputable lemma embedding_to_cardinal : σ ↪ cardinal.{u} :=
classical.choice $embedding.total.resolve_left$ λ ⟨⟨f, hf⟩⟩,
let g : σ → cardinal.{u} := inv_fun f in
let ⟨x, (hx : g x = 2 ^ sum g)⟩ := inv_fun_surjective hf (2 ^ sum g) in
have g x ≤ sum g, from le_sum.{u u} g x,
not_le_of_gt (by rw hx; exact cantor _) this

/-- The relation whose existence is given by the well-ordering theorem -/
def well_ordering_rel : σ → σ → Prop := embedding_to_cardinal ⁻¹'o (<)

instance well_ordering_rel.is_well_order : is_well_order σ well_ordering_rel :=
(order_embedding.preimage _ _).is_well_order


Bhavik Mehta (May 23 2020 at 23:31):

MWE:

import category_theory.comma

universes v u

namespace category_theory

open category_theory category_theory.category category_theory.limits

variables {C : Type u} [category.{v} C] {X : C}

structure sub' (X : C) :=
(arrow : over X)
[is_mono : mono arrow.hom]

instance mono_of_sub' (g : sub'.{v} X) : mono g.arrow.hom := g.is_mono

end category_theory


Any time I use sub' I need to include the {v} - is there any way around this? There was some recent fix which let me remove the include stuff but I can't seem to find anything better here

Reid Barton (May 23 2020 at 23:36):

I've never really tried to figure out why sometimes Lean really wants the universe level--it seems correlated with the type of sub' not mentioning morphisms, which makes sense of course. I've always sort of assumed Lean is correct here and it's not that much trouble to add the universe parameter...

Reid Barton (May 23 2020 at 23:36):

I think bundled categories would fix this.

Reid Barton (May 23 2020 at 23:37):

I think the behavior will change in Lean 4, too

Reid Barton (May 23 2020 at 23:38):

even though I think the Lean 3 behavior is technically correct

Reid Barton (May 23 2020 at 23:38):

Imagine you had a second [category.{w} C]; would Lean know which instance to pick?

Bhavik Mehta (May 23 2020 at 23:39):

Fair enough - do you know why the recent fix lets us get rid of the include stuff?

Reid Barton (May 23 2020 at 23:39):

Yes (since I wrote it :upside_down:)

Reid Barton (May 23 2020 at 23:39):

That was just a bug.

Reid Barton (May 23 2020 at 23:40):

It covered situations where Lean had already figured out it needed to use the category.{v} C variable, but the universe parameter v didn't otherwise appear anywhere

Reid Barton (May 23 2020 at 23:40):

in this case the elaborator would produce a bad declaration

Bhavik Mehta (May 23 2020 at 23:41):

Ah cool, I see. Can I remove the include everywhere in my code then?

Reid Barton (May 23 2020 at 23:41):

You might be wondering why Lean so frequently figures out to use the category.{v} C instance (instead of holding out for a possibly different category.{w} C instance) and this I don't know.

Yes

Reid Barton (May 23 2020 at 23:41):

provided you also remove the instance name of course

Reid Barton (May 23 2020 at 23:41):

https://github.com/leanprover-community/mathlib/commit/cb3a017fa53baf886fca6f10e484b016264abd43

Reid Barton (May 23 2020 at 23:44):

I went through the library pretty quickly and skipped over some where I didn't understand immediately what was going on--those can probably be removed too.

Bhavik Mehta (May 23 2020 at 23:45):

I was just about to send an example where it didn't let me remove it, but in the process of minimising to an mwe I realised the file depended on another one which had an include

Reid Barton (May 23 2020 at 23:46):

hmm, I think these changes should not have any non-local effects...

Bhavik Mehta (May 23 2020 at 23:48):

Maybe I'd done something else wrong too then, in any case I've got something which seems to work now!

Mario Carneiro (May 24 2020 at 00:12):

My understanding is that typeclass inference is not "universe aware". Universe variables are always out params so a category.{v} C and category.{w} C instance would be considered conflicting. (I also think this is the correct behavior.)

Reid Barton (May 24 2020 at 00:16):

Well, that is what Lean 4 is supposed to implement

Reid Barton (May 24 2020 at 00:17):

In Lean 3 it doesn't always happen. I think it has something to do with the difference between regular and temporary metavariables

Reid Barton (May 24 2020 at 00:19):

By "it doesn't always happen" I mean Lean doesn't always use an instance if it would have to assign a universe level metavariable in the goal to do so.

Last updated: Dec 20 2023 at 11:08 UTC