The cardinal `#(Type u)`

Stream: maths

[Mario Carneiro]

I wanted to do a cardinality proof of the impossibility of Type : Type the other day, and so I would use docs#cardinal.univ ; but this is defined to be #cardinal.{u} or #ordinal.{u}, and there are no theorems relating this to #(Type u). But then I realized: I'm not even sure it is true that these cardinals are the same. What can we say about #(Type u) in lean's type theory? I think that univ.{u} <= #(Type u), since every cardinal has a type representing it and distinct cardinals yield distinct types; but beyond this I think there are very few restrictions. I'm not even sure that #(Type u) is monotonic in u, or upper bounded by #cardinal.{u+37}. I wonder if we can find some analogue of Easton's theorem here.

[Mario Carneiro]

We can prove #Prop = 2 though, constructivists be damned

[Floris van Doorn]

I think they are strictly monotone. Given A : Type u I can embed A into ordinal.{u} and I can embed ordinal.{u} into Type u. Since Type u : Type (u+1) I get Type u ↪ Type (u+1).

[Floris van Doorn]

import set_theory.cardinal_ordinal

universe u
open cardinal
open_locale cardinal
noncomputable theory

attribute [trans] function.embedding.trans
attribute [refl] function.embedding.refl

lemma foo1 (A : Type u) : A ↪ Type u :=
calc A ↪ cardinal.{u} : classical.choice nonempty_embedding_to_cardinal
  ... ↪ Type u :
    ⟨quotient.out, λ c₁ c₂ h, (mk_out c₁).symm.trans $ (congr_arg mk h).trans $ mk_out c₂⟩

lemma foo2 : Type u ↪ Type (u+1) := foo1 (Type u)

[Floris van Doorn]

strict monotonicity is basically foo1 (set (Type u)).

[Eric Wieser]

(those should be defs)

[Floris van Doorn]

I guess :-)

[Gabriel Ebner]

There is this lemma: docs#embedding_to_cardinal

#check @embedding_to_cardinal (Type u)   -- embedding_to_cardinal : Type u ↪ cardinal.{u+1}

I think we should also have cardinal.{u+1} ↪ Type u somewhere.

[Floris van Doorn]

I don't think cardinal.{u+1} ↪ Type u is provable...

[Gabriel Ebner]

Indeed, this only gets me #Type u ≤ #cardinal.{u+1} ≤ #Type (u+1).

[Floris van Doorn]

Yes, that sounds right. I expect we cannot say much more

[Junyan Xu]

seems the proof of https://leanprover-community.github.io/mathlib_docs/set_theory/ordinal.html#nonempty_embedding_to_cardinal is by showing the reverse embedding couldn't exist

[Gabriel Ebner]

Interesting observation, this gives us #Type u < #cardinal.{u+1} ≤ #Type (u+1).

[Kevin Buzzard]

And impossibility of Type : Type then follows, right?

[Junyan Xu]

Yes, if Type u : Type u then #Type u < #cardinal.{u} ≤ #Type u.

[Junyan Xu]

It seems impossible to express this in type theory though; Type u : Type u just won't typecheck. You could show given A : Type u we have (Type u ↪ A) -> false and trivially construct Type u ↪Type u, but you could by no means apply the former to Type u.

[Chris Hughes]

There's this fairly direct proof of Type u ne Type (u+1) which has no ordinals or cardinals involved.

example : ulift.{(u+2)} (Type u) ≠ Type (u+1) :=
begin
  intro h,
  have f : {f : Type u → Type (u + 1) // function.surjective f } ,
  { rw [← h],
    exact ⟨ulift.up, λ T, ⟨T.down, by cases T; refl⟩⟩ },
  let T : Type (u+1) := sigma f.1,
  cases f.2 (set T) with U hU,
  let g : set T ↪ T :=
    ⟨λ s, ⟨U, cast hU.symm s⟩, λ s t, by simp⟩,
  exact function.cantor_injective g.1 g.2
end

[Chris Hughes]

You could probably extract a proof from the above that if A : Type u then A does not surject into Type u which is an okay way to state it.

[Chris Hughes]

example (A : Type u) (f : A → Type u) (hf : function.surjective f) : false :=
begin
  let T : Type u := sigma f,
  cases hf (set T) with U hU,
  let g : set T ↪ T :=
    ⟨λ s, ⟨U, cast hU.symm s⟩, λ s t, by simp⟩,
  exact function.cantor_injective g.1 g.2
end

[Mario Carneiro]

Ooh, I like that last proof, it should go next to cantor_injective

[François G. Dorais]

Linked: Cardinality of Type in a given universe