---
title: "后继基数以下的序数单射到其基数"
module: L.GCH.BelowSuccessorCardinal
lang: zh
site: "Bedrock"
description: "后继基数以下的序数单射到其基数"
stage: "证明 GCH"
reading_order: 108
canonical: https://bedrock.institute/zh/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/ja/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` 相配，因为 `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` 用它取得三分法；高于 `κ` 的分支用它取得截断的小目标。