---
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: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

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

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

宇宙レベル `ℓ` を固定し、`lem : LEM (ℓ-suc ℓ)` を仮定する。この仮定は該当するレベルの各命題に判定を与え、以下の構成の明示的なパラメータとして保たれる。

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

```agda
open import FOL.ZFStructure using ( module hPropView )
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 )
```

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

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

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

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

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ )

open hPropView 𝒮ʟ using ( S )
setPL : (a : S) → isSet (⟪ a .fst ⟫)
```

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

```agda
setPL a = small-set (a .fst)
readL : (a b : S) → Σ[ F ∶ S ] InjCode F a b
      → Σ[ f ∶ (⟪ a .fst ⟫ → ⟪ b .fst ⟫) ]
          ((x y : ⟪ a .fst ⟫) → 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 → ⟪ a .fst ⟫)
  (λ 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 ∶ (⟪ a .fst ⟫ → ⟪ b .fst ⟫) ]
       (((x y : ⟪ a .fst ⟫) → h x ≡ h y → x ≡ y)
     × ((y : ⟪ b .fst ⟫) → ∥ Σ[ x ∶ ⟪ a .fst ⟫ ] (h x ≡ y) ∥₁)) ∥₁
mutual-inj→bijection = MutualInjL.∃bijection
```