Type / Type* using cardinal

Stream: maths

[Antoine Chambert-Loir]

The following function gives me the existence an element outside of the range of a function from fin nprovided the cardinal of the target type is greater than n, but that only works when the target type is chosen as a Type but not a Type*.

import set_theory.cardinal

open_locale cardinal

lemma gimme_more {α : Type} (m : ℕ) (x : fin m → α) (hα : ↑m < #α) :
  ∃ (a : α), a ∉ set.range x :=
begin
  suffices : ¬ (function.surjective x),
  exact not_forall.mp this,
  intro h,
  apply (lt_iff_not_ge _ _).mp  hα,
  rw ← cardinal.mk_fin,
  exact cardinal.mk_le_of_surjective h
end

lemma gimme_more' {α : Type*} (m : ℕ) (x : fin m → α) (hα : ↑m < #α) :
  ∃ (a : α), a ∉ set.range x :=
begin
  suffices : ¬ (function.surjective x),
  exact not_forall.mp this,
  intro h,
  apply (lt_iff_not_ge _ _).mp  hα,
  rw ← cardinal.mk_fin,
  exact cardinal.mk_le_of_surjective h
end

(For some time, I was OK with setting alpha as a Type, but later one, Lean complained that I should use set_like.coe_mem with a Type ? as a target, but not just a Type…)

[Eric Rodriguez]

note that fin n is in Type, causing you the issue... try docs#cardinal.lift_mk_of_fin

[Antoine Chambert-Loir]

There is a typo in the name of your function, I'm browsing the library to find the correct one.
Aside : why isn't fin n in Type 0?

[Kevin Buzzard]

It is?

[Kevin Buzzard]

Try #check (fin 37 : Type 0). I'd be surprised if it failed

[Antoine Chambert-Loir]

It doesn't fails but returns fin 37 : Type.

[Filippo A. E. Nuccio]

But I thought that Type=Type 0, no?

[Antoine Chambert-Loir]

Oh! I had presumed the opposite, namely that Type wouldn't refer to a specific universe.

[Filippo A. E. Nuccio]

Well, I am certainly not an expert, but reading Ch. 7 of "Theorem proving in Lean", you can see that they start by saying

We have seen that Lean’s formal foundation includes basic types, Prop, Type 0, Type 1, Type 2, ..., and allows ...

I think that " the types of an unspecified universe" should not really exist.

[Adam Topaz]

Type and Type 0 are indeed the same

[Adam Topaz]

And they're the same as Sort 1, while Prop is Sort 0.

[Adam Topaz]

Generally if we want to make a statement that's polymorphic over all type universes, we would use Type* or Type u after naming a universe variable. If we want to be polymorphic over all Type universes and also Prop, we use Sort* or Sort u

[Adam Topaz]

When you have concrete types such as fin 37, $\mathbb{Z}$, etc., they will usually be in Type (equiv. Type 0).

[Antoine Chambert-Loir]

The question for me seems to transform a surjectiveh :fin m -> t (with m : nat and t : Type u) to a surjective map from a variant of fin m which also belongs to Type u.

[Antoine Chambert-Loir]

This is a proof of gimme_more', but I found it horrible to write! There must be some better way…

import set_theory.cardinal
import control.ulift

open_locale cardinal

lemma gimme_more {α : Type} (m : ℕ) (x : fin m → α) (hα : ↑m < #α) :
  ∃ (a : α), a ∉ set.range x :=
begin
  apply not_forall.mp,
  change ¬ (function.surjective x),
  intro h,
  apply (lt_iff_not_ge _ _).mp  hα,
  rw ← cardinal.mk_fin,
  exact cardinal.mk_le_of_surjective h
end

lemma gimme_more' {α : Type*} (m : ℕ) (x : fin m → α) (hα : ↑m < #α) :
  ∃ (a : α), a ∉ set.range x :=
begin
  apply not_forall.mp,
  -- change ¬ (function.surjective x),
  intro h,
  apply (lt_iff_not_ge _ _).mp  hα,
  --   rw ge_iff_le,
  have h' : function.surjective (ulift.map x),
  { intro a, obtain ⟨i, hi⟩ := h a.down, use i,
    rw [ulift.map_up, hi, ulift.up_down] },
  let z := cardinal.mk_le_of_surjective h',
  simp only [cardinal.mk_ulift, cardinal.mk_fintype,
  fintype.card_ulift, fintype.card_fin] at z,
  rw  cardinal.lift_id at z,
  exact z,
end

[Antoine Chambert-Loir]

Maybe one needs ulift_injective_of_injective and ulift_surjective_of_surjective…

[Antoine Chambert-Loir]

Should I PR these two lemmas ?

import tactic
import control.ulift

namespace ulift
universes u v
variables {α : Type u} {β : Type v}

lemma surjective_of_surjective (f : α → β) (hf : function.surjective f) :
  function.surjective (ulift.map f) :=
begin
  intro b, obtain ⟨a, ha⟩ := hf b.down, use a,
    rw [ulift.map_up, ha, ulift.up_down]
end

lemma injective_of_bijective (f : α → β) (hf : function.injective f) :
  function.injective (ulift.map f) :=
begin
  intros a a',
  rw [← (ulift.up_down a), ← (ulift.up_down a')],
  simp only [ulift.map_up, ulift.ext_iff, ulift.down_up],
  intro h, exact hf h,
end

end ulift

[Eric Rodriguez]

You may find using equiv.ulifteasier

[Antoine Chambert-Loir]

Indeed ! The following is much nicer, but I needed to add two “rfl-lemmas” which I don't know how to invoke otherwise.

lemma comp_ulift_eq_ulift_comp {f : α → β} : f ∘ equiv.ulift = equiv.ulift ∘ (ulift.map f) := rfl

lemma comp_ulift_eq_ulift_comp' {f : α → β} :
 (ulift.map f) ∘ equiv.ulift.symm = equiv.ulift.symm ∘ f := rfl

lemma surjective_iff_surjective {f : α → β} :
  function.surjective f ↔
  function.surjective (ulift.map f) :=
by rw [← equiv.comp_surjective, ← comp_ulift_eq_ulift_comp', equiv.surjective_comp]

[Eric Rodriguez]

I thought this was a bit easier:

lemma gimme_more' {α : Type*} (m : ℕ) (x : fin m → α) (hα : ↑m < #α) :
  ∃ (a : α), a ∉ set.range x :=
begin
  suffices : ¬ (function.surjective x),
  exact not_forall.mp this,
  intro h,
  apply (lt_iff_not_ge _ _).mp hα,
  rw [←cardinal.lift_mk_fin, ←cardinal.mk_ulift],
  refine cardinal.mk_le_of_surjective (show function.surjective (x ∘ equiv.ulift), from _),
  rwa equiv.surjective_comp,
end

[Eric Rodriguez]

or for those last two lines even exact cardinal.mk_le_of_surjective ((equiv.ulift.surjective_comp x).mpr h)

[Antoine Chambert-Loir]

At least, it doesn't require to add some external lemmas. (Which I find structurally interesting to have, anyway…)

[Antoine Chambert-Loir]

One question about my proof : Is there another way than adding “rfl-lemmas” to rewrite a term to semething else? What is the canonical way to do it in Lean/mathlib ?

[Antoine Chambert-Loir]

(In my case, look at comp_ulift_eq_ulift_comp)

[Eric Rodriguez]

I think comp_ulift_eq_ulift_comp is a bit of a weird lemma, as the end result is you're ulifting to another separate universe (look at pp.universes - you have <4> universe variables there)

[Antoine Chambert-Loir]

Isn't it normal ? I am not sure I understand completely how to interpret what VSCode writes, but equiv.ulift hides its arguments and before unification takes place, one cannot guess which universes should be there.

[Eric Rodriguez]

I think this ulifts twice, is what I'm saying; why would you need two free universe params instead of just one?

[Eric Wieser]

It's probably best to write all the universes explicitly for this type of lemma

[Eric Wieser]

To make it clear what you intended

[Antoine Chambert-Loir]

I just experimented with

-- with universe
lemma comp_ulift_eq_ulift_comp' {f : α → β} :
equiv.ulift.{w v} ∘ (ulift.map.{u v w} f) =
  f ∘ equiv.ulift.{w u} := rfl

that involves only 3 universes. However, it makes the proof of ulift.surjective_iff_surjective etc. break down.

[Eric Wieser]

So what's the four-universe version that lean is inferring?

[Eric Wieser]

(and what universes are α and β in there?)

[Antoine Chambert-Loir]

universes u v
variables {α : Type u} {β : Type v}

set_option pp.universes true

lemma comp_ulift_eq_ulift_comp {f : α → β} : equiv.ulift ∘ (ulift.map f) = f ∘ equiv.ulift := rfl

/-
comp_ulift_eq_ulift_comp.{u_1 u_2 u_3 u_4} :
  ⇑equiv.ulift.{u_4 u_2} ∘ ulift.map.{u_1 u_2 u_3 u_4} ?M_3 = ?M_3 ∘ ⇑equiv.ulift.{u_3 u_1}
-/

[Floris van Doorn]

That seems like the right version to me, but writing explicit universe levels might still be useful for future readers.
Btw, the type of ulift.map is

protected def {u v u_1 u_2} ulift.map : Π {α : Type u} {β : Type v}, (α → β) → ulift.{u_1 u} α → ulift.{u_2 v} β