后继基数以下的序数单射到其基数

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

后继基数是严格超过其基数的第一个基数。假设 δ 是 L 内 κ 的后继基数，本章证明每个序数 α ∈ δ 都有到 κ 的内部单射。证明把良基归纳与序数三分法结合起来。排中律有两项明确作用：给出序数三分法；并在 κ ∈ α 的情形，把「α 不是基数」转化为「仅仅存在一个更小的目标」。

{-# 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、序数和内部单射的结构性事实。

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 )

论证在两个结构之间往返。外围层级提供良基的成员关系及其不可反性；可构造宇宙提供序数与基数谓词。序数三分法比较当前序数与 κ，包含关系的编码和单射的传递性则构造并复合所得的内部单射。

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 本身也是命题截断。

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

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

以 SV.S 表示外围层级的论域。成员归纳在这个类型上进行：它的元素是 V 中的集合，此时还没有附带该集合属于 L 的证书。

module SV = hPropStructure 𝒮ᵥ using ( S )

以 SL.S 表示可构造宇宙的论域。它的元素是由外围集合及其可构造性证书组成的依值对；SuccCardL、IsCardinalL 与 InjL 都以这个论域的元素为对象。

module SL = hPropStructure 𝒮ʟ using ( S )

假设 δ 是 κ 的后继基数，并设序数 α 属于 δ。目标 InjL α κ 仅仅断言存在一个从 α 到 κ 的内部单射；这正是「κ 的后继基数以下每个序数的基数都不超过 κ」的形式化表述。

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

良基归纳作用于 α 的底层集合。谓词 P a 恰好补回把外围集合 a 视为当前序数所需的数据：可构造性证书、序数性以及属于 δ 的证明。在这些假设下，它要求从 (a , la) 到 κ 的内部单射。

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 的每个成员处都可用，这恰好是三分法第三个分支所需的条件。

  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 中。

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

考虑 κ ∈ a 的分支。如果 α' 是 L-基数，那么 SuccCardL δ κ 的最小性条款会使 δ 包含于 α'。又因 a ∈ δ，便得到 a ∈ a，与成员关系的不可反性矛盾。因此在这个分支中，α' 不可能是基数。

类型 Ex 以肯定形式表达这里所需的非基数性：仅仅存在某个 γ ∈ α'，使 α' 内部单射到 γ。

    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 应用排中律。若它成立，所需的仅仅见证已经得到；若它被反驳，那么任取成员 γ 以及从 α' 到 γ 的单射都会导出矛盾，这恰好是说序数 α' 为基数的条件。

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

反驳分支与 not-card 矛盾，所以两种结果都给出 Ex。在这一步，排中律给出分支分析；它没有消去截断，也没有选出某个特定的 γ。

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

Ex 的未截断内容给出 γ ∈ a 以及从 α' 到 γ 的内部单射。序数的成员仍是序数，并且 δ 具有传递性，所以 γ 再次满足归纳谓词。归纳假设给出从 γ 到 κ 的单射，再由内部单射的传递性把两者复合。

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

在 γ 处调用归纳假设，需要依次提供 P 的三个条件：γ 的第二分量给出可构造性；由 γ ∈ a 及 a 的序数性得到 γ 的序数性；再由 γ ∈ a ∈ δ 及序数 δ 的传递性得到 γ ∈ δ。

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

三分法的第一个分支是 a ∈ κ。序数具有传递性，所以 a 的每个成员也都是 κ 的成员；把这个包含关系编码起来，就得到从 α' 到 κ 的内部单射。

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

在相等分支中，沿 a ≡ fst κ 搬运同一个包含关系即可得到所需单射。在余下的 κ ∈ a 分支中，把上面得到的截断见证消去到 InjL α' κ；由于 InjL 本身是命题，这个消去是合法的。

    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 用它取得三分法；高于 κ 的分支用它取得截断的小目标。