---
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, V.Hierarchy, V.Presentation, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Cardinal, L.WellOrder.Base, 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: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 为序数选取基数代表

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

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

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

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

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

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

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

```agda
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; leastOf; module SWO )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
```

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

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

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

```agda
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( inl; inr )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

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

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
module SV = hPropStructure 𝒮ᵥ using ( S )
module SL = hPropStructure 𝒮ʟ 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 = ∥ Σ[ δ ∈ SL.S ] ((fst δ ≡ ⟪ T ⟫↪ b) × InjL α δ) ∥₁ , squash₁
```

若索引 `b` 所指的成员是某个可构造集合 `δ` 的底层集合，并且存在内部单射 `α ↪ δ`，就称 `b` 为好索引。`Good b` 中的等式连接索引呈现与可构造见证，截断则使好索引性取值于命题。

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

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

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

```agda
  least : Σ[ b ∈ ⟪ T ⟫ ] IsLeast LC.w Good b
  least = leastOf LC.w lem Good nonempty

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

对良序 `w` 与命题值谓词 `Good` 应用最小元搜索。排中律判定好索引性，非空性保证存在最小的好索引；把它记作 `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 α μ
  α↪μ = PT.rec squash₁ from (fst (snd least))
    where
    from : Σ[ δ ∈ SL.S ] ((fst δ ≡ ⟪ T ⟫↪ m) × InjL α δ) → InjL α μ
```

最小索引的好索引性在截断之下给出可构造集合 `δ`、其底层集合与 `m` 所指成员之间的等式，以及单射 `α ↪ δ`。目标 `InjL α μ` 是命题，所以可以把截断见证消去到这个目标中。

```agda
    from (δ , e , α↪δ) =
      injl-trans α δ μ α↪δ
        (inclusion-coded δ μ (λ z z∈δ → subst (λ v → ⟨ z ∈ˢ v ⟩) e z∈δ))
```

沿索引等式搬运可知 `δ` 包含于 `μ`；包含关系的编码把它化为内部单射 `δ ↪ μ`。再与已有的 `α ↪ δ` 复合，便得到 `α ↪ μ`。

```agda
  cardμ : IsCardinalL μ
  cardμ δ δ∈μ μ↪δ = snd (snd least) 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
    bGood : ⟨ Good b ⟩
    bGood = ∣ δ , sym bδ , injl-trans α μ δ α↪μ μ↪δ ∣₁
```

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

```agda
    b<m : SWO._<∙_ LC.w b 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∈μ =
      Empty.rec (snd (snd least) 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 μ α μ⊆α
```

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