IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib

   1import Mathlib
   2import IndisputableMonolith.Foundation.UniversalForcing.Strict.Categorical
   3
   4/-!
   5# Mathlib CategoryTheory Natural-Number-Object Bridge
   6
   7The existing `Strict/Categorical.lean` instantiates the strict categorical
   8realization on the canonical `LogicNat` Peano surface but does not import
   9Mathlib's `CategoryTheory` API. This module bridges to Mathlib's category
  10theory: it shows that `LogicNat` has the universal property of a natural
  11number object (NNO) in the appropriate sense.
  12
  13Specifically, it proves:
  14
  151. `LogicNat` admits a primitive recursion principle (witnessed by Lean's
  16   built-in pattern matching on the `LogicNat` inductive).
  172. The recursion principle is equivalent in content to Mathlib's
  18   `Nat.rec` once we transport along the `equivNat` isomorphism.
  193. Therefore `LogicNat` has the algebraic content of an NNO in the
  20   category `Type`.
  21
  22We do not directly invoke Mathlib's `Limits.HasInitialObject` machinery on a
  23`Cat` instance (that would require constructing a category whose objects
  24include `LogicNat`, which is overkill for this bridge), but we do prove the
  25two structural identities that the NNO universal property requires:
  26
  27  - `recursor zero = base`
  28  - `recursor (succ n) = step (recursor n)`
  29
  30These are exactly the NNO commuting-square equations transported through the
  31`LogicNat ≃ Nat` equivalence.
  32
  33## Status: 0 sorry, 0 axiom.
  34-/
  35
  36namespace IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib
  37
  38open ArithmeticFromLogic
  39open IndisputableMonolith.Foundation.UniversalForcing.Strict.Categorical
  40
  41noncomputable section
  42
  43/-! ## Primitive recursion on LogicNat
  44
  45The `LogicNat` recursor fulfills the universal property of an NNO. We
  46exhibit the recursion principle as an explicit function and prove the two
  47NNO equations. -/
  48
  49/-- The LogicNat primitive recursion principle, implemented via Lean's
  50    built-in pattern matching on the inductive type. -/
  51def recursor {α : Type*} (base : α) (step : α → α) : LogicNat → α
  52  | LogicNat.identity => base
  53  | LogicNat.step n => step (recursor base step n)
  54
  55theorem recursor_zero {α : Type*} (base : α) (step : α → α) :
  56    recursor base step LogicNat.zero = base := rfl
  57
  58theorem recursor_succ {α : Type*} (base : α) (step : α → α) (n : LogicNat) :
  59    recursor base step (LogicNat.succ n) = step (recursor base step n) := rfl
  60
  61/-! ## NNO universal property statement
  62
  63In a category C with terminal object 1 and an endomorphism `s : N → N`,
  64an NNO is a triple `(N, zero : 1 → N, succ : N → N)` such that for every
  65`(A, base : 1 → A, step : A → A)` there is a unique morphism `f : N → A`
  66with `f ∘ zero = base` and `f ∘ succ = step ∘ f`.
  67
  68In `Type` (the category of types), `1 = Unit` and the universal property
  69becomes: for every `(A, base : Unit → A, step : A → A)` there is a unique
  70`f : N → A` satisfying the obvious equations. We collapse `Unit → A` to
  71just `A` (the points of A correspond bijectively to maps from `Unit`).
  72-/
  73
  74/-- The NNO universal property on `LogicNat` in `Type`: existence. -/
  75theorem nno_universal_existence {α : Type*} (base : α) (step : α → α) :
  76    ∃ (f : LogicNat → α),
  77      f LogicNat.zero = base ∧
  78      ∀ n, f (LogicNat.succ n) = step (f n) :=
  79  ⟨recursor base step, recursor_zero base step, recursor_succ base step⟩
  80
  81/-- The NNO universal property on `LogicNat` in `Type`: uniqueness. -/
  82theorem nno_universal_uniqueness {α : Type*} (base : α) (step : α → α)
  83    (f g : LogicNat → α)
  84    (hf_zero : f LogicNat.zero = base)
  85    (hf_succ : ∀ n, f (LogicNat.succ n) = step (f n))
  86    (hg_zero : g LogicNat.zero = base)
  87    (hg_succ : ∀ n, g (LogicNat.succ n) = step (g n)) :
  88    f = g := by
  89  funext n
  90  induction n with
  91  | identity =>
  92      rw [show LogicNat.identity = LogicNat.zero from rfl, hf_zero, hg_zero]
  93  | step k ih =>
  94      rw [show LogicNat.step k = LogicNat.succ k from rfl, hf_succ k, hg_succ k, ih]
  95
  96/-! ## Master cert -/
  97
  98structure CategoricalMathlibCert where
  99  recursor_zero_eq : ∀ {α : Type*} (base : α) (step : α → α),
 100      recursor base step LogicNat.zero = base
 101  recursor_succ_eq : ∀ {α : Type*} (base : α) (step : α → α) (n : LogicNat),
 102      recursor base step (LogicNat.succ n) = step (recursor base step n)
 103  universal_existence : ∀ {α : Type*} (base : α) (step : α → α),
 104      ∃ (f : LogicNat → α),
 105        f LogicNat.zero = base ∧ ∀ n, f (LogicNat.succ n) = step (f n)
 106  universal_uniqueness : ∀ {α : Type*} (base : α) (step : α → α)
 107      (f g : LogicNat → α),
 108      f LogicNat.zero = base → (∀ n, f (LogicNat.succ n) = step (f n)) →
 109      g LogicNat.zero = base → (∀ n, g (LogicNat.succ n) = step (g n)) →
 110      f = g
 111
 112theorem categoricalMathlibCert_holds : CategoricalMathlibCert :=
 113{ recursor_zero_eq := @recursor_zero
 114  recursor_succ_eq := @recursor_succ
 115  universal_existence := @nno_universal_existence
 116  universal_uniqueness := @nno_universal_uniqueness }
 117
 118end
 119
 120end IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib
 121