Natural operations on ordinals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The goal of this file is to define natural addition and multiplication on ordinals, also known as
the Hessenberg sum and product, and provide a basic API. The natural addition of two ordinals
a ♯ b
is recursively defined as the least ordinal greater than a' ♯ b
and a ♯ b'
for a' < a
and b' < b
. The natural multiplication a ⨳ b
is likewise recursively defined as the least
ordinal such that a ⨳ b ♯ a' ⨳ b'
is greater than a' ⨳ b ♯ a ⨳ b'
for any a' < a
and
b' < b
.
These operations form a rich algebraic structure: they're commutative, associative, preserve order,
have the usual 0
and 1
from ordinals, and distribute over one another.
Moreover, these operations are the addition and multiplication of ordinals when viewed as
combinatorial game
s. This makes them particularly useful for game theory.
Finally, both operations admit simple, intuitive descriptions in terms of the Cantor normal form.
The natural addition of two ordinals corresponds to adding their Cantor normal forms as if they were
polynomials in ω
. Likewise, their natural multiplication corresponds to multiplying the Cantor
normal forms as polynomials.
Implementation notes #
Given the rich algebraic structure of these two operations, we choose to create a type synonym
nat_ordinal
, where we provide the appropriate instances. However, to avoid casting back and forth
between both types, we attempt to prove and state most results on ordinal
.
Todo #
- Define natural multiplication and provide a basic API.
- Prove the characterizations of natural addition and multiplication in terms of the Cantor normal form.
A type synonym for ordinals with natural addition and multiplication.
Equations
Instances for nat_ordinal
- nat_ordinal.has_zero
- nat_ordinal.inhabited
- nat_ordinal.has_one
- nat_ordinal.linear_order
- nat_ordinal.succ_order
- nat_ordinal.has_well_founded
- nat_ordinal.well_founded_lt
- nat_ordinal.has_lt.lt.is_well_order
- nat_ordinal.has_add
- nat_ordinal.add_covariant_class_lt
- nat_ordinal.add_covariant_class_le
- nat_ordinal.add_contravariant_class_le
- nat_ordinal.ordered_cancel_add_comm_monoid
- nat_ordinal.add_monoid_with_one
The identity function between ordinal
and nat_ordinal
.
Equations
The identity function between nat_ordinal
and ordinal
.
Equations
A recursor for nat_ordinal
. Use as induction x using nat_ordinal.rec
.
Equations
- nat_ordinal.rec h = λ (a : nat_ordinal), h (⇑nat_ordinal.to_ordinal a)
ordinal.induction
but for nat_ordinal
.
Natural addition on ordinals a ♯ b
, also known as the Hessenberg sum, is recursively defined
as the least ordinal greater than a' ♯ b
and a ♯ b'
for all a' < a
and b' < b
. In contrast
to normal ordinal addition, it is commutative.
Natural addition can equivalently be characterized as the ordinal resulting from adding up
corresponding coefficients in the Cantor normal forms of a
and b
.
Equations
Equations
- nat_ordinal.ordered_cancel_add_comm_monoid = {add := has_add.add nat_ordinal.has_add, add_assoc := ordinal.nadd_assoc, zero := 0, zero_add := ordinal.zero_nadd, add_zero := ordinal.nadd_zero, nsmul := add_comm_monoid.nsmul._default 0 has_add.add ordinal.zero_nadd ordinal.nadd_zero, nsmul_zero' := nat_ordinal.ordered_cancel_add_comm_monoid._proof_1, nsmul_succ' := nat_ordinal.ordered_cancel_add_comm_monoid._proof_2, add_comm := ordinal.nadd_comm, le := linear_order.le nat_ordinal.linear_order, lt := linear_order.lt nat_ordinal.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := nat_ordinal.ordered_cancel_add_comm_monoid._proof_3, le_of_add_le_add_left := nat_ordinal.ordered_cancel_add_comm_monoid._proof_4}