## Stream: maths

### Topic: Category structure on nat

#### Adam Topaz (Aug 05 2020 at 19:03):

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}$?)

#### Bhavik Mehta (Aug 05 2020 at 19:04):

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

#### Adam Topaz (Aug 05 2020 at 19:05):

Just category_theory.category

#### Adam Topaz (Aug 05 2020 at 19:05):

Bhavik Mehta said:

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

Yeah, this is what I assumed too.

#### Adam Topaz (Aug 05 2020 at 19:06):

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 (Aug 05 2020 at 19:07):

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 (Aug 05 2020 at 19:08):

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

#### Bhavik Mehta (Aug 05 2020 at 19:10):

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

#### Adam Topaz (Aug 05 2020 at 19:10):

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

#### Bhavik Mehta (Aug 05 2020 at 19:11):

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

#### Adam Topaz (Aug 05 2020 at 19:12):

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

#### Adam Topaz (Aug 05 2020 at 19:12):

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

#### Adam Topaz (Aug 05 2020 at 19:12):

What's the best way to say this?

#### Adam Topaz (Aug 05 2020 at 19:15):

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

#### Bhavik Mehta (Aug 05 2020 at 19:15):

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

#### Bhavik Mehta (Aug 05 2020 at 19:16):

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"

No.

#### Adam Topaz (Aug 05 2020 at 19:16):

You can have many many morphisms.

#### Bhavik Mehta (Aug 05 2020 at 19:16):

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

Yeah, exactly.

#### Bhavik Mehta (Aug 05 2020 at 19:18):

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 (Aug 05 2020 at 19:20):

Sounds good. What import do I need for binary_fan?

#### Bhavik Mehta (Aug 05 2020 at 19:20):

ct.limits.shapes.binary_products

#### Kevin Buzzard (Aug 05 2020 at 19:23):

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

#### Adam Topaz (Aug 05 2020 at 19:25):

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 (Aug 05 2020 at 20:28):

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 (Aug 05 2020 at 23:52):

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 (Aug 05 2020 at 23:57):

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 (Aug 05 2020 at 23:58):

E.g.

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


#### Reid Barton (Aug 06 2020 at 00:03):

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

#### Adam Topaz (Aug 06 2020 at 00:09):

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).

Last updated: May 09 2021 at 11:09 UTC