Club guessing

This file formalizes theorem 2.17 in the chapter "Cardinal Arithmetic" in the "Handbook of set theory."

For δ an ordinal, let S ⊆ δ, and f : (α : S) → Club α a function assigning a club to each element of S. Then f is said to be "club guessing" if for every club of δ, C : Club δ, there is some α ∈ S such that f α ⊆ C. That is, f guesses C at α.

There are many existence results on club guessing sequences. The one we need is theorem 2.17: Let Ϟ be an ordinal and let S be a stationary set below Ϟ, such that every element of S has the same cofinality κ. Further assume succ κ < Ϟ.cof. Then there exists a club guessing sequence on S.

Main definitions

• Ordinal.IsClubGuessing {S} f γ says f : (α : S) → Club α is a club guessing sequence for γ. Unlike in the typical definition, we don't assume S ⊆ Iio γ. This makes no mathematical difference but allows us to have IsClubGuessing f γ for many different γ.

Main results

• Ordinal.exists_isClubGuessing_of_cof_uncountable: Let Ϟ be an ordinal and S stationary below Ϟ, such that ∀ α ∈ S, α.cof = κ, for a constant κ satisfying succ κ < Ϟ.cof. Assume also that ℵ₀ < κ. Then there exists f : (α : S) → Club α that is club guessing below Ϟ.

def Ordinal.IsClubGuessing {S : Set Ordinal.{u_1}} (f : (α : ↑S) → (↑α).Club) (γ : Ordinal.{u_1}) : Prop

f : (α : S) → Club α is a club-guessing sequence for γ when every club of γ contains the carrier of f α for some α ∈ S.

Equations

• Ordinal.IsClubGuessing f γ = ∀ (C : γ.Club), ∃ (δ : ↑S), (f δ).carrier ⊆ C.carrier

theorem Ordinal.exists_club_of_not_isClubGuessing {S : Set Ordinal.{u_1}} {γ : Ordinal.{u_1}} (f : (α : ↑S) → (↑α).Club) (h : ¬IsClubGuessing f γ) : ∃ (C : γ.Club), ∀ (δ : ↑S), ¬(f δ).carrier ⊆ ↑C

class Ordinal.ClubGuessing.Assumptions : Type (u + 1)

The assumptions of the theorem and hCont, which says the result is false.

• Ϟ : Ordinal.{u}

  The ambient ordinal Ϟ below which we build the club-guessing sequence.

• κ : Cardinal.{u}

  The common cofinality κ of all elements of the stationary set S.

• hκ : Cardinal.aleph0 < κ

  Hypothesis: κ is uncountable.

• hcof : Order.succ κ < Ϟ.cof

  Hypothesis: succ κ < Ϟ.cof.

• S : Set Ordinal.{u}

  The stationary set on which we build the club-guessing sequence.

• hStat : IsStationary S Ϟ

  Hypothesis: S is stationary below Ϟ.

• hSub : S ⊆ Set.Iio Ϟ

  Hypothesis: S is a subset of Iio Ϟ.

• hS (α : Ordinal.{u}) : α ∈ S → α.cof = κ

  Hypothesis: every element of S has cofinality κ.

• hCont (f : (α : ↑S) → (↑α).Club) : ¬IsClubGuessing f Ϟ

  Contradictory hypothesis used for the proof by contradiction: there is no club-guessing sequence.

instance Ordinal.ClubGuessing.Assumptions.instNonemptyElemIioOrdSuccCardinalκ [assumptions : Assumptions] : Nonempty ↑(Set.Iio (Order.succ κ).ord)

theorem Ordinal.ClubGuessing.Assumptions.isSuccLimit_of_mem_S [assumptions : Assumptions] {α : ↑S} : Order.IsSuccLimit ↑α

theorem Ordinal.ClubGuessing.Assumptions.aleph0_lt_cof_Ϟ [assumptions : Assumptions] : Cardinal.aleph0 < Ϟ.cof

noncomputable def Ordinal.ClubGuessing.Assumptions.f [assumptions : Assumptions] (α : ↑S) : (↑α).Club

A first attempt at a club-guessing sequence: pick an arbitrary club of cardinality κ below each element of S.

Equations

• Ordinal.ClubGuessing.Assumptions.f x✝ = Classical.choose ⋯

noncomputable def Ordinal.ClubGuessing.Assumptions.restrict [assumptions : Assumptions] (E : Ϟ.Club) (α : ↑S) : (↑α).Club

