measurable Cantor-Schroeder-Bernstein

Stream: maths

[Felix Weilacher]

I recently wrote up what I think is a nice fact: that the Cantor-Schroeder-Bernstein theorem holds for measurable embeddings and measurable equivalences:

variables {α β : Type*}
variables [measurable_space α] [measurable_space β]
noncomputable
def schroeder_bernstein {f : α → β} {g : β → α}
  (hf : measurable_embedding f)(hg : measurable_embedding g) : (α ≃ᵐ β)

You can see the proof here. (There are some unrelated sorry's in the first half of the file which this proof does not depend on.) My goal is to prove the Borel isomorphism theorem : Two Polish spaces are Borel isomorphic iff they have the same cardinality. This is now almost complete.

[Rémy Degenne]

@Felix Weilacher this is great! I hope you are planning to PR the Borel isomorphism theorem to mathlib. I am currently writing code about transition kernels and regular conditional probability, and a big missing piece is the first step of some proofs: "we can wlog prove the result when the space is [0,1]."

[Felix Weilacher]

@Rémy Degenne Thank you! I will PR this stuff once I learn how that process works. In the meantime, the theorem is now done. You can see the two main statements here. They are:

variables {α β : Type*}
variables [measurable_space α] [topological_space α] [borel_space α] [polish_space α]
variables [measurable_space β] [topological_space β] [borel_space β] [polish_space β]

theorem borel_equiv_of_uncountable (ha : ¬countable α) (hb : ¬countable β)
  : nonempty (α ≃ᵐ β)

theorem borel_equiv_iff_equiv : nonempty (α ≃ᵐ β) ↔ nonempty (α ≃ β)

(Note the first statement is not obviously generalized by the second)

[Yaël Dillies]

Should we make an uncountable class by the way?

[Kevin Buzzard]

We have empty, nonempty, and finite classes. Do we have an infinite class? Do we have a countable class? I remember people discussing encodable but I don't remember the decisions. If we have most or all of these then I guess it's a natural continuation of what we have.

[Yaël Dillies]

docs#countable, docs#infinite

[Kevin Buzzard]

If these things are all classes then it looks like an uncountable class is a natural extension I guess.

[Kalle Kytölä]

Rémy Degenne said:

Felix Weilacher this is great! I hope you are planning to PR the Borel isomorphism theorem to mathlib. I am currently writing code about transition kernels and regular conditional probability, and a big missing piece is the first step of some proofs: "we can wlog prove the result when the space is [0,1]."

I also very much hope that Felix will PR the result to mathlib, and I'm moreover super happy to hear that Rémy is working on transition kernels and regular conditional probabilities. Those would enable a huge amount of probability theory to be done in the right way in mathlib.

[Rémy Degenne]

@Kalle Kytölä the work I have on kernels is on branch#RD_kernel, if you want to have a look. There is nothing on disintegration or conditionals for now, so no use of the borel isomorphism theorem either. For now the main result I have in the measure_theory/measure/kernel file is the construction of the composition of two s-finite kernels.

[Bolton Bailey]

I seem to recall that the pea/sun version of the Banach-Tarski paradox uses yet another version of Cantor-Schroder-Bernstein - If A is equidecomposable with a subset of B and B is equidecomposable with a subset of A then A and B are equidecomposable. Is there some more general principle at play?

[Felix Weilacher]

Bolton Bailey said:

I seem to recall that the pea/sun version of the Banach-Tarski paradox uses yet another version of Cantor-Schroder-Bernstein - If A is equidecomposable with a subset of B and B is equidecomposable with a subset of A then A and B are equidecomposable. Is there some more general principle at play?

I think this one comes down to the fact that if f and g are the injections in the assumptions of CSB, then the bijection one builds is a subset of f union g^{-1}

[Felix Weilacher]

another way to say this is that if G is bipartite graph with bipartition {A,B}, and there is a matching from A to B and a matching from B to A, then there is a perfect matching of G.