---
title: "为序数选取基数代表"
module: L.GCH.CardinalRepresentative
lang: zh
site: "Bedrock"
description: "为序数选取基数代表"
stage: "证明 GCH"
reading_order: 110
canonical: https://bedrock.institute/zh/L.GCH.CardinalRepresentative.html
html: L.GCH.CardinalRepresentative.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/CardinalRepresentative.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Semantics, V.Hierarchy, V.Presentation, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Cardinal, L.WellOrder.Base, L.DefinableInjection, L.InjectionComposition]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.CardinalRepresentative.md, https://bedrock.institute/ja/L.GCH.CardinalRepresentative.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# 为序数选取基数代表

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

固定宇宙层级 `ℓ`，并假设 `lem : LEM (ℓ-suc ℓ)`。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

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

```agda
open import FOL.ZFStructure using ( module hPropView )
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Presentation {ℓ} using ( member; fiber )
open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd; isL; isL-trans )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord )
open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri )
open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL; module LeastCardInjL )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( IsLeast; leastOfFormula; module SWO )
open import L.DefinableInjection {ℓ} lem using ( injLAt; module InjLAt )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
```

`L` 内部的计数以基数表述，而具体构造往往只产生任意序数。对 `L` 中的序数 `α`，本章找出包含于 `α` 的内部基数 `μ`，并给出两个方向的内部单射。因此，`μ` 在模型内部代表 `α` 的基数。构造在 `α` 的后继中搜索，选取 `α` 能够内部单射到的最小序数。

假设在层级 `ℓ-suc ℓ` 上成立排中律。良序搜索与序数三分法都会使用这个假设。结论中的单射全部位于 `L` 内部：它们由可构造的图见证，并非外部函数。

这里同时出现两个结构。外围层级提供成员关系以及搜索所用的小呈现；可构造结构提供序数、基数与内部单射谓词。可构造性沿成员关系向下传递，所以在外围层级中找到的元素可以重新进入 `L` 的论域。

搜索建立在呈现序数的索引良序之上；这个次序与所指元素之间的成员关系一致。包含关系的编码把包含化为内部单射，单射的传递性则复合连续的内部单射。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( sucV )
```

候选集合取为后继 `sucV α`。命题截断表达适当代表的存在，而不在外部选择一个代表；和类型与空类型用于后面的三分法论证。

以 `SV.S` 表示外围集合，以 `SL.S` 表示可构造集合。`SL.S` 的元素由外围集合及其可构造性证书组成。成员关系比较作用于第一分量，而 `InjL` 与 `IsCardinalL` 以完整的可构造元素为对象。

```agda
open hPropView 𝒮ᵥ using ( _∈ˢ_ )
module SV = hPropView 𝒮ᵥ using ( S )
module SL = hPropView 𝒮ʟ using ( S )
```

给定序数 `α`，定理仅仅断言存在满足五项性质的 `μ`：`μ` 是序数，是内部基数，满足 `μ ⊆ α`，并且存在内部单射 `α ↪ μ` 与 `μ ↪ α`。截断使整个结论成为命题。

```agda
cardOf :
    (α : SL.S) → IsOrd (α .fst)
  → ∥ Σ[ μ ∶ SL.S ]
       ( IsOrd (μ .fst) × IsCardinalL μ
```

最终见证由代表 `μ` 与下面构造的五项证明组成。由于目标已经截断，只要这些分量齐备，放入这个依值对即可完成定理。

```agda
       × ((z : SV.S) → ⟨ z ∈ˢ μ .fst ⟩ → ⟨ z ∈ˢ α .fst ⟩)
       × InjL α μ × InjL μ α ) ∥₁
```

关于 `α` 的辅助搜索准备提供后继的可构造性、指名 `α` 自身的索引及相应等式，还提供呈现索引上的良序 `w`。`w` 的次序关系就是所指序数之间的成员关系。

```agda
cardOf α oα = ∣ μ , oμ , cardμ , μ⊆α , α↪μ , μ↪α ∣₁
  where
  module LC = LeastCardInjL α oα using ( hSucα; self; self-eq; w; w-lt )
