順序数の基数代表を選ぶ

L の内部での計数は基数によって述べますが、具体的な構成が与えるのは任意の順序数であることが少なくありません。L の順序数 α に対し、本章では α に含まれる内部基数 μ と、両方向の内部単射を構成します。したがって μ はモデルの内部で α の濃度を代表します。この代表は、α の後続の中から、α が内部単射する最小の順序数を探して得られます。

{-# 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 の内部にあり、そのグラフは外部関数ではなく構成可能集合です。

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 の論域へ戻せます。

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 )

探索は、順序数を表示するインデックスの整列順序に基づきます。この順序は、表示される要素の間の所属と一致します。包含の符号化が包含を内部単射に変え、単射の推移性が内部単射を合成します。

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

候補集合は後続 sucV α です。命題的切り詰めは、外部で代表を選ぶことなく適切な代表の存在を表します。和型と空型は後の三分法の議論で使われます。

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 は完全な構成可能要素について述べます。

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
module SV = hPropStructure 𝒮ᵥ using ( S )
module SL = hPropStructure 𝒮ʟ using ( S )

順序数 α に対し、定理は五つの性質を持つ μ が単に存在することを述べます。μ は順序数かつ内部基数で、μ ⊆ α であり、内部単射 α ↪ μ と μ ↪ α があります。切り詰めにより結論全体は命題になります。

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

最終的な証人は、代表 μ と以下で構成する五つの証明からなります。目標は切り詰められているので、成分がそろえばこの一つの依存対を入れることで定理が閉じます。

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

α に対する補助的な探索の準備は、後続の構成可能性、α 自身を名指すインデックスとその等式、表示インデックス上の整列順序 w を与えます。w の順序関係は、名指された順序数の間の所属です。

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

T を、順序数 α の基礎集合の後続とします。後続も順序数なので、T の各要素は順序数であり、探索の全体で所属から得られる順序を使えます。

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

  oT : IsOrd T
  oT = suc-ord oα

集合 T は構成可能です。この証明が必要なのは、探索インデックスが最初に名指すのは T の周囲の要素にすぎず、構成可能性の下方閉性によって初めてその要素を SL.S の要素にできるからです。

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

T の表示インデックス b に対し、upL b は名指された要素とその構成可能性の証明を対にします。後者は、その要素が T に属することと T の構成可能性から従います。

  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 の等式はインデックス表示と構成可能な証人を結び、切り詰めは良さを命題値にします。

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

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

α を名指すインデックスは良いものです。名指された要素は α に等しく、恒等的な包含が α から自身への内部単射を符号化します。したがって良いインデックスの型には単に要素が存在します。

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

  m : ⟪ T ⟫
  m = fst least

整列順序 w と命題値の述語 Good に最小元探索を適用します。排中律が良さを判定し、非空性が最小の良いインデックスを保証します。そのインデックスを m と書きます。

  μ : SL.S
  μ = upL m

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

選んだインデックス m を構成可能な論域へ持ち上げ、その結果を μ と呼びます。定義により、μ の基礎集合は m が T の中で名指す要素です。

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

表示の定理から μ ∈ T が得られます。T は順序数なので、その各要素も順序数です。したがって μ は必要な順序数性を持ちます。

  α↪μ : InjL α μ
  α↪μ = PT.rec squash₁ from (fst (snd least))
    where
    from : Σ[ δ ∈ SL.S ] ((fst δ ≡ ⟪ T ⟫↪ m) × InjL α δ) → InjL α μ

最小インデックスの良さは、切り詰めの下で、構成可能集合 δ、その基礎集合と m が名指す要素との等式、単射 α ↪ δ を与えます。目標 InjL α μ は命題なので、切り詰められた証人をそこへ消去できます。

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

インデックスの等式に沿って移送すると δ が μ に含まれることが分かり、包含の符号化により内部単射 δ ↪ μ を得ます。これを与えられた α ↪ δ と合成して α ↪ μ を証明します。

  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 を与えます。

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

ファイバーの定理は、インデックス b と、その表示要素を δ と同一視する等式を与えます。このデータにより、所属と単射の主張を、インデックスで表された要素と構成可能要素 δ の間で移送できます。

    bδ = fiber T δ∈T .snd
    bGood : ⟨ Good b ⟩
    bGood = ∣ δ , sym bδ , injl-trans α μ δ α↪μ μ↪δ ∣₁

インデックス b は良いものです。α ↪ μ と仮定した μ ↪ δ を合成し、ファイバーの等式でインデックスの表示要素に合わせます。したがって b は同じ探索の別の候補です。

    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 の関係は表示された順序数の間の所属であり、仮定 δ ∈ μ を移送すると、まさにこの比較が得られます。最小の良いインデックスより下に良いインデックスがあることは不可能なので、そのような単射 μ ↪ δ は存在しません。したがって μ は内部基数です。

  μ⊆α : (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 α ⟩

残るのは μ ⊆ α です。順序数の三分法で二つの基礎順序数を比較します。μ ∈ α なら α の推移性から包含が従い、μ = α なら等式に沿う移送で得られます。

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

第三の場合 α ∈ μ は最小性に反します。α を名指すインデックスは良く、α ∈ μ はそのインデックスが w で m より真に小さいことを意味します。したがって三分法の最初の二つの場合だけが残ります。

    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 を離れずにこの内部基数へ移せます。

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

代表 μ は順序数基数であり、α へ内部単射でき、α からも内部単射でき、α の中に含まれます。これにより、任意の構成可能順序数に関する基数算術を、内部基数に関する基数算術へ帰着できます。