mathlib documentation

set_theory.ordinal.principal

Principal ordinals #

We define principal or indecomposable ordinals, and we prove the standard properties about them.

Main definitions and results #

principal: A principal or indecomposable ordinal under some binary operation. We include 0 and any other typically excluded edge cases for simplicity.
unbounded_principal: Principal ordinals are unbounded.
principal_add_iff_zero_or_omega_opow: The main characterization theorem for additive principal ordinals.
principal_mul_iff_le_two_or_omega_opow_opow: The main characterization theorem for multiplicative principal ordinals.

Todo #

Prove that exponential principal ordinals are 0, 1, 2, ω, or epsilon numbers, i.e. fixed points of λ x, ω ^ x.

Principal ordinals #

def ordinal.principal (op : ordinal → ordinal → ordinal) (o : ordinal) :

Prop

An ordinal o is said to be principal or indecomposable under an operation when the set of ordinals less than it is closed under that operation. In standard mathematical usage, this term is almost exclusively used for additive and multiplicative principal ordinals.

For simplicity, we break usual convention and regard 0 as principal.

Equations

ordinal.principal op o = ∀ ⦃a b : ordinal⦄, a < o → b < o → op a b < o

theorem ordinal.principal_iff_principal_swap {op : ordinal → ordinal → ordinal} {o : ordinal} :

ordinal.principal op o ↔ ordinal.principal (function.swap op) o

theorem ordinal.principal_zero {op : ordinal → ordinal → ordinal} :

ordinal.principal op 0

@[simp]

theorem ordinal.principal_one_iff {op : ordinal → ordinal → ordinal} :

ordinal.principal op 1 ↔ op 0 0 = 0

theorem ordinal.principal.iterate_lt {op : ordinal → ordinal → ordinal} {a o : ordinal} (hao : a < o) (ho : ordinal.principal op o) (n : ℕ) :

op a^[n] a < o

