Analysis I, Chapter 2 epilogue

In this (technical) epilogue, we show that the "Chapter 2" natural numbers Chapter2.Nat are isomorphic in various standard senses to the standard natural numbers ℕ.

From this point onwards, Chapter2.Nat will be deprecated, and we will use the standard natural numbers ℕ instead. In particular, one should use the full Mathlib API for ℕ for all subsequent chapters, in lieu of the Chapter2.Nat API.

Filling the sorries here requires both the Chapter2.Nat API and the Mathlib API for the standard natural numbers ℕ. As such, they are excellent exercises to prepare you for the aforementioned transition.

In second half of this section we also give a fully axiomatic treatment of the natural numbers via the Peano axioms. The treatment in the preceding three sections was only partially axiomatic, because we used a specific construction Chapter2.Nat of the natural numbers that was an inductive type, and used that inductive type to construct a recursor. Here, we give some exercises to show how one can accomplish the same tasks directly from the Peano axioms, without knowing the specific implementation of the natural numbers.

@[reducible, inline]

abbrev Chapter2.Nat.toNat (n : Nat) : ℕ

Equations

• Chapter2.Nat.zero.toNat = 0
• n'++.toNat = n'.toNat + 1

theorem Chapter2.Nat.zero_toNat : toNat 0 = 0

theorem Chapter2.Nat.succ_toNat (n : Nat) : n++.toNat = n.toNat + 1

@[reducible, inline]

abbrev Chapter2.Nat.equivNat : Nat ≃ ℕ

Equations

• Chapter2.Nat.equivNat = { toFun := Chapter2.Nat.toNat, invFun := fun (n : ℕ) => ↑n, left_inv := Chapter2.Nat.equivNat._proof_2, right_inv := Chapter2.Nat.equivNat._proof_3 }

@[reducible, inline]

abbrev Chapter2.Nat.equivNat_order : Nat ≃o ℕ

Equations

• Chapter2.Nat.equivNat_order = { toEquiv := Chapter2.Nat.equivNat, map_rel_iff' := @Chapter2.Nat.equivNat_order._proof_4 }

@[reducible, inline]

abbrev Chapter2.Nat.equivNat_ring : Nat ≃+* ℕ

Equations

• Chapter2.Nat.equivNat_ring = { toEquiv := Chapter2.Nat.equivNat, map_mul' := Chapter2.Nat.equivNat_ring._proof_5, map_add' := Chapter2.Nat.equivNat_ring._proof_6 }

theorem Chapter2.Nat.pow_eq_pow (n m : Nat) : ↑n.toNat ^ m.toNat = n ^ m

class PeanoAxioms : Type 1

The Peano axioms for an abstract type Nat

• Nat : Type
• zero : Nat
• succ : Nat → Nat
• succ_ne (n : Nat) : succ n ≠ zero
• succ_cancel {n m : Nat} : succ n = succ m → n = m
• induction (P : Nat → Prop) : P zero → (∀ (n : Nat), P n → P (succ n)) → ∀ (n : Nat), P n

theorem PeanoAxioms.ext {x y : PeanoAxioms} (Nat : Nat = Nat) (zero : HEq zero zero) (succ : HEq succ succ) : x = y

theorem PeanoAxioms.ext_iff {x y : PeanoAxioms} : x = y ↔ Nat = Nat ∧ HEq zero zero ∧ HEq succ succ

def PeanoAxioms.Chapter2.Nat : PeanoAxioms

The Chapter 2 natural numbers obey the Peano axioms.

Equations

• PeanoAxioms.Chapter2.Nat = { Nat := Chapter2.Nat, zero := Chapter2.Nat.zero, succ := Chapter2.Nat.succ, succ_ne := Chapter2.Nat.succ_ne, succ_cancel := ⋯, induction := Chapter2.Nat.induction }

def PeanoAxioms.Mathlib.Nat : PeanoAxioms

The Mathlib natural numbers obey the Peano axioms.

Equations

• PeanoAxioms.Mathlib.Nat = { Nat := ℕ, zero := 0, succ := Nat.succ, succ_ne := Nat.succ_ne_zero, succ_cancel := @PeanoAxioms.Mathlib.Nat._proof_7, induction := ⋯ }

@[reducible, inline]

abbrev PeanoAxioms.natCast (P : PeanoAxioms) : ℕ → Nat

One can map the Mathlib natural numbers into any other structure obeying the Peano axioms.

Equations

• P.natCast Nat.zero = PeanoAxioms.zero
• P.natCast n_2.succ = PeanoAxioms.succ (P.natCast n_2)

theorem PeanoAxioms.natCast_injective (P : PeanoAxioms) : Function.Injective P.natCast

theorem PeanoAxioms.natCast_surjective (P : PeanoAxioms) : Function.Surjective P.natCast

class PeanoAxioms.Equiv (P Q : PeanoAxioms) : Type

The notion of an equivalence between two structures obeying the Peano axioms

• equiv : Nat ≃ Nat
• equiv_zero : equiv zero = zero
• equiv_succ (n : Nat) : equiv (succ n) = succ (equiv n)

@[reducible, inline]

abbrev PeanoAxioms.Equiv.symm {P Q : PeanoAxioms} (equiv : P.Equiv Q) : Q.Equiv P

Equations

• equiv.symm = { equiv := PeanoAxioms.Equiv.equiv.symm, equiv_zero := ⋯, equiv_succ := ⋯ }

@[reducible, inline]

abbrev PeanoAxioms.Equiv.trans {P Q R : PeanoAxioms} (equiv1 : P.Equiv Q) (equiv2 : Q.Equiv R) : P.Equiv R

Equations

• equiv1.trans equiv2 = { equiv := PeanoAxioms.Equiv.equiv.trans PeanoAxioms.Equiv.equiv, equiv_zero := ⋯, equiv_succ := ⋯ }

@[reducible, inline]

abbrev PeanoAxioms.Equiv.fromNat (P : PeanoAxioms) : Mathlib.Nat.Equiv P

Equations

• PeanoAxioms.Equiv.fromNat P = { equiv := { toFun := P.natCast, invFun := sorry, left_inv := ⋯, right_inv := ⋯ }, equiv_zero := ⋯, equiv_succ := ⋯ }

@[reducible, inline]

abbrev PeanoAxioms.Equiv.mk' (P Q : PeanoAxioms) : P.Equiv Q

Equations

• PeanoAxioms.Equiv.mk' P Q = sorry

theorem PeanoAxioms.Equiv.uniq {P Q : PeanoAxioms} (equiv1 equiv2 : P.Equiv Q) : equiv1 = equiv2

theorem PeanoAxioms.Nat.recurse_uniq {P : PeanoAxioms} (f : Nat → Nat → Nat) (c : Nat) : ∃! a : Nat → Nat, a zero = c ∧ ∀ (n : Nat), a (succ n) = f n (a n)

A sample result: recursion is well-defined on any structure obeying the Peano axioms