Principal ordinals #
We define principal or indecomposable ordinals, and we prove the standard properties about them.
Todo #
- Prove the characterization of additive principal ordinals.
- Prove the characterization of multiplicative principal ordinals.
- Refactor any related theorems from
ordinal_arithmetic
into this file.
Principal ordinals #
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.
theorem
ordinal.principal_iff_principal_swap
{op : ordinal → ordinal → ordinal}
{o : ordinal} :
ordinal.principal op o ↔ ordinal.principal (function.swap op) o
@[simp]
theorem
ordinal.principal_one_iff
{op : ordinal → ordinal → ordinal} :
ordinal.principal op 1 ↔ op 0 0 = 0
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 #
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 (quotient.out o).r x.fst) (ordinal.typein (quotient.out o).r 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}