theorem ordinal.op_eq_self_of_principal {op : ordinal → ordinal → ordinal} {a o : ordinal} (hao : a < o) (H : ordinal.is_normal (op a)) (ho : ordinal.principal op o) (ho' : o.is_limit) :

op a o = o

theorem ordinal.nfp_le_of_principal {op : ordinal → ordinal → ordinal} {a o : ordinal} (hao : a < o) (ho : ordinal.principal op o) :

ordinal.nfp (op a) a ≤ o

Principal ordinals are unbounded #

noncomputable def ordinal.blsub₂ (op : ordinal → ordinal → ordinal) (o : ordinal) :

The least strict upper bound of op applied to all pairs of ordinals less than o. This is essentially a two-argument version of ordinal.blsub.

Equations

ordinal.blsub₂ op o = ordinal.lsub (λ (x : (quotient.out o).α × (quotient.out o).α), op (ordinal.typein has_lt.lt x.fst) (ordinal.typein has_lt.lt x.snd))

theorem ordinal.lt_blsub₂ (op : ordinal → ordinal → ordinal) {o a b : ordinal} (ha : a < o) (hb : b < o) :

op a b < ordinal.blsub₂ op o

theorem ordinal.principal_nfp_blsub₂ (op : ordinal → ordinal → ordinal) (o : ordinal) :

ordinal.principal op (ordinal.nfp (ordinal.blsub₂ op) o)

theorem ordinal.unbounded_principal (op : ordinal → ordinal → ordinal) :

set.unbounded has_lt.lt {o : ordinal | ordinal.principal op o}

Additive principal ordinals #

theorem ordinal.principal_add_one :

ordinal.principal has_add.add 1

theorem ordinal.principal_add_of_le_one {o : ordinal} (ho : o ≤ 1) :

ordinal.principal has_add.add o

theorem ordinal.principal_add_is_limit {o : ordinal} (ho₁ : 1 < o) (ho : ordinal.principal has_add.add o) :

theorem ordinal.principal_add_iff_add_left_eq_self {o : ordinal} :

ordinal.principal has_add.add o ↔ ∀ (a : ordinal), a < o → a + o = o

theorem ordinal.exists_lt_add_of_not_principal_add {a : ordinal} (ha : ¬ordinal.principal has_add.add a) :

∃ (b c : ordinal) (hb : b < a) (hc : c < a), b + c = a

theorem ordinal.principal_add_iff_add_lt_ne_self {a : ordinal} :

ordinal.principal has_add.add a ↔ ∀ ⦃b c : ordinal⦄, b < a → c < a → b + c ≠ a

theorem ordinal.add_omega {a : ordinal} (h : a < ω) :

theorem ordinal.principal_add_omega :

ordinal.principal has_add.add ω

theorem ordinal.add_omega_opow {a b : ordinal} (h : a < ω ^ b) :

a + ω ^ b = ω ^ b

theorem ordinal.principal_add_omega_opow (o : ordinal) :

ordinal.principal has_add.add (ω ^ o)

theorem ordinal.principal_add_iff_zero_or_omega_opow {o : ordinal} :

ordinal.principal has_add.add o ↔ o = 0 ∨ ∃ (a : ordinal), o = ω ^ a

The main characterization theorem for additive principal ordinals.

theorem ordinal.opow_principal_add_of_principal_add {a : ordinal} (ha : ordinal.principal has_add.add a) (b : ordinal) :

ordinal.principal has_add.add (a ^ b)

theorem ordinal.add_absorp {a b c : ordinal} (h₁ : a < ω ^ b) (h₂ : ω ^ b ≤ c) :

a + c = c

theorem ordinal.mul_principal_add_is_principal_add (a : ordinal) {b : ordinal} (hb₁ : b ≠ 1) (hb : ordinal.principal has_add.add b) :

ordinal.principal has_add.add (a * b)

Multiplicative principal ordinals #

theorem ordinal.principal_mul_one :

ordinal.principal has_mul.mul 1

theorem ordinal.principal_mul_two :

ordinal.principal has_mul.mul 2

theorem ordinal.principal_mul_of_le_two {o : ordinal} (ho : o ≤ 2) :

ordinal.principal has_mul.mul o

theorem ordinal.principal_add_of_principal_mul {o : ordinal} (ho : ordinal.principal has_mul.mul o) (ho₂ : o ≠ 2) :

ordinal.principal has_add.add o

theorem ordinal.principal_mul_is_limit {o : ordinal} (ho₂ : 2 < o) (ho : ordinal.principal has_mul.mul o) :

theorem ordinal.principal_mul_iff_mul_left_eq {o : ordinal} :

ordinal.principal has_mul.mul o ↔ ∀ (a : ordinal), 0 < a → a < o → a * o = o

theorem ordinal.principal_mul_omega :

ordinal.principal has_mul.mul ω

theorem ordinal.mul_omega {a : ordinal} (a0 : 0 < a) (ha : a < ω) :

theorem ordinal.mul_lt_omega_opow {a b c : ordinal} (c0 : 0 < c) (ha : a < ω ^ c) (hb : b < ω) :

a * b < ω ^ c

theorem ordinal.mul_omega_opow_opow {a b : ordinal} (a0 : 0 < a) (h : a < ω ^ ω ^ b) :

a * ω ^ ω ^ b = ω ^ ω ^ b

theorem ordinal.principal_mul_omega_opow_opow (o : ordinal) :

ordinal.principal has_mul.mul (ω ^ ω ^ o)

theorem ordinal.principal_add_of_principal_mul_opow {o b : ordinal} (hb : 1 < b) (ho : ordinal.principal has_mul.mul (b ^ o)) :

ordinal.principal has_add.add o

theorem ordinal.principal_mul_iff_le_two_or_omega_opow_opow {o : ordinal} :

ordinal.principal has_mul.mul o ↔ o ≤ 2 ∨ ∃ (a : ordinal), o = ω ^ ω ^ a

The main characterization theorem for multiplicative principal ordinals.

theorem ordinal.mul_omega_dvd {a : ordinal} (a0 : 0 < a) (ha : a < ω) {b : ordinal} :

ω ∣ b → a * b = b

theorem ordinal.mul_eq_opow_log_succ {a b : ordinal} (ha : 0 < a) (hb : ordinal.principal has_mul.mul b) (hb₂ : 2 < b) :

a * b = b ^ (b.log a).succ

Exponential principal ordinals #

theorem ordinal.principal_opow_omega :

ordinal.principal (λ (_x _y : ordinal), _x ^ _y) ω

theorem ordinal.opow_omega {a : ordinal} (a1 : 1 < a) (h : a < ω) :