Choosing a cardinal representative for an ordinal

Fix a universe level ℓ and assume lem : LEM (ℓ-suc ℓ). This hypothesis supplies a decision for each proposition at that level; it remains an explicit parameter of the constructions below.

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

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.

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.

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.

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.

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 hPropView 𝒮ᵥ using ( _∈ˢ_ )
module SV = hPropView 𝒮ᵥ using ( S )
module SL = hPropView 𝒮ʟ 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 = InjL α (upL b) , squash₁

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

Call an index b good when there is an internal coded injection from α to the constructible member upL b that it names. The package definedGood exposes this property through injLAt: its two environment slots contain α and upL b, while InjLAt.fill and InjLAt.read prove the two semantic directions. Thus the later least search sees a fixed object-language formula rather than an arbitrary host predicate.

  selfGood : ⟨ Good LC.self ⟩
  selfGood = 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 = leastOfFormula LC.w definedGood lem nonempty

  m : ⟪ T ⟫
  m = least .fst

Apply the formula-facing least-element search to the well-order w and definedGood. Excluded middle decides satisfaction of the displayed injection formula, 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 α μ
  α↪μ = (least .snd) .fst

Goodness of the least index is now stated directly as the formula-defined proposition InjL α μ, because μ is the constructible member named by m. Thus the selected candidate immediately supplies the forward injection.

  cardμ : IsCardinalL μ
  cardμ δ δ∈μ μ↪δ = (least .snd) .snd 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
    bS : upL b ≡ δ
    bS = Σ≡Prop (λ x → (isL x) .snd) bδ
    bGood : ⟨ Good b ⟩
    bGood = subst (InjL α) (sym bS) (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 : 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δ) δ∈μ)

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

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.