Zulip Chat Archive

Stream: maths

Topic: Schroeder-Bernstein


view this post on Zulip 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? :-)

view this post on Zulip Kevin Buzzard (Sep 13 2019 at 03:56):

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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Sep 13 2019 at 04:06):

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

view this post on Zulip Keeley Hoek (Sep 13 2019 at 04:08):

what does '' mean in e.g. https://github.com/leanprover-community/mathlib/blob/b5b40c749f2f581778e5d72907eca1aa663962b1/src/set_theory/schroeder_bernstein.lean

view this post on Zulip Alex J. Best (Sep 13 2019 at 04:11):

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

view this post on Zulip Alex J. Best (Sep 13 2019 at 04:12):

Tldr: image

view this post on Zulip Scott Morrison (Sep 13 2019 at 04:23):

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

view this post on Zulip 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 : xs, ys, 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 13 2019 at 23:09):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Jesse Michael Han (Sep 14 2019 at 14:38):

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

view this post on Zulip 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