Given a club E of Ϟ not guessed by f, we "force" f to guess E at every point in S that is an accumulation point of E by intersecting every f α with E.

Equations

• Ordinal.ClubGuessing.Assumptions.restrict E α = if h : (↑α).IsAccPt ↑E then { carrier := (Ordinal.ClubGuessing.Assumptions.f α).carrier ∩ ↑E, isClub := ⋯ } else Ordinal.univClub ⋯

noncomputable def Ordinal.ClubGuessing.Assumptions.F [assumptions : Assumptions] : ↑(Set.Iio (Order.succ κ).ord) → Ϟ.Club

The sequence of clubs E_α obtained by repeatedly choosing a club not guessed by the current restriction of f.

Equations

• One or more equations did not get rendered due to their size.

def Ordinal.ClubGuessing.Assumptions.F' [assumptions : Assumptions] : ↑(Set.Iio (Order.succ κ).ord) → Ϟ.Club

Prefix intersections of F.

Equations

• Ordinal.ClubGuessing.Assumptions.F' δ = { carrier := ⋂ (α : ↑(Set.Iio δ)), ↑(Ordinal.ClubGuessing.Assumptions.F ↑α), isClub := ⋯ }

def Ordinal.ClubGuessing.Assumptions.E [assumptions : Assumptions] : Ϟ.Club

The intersection of all clubs F α for α < succ κ.

Equations

• Ordinal.ClubGuessing.Assumptions.E = { carrier := ⋂ (α : ↑(Set.Iio (Order.succ Ordinal.ClubGuessing.Assumptions.κ).ord)), ↑(Ordinal.ClubGuessing.Assumptions.F α), isClub := ⋯ }

noncomputable def Ordinal.ClubGuessing.Assumptions.α [assumptions : Assumptions] : ↑S

Since E is a club and S is stationary, there is some α ∈ S ∩ E'; this is one such witness.

Equations

• Ordinal.ClubGuessing.Assumptions.α = ⟨Classical.choose ⋯, ⋯⟩

theorem Ordinal.ClubGuessing.Assumptions.isAcc_α [assumptions : Assumptions] : (↑α).IsAccPt ↑E

theorem Ordinal.ClubGuessing.Assumptions.isAcc_α_F' [assumptions : Assumptions] (β : ↑(Set.Iio (Order.succ κ).ord)) : (↑α).IsAccPt ↑(F' β)

theorem Ordinal.ClubGuessing.Assumptions.restrict_subset_α [assumptions : Assumptions] (β : ↑(Set.Iio (Order.succ κ).ord)) : restrict (F' β) α ⊆ f α

theorem Ordinal.ClubGuessing.Assumptions.restrict_subset_restrict [assumptions : Assumptions] {C D : Ϟ.Club} (h : C ⊆ D) (ha : (↑α).IsAccPt ↑C) : restrict C α ⊆ restrict D α

theorem Ordinal.ClubGuessing.Assumptions.restrict_not_subset [assumptions : Assumptions] (β : ↑(Set.Iio (Order.succ κ).ord)) : ¬(restrict (F' β) α).carrier ⊆ (F β).carrier

theorem Ordinal.ClubGuessing.Assumptions.restrict_subset [assumptions : Assumptions] {β γ : ↑(Set.Iio (Order.succ κ).ord)} (h : β < γ) : (restrict (F' γ) α).carrier ⊆ (F β).carrier

theorem Ordinal.ClubGuessing.Assumptions.restrict_ssubset_restrict [assumptions : Assumptions] {β γ : ↑(Set.Iio (Order.succ κ).ord)} (h : β < γ) : restrict (F' γ) α ⊂ restrict (F' β) α

theorem Ordinal.ClubGuessing.Assumptions.contradiction [assumptions : Assumptions] : False

theorem Ordinal.exists_isClubGuessing_of_cof_uncountable {Ϟ : Ordinal.{u_1}} {κ : Cardinal.{u_1}} (hκ : Cardinal.aleph0 < κ) (hcof : Order.succ κ < Ϟ.cof) {S : Set Ordinal.{u_1}} (hStat : IsStationary S Ϟ) (hS : ∀ α ∈ S, α.cof = κ) : ∃ (f : (α : ↑S) → (↑α).Club), IsClubGuessing f Ϟ