Choosing a cardinal representative for an ordinal

Counting inside L is expressed in terms of cardinals, while a construction often produces an arbitrary ordinal. For an ordinal α of L, this chapter finds an internal cardinal μ contained in α, together with internal injections in both directions. Thus μ represents the cardinality of α inside the model. The representative is obtained by searching the successor of α for the least ordinal into which α internally injects.

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

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

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

Fix excluded middle at level ℓ-suc ℓ. It is used by the well-order search and by ordinal trichotomy. All injections in the conclusion remain internal to L: their graphs are constructible sets rather than external functions.

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 )

Two structures are present. The ambient hierarchy supplies membership and the small presentations used for search. The constructible structure supplies the ordinal, cardinal and internal-injection predicates. Constructibility descends along membership, allowing a member found in the ambient hierarchy to be returned to the carrier of 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 )

The search rests on the well-order of the indices presenting an ordinal. Its order agrees with membership between the represented elements. Inclusion coding turns containment into an internal injection, and transitivity composes successive internal injections.

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

The candidate set is the successor sucV α. Propositional truncation expresses the existence of a suitable representative without choosing one externally; sums and the empty type support the later trichotomy argument.

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₁ )

Write SV.S for ambient sets and SL.S for constructible sets. An element of SL.S pairs an ambient set with its constructibility certificate. Membership comparisons occur on first components, whereas InjL and IsCardinalL concern the complete constructible elements.

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

Given an ordinal α, the theorem merely asserts the existence of μ with five properties: μ is an ordinal, μ is an internal cardinal, μ ⊆ α, and there are internal injections α ↪ μ and μ ↪ α. The truncation makes the conclusion a proposition.

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

The final witness is assembled from the representative μ and the five proofs constructed below. Since the target is truncated, producing this single tuple closes the theorem once its components are available.

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

The auxiliary search setup for α supplies the successor's constructibility, the index naming α itself, the corresponding equality, and a well-order w on the presentation indices. The order relation of w is membership between the named ordinals.

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

Let T be the successor of the underlying ordinal α. The successor is again an ordinal, so every member of T is an ordinal and the order inherited from membership is available throughout the search.

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

  oT : IsOrd T
  oT = suc-ord oα

The set T is constructible. This certificate is needed because a search index names only an ambient member of T; downward closure of constructibility will turn that member into an element of SL.S.

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

For an index b of the presentation of T, upL b pairs the represented member with its constructibility proof. The latter follows from membership in T and the constructibility of 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₁

Call an index b good when the member it names is the underlying set of some constructible δ and there is an internal injection α ↪ δ. The equality in Good b connects the indexed presentation with the constructible witness; truncation keeps goodness proposition-valued.

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

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

The index naming α is good: its represented member equals α, and the identity inclusion codes an internal injection from α to itself. Hence the type of good indices is merely inhabited.

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

  m : ⟪ T ⟫
  m = fst least

Apply least-element search to the well-order w and the proposition-valued predicate Good. Excluded middle decides goodness, and nonemptiness guarantees a least good index. Denote that index by m.

  μ : SL.S
  μ = upL m

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

Lift the chosen index m to the constructible carrier and call the result μ. By construction its underlying set is the member of T named by m.

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

The presentation theorem gives μ ∈ T. Since T is an ordinal, every member of it is an ordinal; consequently μ is an ordinal as required.

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

Goodness of the least index supplies, under truncation, a constructible δ, an equality between its underlying set and the member named by m, and an injection α ↪ δ. The goal InjL α μ is a proposition, so the truncated witness may be eliminated into it.

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

Transport along the indexed equality shows that δ is included in μ; inclusion coding turns this into an internal injection δ ↪ μ. Composing it with the supplied α ↪ δ proves α ↪ μ.

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

To prove that μ is a cardinal, suppose a member δ ∈ μ admitted an internal injection μ ↪ δ. Transitivity of the ordinal T places δ in T, so its presentation yields an index b.

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

The fibre theorem gives both the index b and the equality identifying its represented member with δ. These data let membership and injection statements be transported between the indexed member and the constructible element δ.

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

The index b is good: compose α ↪ μ with the assumed μ ↪ δ, and use the fibre equality to match the indexed member. Thus b is another candidate in the same search.

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

Moreover b < m. The relation of w is membership between represented ordinals, and the assumed δ ∈ μ transports to precisely this comparison. A good index strictly below the least good index is impossible, so no such injection μ ↪ δ exists. Hence μ is an internal cardinal.

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

It remains to show μ ⊆ α. Ordinal trichotomy compares their underlying ordinals. If μ ∈ α, transitivity of α gives the inclusion; if μ = α, transport gives it.

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

The third case α ∈ μ contradicts minimality. The index naming α is good, and the membership α ∈ μ says that this index lies strictly below m in w. Thus only the first two trichotomy cases remain.

    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) α∈μ)))

The inclusion μ ⊆ α codes an internal injection μ ↪ α. Together with α ↪ μ, ordinalhood and cardinality of μ, it completes the promised representative. Any argument about the size of an ordinal may now pass to this internal cardinal without leaving L.

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

The representative μ is an ordinal cardinal internally injectable into α and receiving an internal injection from α, and it lies inside α. This reduces cardinal arithmetic on arbitrary constructible ordinals to cardinal arithmetic on internal cardinals.