Mathlib.SetTheory.Cardinal.SchroederBernstein

Module docstring

{"# Schröder-Bernstein theorem, well-ordering of cardinals

This file proves the Schröder-Bernstein theorem (see schroeder_bernstein), the well-ordering of cardinals (see min_injective) and the totality of their order (see total).

Notes

Cardinals are naturally ordered by α ≤ β ↔ ∃ f : a → β, Injective f: * schroeder_bernstein states that, given injections α → β and β → α, one can get a bijection α → β. This corresponds to the antisymmetry of the order. * The order is also well-founded: any nonempty set of cardinals has a minimal element. min_injective states that by saying that there exists an element of the set that injects into all others.

Cardinals are defined and further developed in the folder SetTheory.Cardinal. "}

Function.Embedding.schroeder_bernstein theorem

 {f : α → β} {g : β → α} (hf : Function.Injective f) (hg : Function.Injective g) : ∃ h : α → β, Bijective h

Full source

/-- **The Schröder-Bernstein Theorem**:
Given injections `α → β` and `β → α`, we can get a bijection `α → β`. -/
theorem schroeder_bernstein {f : α → β} {g : β → α} (hf : Function.Injective f)
    (hg : Function.Injective g) : ∃ h : α → β, Bijective h := by
  classical
  rcases isEmpty_or_nonempty β with hβ | hβ
  · have : IsEmpty α := Function.isEmpty f
    exact ⟨_, ((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm).bijective⟩
  set F : Set α →o Set α :=
    { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ
      monotone' := fun s t hst =>
        compl_subset_compl.mpr <| image_subset _ <| compl_subset_compl.mpr <| image_subset _ hst }
  set s : Set α := F.lfp
  have hs : (g '' (f '' s)ᶜ)ᶜ = s := F.map_lfp
  have hns : g '' (f '' s)ᶜ = sᶜ := compl_injective (by simp [hs])
  set g' := invFun g
  have g'g : LeftInverse g' g := leftInverse_invFun hg
  have hg'ns : g' '' sᶜ = (f '' s)ᶜ := by rw [← hns, g'g.image_image]
  set h : α → β := s.piecewise f g'
  have : Surjective h := by rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]
  have : Injective h := by
    refine (injective_piecewise_iff _).2 ⟨hf.injOn, ?_, ?_⟩
    · intro x hx y hy hxy
      obtain ⟨x', _, rfl⟩ : x ∈ g '' (f '' s)ᶜ := by rwa [hns]
      obtain ⟨y', _, rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
      rw [g'g _, g'g _] at hxy
      rw [hxy]
    · intro x hx y hy hxy
      obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
      rw [g'g _] at hxy
      exact hy' ⟨x, hx, hxy⟩
  exact ⟨h, ‹Injective h›, ‹Surjective h›⟩

Schröder-Bernstein Theorem: Existence of Bijection from Injective Functions

Informal description

Given two injective functions $f \colon \alpha \to \beta$ and $g \colon \beta \to \alpha$, there exists a bijective function $h \colon \alpha \to \beta$.

Function.Embedding.antisymm theorem

: (α ↪ β) → (β ↪ α) → Nonempty (α ≃ β)

Full source

/-- **The Schröder-Bernstein Theorem**: Given embeddings `α ↪ β` and `β ↪ α`, there exists an
equivalence `α ≃ β`. -/
theorem antisymm : (α ↪ β) → (β ↪ α) → Nonempty (α ≃ β)
  | ⟨_, h₁⟩, ⟨_, h₂⟩ =>
    let ⟨f, hf⟩ := schroeder_bernstein h₁ h₂
    ⟨Equiv.ofBijective f hf⟩

Schröder-Bernstein Theorem: Antisymmetry of Cardinal Embeddings

Informal description

Given injective functions (embeddings) $f \colon \alpha \hookrightarrow \beta$ and $g \colon \beta \hookrightarrow \alpha$, there exists a bijection (equivalence) between $\alpha$ and $\beta$, i.e., $\alpha \simeq \beta$ is nonempty.

Function.Embedding.min_injective theorem

[I : Nonempty ι] : ∃ i, Nonempty (∀ j, β i ↪ β j)

Full source

/-- The cardinals are well-ordered. We express it here by the fact that in any set of cardinals
there is an element that injects into the others.
See `Cardinal.conditionallyCompleteLinearOrderBot` for (one of) the lattice instances. -/
theorem min_injective [I : Nonempty ι] : ∃ i, Nonempty (∀ j, β i ↪ β j) :=
  let ⟨s, hs⟩ := show ∃ s, Maximal (· ∈ sets β) s by
    refine zorn_subset _ fun c hc hcc ↦
      ⟨⋃₀ c, fun i x ⟨p, hpc, hxp⟩ y ⟨q, hqc, hyq⟩ hi ↦ ?_, fun _ ↦ subset_sUnion_of_mem⟩
    exact (hcc.total hpc hqc).elim (fun h ↦ hc hqc i (h hxp) hyq hi)
      fun h ↦ hc hpc i hxp (h hyq) hi
  let ⟨i, e⟩ :=
    show ∃ i, Surjective fun x : s => x.val i from
      Classical.by_contradiction fun h =>
        have h : ∀ i, ∃ y, ∀ x ∈ s, (x : ∀ i, β i) i ≠ y := by
          simpa [Surjective] using h
        let ⟨f, hf⟩ := Classical.axiom_of_choice h
        have : f ∈ s :=
          have : insertinsert f s ∈ sets β := fun i x hx y hy => by
            rcases hx with hx | hx <;> rcases hy with hy | hy; · simp [hx, hy]
            · subst x
              exact fun e => (hf i y hy e.symm).elim
            · subst y
              exact fun e => (hf i x hx e).elim
            · exact hs.prop i hx hy
          hs.eq_of_subset this (subset_insert _ _) ▸ mem_insert ..
        let ⟨i⟩ := I
        hf i f this rfl
  ⟨i, ⟨fun j => ⟨s.restrict (fun x => x j) ∘ surjInv e,
    ((hs.1 j).injective).comp (injective_surjInv _)⟩⟩⟩

Existence of Minimal Injective Cardinal in a Nonempty Family

Informal description

Let $\{\beta_i\}_{i \in \iota}$ be a nonempty family of types indexed by $\iota$. Then there exists an index $i_0 \in \iota$ such that for every $j \in \iota$, there exists an injective function from $\beta_{i_0}$ to $\beta_j$.

Function.Embedding.total theorem

(α : Type u) (β : Type v) : Nonempty (α ↪ β) ∨ Nonempty (β ↪ α)

Full source

/-- The cardinals are totally ordered. See
`Cardinal.conditionallyCompleteLinearOrderBot` for (one of) the lattice
instance. -/
-- Porting note: `ULift.{max u v, u} α` was `ULift α`
theorem total (α : Type u) (β : Type v) : NonemptyNonempty (α ↪ β) ∨ Nonempty (β ↪ α) :=
  match @min_injective Bool (fun b => cond b (ULift.{max u v, u} α) (ULift.{max u v, v} β)) ⟨true⟩
    with
  | ⟨true, ⟨h⟩⟩ =>
    let ⟨f, hf⟩ := h false
    Or.inl ⟨Embedding.congr Equiv.ulift Equiv.ulift ⟨f, hf⟩⟩
  | ⟨false, ⟨h⟩⟩ =>
    let ⟨f, hf⟩ := h true
    Or.inr ⟨Embedding.congr Equiv.ulift Equiv.ulift ⟨f, hf⟩⟩

Totality of Cardinal Ordering via Injections

Informal description

For any two types $\alpha$ and $\beta$, there exists either an injective function from $\alpha$ to $\beta$ or an injective function from $\beta$ to $\alpha$.