---
title: "L の内部における Cantor–Schröder–Bernstein の定理"
module: L.CantorBernstein
lang: ja
site: "Bedrock"
description: "L の内部における Cantor–Schröder–Bernstein の定理"
stage: "順序数，単射，基数"
reading_order: 94
canonical: https://bedrock.institute/ja/L.CantorBernstein.html
html: L.CantorBernstein.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/CantorBernstein.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.CantorBernstein, L.Constructible, L.Cardinal, L.Coding.Injection]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.CantorBernstein.md, https://bedrock.institute/zh/L.CantorBernstein.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L の内部における Cantor–Schröder–Bernstein の定理

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

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

```agda
{-# 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-集合の証明を与えます。

```agda
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 )
```

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

```agda
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` の要素への実際の関数と、出力が等しければ入力も等しいという証明を返します。この構成は、先に行った符号化単射の解析から得られます。

```agda
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` が、必要な二つの構造条件を満たします。同じ具体化から、明示的な証人を用いる版と、証人が単に存在する版の両方が得られます。

```agda
  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-集合の条件から復元され、選択原理には依存しません。

```agda
  → ∥ Σ[ 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
```