---
title: "後続基数より小さい順序数をその基数へ単射する"
module: L.GCH.BelowSuccessorCardinal
lang: ja
site: "Bedrock"
description: "後続基数より小さい順序数をその基数へ単射する"
stage: "GCH の証明"
reading_order: 108
canonical: https://bedrock.institute/ja/L.GCH.BelowSuccessorCardinal.html
html: L.GCH.BelowSuccessorCardinal.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/BelowSuccessorCardinal.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Cardinal, L.InjectionComposition]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.BelowSuccessorCardinal.md, https://bedrock.institute/zh/L.GCH.BelowSuccessorCardinal.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 後続基数より小さい順序数をその基数へ単射する

後続基数は、もとの基数を真に上回る最初の基数です。`δ` が `L` の中で `κ` の後続基数であると仮定します。本章では、任意の順序数 `α ∈ δ` から `κ` への内部単射があることを証明します。証明は整礎帰納法と順序数の三分法を組み合わせます。排中律には二つの明確な役割があります。順序数の三分法を与えることと、`κ ∈ α` の場合に、`α` が基数でないことを、より小さい行き先が単に存在するという形へ変えることです。

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

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

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

宇宙レベルを一つ固定し、階層で使われる命題のレベルにおける排中律を仮定します。この古典的仮定は明示され、そのレベルも正確に定められています。証明では、まず順序数の三分法を通して使い、後に `Ex` を直接判定するためにもう一度使います。残りの材料は `V`、`L`、順序数、内部単射についての構造的事実です。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV; ∈-irrefl )
open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd; isL )
open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri )
```

議論は二つの構造の間を行き来します。周囲の階層は整礎的な所属関係とその非反射性を与え、構成可能宇宙は順序数と基数の述語を与えます。順序数の三分法が現在の順序数と `κ` を比較し、包含の符号化と単射の推移性が内部単射を構成して合成します。

```agda
open import L.Cardinal {ℓ} lem using ( InjL; SuccCardL; IsCardinalL )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )

open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
```

例外となる分岐が与えるのは、切り詰められた証人だけです。そのため、証明は和型と空型で判定を場合分けし、命題的切り詰めで単なる存在を表し、整礎帰納法で所属関係を降ります。これらの論理形式は、命題的に切り詰められた結論 `InjL` と一致します。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
import Cubical.Induction.WellFounded as WF

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
```

周囲の階層の論域を `SV.S` と書きます。所属に関する帰納法はこの型の上で行われます。その要素は `V` の集合であり、この時点では `L` に属する証明をまだ伴いません。

```agda
module SV = hPropStructure 𝒮ᵥ using ( S )
```

構成可能宇宙の論域を `SL.S` と書きます。その要素は、周囲の集合とその構成可能性の証明からなる依存対です。`SuccCardL`、`IsCardinalL`、`InjL` はいずれもこの論域の要素について述べます。

```agda
module SL = hPropStructure 𝒮ʟ using ( S )
```

`δ` が `κ` の後続基数であり、順序数 `α` が `δ` に属すると仮定します。目標 `InjL α κ` は、`α` から `κ` への内部単射が単に存在することを述べます。これは、`κ` の後続基数より小さい順序数の濃度はすべて `κ` 以下である、という主張の正確な形です。

```agda
below-succ-injects :
    (κ δ : SL.S) → SuccCardL δ κ
  → (α : SL.S) → IsOrd (fst α) → ⟨ fst α ∈ˢ fst δ ⟩
  → InjL α κ
```

整礎帰納法は `α` の基礎となる集合に施されます。述語 `P a` は、周囲の集合 `a` を考察中の順序数とみなすために必要なデータ、すなわち構成可能性の証明、順序数であること、`δ` に属することをちょうど補います。これらの仮定のもとで、`(a , la)` から `κ` への内部単射を要求します。

```agda
below-succ-injects κ δ (ordδ , _ , κ∈δ , least) α =
  WF.WFI.induction regularityV {P = P} step (fst α) (snd α)
  where
  P : SV.S → Type (ℓ-suc ℓ)
  P a = (la : ⟨ isL a ⟩) → IsOrd a → ⟨ a ∈ˢ fst δ ⟩ → InjL (a , la) κ
```

`κ ∈ δ` であり `δ` が順序数なので、`κ` 自身も順序数です。したがって帰納段階では、`a` と `κ` の基礎となる集合に順序数の三分法を適用できます。帰納仮定は `a` の各要素で利用でき、これは三分法の第三の分岐が必要とするものです。

```agda
  ordκ : IsOrd (fst κ)
  ordκ = mem-ord {A = fst δ} ordδ (fst κ) κ∈δ

  step : (a : SV.S) → (∀ a' → ⟨ a' ∈ˢ a ⟩ → P a') → P a
  step a ih la orda a∈δ = go (ord-tri a orda (fst κ) ordκ)
    where
```

