## Stream: maths

### Topic: Schroeder-Bernstein

#### Scott Morrison (Sep 13 2019 at 03:46):

There's a stronger version of the Schroeder-Bernstein theorem

theorem schroeder_bernstein {f : α → β} {g : β → α}
(hf : injective f) (hg : injective g) : ∃h:α→β, bijective h := ...


that further promises that for each a : α, either h a = f a, or \exists b : β, g (h a) = a oops, g (h a) = a.

We don't seem to have that form. Does anyone have it in a secret stash, or feels like adding it? :-)

#### Kevin Buzzard (Sep 13 2019 at 03:56):

It follows from the proof! What more do you need? ;-)

#### Mario Carneiro (Sep 13 2019 at 03:59):

I agree with Kevin, it's pretty easy to adapt the proof to get this (also, the exists b should be deleted in that statement)

#### Kevin Buzzard (Sep 13 2019 at 04:06):

(Assuming mathlib used the proof I know ;-) )

#### Alex J. Best (Sep 13 2019 at 04:11):

https://github.com/leanprover-community/mathlib/blob/34d69b5054549f6cc2de9a6311be5cba9c595977/src/data/set/basic.lean#L809

Tldr: image

#### Scott Morrison (Sep 13 2019 at 04:23):

Okay... I'm unlikely to do this myself, but I hope someone does it sometime!

#### Jesse Michael Han (Sep 13 2019 at 16:44):

import order.fixed_points data.set.lattice logic.function logic.embedding order.zorn tactic

open lattice set classical
local attribute [instance] prop_decidable

universes u v

namespace function
namespace embedding

variables {α : Type u} {β : Type v}

theorem schroeder_bernstein' {f : α → β} {g : β → α}
(hf : injective f) (hg : injective g) : ∃ h : α → β, bijective h ∧ ∀ {a}, h a = f a ∨ g (h a) = a :=
let s : set α := lfp $λs, - (g '' - (f '' s)) in have hs : s = - (g '' - (f '' s)), from lfp_eq$ assume s t h,
compl_subset_compl.mpr $image_subset _$
compl_subset_compl.mpr $image_subset _ h, have hns : - s = g '' - (f '' s), from lattice.neg_eq_neg_of_eq$ by simp [hs.symm],

let g' := λa, @inv_fun β ⟨f a⟩ α g a in
have g'g : g' ∘ g = id,
from funext $assume b, @left_inverse_inv_fun _ ⟨f (g b)⟩ _ _ hg b, have hg'ns : g' '' (-s) = - (f '' s), by rw [hns, ←image_comp, g'g, image_id], let h := λa, if a ∈ s then f a else g' a in have h '' univ = univ, from calc h '' univ = h '' s ∪ h '' (- s) : by rw [←image_union, union_compl_self] ... = f '' s ∪ g' '' (-s) : congr (congr_arg (∪) (image_congr$ by simp [h, if_pos] {contextual := tt}))
(image_congr \$ by simp [h, if_neg] {contextual := tt})
... = univ : by rw [hg'ns, union_compl_self],
have surjective h,
from assume b,
have b ∈ h '' univ, by rw [this]; trivial,
let ⟨a, _, eq⟩ := this in
⟨a, eq⟩,

have split : ∀x∈s, ∀y∉s, h x = h y → false,
from assume x hx y hy eq,
have y ∈ g '' - (f '' s), by rwa [←hns],
let ⟨y', hy', eq_y'⟩ := this in
have f x = y',
from calc f x = g' y : by simp [h, hx, hy, if_pos, if_neg] at eq; assumption
... = (g' ∘ g) y' : by simp [(∘), eq_y']
... = _ : by simp [g'g],
have y' ∈ f '' s, from this ▸ mem_image_of_mem _ hx,
hy' this,
have injective h,
from assume x y eq,
by_cases
(assume hx : x ∈ s, by_cases
(assume hy : y ∈ s, by simp [h, hx, hy, if_pos, if_neg] at eq; exact hf eq)
(assume hy : y ∉ s, (split x hx y hy eq).elim))
(assume hx : x ∉ s, by_cases
(assume hy : y ∈ s, (split y hy x hx eq.symm).elim)
(assume hy : y ∉ s,
have x ∈ g '' - (f '' s), by rwa [←hns],
let ⟨x', hx', eqx⟩ := this in
have y ∈ g '' - (f '' s), by rwa [←hns],
let ⟨y', hy', eqy⟩ := this in
have g' x = g' y, by simp [h, hx, hy, if_pos, if_neg] at eq; assumption,
have (g' ∘ g) x' = (g' ∘ g) y', by simp [(∘), eqx, eqy, this],
have x' = y', by rwa [g'g] at this,
calc x = g x' : eqx.symm
... = g y' : by rw [this]
... = y : eqy)),

by {refine ⟨h, ⟨⟨‹injective h›, ‹surjective h›⟩,_⟩⟩,
{ intro a, by_cases Ha : a ∈ s,
{ left, dsimp [h], simp [Ha] },
{ right, dsimp [h], rw (if_neg ‹_›), apply inv_fun_eq,
have Ha' : a ∈ -s := by rwa set.mem_compl_eq, finish }}}

end embedding
end function


#### Jesse Michael Han (Sep 13 2019 at 16:47):

i'm not a fan of huge proofs like this

is it worse to define auxiliary constructions and lemmas as private declarations in a separate section?

#### Scott Morrison (Sep 13 2019 at 23:08):

Yes, I was surprised how monolithic this proof was, and I think it's definitely better style to break out intermediate lemmas and constructions. Ideally one would have been able to prove this stronger version of SB just by adding some lemmas, not having to break into the old proof.

#### Scott Morrison (Sep 13 2019 at 23:09):

I don't think the intermediate results even need to be private.

#### David Michael Roberts (Sep 14 2019 at 10:41):

You could prove the Knaster-Tarski theorem first (https://ncatlab.org/nlab/show/fixed+point#knastertarski_theorem), then CBS, as in https://ncatlab.org/nlab/show/Cantor-Schroeder-Bernstein+theorem#proof (interestingly, this still constructs the same bijection, which has the properties Scott wanted above)

#### David Michael Roberts (Sep 14 2019 at 10:43):

There's also some deep discussion here: https://golem.ph.utexas.edu/category/2014/12/a_categorical_understanding_of.html

#### Jesse Michael Han (Sep 14 2019 at 14:38):

i thought this proof did use tarski-knaster, in the guise of lfp

#### David Michael Roberts (Sep 17 2019 at 21:35):

Oh, I see. I didn't read through it :sweat:

Last updated: May 09 2021 at 11:09 UTC