Fundamental sequences

A fundamental sequence for a countable limit ordinal o is a strictly monotone function ℕ → Iio o with cofinal range. We can generalize this notion to arbitrary ordinals by setting the domain as Iio o.cof.card. Note that for a countable limit ordinal, one has o.cof.card = ω.

Main results

• Ordinal.exists_isFundamentalSeq: every ordinal has a fundamental sequence.

structure Ordinal.IsFundamentalSeq {a o : Ordinal.{u_1}} (f : ↑(Set.Iio a) → ↑(Set.Iio o)) : Prop

A fundamental sequence for o is a strictly monotonic function Iio o.cof.ord → Iio o with cofinal range. We provide a = o.cof.ord explicitly to avoid type rewrites.

• le_ord_cof : a ≤ o.cof.ord

  This condition alongside the others is enough to conclude o.cof.ord = a, see IsFundamentalSeq.ord_cof.

• strictMono : StrictMono f

  A fundamental sequence is strictly monotonic.

• isCofinal_range : IsCofinal (Set.range f)

  A fundamental sequence for o has cofinal range, i.e. its least strict upper bound equals the ordinal o. See IsFundamentalSeq.iSup_add_one_eq and IsFundamentalSeq.iSup_eq.

theorem Ordinal.IsFundamentalSeq.iSup_add_one_eq {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} (hf : IsFundamentalSeq f) : ⨆ (i : ↑(Set.Iio a)), ↑(f i) + 1 = o

theorem Ordinal.IsFundamentalSeq.ord_cof {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} (hf : IsFundamentalSeq f) : o.cof.ord = a

theorem Ordinal.IsFundamentalSeq.iSup_eq {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} (hf : IsFundamentalSeq f) (ha : 1 < a) : ⨆ (i : ↑(Set.Iio a)), ↑(f i) = o

theorem Ordinal.IsFundamentalSeq.id {o : Ordinal.{u_1}} (ho : o ≤ o.cof.ord) : IsFundamentalSeq id

A regular ordinal o has a fundamental sequence given by all smaller ordinals.

theorem Ordinal.IsFundamentalSeq.zero (f : ↑(Set.Iio 0) → ↑(Set.Iio 0)) : IsFundamentalSeq f

The empty function is a fundamental sequence for 0.

theorem Ordinal.IsFundamentalSeq.add_one (o : Ordinal.{u_1}) : IsFundamentalSeq fun (x : ↑(Set.Iio 1)) => ⟨o, ⋯⟩

The length one sequence (o) is a fundamental sequence for o + 1.

theorem Ordinal.IsFundamentalSeq.comp {a b o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} {g : ↑(Set.Iio b) → ↑(Set.Iio a)} (hf : IsFundamentalSeq f) (hg : IsFundamentalSeq g) : IsFundamentalSeq (f ∘ g)

theorem Ordinal.IsFundamentalSeq.comp_isNormal {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} {g : Ordinal.{u_1} → Ordinal.{u_1}} (hg : Order.IsNormal g) (hf : IsFundamentalSeq f) (ho : Order.IsSuccLimit o) : IsFundamentalSeq fun (i : ↑(Set.Iio a)) => ⟨g ↑(f i), ⋯⟩

If f is a fundamental sequence for a limit ordinal o and g is normal, then g ∘ f is a fundamental sequence for g o.

theorem Ordinal.exists_isFundamentalSeq {a o : Ordinal.{u_1}} (ha : o.cof.ord = a) : ∃ (f : ↑(Set.Iio a) → ↑(Set.Iio o)), IsFundamentalSeq f

Every ordinal has a fundamental sequence.