Zulip Chat Archive

Stream: new members

Topic: universe levels


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 01 2019 at 16:06):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Apr 01 2019 at 16:08):

Can you point me to the definition of dim?

view this post on Zulip Fabian Glöckle (Apr 01 2019 at 16:09):

vector_space.dim in linear_algebra.dimension

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 01 2019 at 16:11):

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

view this post on Zulip Reid Barton (Apr 01 2019 at 16:12):

You could use cardinal.lift

view this post on Zulip Kevin Buzzard (Apr 01 2019 at 16:12):

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

view this post on Zulip Kevin Buzzard (Apr 01 2019 at 16:12):

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

view this post on Zulip 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!

view this post on Zulip Kenny Lau (Jul 12 2019 at 06:45):

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

view this post on Zulip Kenny Lau (Jul 12 2019 at 06:46):

Why isn't it B : Type u?

view this post on Zulip Ken Lee (Jul 12 2019 at 06:50):

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

view this post on Zulip Kenny Lau (Jul 12 2019 at 06:51):

it's specifying the universe parameters

view this post on Zulip Ken Lee (Jul 12 2019 at 06:54):

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

view this post on Zulip Kenny Lau (Jul 12 2019 at 07:01):

right

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jul 12 2019 at 07:11):

thanks

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Reid Barton (May 23 2020 at 23:36):

I think bundled categories would fix this.

view this post on Zulip Reid Barton (May 23 2020 at 23:37):

I think the behavior will change in Lean 4, too

view this post on Zulip Reid Barton (May 23 2020 at 23:38):

even though I think the Lean 3 behavior is technically correct

view this post on Zulip Reid Barton (May 23 2020 at 23:38):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (May 23 2020 at 23:39):

Yes (since I wrote it :upside_down:)

view this post on Zulip Reid Barton (May 23 2020 at 23:39):

That was just a bug.

view this post on Zulip 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

view this post on Zulip Reid Barton (May 23 2020 at 23:40):

in this case the elaborator would produce a bad declaration

view this post on Zulip Bhavik Mehta (May 23 2020 at 23:41):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 23 2020 at 23:41):

Yes

view this post on Zulip Reid Barton (May 23 2020 at 23:41):

provided you also remove the instance name of course

view this post on Zulip Reid Barton (May 23 2020 at 23:41):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (May 23 2020 at 23:46):

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

view this post on Zulip 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!

view this post on Zulip 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.)

view this post on Zulip Reid Barton (May 24 2020 at 00:16):

Well, that is what Lean 4 is supposed to implement

view this post on Zulip 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

view this post on Zulip 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: May 13 2021 at 17:42 UTC