後続基数より小さい順序数をその基数へ単射する

この章を読むか、読書案内と依存マップで別のルートを選べます。

読書案内 · 依存マップ

後続基数は、もとの基数を真に上回る最初の基数です。δ が 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 と一致します。

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 が三分法を得る箇所と、κ より上の分岐が切り詰められた小さい行き先を得る箇所です。