周囲の集合 `a` と証明 `la` を対にして、`L` の対応する要素 `α'` を得ます。これにより、整礎帰納法は単純な論域 `SV.S` 上で行いながら、濃度に関する主張は本来の論域 `SL.S` で述べられます。

```agda
    α' : SL.S
    α' = a , la
```

`κ ∈ a` の分岐を考えます。もし `α'` が `L`-基数なら、`SuccCardL δ κ` の最小性により `δ` は `α'` に含まれます。`a ∈ δ` なので `a ∈ a` が従い、所属の非反射性に反します。したがってこの分岐では `α'` は基数ではありえません。

型 `Ex` は、ここで必要な非基数性を肯定的に表します。すなわち、`α'` が内部単射するような `γ ∈ α'` が単に存在する、という主張です。

```agda
    not-card : ⟨ fst κ ∈ˢ a ⟩ → IsCardinalL α' → Empty.⊥
    not-card κ∈a c = ∈-irrefl a (least α' orda c κ∈a α' a∈δ)

    Ex : Type (ℓ-suc ℓ)
    Ex = ∥ Σ[ γ ∈ SL.S ] (⟨ fst γ ∈ˢ a ⟩ × InjL α' γ) ∥₁
```

命題 `Ex` に排中律を適用します。成立するなら、必要な単なる証人はすでに得られています。反証されるなら、任意の要素 `γ` と `α'` から `γ` への単射が矛盾を導きます。これは順序数 `α'` が基数であるという条件にほかなりません。

```agda
    some-γ : ⟨ fst κ ∈ˢ a ⟩ → Ex
    some-γ κ∈a = decide (lem (Ex , squash₁))
      where
      decide : Ex ⊎ (Ex → Empty.⊥) → Ex
```

反証の分岐は `not-card` と矛盾するため、どちらの結果からも `Ex` が得られます。この段階で排中律が与えるのは場合分けです。切り詰めを取り除くことも、特定の `γ` を選ぶこともありません。

```agda
      decide (inl e)  = e
      decide (inr ¬e) =
        Empty.rec (not-card κ∈a (λ γ γ∈a inj → ¬e ∣ γ , γ∈a , inj ∣₁))
```

`Ex` の切り詰め前の内容は、`γ ∈ a` と `α'` から `γ` への内部単射からなります。順序数の要素は順序数であり、`δ` は推移的なので、`γ` は再び帰納述語を満たします。帰納仮定が `γ` から `κ` への単射を与え、内部単射の推移性が二つを合成します。

```agda
    from-γ : Σ[ γ ∈ SL.S ] (⟨ fst γ ∈ˢ a ⟩ × InjL α' γ) → InjL α' κ
    from-γ (γ , γ∈a , α↪γ) =
      injl-trans α' γ κ α↪γ
```

`γ` で帰納仮定を使うには、`P` の三つの条件をすべて与えます。構成可能性は `γ` の第二成分であり、順序数であることは `γ ∈ a` と `a` の順序数性から従い、`δ` への所属は `γ ∈ a ∈ δ` と順序数 `δ` の推移性から従います。

```agda
        (ih (fst γ) γ∈a (snd γ)
            (mem-ord {A = a} orda (fst γ) γ∈a)
            (ordδ .fst γ∈a a∈δ))
```

三分法の第一の分岐は `a ∈ κ` です。順序数は推移的なので、`a` の各要素は `κ` の要素でもあります。この包含を符号化すれば、`α'` から `κ` への内部単射が得られます。

```agda
    go : Tri a (fst κ) → InjL α' κ
    go (inl a∈κ)       =
      inclusion-coded α' κ (λ z z∈a → ordκ .fst z∈a a∈κ)
```

等しい場合には、`a ≡ fst κ` に沿って同じ包含を移送すれば、必要な単射が得られます。残る `κ ∈ a` の場合には、先に得た切り詰められた証人を `InjL α' κ` へ消去します。`InjL` 自身が命題なので、この消去は正当です。

```agda
    go (inr (inl e))   =
      inclusion-coded α' κ (λ z z∈a → subst (λ w → ⟨ z ∈ˢ w ⟩) e z∈a)
    go (inr (inr κ∈a)) = PT.rec squash₁ from-γ (some-γ κ∈a)
```

これで順序数の三分法の三つの分岐がすべて閉じます。したがって、後続基数 `δ` より小さい任意の順序数は、その基数 `κ` へ内部単射します。所属の整礎性により、証明は `γ` へ降りられます。排中律は二箇所で使われます。`ord-tri` が三分法を得る箇所と、`κ` より上の分岐が切り詰められた小さい行き先を得る箇所です。