Expressing ℕ as a category and Fibonacci as a functor

Stream: new members

[Lars Ericson]

A blog post by Tai-Danae Bradley shows that ℕ is a complete category where

• The objects are non-negative integers
• The morphism is divisibility

and the Fibonacci sequence F(n) where is exactly nat.fib and roughly (but this doesn't quite work):

def F : ℕ → ℕ
| 1 := 1
| 2 := 1
| n := F (n-1) + F(n-2)

is a functor given nat.gcd(F n) ( F m) = F (nat.gcd n m).

Using the category structure of mathlib, how do I prove ℕ is a category under nat.gcd?

I don't quite understand all I need to prove because the definition of category uses some complicated language extends category_struct.{v} obj . With the inclusion of the tactic . obviously, the category fields should prove themselves for the most part:

class category (obj : Type u)
extends category_struct.{v} obj : Type (max u (v+1)) :=
(id_comp' : ∀ {X Y : obj} (f : hom X Y), 𝟙 X ≫ f = f . obviously)
(comp_id' : ∀ {X Y : obj} (f : hom X Y), f ≫ 𝟙 Y = f . obviously)
(assoc'   : ∀ {W X Y Z : obj} (f : hom W X) (g : hom X Y) (h : hom Y Z),
  (f ≫ g) ≫ h = f ≫ (g ≫ h) . obviously)

Having proven ℕ is a category under divisibility, how do I show that nat.fib is a functor?

This is as far as I could get:

import category_theory.category.default
import data.nat.fib
open category_theory

instance  : category ℕ := {
-- something with nat.gcd
}

#check functor
-- something with nat.fib

Also, what in mathlib marks that a category is a complete category? complete_space? is_complete?

[Alex J. Best]

Here's a start to setting this up

import data.nat.fib
import category_theory.functor
open category_theory
def mynat : Type := nat
def to_nat : mynat → nat := id
instance : has_dvd mynat :=
{dvd := λ a b, to_nat a ∣ b}
instance a : preorder mynat :=
{ le := (∣),
le_refl := λ a, dvd_refl a,
le_trans := λ a b c h g, dvd_trans h g, }
lemma fib_dvd_fib {m n : ℕ} (h : m ∣ n) : m.fib ∣ n.fib :=
begin
  sorry
end
def fib : mynat ⥤ mynat :=
{ obj := nat.fib,
  map := λ m n h, hom_of_le (fib_dvd_fib (le_of_hom h)),
  map_id' := λ _, rfl,
  map_comp' := λ a b c f g, by simp}

[Alex J. Best]

We make mynat a type alias for nat so that we can put the divisibility order on it

[Alex J. Best]

docs#preorder.small_category automatically makes this a category then, so that the functor notation ⥤ works

[Alex J. Best]

I don't think we have the key lemma about divisibility of fibonaccis yet?

[Lars Ericson]

Thanks for the sketch @Alex J. Best .

Tai-Danae Bradley expressed the "functorial-ness" of nat.fib in terms of nat.gcd(nat.fib n) ( nat.fib m) = nat.fib (nat.gcd n m). How is this represented in the sketch, and how is nat.gcd as the greatest lower bound operator of the ℕ lattice represented in your sketch?

Another question, the definition of nat.fib says "We use a stream iterator for better performance when compared to the naive recursive implementation." The documentation for stream is terse. Is there a writeup somewhere for the use of stream iterators?

[Alex J. Best]

It's not, this was just the first step, setting up N with divisibility as a category and showing that fib defines a functor.

[Alex J. Best]

If you want to formalise the rest you would be showing that this category has (co)products (this would be lcm / gcd) and that the fib functor preserves limits

[Alex J. Best]

As for streams, I believe they're the same as the stream concept in haskell https://hackage.haskell.org/package/Stream-0.4.7.2/docs/Data-Stream.html

[Lars Ericson]

How do you say that mynat is an instance of category and that it is a complete category?

[Alex J. Best]

instance : category mynat := by apply_instance

for the first, lean is doing this behind the scenes when you use the functor notation, that won't work unless lean "knows" that mynat is a category

[Alex J. Best]

So adding that line to the file is only needed for you to check as a user that lean knows how to find the category instance.

[Alex J. Best]

docs#category_theory.limits.has_limits is what mathlib calls a complete category I believe

[Alex J. Best]

To actually make an instance of this class probably requires some work

[Alex J. Best]

You can see several examples by searching for instance has_limits in mathlib

[Alex J. Best]

Actually maybe I'm wrong and this is already there, if you import category_theory.limits.lattice then proving an instance of complete_lattice mynat will give you the has_limits mynat instance for free

[Alex J. Best]

ok but maybe mynat isn't a complete lattice? so the best you can do is make an instance of semilattice_inf_top mynat and get has_finite_limits mynat from that, or maybe the dual lol

[Alex J. Best]

Ok I guess it is a complete lattice after all but I'm not sure the best way to prove that, you need to define has_Inf mynat which should be the gcd of a (possibly infinite) set, the way I would do this by hand is just to say a set of naturals is a set of integers which generates some ideal, which is principal so take the positive generator to be the Inf of your set, no idea what the easiest way to do this in lean is.

[Alex J. Best]

import data.nat.fib
import category_theory.functor
import category_theory.limits.limits
import category_theory.limits.lattice

open category_theory
def mynat : Type := nat
def to_nat : mynat → nat := id
instance : has_dvd mynat :=
{dvd := λ a b, to_nat a ∣ b}

instance : semilattice_inf_top mynat :=
{ le := (∣),
le_refl := λ a, dvd_refl a,
le_trans := λ a b c h g, dvd_trans h g,
top := (0 : ℕ),
inf := λ a b , nat.gcd a b,
le_antisymm := λ a b, nat.dvd_antisymm,
inf_le_left := nat.gcd_dvd_left,
inf_le_right := nat.gcd_dvd_right,
le_top := λ a, ⟨0, rfl⟩,
le_inf := λ a b c, nat.dvd_gcd,
 }

-- instance : complete_lattice mynat :=  complete_lattice_of_Inf mynat
lemma fib_dvd_fib {m n : ℕ} (h : m ∣ n) : m.fib ∣ n.fib :=
begin
  sorry
end
def fib : mynat ⥤ mynat :=
{ obj := nat.fib,
  map := λ m n h, hom_of_le (fib_dvd_fib (le_of_hom h)),
  map_id' := λ _, rfl,
  map_comp' := λ a b c f g, by simp}
instance : category mynat := by apply_instance
instance : limits.has_finite_limits mynat := by apply_instance

uses the category machinery to show finite limits at least

[Johan Commelin]

Is there a complete_lattice_of_Sup?

[Alex J. Best]

Yes, Sup seemed harder to define to me than Inf though?

[Johan Commelin]

Isn't it finset.lcm for finite input and 0 otherwise?

[Alex J. Best]

Ah yes it is

[Alex J. Best]

Ok well I think these are the right definitions at least then, just a sorry to fill :smile:

import data.nat.fib
import category_theory.functor
import category_theory.limits.limits
import category_theory.limits.lattice
import data.finset.gcd
open category_theory
def mynat : Type := nat
def to_nat : mynat → nat := id
instance : has_dvd mynat :=
{dvd := λ a b, to_nat a ∣ b}
-- instance : semilattice_inf_top mynat :=
-- { le := (∣),
-- le_refl := λ a, dvd_refl a,
-- le_trans := λ a b c h g, dvd_trans h g,
-- top := (0 : ℕ),
-- inf := λ a b , nat.gcd a b,
-- le_antisymm := λ a b, nat.dvd_antisymm,
-- inf_le_left := nat.gcd_dvd_left,
-- inf_le_right := nat.gcd_dvd_right,
-- le_top := λ a, ⟨0, rfl⟩,
-- le_inf := λ a b c, nat.dvd_gcd,
--  }
instance : semilattice_sup_bot mynat :=
{ le := (∣),
le_refl := λ a, dvd_refl a,
le_trans := λ a b c h g, dvd_trans h g,
bot := (1 : ℕ),
sup := λ a b , nat.lcm a b,
le_antisymm := λ a b, nat.dvd_antisymm,
le_sup_left := nat.dvd_lcm_left,
le_sup_right := nat.dvd_lcm_right,
bot_le := λ (a:ℕ), ⟨a, (one_mul a).symm⟩,
sup_le := λ a b c, nat.lcm_dvd,
 }

open_locale classical
noncomputable theory
instance : has_Sup mynat := ⟨λ s, if h : s.finite then finset.sup (set.finite.to_finset h) id else (0: ℕ)⟩
instance : complete_lattice mynat := complete_lattice_of_Sup mynat  (λ s, sorry)
lemma fib_dvd_fib {m n : ℕ} (h : m ∣ n) : m.fib ∣ n.fib :=
begin
  sorry
end
def fib : mynat ⥤ mynat :=
{ obj := nat.fib,
  map := λ m n h, hom_of_le (fib_dvd_fib (le_of_hom h)),
  map_id' := λ _, rfl,
  map_comp' := λ a b c f g, by simp}
instance : category mynat := by apply_instance
instance : limits.has_finite_limits mynat := by apply_instance

[Eric Wieser]

Am I right in thinking thatinstance : semilattice_inf_top mynat could be PR'd as def dvd.semilattice_inf_top?

[Eric Wieser]

Seems like a nice way to group together all the structure, even if it's not desirable to register it as an instance

[Alex J. Best]

Yes I think so? Or the complete lattice version if someone fills in the proof :smile:.
Maybe @Aaron Anderson has some ideas on whats a good way to set this all up though? Taking the naturals as a partial order w.r.t. divisibility is quite close to some of the moebius function machinery Aaron has developed.

[Kevin Buzzard]

If only the order were total -- then it would be an answer to this

[Aaron Anderson]

There is already a partial order representing divisibility of naturals in mathlib - it’s associates nat

[Aaron Anderson]

I haven’t explicitly defined an equivalence between N and that, but the ingredients are there (the assumption you want is [unique (units N)])

[Aaron Anderson]

For any comm_monoid, there should be a <= on associates which is defeq to |, and with possibly a few assumptions, it's a partial_order.

[Aaron Anderson]

Unfortunately, the lattice instances on it are defined only for unique_factorization_monoid, and not for gcd_monoid, and I've found that hard to generalize without screwing up the flow of the unique_factorization_monoid file, but that's ok for this, because we have unique_factorization_monoid N.

[Aaron Anderson]

We do not however have a complete_lattice instance.

[Aaron Anderson]

Some definitions I've been vaguely thinking about defining for a while is a locally_finite_partial_order_with_top, which would apply to the partial order of the associates of a unique_factorization_monoid, and allow us to use your complete_lattice definition.

[Kevin Buzzard]

Aah -- on a DVR the <= on associates will be totally ordered: does associates have mul`?

[Kevin Buzzard]

Oh it does! There's my example!

[Lars Ericson]

Nice benchmark problem! Thanks for thinking about it.

[Lars Ericson]

It's a nice cold Saturday morning. I'm looking at this again. The above sketch from @Alex J. Best creates an alias of ℕ, mynat. However I noticed that a lot of pieces are there already in ℕ in particular

#check nat.has_dvd
#check nat.semilattice_sup_bot

What's missing is | as a relation with the same status as ≤, with corresponding hom_of_dvd and dvd_of_hom in category. I tried to redo the sketch purely in ℕ, but it fails at definitions of hom_of_dvd and dvd_of_hom and hence thereafter in this revised sketch:

import category_theory.functor
import category_theory.limits.limits
import category_theory.limits.lattice
import data.finset.gcd
import data.nat.gcd
import data.set.finite
import data.nat.fib

open category_theory
open_locale classical
noncomputable theory

instance : has_Sup ℕ := ⟨λ s, if h : s.finite then finset.sup (set.finite.to_finset h) id else (0: ℕ)⟩
instance : complete_lattice ℕ := complete_lattice_of_Sup ℕ  (λ s, sorry)

universe u
variables {α : Type u} [preorder α]

def category_theory.hom_of_dvd {U V : α} (h : (U | V)) : U ⟶  V := ulift.up (plift.up h) -- ERROR
lemma category_theory.dvd_of_hom {U V : α} (h : U ⟶ V) : (U | V) := h.down.down -- ERROR

def nat.fib_as_functor : ℕ ⥤ ℕ :=
{ obj := nat.fib,
  map := λ m n h, hom_of_dvd (nat.fib_dvd_fib (dvd_of_hom h)),
  map_id' := λ _, rfl,
  map_comp' := λ a b c f g, by simp
}

lemma nat.fib_dvd_fib {m n : ℕ }  : (m.fib_as_functor | n.fib_as_functor) :=
begin
  sorry
end

instance : category ℕ := by apply_instance
instance : limits.has_finite_limits ℕ := by apply_instance

If it's possible to make this work (with sorry in proofs is OK, just the types and ability to extend ℕ directly without making a mynat), that would be interesting.

[Johan Commelin]

@Lars Ericson it looks like you are trying to put two different order structures on the same type. Lean will not like that.

[Lars Ericson]

OK I'll stick with the mynat version, thanks.

[Adam Topaz]

Lean and typeclass inference should be able to deduce the category structure on the naturals obtained by divisibility using associates nat as Aaron hinted to above.

[Lars Ericson]

There are a number of assertions made in Fibonacci Sequence as a Functor. I'm using x_y for things defined in mathlib and x y for things that I don't know are defined in mathlib:

• ℕ has a partial_order under divisibility
  • Hence ℕ is a category
  • ℕ is also a complete category
• ℕ has a meet defined as n ⊓ m = nat.gcd n m
  • Hence ℕ has a categorical limit
• nat.fib preserves meets, where we define "preserve meets" by (nat.fib n)⊓ (nat.fib m) = nat.fib (n ⊓ m)
  • Hence ℕ is a meet semilattice
  • Hence nat.fib is a meet semilattice homomorphism
  • Hence nat.fib is a functor because nat.gcd(nat.fib n, nat.fib m) = nat.fib(nat.gcd n m)
  • Hence nat.fib is a continuous functor, because it preserves limits
• nat.gcd n m is
  * The categorical product of n and m
  * The pullback of n and m
  * The inverse limit of n and m
  * The equalizer of n and m

I would like to annotate the mynat proof sketch above with all of these assertions and be able to point out in Lean how each of the concepts is expressed. My placement of assertions next to related proofs is very approximate:

import category_theory.functor
import category_theory.limits.limits
import category_theory.limits.lattice
import data.finset.gcd
import data.nat.gcd
import data.set.finite
import data.nat.fib

open category_theory
open_locale classical
noncomputable theory

-- nat.gcd n m is the categorical product of n and m
-- nat.gcd n m is the pullback of n and m
-- nat.gcd n m is the inverse limit of n and m
-- nat.gcd n m is the equalizer of n and m

def mynat : Type := nat
def to_nat : mynat → nat := id
instance : has_dvd mynat := {dvd := λ a b, to_nat a ∣ b}

instance : semilattice_sup_bot mynat :=
{ le := (∣),
  le_refl := λ a, dvd_refl a,
  le_trans := λ a b c h g, dvd_trans h g,
  bot := (1 : ℕ),
  sup := λ a b , nat.lcm a b,
  le_antisymm := λ a b, nat.dvd_antisymm,
  le_sup_left := nat.dvd_lcm_left,
  le_sup_right := nat.dvd_lcm_right,
  bot_le := λ (a:ℕ), ⟨a, (one_mul a).symm⟩,
  sup_le := λ a b c, nat.lcm_dvd,
 }

-- ℕ has a partial_order under divisibility
-- ℕ has a meet defined as n ⊓ m = nat.gcd n m
-- ℕ is a meet semilattice

instance : has_Sup mynat := ⟨λ s, if h : s.finite then finset.sup (set.finite.to_finset h) id else (0: ℕ)⟩

instance : complete_lattice mynat := complete_lattice_of_Sup mynat  (λ s, sorry)

-- nat.fib preserves meets, where we define  "preserve meets" by  (nat.fib n)⊓ (nat.fib m) = nat.fib (n ⊓ m)
-- nat.fib is a meet semilattice homomorphism

lemma fib_dvd_fib {m n : ℕ} (h : m ∣ n) : m.fib ∣ n.fib :=
begin
  sorry
end

-- nat.fib is a functor because nat.gcd(nat.fib n, nat.fib m) = nat.fib(nat.gcd n m)
-- nat.fib is a continuous functor, because it preserves limits

def fib : mynat ⥤ mynat :=
{ obj := nat.fib,
  map := λ m n h, hom_of_le (fib_dvd_fib (le_of_hom h)),
  map_id' := λ _, rfl,
  map_comp' := λ a b c f g, by simp}

-- ℕ is a category
-- ℕ is also a complete category

instance : category mynat := by apply_instance

-- ℕ has a categorical limit

instance : limits.has_finite_limits mynat := by apply_instance

[Alex J. Best]

The sketch provided doesn't show that fib preserves meets, the unproven lemma lemma fib_dvd_fib {m n : ℕ} (h : m ∣ n) : m.fib ∣ n.fib := just says that fib is order preserving with the order on mynat given by division.

[Alex J. Best]

The reason for introducing mynat as a type alias for nat is to make use of notation and lemmas proved for types equipped with an order relation. Lean (naturally) gets confused if you put a two different order relations on the same type and want to use the same symbols to represent them both, so when you have two different relations on some type that both make it a preorder one way to circumvent this is to make a new type which is definitionally equal to the old one but with a different name. Lean will not automatically introduce the typeclasses from the old type for the new one, so we can set up an order relation on mynat that doesn't conflict with the usual ordering on natural numbers. As the types are equal by definition we can still use things proved about nat to prove things about mynat and lean will accept the proofs, hence why lines like le_sup_left := nat.dvd_lcm_left, work to prove things about mynat.

[Alex J. Best]

I'm not sure if you are intending your annotations to be before or after the corresponding declaration?

[Alex J. Best]

The statement that fib is a functor isn't the same as nat.gcd(nat.fib n, nat.fib m) = nat.fib(nat.gcd n m) that is the statement that fib preserves limits.

[Alex J. Best]

Being a complete category in lean is the statement limits.has_limits I believe, has_finite_limits would just be called finitely complete.

[Alex J. Best]

But given that we've added an incomplete proof that mynat is a complete lattice, the last line can be changed to

instance : limits.has_finite_limits mynat := by apply_instance