Schroeder-Bernstein

Stream: maths

[Scott Morrison]

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]

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

[Mario Carneiro]

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]

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

[Keeley Hoek]

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

[Alex J. Best]

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

[Alex J. Best]

Tldr: image

[Scott Morrison]

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

[Jesse Michael Han]

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]

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]

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]

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

[David Michael Roberts]

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]

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

[Jesse Michael Han]

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

[David Michael Roberts]

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