Why is equivalence of type, zero, and succ sufficient here?

Stream: Analysis I

[Dan Abramov]

This may be more of a math question than a Lean question.

In Tao's Analysis book formalization, there's a chapter where he shows all Peano number systems are equivalent. He does it by definining

/-- The Peano axioms for an abstract type `Nat` -/
@[ext]
class PeanoAxioms where
  Nat : Type
  zero : Nat -- Axiom 2.1
  succ : Nat → Nat -- Axiom 2.2
  succ_ne : ∀ n : Nat, succ n ≠ zero -- Axiom 2.3
  succ_cancel : ∀ {n m : Nat}, succ n = succ m → n = m -- Axiom 2.4
  induction : ∀ (P : Nat → Prop),
    P zero → (∀ n : Nat, P n → P (succ n)) → ∀ n : Nat, P n -- Axiom 2.5

Then he defines a notion of equivalence between them (not to be confused with Lean's Equiv)

namespace PeanoAxioms
-- ...

/-- The notion of an equivalence between two structures obeying the Peano axioms.
    The symbol `≃` is an alias for Mathlib's `Equiv` class; for instance `P.Nat ≃ Q.Nat` is
    an alias for `_root_.Equiv P.Nat Q.Nat`. -/
class Equiv (P Q : PeanoAxioms) where
  equiv : P.Nat ≃ Q.Nat
  equiv_zero : equiv P.zero = Q.zero
  equiv_succ : ∀ n : P.Nat, equiv (P.succ n) = Q.succ (equiv n)

And then you're left to prove a bunch of things about it, including the uniqueness of such equivalence

/-- There is only one equivalence between any two structures obeying the Peano axioms. -/
theorem Equiv.uniq {P Q : PeanoAxioms} (equiv1 equiv2 : PeanoAxioms.Equiv P Q) :
    equiv1 = equiv2 := by
  sorry

My question isn't about solving these, but more theoretical: Why is PeanoAxioms.Equiv with these definitions of equiv, equiv_zero and equiv_succ "enough" to represent the entire system?

I.e. why is it these fields, but not, say anything about the axioms like succ_ne? Or — taken the other way — why do we need to have equiv_succ and say, not equiv_zero alone?

How does one "look" at PeanoNumbers definition and decide: "here's the minimal necessary set of equivalences that describes the entire system"?

[Kenny Lau]

@Dan Abramov the long answer will involve category theory and model theory, and the short answer is that you only need to preserve the "data" so that it isn't just some random bijection; as long as your bijection preserves data, then any theorem that you prove using P can be automatically transported to a theorem in Q

[Kenny Lau]

(bonus question for no points: deduce equiv_zero from the other existing information :upside_down: )

[Dan Abramov]

Ah interesting.

So generally even we have a bijection, that bijection might not preserve laws if the structure doesn't "match up". Making the structure "match up" guarantees preserving laws (since they "fall out" of the structure).

I wonder then if it's possible to come up with a bijection that preserves laws without the structure "matching up"? Or would the laws matching up necessarily make the structure match up?

I'm speaking a bit fuzzy here so not sure if it makes strict sense.

[Kenny Lau]

so basically by "preserving law" you mean that e.g. succ_ne becomes ∀ n : Nat, equiv (succ n) ≠ equiv(zero)? or did you mean ∀ n : Nat, succ (equiv n) ≠ zero?

[Kenny Lau]

(which are the same if you make the previous assumptions)

[Dan Abramov]

This is actually too hard to think about for me yet so I don't know what I mean. Sorry. :)

[Dan Abramov]

I'll think some more about this.

[Jireh Loreaux]

Kenny Lau said:

(bonus question for no points: deduce equiv_zero from the other existing information :upside_down: )

Alternatively, assume that equiv : P.Nat ≃ Q.Nat is instead just a bare function P.Nat → Q.Nat, keep the equiv_zero and equiv_succ fields, and then build a _root_.Equiv from this bare function

[Kyle Miller]

Here's a possible exercise:

Define a class that's just the data of a Peano system:

class PrePeanoAxioms where
  Nat : Type
  zero : Nat -- Axiom 2.1
  succ : Nat → Nat -- Axiom 2.2

Modify PeanoAxioms to extend PrePeanoAxioms.

Modify equiv to use PrePeanoAxioms instead.

The theorem

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

should still be provable without any changes (note! P and Q are still full PeanoAxioms).

Now, new theorem:

def PeanoAxioms.transfer {P : PeanoAxioms} {Q : PrePeanoAxioms} (equiv1 equiv2 : PrePeanoAxioms.Equiv P Q) :
    PeanoAxioms :=
  { Q with
    [... your code here to show you can transfer the proofs from P to Q ...] }

theorem PeanoAxioms.transfer_toPrePeanoAxioms_eq
    {P : PeanoAxioms} {Q : PrePeanoAxioms (equiv1 equiv2 : PrePeanoAxioms.Equiv P Q) :
    (PeanoAxioms.transfer equiv1 equiv2).toPrePeanoAxioms = Q := rfl

(All of this is untested — just writing right on Zulip)

[Matt Diamond]

Dan Abramov said:

Ah interesting.

So generally even we have a bijection, that bijection might not preserve laws if the structure doesn't "match up". Making the structure "match up" guarantees preserving laws (since they "fall out" of the structure).

I wonder then if it's possible to come up with a bijection that preserves laws without the structure "matching up"? Or would the laws matching up necessarily make the structure match up?

I'm speaking a bit fuzzy here so not sure if it makes strict sense.

It might be helpful to look at some structure-preserving equivalences in Mathlib, such as docs#MulEquiv. Notice the similarity between equiv_succ and map_mul'... in both cases we're showing that an operation "commutes" with the equivalence in some way (i.e. you get to the same place if you do the operation first and then map, or map and then do the operation). More specifically, these are both homomorphisms.

[Notification Bot]

This topic was moved here from #new members > Why is equivalence of type, zero, and succ sufficient here? by Johan Commelin.