Category structure on nat

Stream: maths

[Adam Topaz]

Mathlib thinks that $\mathbb{N}$ has a canonical categorical structure.

example : category ℕ := by apply_instance

Why? (Is this the one coming from the ordering on $\mathbb{N}$?)

[Kevin Buzzard]

what are your imports?

[Bhavik Mehta]

It might be the one inferred from the partial order on nat

[Adam Topaz]

Just category_theory.category

[Adam Topaz]

Bhavik Mehta said:

It might be the one inferred from the partial order on nat

Yeah, this is what I assumed too.

[Adam Topaz]

The thing is, after the discussion yesterday about Lawvere theories, I wanted to do this:

class lawvere extends category ℕ :=
(lift {a b c : ℕ} : (c ⟶ a) → (c ⟶ b) → (c ⟶ (a + b)))
(π₁ {a b : ℕ} : (a + b) ⟶ a)
(π₂ {a b : ℕ} : (a + b) ⟶ b)
(lift_π₁ {a b c : ℕ} (f₁ : c ⟶ a) (f₂ : c ⟶ b) : lift f₁ f₂ ≫ π₁ = f₁)
(lift_π₂ {a b c : ℕ} (f₁ : c ⟶ a) (f₂ : c ⟶ b) : lift f₁ f₂ ≫ π₂ = f₂)
(lift_unique {a b c : ℕ} (f₁ : c ⟶ a) (f₂ : c ⟶ b) (g : c ⟶ (a + b)) :
  g ≫ π₁ = f₁ → g ≫ π₂ = f₂ → g = lift f₁ f₂

[Kevin Buzzard]

import category_theory.category

open category_theory

def ZZZ : category ℕ := by apply_instance
#print ZZZ -- preorder.small_category

#check preorder.small_category
/-
preorder.small_category : Π (α : Type u_1) [_inst_1 : preorder α], small_category α
-/

[Adam Topaz]

I guess I can get around this by introducing def foo := \N, and extending a category structure on foo.

[Bhavik Mehta]

isn't your lawvere just giving the structure of binary products on N?

[Adam Topaz]

Yup! A Lawvere theory is a category structure on the naturals where n is the n-fold product of 1

[Bhavik Mehta]

Right, but why are you redefining binary products yourself instead of using the mathlib version?

[Adam Topaz]

good question! Because I don't have much experience with mathlib's category theory :)

[Adam Topaz]

I need a predicate saying that a+b is the categorical product of a and b.

[Adam Topaz]

What's the best way to say this?

[Adam Topaz]

I guess using something from category_theory.limits.shapes.products.

[Bhavik Mehta]

Hang on, I'm a little confused what you're trying to define here

[Bhavik Mehta]

The structure you're describing here is unique, right "A Lawvere theory is a category structure on the naturals where n is the n-fold product of 1"

[Adam Topaz]

No.

[Adam Topaz]

You can have many many morphisms.

[Bhavik Mehta]

Ah, by naturals you don't mean the category structure being the preorder - I see

[Adam Topaz]

Yeah, exactly.

[Bhavik Mehta]

That makes much more sense - if you have f : a+b -> a and g : a+b -> b, then you can say is_limit (binary_fan.mk f g) to express that a+b with the projections f and g are a limit

[Adam Topaz]

Sounds good. What import do I need for binary_fan?

[Bhavik Mehta]

ct.limits.shapes.binary_products

[Kevin Buzzard]

To answer this sort of question I just type ml binary_fan into my browser search bar, following Rob Lewis' tip

[Adam Topaz]

That looks nice! Is anyone doing this on firefox? I don't see an option to add a custom search engine.

[Ruben Van de Velde]

https://superuser.com/questions/7327/how-to-add-a-custom-search-engine-to-firefox has some answers - I recall this having been easier in the past, though

[Scott Morrison]

If anyone is finding it annoying that category ℕ works out of the box (picking up the preorder structure), I'd be happy if you wanted to make a PR that introduced a type synonym def preorder_category (X : Type*) := X, and just put the category structure on that.

[Adam Topaz]

I actually think it makes more sense to make a synonym for $\mathbb{N}$ when we need a different category structure on it.

[Adam Topaz]

E.g.

def FinSet := ℕ
instance : category FinSet :=
{ hom := λ a b, fin a → fin b,
  id := λ a, id,
  comp := λ _ _ _ f g, g ∘ f }

[Reid Barton]

Right, it's not like you could use nat for several different Lawvere theories anyways

[Adam Topaz]

Here's an initial definition of Lawvere theories:
https://github.com/leanprover-community/mathlib/blob/univ_alg/src/algebra/universal/lawvere.lean

I didn't use the binary_fan.mk approach that @Bhavik Mehta mentioned, because it ended up being pretty awkward (this is most likely because I never seriously used the category theory library).