```

令 `T` 为序数 `α` 的底层集合的后继。后继仍是序数，因此 `T` 的每个元素都是序数，搜索全程都可使用由成员关系给出的次序。

```agda
  T : SV.S
  T = sucV (α .fst)

  oT : IsOrd T
  oT = suc-ord oα
```

集合 `T` 是可构造的。这个证书不可或缺，因为搜索索引最初只指名 `T` 的外围元素；可构造性的向下封闭把该元素化为 `SL.S` 的元素。

```agda
  opaque
    hT : ⟨ isL T ⟩
    hT = LC.hSucα
```

对 `T` 的呈现索引 `b`，`upL b` 把所指元素与其可构造性证明配成依值对。后一个证明由该元素属于 `T` 以及 `T` 的可构造性得到。

```agda
  upL : ⟪ T ⟫ → SL.S
  upL b = ⟪ T ⟫↪ b , isL-trans (member T b) hT
  Good : ⟪ T ⟫ → hProp (ℓ-suc ℓ)
  Good b = InjL α (upL b) , squash₁

  definedGood : FOL.Semantics.FormulaPredicate 𝒮ʟ ⟪ T ⟫ SL.S id Good
  definedGood = FOL.Semantics.presented 2 (injLAt zero (suc zero))
    (λ b → α ∷ upL b ∷ [])
    (λ b → ⇔toPath
      (InjLAt.fill zero (suc zero) (α ∷ upL b ∷ []))
      (InjLAt.read zero (suc zero) (α ∷ upL b ∷ [])))
```

若存在从 `α` 到索引 `b` 所指可构造元素 `upL b` 的内部编码单射，就称 `b` 为好索引。包 `definedGood` 通过 `injLAt` 显露这个性质：两个环境槽分别放入 `α` 与 `upL b`，而 `InjLAt.fill` 和 `InjLAt.read` 证明语义的两个方向。因此，后续最小元搜索看到的是一条固定的对象语言公式，而不是任意宿主谓词。

```agda
  selfGood : ⟨ Good LC.self ⟩
  selfGood = inclusion-coded α α (λ z z∈α → z∈α)

  nonempty : ∥ Σ[ b ∶ ⟪ T ⟫ ] ⟨ Good b ⟩ ∥₁
  nonempty = ∣ LC.self , selfGood ∣₁
```

指名 `α` 的索引是好的：它所指元素等于 `α`，恒等包含则编码出从 `α` 到自身的内部单射。因此，好索引的类型仅仅非空。

```agda
  least : Σ[ b ∶ ⟪ T ⟫ ] IsLeast LC.w Good b
  least = leastOfFormula LC.w definedGood lem nonempty

  m : ⟪ T ⟫
  m = least .fst
```

对良序 `w` 与 `definedGood` 应用面向公式的最小元搜索。排中律判定所展示单射公式的满足关系，非空性保证存在最小的好索引；把它记作 `m`。

```agda
  μ : SL.S
  μ = upL m

  μ∈T : ⟨ μ .fst ∈ˢ T ⟩
  μ∈T = member T m
```

把选中的索引 `m` 提升到可构造论域，并把所得元素记作 `μ`。依定义，`μ` 的底层集合就是 `m` 在 `T` 中指名的元素。

```agda
  oμ : IsOrd (μ .fst)
  oμ = mem-ord {A = T} oT (μ .fst) μ∈T
```

呈现定理给出 `μ ∈ T`。由于 `T` 是序数，其每个元素仍是序数，所以 `μ` 具有所需的序数性。

```agda
  α↪μ : InjL α μ
  α↪μ = (least .snd) .fst
```

最小索引的合格性如今直接表述为由公式定义的命题 `InjL α μ`，因为 `μ` 正是 `m` 指名的可构造元素。因此，选中的候选立即给出正向单射。

```agda
  cardμ : IsCardinalL μ
  cardμ δ δ∈μ μ↪δ = (least .snd) .snd b bGood b<m
    where
    δ∈T : ⟨ δ .fst ∈ˢ T ⟩
    δ∈T = oT .fst {x = μ .fst} {y = δ .fst} δ∈μ μ∈T
