Surjective function from Type u to some `α :Type u`

Stream: Is there code for X?

[Robert Maxton]

"Clearly", I claim, there must exist some surjective function from all of Type u to any specific α : Type u. But I'm having a bear of a time coming up with a construction. I can make it work by importing Cardinal, though even then it's less clean than I'd like:

import Mathlib.SetTheory.Cardinal.Arithmetic

lemma exists_surj {α : Type u} [Inhabited α] : ∃ (f : Type u → α), f.Surjective := by
  suffices #{ f : Type u → α | f.Surjective } ≠ 0 by
    simpa [mk_eq_zero_iff]
  intro h
  rw [mk_surjective_eq_zero_iff_lift] at h
  contrapose! h
  simp only [ne_eq, mk_ne_zero, not_false_eq_true, imp_self, and_true]
  suffices IsEmpty {f : α → Type u // f.Surjective} by
    erw [← mk_eq_zero_iff, mk_surjective_eq_zero_iff_lift] at this
    simp at this; exact le_of_lt this
  rw [isEmpty_iff]
  rintro ⟨f, hf⟩
  exact Function.not_surjective_Type f hf

... which I'm moderately okay with, since this is fundamentally a size argument: Type u is much bigger than any specific Type u, so of course there's a surjective function. But surely there's something cleaner than this? It feels just a step away from Cantor, but it's a step I don't quite see.

[Robert Maxton]

I suppose it boils down to: what's the cleanest way to show that for any two sets, there exists a surjective function in at least one direction?

[Matt Diamond]

I wonder if docs#Function.Embedding.total could help here (by proving an injection in the reverse direction and then getting the surjection from that)

[Matt Diamond]

it just says "for any two types, there must be an injection going from one of them to the other"

[Matt Diamond]

also it sounds like you want to prove it in a specific direction, so maybe that's not so helpful...

[Matt Diamond]

here's one approach:

import Mathlib.SetTheory.Cardinal.SchroederBernstein

lemma exists_surj {α : Type u} [Inhabited α] : ∃ (f : Type u → α), f.Surjective := by
  have h : ¬Nonempty (Type u ↪ α) := by
    have : ¬∃ (g : α → Type u), g.Surjective := by
      intro ⟨g, hg⟩
      exact Function.not_surjective_Type g hg
    simpa [Function.exists_surjective_iff]
  have ⟨g, hg⟩ := (Function.Embedding.total _ _).resolve_left h
  use Function.invFun g, Function.invFun_surjective hg

[Robert Maxton]

Oh hey. Yes, that does clean up the lemma a bunch, thanks~

[Mario Carneiro]

But surely there's something cleaner than this? It feels just a step away from Cantor, but it's a step I don't quite see.

I think the core theorem you want here (which does not use cardinals) is docs#Function.not_surjective_Type, used in Matt's proof above.

[Mario Carneiro]

and indeed it is one step away from cantor - it's literally the following theorem :grinning_face_with_smiling_eyes:

[Robert Maxton]

Ha! Indeed it is. But also, see my original proof, which uses it as well -- but I don't see a way to get from "no surjective (α : Type u) → Type u" to "yes surjective Type u → (α : Type u)" without a cardinality argument.

[Matt Diamond]

right, which is why I suggested docs#Function.Embedding.total ... I guess the question is whether or not that lemma relies on a cardinality argument

[Robert Maxton]

... Huh. Apparently not, to my surprise; it's imported by Cardinal.Basic. Alright, neat, no further remarks! :p