L の内部における Cantor–Schröder–Bernstein の定理

二つの構成可能集合の間に、両方向の符号化された単射があるとします。このとき、それらの要素型の間には全単射が単に存在します。これが本章で用いる Cantor–Schröder–Bernstein の定理の内部版です。仮定は L の言語で述べられ、得られる全単射は二つの集合を提示する通常の型を比較します。

議論は二つの層にまたがります。L の集合は周囲の累積階層に基礎となる集合をもち、その要素は通常の型 ⟪ fst a ⟫ をなします。符号化された単射は対象理論に属し、これらの要素型の間の関数はメタ理論に属します。

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM; lowerLEM )

module L.CantorBernstein {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import FOL.ZFStructure using ( module hPropStructure )

型の定理を適用するには、各要素型がh-集合でなければなりません。累積階層はすでにこの性質を備えており、二つの要素の間のパスにはそれ以上の高次情報がありません。したがって setPL は、各提示に必要なh-集合の証明を与えます。

open import V.CantorBernstein {ℓ} (lowerLEM lem)
  using ( small-set; module MutualInj )
open import L.Constructible {ℓ} using ( 𝒮ʟ )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.Coding.Injection {ℓ} lem using ( module Small )

単射の符号は、構成可能なグラフ、三つの充足事実、および一つの値域条件からなります。それらは、グラフが一価であり、指定された定義域をもち、単射的であり、各入力を指定された終域へ送ることを述べます。これらの条件から、メタ理論の単射をちょうど復元できます。

open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

open hPropStructure 𝒮ʟ using ( S )
setPL : (a : S) → isSet (⟪ fst a ⟫)

関数 readL がこの移行を行います。a から b への符号化されたグラフを受け取り、a の要素から b の要素への実際の関数と、出力が等しければ入力も等しいという証明を返します。この構成は、先に行った符号化単射の解析から得られます。

setPL a = small-set (fst a)
readL : (a b : S) → Σ[ F ∈ S ] InjCode F a b
      → Σ[ f ∈ (⟪ fst a ⟫ → ⟪ fst b ⟫) ]
          ((x y : ⟪ fst a ⟫) → f x ≡ f y → x ≡ y)
readL a b (F , sv , dm , ij , ran) = SM.small , SM.small-inj

これで抽象的な Cantor–Schröder–Bernstein の議論を具体化できます。対象を構成可能集合、提示をその要素型、単射を符号化されたグラフとします。h-集合の証明と readL が、必要な二つの構造条件を満たします。同じ具体化から、明示的な証人を用いる版と、証人が単に存在する版の両方が得られます。

  where
  module SM = Small F a b sv dm ij ran

module MutualInjL = MutualInj S (λ a → ⟪ fst a ⟫)
  (λ a b → Σ[ F ∈ S ] InjCode F a b) setPL readL
mutual-inj→bijection : (a b : S) → InjL a b → InjL b a

公開される定理は後者を用います。InjL は単射の符号の命題的切り詰めだけを記録するからです。したがって、二つの切り詰められた仮定から、切り詰められた全単射が導かれます。排中律は基礎となる型の証明で Cantor–Schröder–Bernstein 構成の場合分けに用いられます。一意な逆像は単射性とh-集合の条件から復元され、選択原理には依存しません。

  → ∥ Σ[ h ∈ (⟪ fst a ⟫ → ⟪ fst b ⟫) ]
       (((x y : ⟪ fst a ⟫) → h x ≡ h y → x ≡ y)
     × ((y : ⟪ fst b ⟫) → ∥ Σ[ x ∈ ⟪ fst a ⟫ ] (h x ≡ y) ∥₁)) ∥₁
mutual-inj→bijection = MutualInjL.∃bijection