Cardinal.lift_mk_le_lift_mk_of_surjective

Stream: Is there code for X?

[Jz Pan]

Do we have this?

import Mathlib.SetTheory.Cardinal.Basic
import Mathlib.Logic.Function.Basic

universe u v

-- TODO: should not use classical
-- TODO: move to suitable place
theorem _root_.Cardinal.lift_mk_le_lift_mk_of_surjective {α : Type u} {β : Type v} {f : α → β}
    (hf : Function.Surjective f) :
    Cardinal.lift.{u} (Cardinal.mk β) ≤ Cardinal.lift.{v} (Cardinal.mk α) :=
  Cardinal.lift_mk_le_lift_mk_of_injective (Function.injective_surjInv hf)

I have this quick and dirty proof, which uses classical (i.e. axiom of choice). Are there proofs without using classical? Should this be added to mathlib?

[Ruben Van de Velde]

Do you have a purpose in not using classical besides "not using classical"?

[Ruben Van de Velde]

But this seems reasonable to add

[Jz Pan]

Ruben Van de Velde said:

Do you have a purpose in not using classical besides "not using classical"?

No. I just think that such fundamental result should be provable without using choice, but maybe I'm wrong.

[Edward van de Meent]

since ordering on cardinals (in mathlib) is defined with existence of injective maps, i think this might not be provable without axiom of choice?

[Edward van de Meent]

because afaik constructing an injective map a -> b from a surjective map b -> a can't be done without axiom of choice? i could be wrong though

[Jz Pan]

Edward van de Meent said:

since ordering on cardinals (in mathlib) is defined with existence of injective maps, i think this might not be provable without axiom of choice?

OK I see. So it's fine using choice to prove this?

[Edward van de Meent]

absolutely. there was never anything wrong with it to begin with

[Kevin Buzzard]

The statement "every surjection has a one-sided injective inverse" is, in set theory, equivalent to the axiom of choice.

[Edward van de Meent]

right. it's just the "one-sided inverse" part that we don't need, so this statement might be slightly weaker

[Jz Pan]

PR created as #13397.

[Kevin Buzzard]

Right, but this is evidence that choice is highly important in this domain so should be used when necessary. IIRC there's a model of ZF and two sets A,B with an injection from A to B and a surjection, but no bijection.

[Jz Pan]

Let me check the proof of docs#Cardinal.mk_le_of_surjective which already in mathlib but is same-universe version.

[Ruben Van de Velde]

I highly recommend not spending time on this

[Jz Pan]

It uses docs#Function.Embedding.ofSurjective which said that

A right inverse surjInv of a surjective function as an Embedding.

So basically it is the same proof which uses docs#Function.surjInv

[Andrew Yang]

According to this mse, whether this implies AC is open (at least it was 10+years ago).

[Kevin Buzzard]

https://mathoverflow.net/questions/65369/half-cantor-bernstein-without-choice apparently gives a counterexample or two if AC fails sufficiently badly.