```

为证明 `μ` 是基数，假设某个元素 `δ ∈ μ` 允许内部单射 `μ ↪ δ`。序数 `T` 的传递性给出 `δ ∈ T`，于是 `T` 的呈现产生一个指名 `δ` 的索引 `b`。

```agda
    b : ⟪ T ⟫
    b = fiber T δ∈T .fst
    bδ : ⟪ T ⟫↪ b ≡ δ .fst
```

纤维定理同时给出索引 `b` 以及把它所指元素识别为 `δ` 的等式。这些数据使成员关系与单射陈述可以在索引元素和可构造元素 `δ` 之间搬运。

```agda
    bδ = fiber T δ∈T .snd
    bS : upL b ≡ δ
    bS = Σ≡Prop (λ x → (isL x) .snd) bδ
    bGood : ⟨ Good b ⟩
    bGood = subst (InjL α) (sym bS) (injl-trans α μ δ α↪μ μ↪δ)
```

索引 `b` 是好的：把 `α ↪ μ` 与假设的 `μ ↪ δ` 复合，再用纤维等式匹配索引所指的元素。于是 `b` 是同一次搜索中的另一个候选。

```agda
    b<m : let module W = SWO LC.w in b W.<∙ m
    b<m = transport (λ i → sym (LC.w-lt b m) i)
            (subst (λ z → ⟨ z ∈ˢ μ .fst ⟩) (sym bδ) δ∈μ)
```

而且 `b < m`。良序 `w` 的关系就是所指序数之间的成员关系，假设 `δ ∈ μ` 搬运后恰好给出这个比较。最小好索引之下不可能再有好索引，所以这样的单射 `μ ↪ δ` 不存在；因此 `μ` 是内部基数。

```agda
  μ⊆α : (z : SV.S) → ⟨ z ∈ˢ μ .fst ⟩ → ⟨ z ∈ˢ α .fst ⟩
  μ⊆α = go (ord-tri (μ .fst) oμ (α .fst) oα)
    where
    go : Tri (μ .fst) (α .fst) → (z : SV.S) → ⟨ z ∈ˢ μ .fst ⟩ → ⟨ z ∈ˢ α .fst ⟩
```

还需证明 `μ ⊆ α`。序数三分法比较二者的底层序数。若 `μ ∈ α`，由 `α` 的传递性得到包含；若 `μ = α`，沿等式搬运即可。

```agda
    go (inl μ∈α)       z z∈μ = oα .fst z∈μ μ∈α
    go (inr (inl e))   z z∈μ = subst (λ v → ⟨ z ∈ˢ v ⟩) e z∈μ
```

第三种情形 `α ∈ μ` 与最小性矛盾。指名 `α` 的索引是好的，而 `α ∈ μ` 表明这个索引在良序 `w` 中严格位于 `m` 之前。因此只剩三分法的前两种情形。

```agda
    go (inr (inr α∈μ)) z z∈μ =
      ⊥₀-rec ((least .snd) .snd LC.self selfGood
        (transport (λ i → sym (LC.w-lt LC.self m) i)
          (subst (λ v → ⟨ v ∈ˢ μ .fst ⟩) (sym LC.self-eq) α∈μ)))
```

包含 `μ ⊆ α` 编码出内部单射 `μ ↪ α`。连同 `α ↪ μ` 以及 `μ` 的序数性和基数性，这就完成了所承诺的代表。此后关于序数大小的论证可以在不离开 `L` 的前提下转到这个内部基数上。

```agda
  μ↪α : InjL μ α
  μ↪α = inclusion-coded μ α μ⊆α
```

代表 `μ` 是一个序数基数；它可以内部单射到 `α`，`α` 也可以内部单射到它，并且包含于 `α`。由此，任意可构造序数上的基数算术都可以化归为内部基数上的基数算术。