Zulip Chat Archive

Stream: maths

Topic: The cardinal `#(Type u)`


Mario Carneiro (Feb 25 2022 at 17:27):

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 (Feb 25 2022 at 17:29):

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

Floris van Doorn (Feb 25 2022 at 17:51):

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 (Feb 25 2022 at 18:05):

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 (Feb 25 2022 at 18:06):

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

Eric Wieser (Feb 25 2022 at 18:07):

(those should be defs)

Floris van Doorn (Feb 25 2022 at 18:07):

I guess :-)

Gabriel Ebner (Feb 25 2022 at 18:07):

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 (Feb 25 2022 at 18:14):

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

Gabriel Ebner (Feb 25 2022 at 18:14):

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

Floris van Doorn (Feb 25 2022 at 18:15):

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

Junyan Xu (Feb 25 2022 at 18:15):

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 (Feb 25 2022 at 18:27):

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

Kevin Buzzard (Feb 25 2022 at 18:37):

And impossibility of Type : Type then follows, right?

Junyan Xu (Feb 25 2022 at 18:44):

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

Junyan Xu (Feb 25 2022 at 19:02):

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 (Feb 25 2022 at 19:35):

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 (Feb 25 2022 at 19:59):

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 (Feb 25 2022 at 20:02):

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 (Feb 26 2022 at 01:48):

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

François G. Dorais (Jul 24 2022 at 10:47):

Linked: Cardinality of Type in a given universe


Last updated: Dec 20 2023 at 11:08 UTC