working with club sets

Stream: new members

[Connor Gordon]

This may already be in the library somewhere, but I am hoping to prove the result that the intersection of two club sets on ω₁ (https://en.wikipedia.org/wiki/Club_set) is club. However, I'm having trouble even getting started with formalizing these definitions (if you think this is a bit ambitious for someone at my level, let me know).

My first goal was to get omega_1 into my code. To do this, I wrote

noncomputable def ω₁ := cardinal.ord (cardinal.aleph 1)

matching the documentation in set_theory.cardinal.ordinal and set_theory.ordinal.basic (as a side note, what does "noncomputable" mean in this context?). Typing #check ω₁ does indeed give something of type ordinal, as one would expect.

Since I'm only interested in subsets of ω₁, it would be great if I could somehow create a type (or some other structure?) of such subsets, but I'm not sure how to do this. Is this possible, and if so, how would I go about it?

Supposing such a type exists, the next thing would be to define notions of is_closed,is_unbounded, and is_club (or perhaps some better naming convention) for subsets of ω₁. These would roughly correspond to the assertions that

is_closed S : (∀ A ⊆ S) (sup A < ω₁ → sup A ∈ A)
is_unbounded S : (∀ α < ω₁) (∃ β ∈ S) α ≤ β
is_club S : is_closed S ∧ is_unbounded S

(pardon the almost certainly incorrect syntax). How would I properly go about implementing these properties?

Should I continue to pursue this project, I'll definitely have more questions, but this seems like a reasonable place to end for now. Thank you so much for your time!

[Junyan Xu]

An ordinal in Lean is an "equivalence class" (implemented via quotient type) of well orders, so one needs docs#quotient.out to get back a type; if o is an ordinal then (quotient.out o).r is a well order on the type (quotient.out o).α with ordinal o (docs#ordinal.type_out), and set (quotient.out o).α is your desired type of subsets. However, (quotient.out o).α is some random type obtained from choice and its elements are not ordinals, and moreover it isn't automatically equipped with the well order (quotient.out o).r so you can't directly use <, which make it hard to work with. So I instead recommend you just use subsets of ordinals (set ordinal) and requiring such a subset to be a subset of ω₁ amounts to requiring it's contained in the left-infinite, right-open interval docs#set.Iio:

import set_theory.cardinal.ordinal

universe u

noncomputable def ω₁ := (cardinal.aleph 1).ord -- using dot notation here

variables (S : set ordinal.{u}) (α : ordinal.{u})

def set.is_subset_of : Prop := S ⊆ set.Iio α
def set.is_closed : Prop := ∀ A ⊆ S, Sup A < α → Sup A ∈ A
def set.is_unbounded : Prop := ∀ β < α, ∃ γ ∈ S, β ≤ γ
def set.is_club : Prop := S.is_subset_of α ∧ S.is_closed α ∧ S.is_unbounded α

[Eric Wieser]

Note that docs#set.unbounded already exists, but maybe that has a different meaning

[Kevin Buzzard]

I would say that these definitions are nothing to do with ordinals and should probably be made much more generally (and indeed might well be there already).

[Connor Gordon]

Thanks for the help! (And the comments about some of this already existing and/or this could/should be made in greater generality have been noted, but I am still rather new to this so I think I'll stick to doing this as-is for now and if I want to add it to mathlib eventually I can implement it in such generality).

With your help, I have managed to formalize the theorem I am trying to prove, and the proof that the intersection of two closed sets is closed. However, I am not really sure how to implement the proof of unboundedness.

import set_theory.ordinal.basic
import set_theory.ordinal.arithmetic
import set_theory.ordinal.topology
import set_theory.cardinal.basic
import set_theory.cardinal.ordinal
import set_theory.cardinal.cofinality

-- Based on https://en.wikipedia.org/wiki/Club_set

universe u

variables (S : set ordinal.{u}) (α : ordinal.{u})

def set.is_subset_of : Prop := S ⊆ set.Iio α
def set.is_closed : Prop := ∀ A ⊆ S, Sup A < α → Sup A ∈ A
def set.is_unbounded : Prop := ∀ β < α, ∃ γ ∈ S, β ≤ γ
def set.is_club : Prop := S.is_subset_of α ∧ S.is_closed α ∧ S.is_unbounded α

-- Proof that the intersection of two club sets is club
theorem inter_club_is_club  {C₁ : set ordinal.{u}} {C₂ : set ordinal.{u}} {κ : ordinal.{u}}
{h1 : set.is_club C₁ κ} {h2 : set.is_club C₂ κ} {hκ : κ.cof > cardinal.aleph_0} :
set.is_club (C₁ ∩ C₂) κ :=
begin
  simp only [set.is_club, set.is_subset_of, set.is_closed, set.is_unbounded],
  split,
-- Proof of being a subset of κ
  {
    sorry, --omitted
  },
  split,
-- Proof of being closed
  {
    sorry, --omitted
  },
-- Proof of being unbounded
  intros β hβ,
  -- Construct a sequence of γ n recursively such that β ≤ γ 1 ≤ γ 2 ≤ ...,
  -- γ 1, γ 3, γ 5, ... are in C₁, and γ 2, γ 4, γ 6, ... are in C₂. Since C₁
  -- and C₂ are closed and the cofinality of κ is uncountable, we can take
  -- the supremum of each of these to get  elements of C₁ and C₂, and
  -- by the interweaving they are equal to the same value γ, which is
  -- in C₁ ∩ C₂. Then β ≤ γ, showing unboundedness
  sorry,

I've looked at induction and recursion, but I have no idea how I might go about implementing the construction outlined in the comments using this. In particular, the choice for each γ n is non-constructive; we simply use unboundedness to know such γ n exist. I don't know how to invoke this existential quantifier in a recursive definition. Could I get some help?

[Kevin Buzzard]

I have errors on your code. I added import set_theory.cardinal.ordinal but I still have an error in hypothesis h\kappa. The error is

invalid field notation, 'cof' is not a valid "field" because environment does not contain 'ordinal.cof'

Do I need more imports? I don't know my way around the set theory part of the library at all.

[Kevin Buzzard]

Oh I got it -- import set_theory.cardinal.cofinality. It's helpful if you post fully working code when you're asking questions.

[Kevin Buzzard]

Yes, I see your problem. Defining functions in the middle of a tactic proof is tricky. I would be tempted to make the definition outside the proof and make a basic API for it (i.e. prove some lemmas about it) so you don't have to do all this when you're in the middle of a proof and your main goal is something else. In Lean it's much better to have 5 short lemmas/definitions than one monster one which tries to do everything at once, this is part of the art of translating mathematics into Lean. I'll see if I can write something coherent.

[Kevin Buzzard]

Here's a start (I need to do other things right now). I've defined the gamma sequence and proved its values alternate between the two sets.

import set_theory.cardinal.ordinal
import set_theory.cardinal.cofinality

universe u

variables (S : set ordinal.{u}) (α : ordinal.{u})

def set.is_subset_of : Prop := S ⊆ set.Iio α
def set.is_closed : Prop := ∀ A ⊆ S, Sup A < α → Sup A ∈ A
def set.is_unbounded : Prop := ∀ β < α, ∃ γ ∈ S, β ≤ γ
def set.is_club : Prop := S.is_subset_of α ∧ S.is_closed α ∧ S.is_unbounded α

-- you have written no API for your definitions. Here's an example of a useful lemma or two.
-- The idea is that every definition comes with a cost; you make it easier to use
-- by writing lemmas about it and then it's nicer to use when you're proving harder stuff
-- using it. You didn't pay the cost yet so it's hard work working with your definitions.
-- These make it a bit easier.
lemma set.is_club.is_unbounded : S.is_club α → S.is_unbounded α := λ h, h.2.2
lemma set.is_subset_of.lt : S.is_subset_of α → ∀ β ∈ S, β < α := λ h b hβ, h hβ
lemma set.is_club.is_subset_of : S.is_club α → S.is_subset_of α := λ h, h.1

/-- Given two unbounded subsets C₁ and C₂ of an ordinal α, and an initial value β, construct
a sequence `β = γ 0 ≤ γ 1 ≤ γ 2 ≤ ...` with γ i in C (i mod 2). -/
noncomputable def gamma_sequence {β : ordinal.{u}} (hβ : β < α) {C₁ C₂ : set ordinal.{u}}
  (h1 : C₁.is_club α) (h2 : C₂.is_club α) : ℕ → { x : ordinal.{u} // x < α}
| 0 := ⟨β, hβ⟩
| (n+1) := if n % 2 = 0 then -- odd case
    let is_unbounded := (h1.is_unbounded C₁ α (gamma_sequence n).1 (gamma_sequence n).2) in
    ⟨is_unbounded.some, (h1.is_subset_of C₁ α).lt C₁ α _ is_unbounded.some_spec.some⟩ else
    let is_unbounded := (h2.is_unbounded C₂ α (gamma_sequence n).1 (gamma_sequence n).2) in
    ⟨is_unbounded.some, (h2.is_subset_of C₂ α).lt C₂ α _ is_unbounded.some_spec.some⟩

-- I've made the definition so now I need to prove lots of things about it to make it usable
lemma gamma_sequence_even_aux (n : ℕ) {β : ordinal.{u}} (hβ : β < α) {C₁ C₂ : set ordinal.{u}}
  (h1 : C₁.is_club α) (h2 : C₂.is_club α) :
(gamma_sequence α hβ h1 h2 (2 * n + 2)) =
    let is_unbounded := (h2.is_unbounded C₂ α (gamma_sequence α hβ h1 h2 (2 * n + 1)).1
      (gamma_sequence α hβ h1 h2 (2 * n + 1)).2) in
    ⟨is_unbounded.some, (h2.is_subset_of C₂ α).lt C₂ α _ is_unbounded.some_spec.some⟩ :=
begin
  simp only [gamma_sequence],
  have foo : (2 * n + 1) % 2 ≠ 0,
  { rw [mul_comm, nat.mul_add_mod], norm_num },
  simp_rw if_neg foo,
end

lemma gamma_sequence_odd_aux' (n : ℕ) {β : ordinal.{u}} (hβ : β < α) {C₁ C₂ : set ordinal.{u}}
  (h1 : C₁.is_club α) (h2 : C₂.is_club α) :
(gamma_sequence α hβ h1 h2 (2 * n + 3)) =
    let is_unbounded := (h1.is_unbounded C₁ α (gamma_sequence α hβ h1 h2 (2 * n + 2)).1
      (gamma_sequence α hβ h1 h2 (2 * n + 2)).2) in
    ⟨is_unbounded.some, (h1.is_subset_of C₁ α).lt C₁ α _ is_unbounded.some_spec.some⟩ :=
begin
  simp only [gamma_sequence],
  have foo : (2 * n + 2) % 2 = 0,
  { rw [mul_comm, nat.mul_add_mod], norm_num },
  simp_rw if_pos foo,
end

lemma gamma_sequence_odd_aux (n : ℕ) {β : ordinal.{u}} (hβ : β < α) {C₁ C₂ : set ordinal.{u}}
  (h1 : C₁.is_club α) (h2 : C₂.is_club α) :
(gamma_sequence α hβ h1 h2 (2 * n + 1)) =
    let is_unbounded := (h1.is_unbounded C₁ α (gamma_sequence α hβ h1 h2 (2 * n)).1
      (gamma_sequence α hβ h1 h2 (2 * n)).2) in
    ⟨is_unbounded.some, (h1.is_subset_of C₁ α).lt C₁ α _ is_unbounded.some_spec.some⟩ :=
begin
  cases n,
  { refl, },
  exact gamma_sequence_odd_aux' α n hβ h1 h2,
end

-- the even elements of the sequence beyond 2 are in C₂
lemma gamma_sequence_even (n : ℕ) {β : ordinal.{u}} (hβ : β < α) {C₁ C₂ : set ordinal.{u}}
  (h1 : C₁.is_club α) (h2 : C₂.is_club α) : (gamma_sequence α hβ h1 h2 (2 * n + 2)).1 ∈ C₂ :=
begin
  let is_unbounded := (h2.is_unbounded C₂ α (gamma_sequence α hβ h1 h2 (2 * n + 1)).1
      (gamma_sequence α hβ h1 h2 (2 * n + 1)).2),
  rw gamma_sequence_even_aux,
  exact is_unbounded.some_spec.some,
end

-- the odd elements of the sequence are in C₁
lemma gamma_sequence_odd (n : ℕ) {β : ordinal.{u}} (hβ : β < α) {C₁ C₂ : set ordinal.{u}}
  (h1 : C₁.is_club α) (h2 : C₂.is_club α) : (gamma_sequence α hβ h1 h2 (2 * n + 1)).1 ∈ C₁ :=
begin
  let is_unbounded := (h1.is_unbounded C₁ α (gamma_sequence α hβ h1 h2 (2 * n)).1
      (gamma_sequence α hβ h1 h2 (2 * n)).2),
  rw gamma_sequence_odd_aux,
  exact is_unbounded.some_spec.some,
end

[Kevin Buzzard]

This is the pattern to proving stuff like this about the sequence; prove it outside your main proof and then just drop it in.

[Connor Gordon]

Thank you so much! I'll work with this and see if I can complete the proof from here.

[Connor Gordon]

Alright, I very nearly have it all now; all that's left is to use the cofinality assumption to show that the supremum of the gamma sequence is less than kappa. I have a bit of code that almost does what I want, but there's seemingly an issue with types and the universes those types come from, or something like that? Not totally clear. Here's the error message I'm getting:

type mismatch at application
  ordinal.sup_lt_ord
term
  γ_seq_val κ hβ h1 h2
has type
  ℕ → ordinal
but is expected to have type
  ?m_1 → ordinal

Here's a minimal (almost-)working example:

import set_theory.ordinal.basic
import set_theory.ordinal.arithmetic
import set_theory.ordinal.topology
import set_theory.cardinal.basic
import set_theory.cardinal.ordinal
import set_theory.cardinal.cofinality
import data.nat.parity

-- Based on https://en.wikipedia.org/wiki/Club_set

universe u

variables (S : set ordinal.{u}) (κ : ordinal.{u}) (α : ordinal.{u})

-- Basic definitions
def set.is_subset_of : Prop := S ⊆ set.Iio κ
def set.is_closed : Prop := ∀ A ⊆ S, Sup A < κ → Sup A ∈ A
def set.is_unbounded : Prop := ∀ β < κ, ∃ γ ∈ S, β < γ
def set.is_club : Prop := S.is_subset_of κ ∧ S.is_closed κ ∧ S.is_unbounded κ

-- Convenience lemmas
lemma set.is_club.is_unbounded : S.is_club κ → S.is_unbounded κ := λ h, h.2.2
lemma set.is_subset_of.lt : S.is_subset_of κ → ∀ β ∈ S, β < κ := λ h β hβ, h hβ
lemma set.is_club.is_subset_of : S.is_club κ → S.is_subset_of κ := λ h, h.1
lemma set.is_club.is_closed : S.is_club κ → S.is_closed κ := λ h, h.2.1

-- The proof of unboundedness involves a recursive construction of a sequence of ordinals γ n
-- The following is based heavily on code from Kevin Buzzard on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/working.20with.20club.20sets

-- Define the sequence recursively
noncomputable def γ_seq {β : ordinal.{u}} (hβ : β < κ) {C₁ C₂ : set ordinal.{u}} (h1 : C₁.is_club κ) (h2 : C₂.is_club κ) : ℕ → { x : ordinal.{u} // x < κ}
| 0 := ⟨β, hβ⟩
| (n+1) := if n % 2 = 0 then -- odd
    let is_unbounded := (h1.is_unbounded C₁ κ (γ_seq n).1 (γ_seq n).2) in
    ⟨is_unbounded.some, (h1.is_subset_of C₁ κ).lt C₁ κ _ is_unbounded.some_spec.some⟩
    else let is_unbounded := (h2.is_unbounded C₂ κ (γ_seq n).1 (γ_seq n).2) in
    ⟨is_unbounded.some, (h2.is_subset_of C₂ κ).lt C₂ κ _ is_unbounded.some_spec.some⟩

-- Extract the values from the gamma sequence
noncomputable def γ_seq_val {β : ordinal.{u}} (hβ : β < κ) {C₁ C₂ : set ordinal.{u}} (h1 : C₁.is_club κ) (h2 : C₂.is_club κ) : ℕ → ordinal.{u} := λ n, (γ_seq κ hβ h1 h2 n).1

-- Define the supremum of the sequence
noncomputable def γ_sup {β : ordinal.{u}} (hβ : β < κ) {C₁ C₂ : set ordinal.{u}} (h1 : C₁.is_club κ) (h2 : C₂.is_club κ) : ordinal.{u} := ordinal.sup (γ_seq_val κ hβ h1 h2)

-- Show this supremum is less than κ
lemma sup_lt_kappa {β : ordinal.{u}} (hβ : β < κ) {C₁ C₂ : set ordinal.{u}} (h1 : C₁.is_club κ) (h2 : C₂.is_club κ) (hκ : κ.cof > cardinal.aleph_0) : (γ_sup κ hβ h1 h2) < κ :=
begin
  simp only [γ_sup],
  have foo : (∀ n : ℕ, (γ_seq_val κ hβ h1 h2 n) < κ) → ordinal.sup (γ_seq_val κ hβ h1 h2) < κ,
  begin
    -- apply @ordinal.sup_lt_ord.{u} _ ((γ_seq_val κ hβ h1 h2)) κ,
    -- this really should work but it doesn't quite
    sorry,
  end,
  apply foo,
  intro n,
  exact (γ_seq κ hβ h1 h2 n).property,
end

If I can get this last bit, I will have completed the proof that the intersection of two club sets is club. Any ideas on how I could make this work?