inductive sets and cardinality

Stream: general

[Violeta Hernández]

I have an inductive set that’s roughly built up like this

• It includes all ordinals less than Aleph n
• It includes sums of ordinals in the set
• It includes applications of some ordinal function to values in the set

I want to prove that the minimum excluded value of this set is strictly smaller than Aleph (n + 1). The way I’m thinking to do this is by induction on the “height” of an element of the set; at each step I have Aleph n ordinals, and after countably many steps I will still. I’m pretty much lost on what the best way to do this in Lean is, though.

[Reid Barton]

Does "sums" mean binary/finite sums?

[Violeta Hernández]

Yep (I used binary sums for simplicity)

[Reid Barton]

so something like this?

import set_theory.cardinal_ordinal

universe u
variables (n : ℕ) (f : ordinal.{u} → ordinal.{u})

inductive S : ordinal.{u} → Prop
| low : ∀ o, o < (cardinal.aleph n).ord → S o
| add : ∀ o o', S o → S o' → S (o + o')
| app : ∀ o, S o → S (f o)

[Violeta Hernández]

Yeah, that’s pretty much it

[Violeta Hernández]

I’m thinking… if I were given some injection from sets of “height” k to Aleph n, I could build an injection from sets of height k + 1 to (Aleph n x Aleph n) + Aleph n, which should then allow me to build an injection from those sets to Aleph n. So overall, I should have an injection from all of these sets to N.card x Aleph n which should then inject into Aleph n as well. Is this the right approach for problems like these?

[Violeta Hernández]

Not sure if I should phrase things in terms of injections, or just in terms of cardinalities

[Reid Barton]

So the general strategy that I use for this is to introduce an auxiliary inductive type which indexes the possible "shapes" of the terms of S (which for some reason I call time) and another inductive type which is parameterized by it:

import set_theory.cardinal_ordinal

universe u
variables (n : ℕ) (f : ordinal.{u} → ordinal.{u})

inductive S : ordinal.{u} → Prop
| low : ∀ o, o < (cardinal.aleph n).ord → S o
| add : ∀ o o', S o → S o' → S (o + o')
| app : ∀ o, S o → S (f o)

inductive time
| t_low : time
| t_add : time → time → time
| t_app : time → time
open time

lemma countable_time : cardinal.mk time = cardinal.omega := sorry

inductive timed_S : ordinal.{u} → time → Type (u+1)
| low : ∀ o, o < (cardinal.aleph n).ord → timed_S o t_low
| add : ∀ o t o' t', timed_S o t → timed_S o' t' → timed_S (o + o') (t_add t t')
| app : ∀ o t, timed_S o t → timed_S (f o) (t_app t)

lemma exists_time (o : ordinal.{u}) (h : S n f o) : ∃ t, nonempty (timed_S n f o t) :=
begin
  induction h,
  { refine ⟨t_low, ⟨timed_S.low _ _⟩⟩, assumption },
  { sorry },
  { sorry }
end

lemma timed_small (t : time) : cardinal.mk (Σ o, timed_S n f o t) < cardinal.aleph (n+1) :=
begin
  induction t with t₁ t₂ h₁ h₂ t' h',
  { sorry },
  { let F :
      (Σ (o : ordinal), timed_S n f o t₁) × (Σ (o : ordinal), timed_S n f o t₂) →
      (Σ (o : ordinal), timed_S n f o (t_add t₁ t₂)) :=
      λ ⟨⟨o, s⟩, ⟨o', s'⟩⟩, ⟨o + o', timed_S.add o t₁ o' t₂ s s'⟩,
    have : function.surjective F,
    { rintro ⟨_, s⟩,
      cases s with _ _ o t₁ o' t₂ s₁ s₂,
      exact ⟨(⟨o, s₁⟩, ⟨o', s₂⟩), rfl⟩ },
    refine lt_of_le_of_lt (cardinal.mk_le_of_surjective this) _,
    sorry },
  { sorry }
end

[Reid Barton]

Then, by combining these lemmas, you get a surjection from something whose cardinality you can bound by aleph (n+1) to {o | S n f o}

[Violeta Hernández]

Wait, small question regarding induction h

[Violeta Hernández]

Why doesn't cases h work?

[Reid Barton]

In the other cases, you will need the induction hypothesis to know that you can build the constituent Ss as timed_Ss

[Reid Barton]

It might end up being that proving countable_time is the most annoying part, in which case I didn't improve much on what you were already suggesting...

[Reid Barton]

So I guess a variant that combines both is to replace time by nat and timed_S by

inductive timed_S' : ordinal.{u} → ℕ → Type (u+1)
| low : ∀ o, o < (cardinal.aleph n).ord → timed_S' o 0
| add : ∀ o t o' t' t'', timed_S' o t → timed_S' o' t' → t < t'' → t' < t'' → timed_S' (o + o') t''
| app : ∀ o t t', timed_S' o t → t < t' → timed_S' (f o) t'

(there's no real need to generate each element exactly once) and use strong induction to prove timed_small, with more complicated F & cardinal arithmetic there

[Violeta Hernández]

This is a bit off-topic, but are there any statements about additive principal ordinals? I'm stuck proving a statement of the form a < (cardinal.aleph n).ord → b < (cardinal.aleph n).ord → a + b < (cardinal.aleph n).ord.

[Violeta Hernández]

The lemmas α < omega ^ γ → β < omega ^ γ → α + β < omega ^ γ and (cardinal.aleph n).ord = omega ^ (cardinal.aleph n).ord would suffice for this, but I don't think either of them exist...

[Violeta Hernández]

The first of these lemmas should be provable by building the Cantor Normal Form of α and β. Not sure how I'd tackle the second.

[Violeta Hernández]

Ah, found ordinal.add_lt_omega_power

[Violeta Hernández]

I have no idea how to prove the second part though :pensive:

[Violeta Hernández]

I believe the lemma α < ℵ_n → ω ^ α < ℵ_n should do it, after that I could just use the definition of ordinal exponentiation

[Violeta Hernández]

(in fact, this lemma should generalize to α < ℵ_n → β < ℵ_n → α ^ β < ℵ_n, which would then allow one to prove α < ℵ_n → α ^ ℵ_n = ℵ_n)

[Violeta Hernández]

...I have yet another question pertaining to ordinals. Can I prove (cardinal.aleph.{u} n).lift = cardinal.aleph.{u+1} n for n : ℕ?

[Violeta Hernández]

(or more generally, cardinal.aleph (α.lift) = (cardinal.aleph α).lift)

[Kevin Buzzard]

Is it definitely true? I'm serious.

[Kevin Buzzard]

I somehow imagine that changing your universe of sets can screw up cardinals. But I might be way off.

[Kevin Buzzard]

I'm not even sure if I believe an inequality. But I might just be being paranoid.

[Violeta Hernández]

I have no idea, but if it isn't true, there goes the last hour of my life :sob:

[Violeta Hernández]

There's a lot of lift lemmas for ordinals, so I'm at least hopeful

[Violeta Hernández]

In the best case scenario, this would be true:

theorem cardinal.aleph_lift (α : ordinal.{u}) :
  cardinal.aleph (ordinal.lift.{max v u} α) = cardinal.lift.{max v u} (cardinal.aleph.{u} α) :=
sorry

[Mario Carneiro]

that theorem should be true

[Mario Carneiro]

Actually you can generalize it to

theorem cardinal.aleph_lift (α : ordinal.{u}) :
  cardinal.aleph (ordinal.lift.{v} α) = cardinal.lift.{v} (cardinal.aleph.{u} α) :=
sorry

[Mario Carneiro]

The stuff about α < ℵ_n → ω ^ α < ℵ_n should generalize to a class of ordinals, I think they are called additive indecomposable ordinals

[Reid Barton]

Violeta Hernández said:

This is a bit off-topic, but are there any statements about additive principal ordinals? I'm stuck proving a statement of the form a < (cardinal.aleph n).ord → b < (cardinal.aleph n).ord → a + b < (cardinal.aleph n).ord.

Isn't a < x.ord equivalent to a.card < x? (Since x.ord is the smallest ordinal with cardinal x.)
Then it transposes to a more basic fact about the sum of infinite cardinals right?

[Reid Barton]

docs#cardinal.lt_ord

[Kevin Buzzard]

ord and card form a Galois insertion or coinsertion I guess.

[Kevin Buzzard]

coincidentally, https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20mathlib.3Amaster/near/264693273