universe levels

Stream: new members

[Fabian Glöckle]

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]

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

[Kevin Buzzard]

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]

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]

Can you point me to the definition of dim?

[Fabian Glöckle]

vector_space.dim in linear_algebra.dimension

[Kevin Buzzard]

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]

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

[Reid Barton]

You could use cardinal.lift

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Fabian Glöckle]

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]

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

[Kenny Lau]

Why isn't it B : Type u?

[Ken Lee]

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

[Kenny Lau]

it's specifying the universe parameters

[Ken Lee]

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

[Kenny Lau]

right

[Chris Hughes]

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)

[Kenny Lau]

thanks

[Chris Hughes]

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]

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]

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]

I think bundled categories would fix this.

[Reid Barton]

I think the behavior will change in Lean 4, too

[Reid Barton]

even though I think the Lean 3 behavior is technically correct

[Reid Barton]

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

[Bhavik Mehta]

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

[Reid Barton]

Yes (since I wrote it :upside_down:)

[Reid Barton]

That was just a bug.

[Reid Barton]

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]

in this case the elaborator would produce a bad declaration

[Bhavik Mehta]

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

[Reid Barton]

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.

[Reid Barton]

Yes

[Reid Barton]

provided you also remove the instance name of course

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Bhavik Mehta]

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

[Mario Carneiro]

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]

Well, that is what Lean 4 is supposed to implement

[Reid Barton]

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]

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.