Enderton (set). Isomorphism from ℕ to peano systems.

finite-set-exercises
Joshua Potter 2023-09-09 05:15:52 -06:00
parent 1e662bd1fe
commit 66ca483671
3 changed files with 112 additions and 3 deletions

View File

@ -6378,7 +6378,7 @@
\end{proof}
\subsection{\pending{Theorem 4H}}%
\subsection{\verified{Theorem 4H}}%
\hyperlabel{sub:theorem-4h}
\begin{theorem}[4H]
@ -6389,6 +6389,9 @@
$$h(\sigma(n)) = S(h(n))$$ and the zero element $$h(0) = e.$$
\end{theorem}
\code{Common/Set/Peano}
{Peano.nat\_isomorphism}
\begin{proof}
Let $\langle N, S, e \rangle$ be a \nameref{ref:peano-system}.

View File

@ -1,5 +1,6 @@
import Common.Logic.Basic
import Common.Set.Basic
import Common.Set.Peano
import Mathlib.Data.Set.Basic
import Mathlib.SetTheory.Ordinal.Basic

View File

@ -1,5 +1,6 @@
import Mathlib.Data.Rel
import Mathlib.Data.Set.Basic
import Mathlib.Tactic.LibrarySearch
/-! # Common.Set.Peano
@ -18,13 +19,16 @@ met:
3. Every subset `A` of `N` containing `e` and closed under `S` is `N` itself.
-/
class System (N : Set α) (S : αα) (e : α) where
maps_to : Set.MapsTo S N N
mem : e ∈ N
zero_range : e ∉ Set.range S
injective : Function.Injective S
induction : ∀ A, A ⊆ N ∧ e ∈ A ∧ (∀ a ∈ A, S a ∈ A) → A = N
instance : System (N := @Set.univ ) (S := Nat.succ) (e := 0) where
zero_range := by
simp
maps_to := by simp
mem := by simp
zero_range := by simp
injective := by
intro x₁ x₂ h
injection h
@ -39,4 +43,105 @@ instance : System (N := @Set.univ ) (S := Nat.succ) (e := 0) where
refine h.right.right n (ih ?_)
simp
/--
The unique (by virtue of the Recursion Theorem for `ω`) function that maps the
natural numbers to an arbitrary Peano system.
-/
def of_nat {e : α} [h : System N S e] : Nat → α
| 0 => e
| n + 1 => S (@of_nat _ _ _ _ h n)
/--
The `of_nat` function maps all natural numbers to the set `N` defined in the
provided Peano system.
-/
theorem nat_maps_to [h : System N S e]
: Set.MapsTo (@of_nat _ _ _ _ h) Set.univ N := by
unfold Set.MapsTo
intro x hx
unfold of_nat
induction x with
| zero => exact h.mem
| succ x ih =>
simp only
by_cases hx' : x = 0
· rw [hx']
unfold of_nat
exact h.maps_to h.mem
· have ⟨p, hp⟩ := Nat.exists_eq_succ_of_ne_zero hx'
rw [hp] at ih ⊢
simp only [Set.mem_univ, forall_true_left] at ih
exact h.maps_to ih
/--
Let `⟨N, S, e⟩` be a Peano system. Then `⟨ω, σ, 0⟩` is isomorphic to
`⟨N, S, e⟩`, i.e., there is a function `h` mapping `ω` one-to-one onto `N` in a
way that preserves the successor operation
```
h(σ(n)) = S(h(n))
```
and the zero element
```
h(0) = e.
```
-/
theorem nat_isomorphism [h : System N S e]
: let n2p := @of_nat _ _ _ _ h
Set.BijOn n2p Set.univ N ∧
(∀ n : , n2p n.succ = S (n2p n)) ∧ n2p 0 = e := by
let n2p := @of_nat _ _ _ _ h
refine ⟨⟨nat_maps_to, ?_, ?_⟩, ?_, rfl⟩
· -- Prove `of_nat` is one-to-one.
suffices ∀ n : , ∀ m, n2p m = n2p n → m = n by
unfold Set.InjOn
intro m _ n _
exact this n m
intro n
induction n with
| zero =>
intro m hm
by_contra nm
have ⟨p, hp⟩ := Nat.exists_eq_succ_of_ne_zero nm
rw [hp] at hm
unfold of_nat at hm
exact absurd ⟨n2p p, hm⟩ h.zero_range
| succ n ih =>
intro m hm
by_cases nm : m = 0
· rw [nm] at hm
unfold of_nat at hm
exact absurd ⟨n2p n, hm.symm⟩ h.zero_range
· have ⟨p, hp⟩ := Nat.exists_eq_succ_of_ne_zero nm
rw [hp] at hm
unfold of_nat at hm
have := h.injective hm
rwa [← ih p this]
· -- Prove `of_nat` is onto.
suffices e ∈ Set.range n2p ∧ (∀ y, y ∈ Set.range n2p → S y ∈ Set.range n2p) by
unfold Set.SurjOn
simp only [Set.image_univ]
have hN : Set.range n2p = N := by
refine h.induction (Set.range n2p) ⟨?_, this⟩
show ∀ t, t ∈ Set.range n2p → t ∈ N
intro t ht
unfold Set.range at ht
simp only [Set.mem_setOf_eq] at ht
have ⟨y, hy⟩ := ht
rw [← hy]
exact nat_maps_to (by simp)
exact Eq.subset (id (Eq.symm hN))
refine ⟨?_, ?_⟩
· unfold Set.range
simp only [Set.mem_setOf_eq]
exact ⟨0, rfl⟩
· intro y hy
have ⟨n, hn⟩ := hy
refine ⟨n + 1, ?_⟩
unfold of_nat
simp only [Nat.add_eq, Nat.add_zero]
dsimp only at hn
rw [hn]
· intro _
conv => left; unfold of_nat
end Peano