Zulip Chat Archive

Stream: maths

Topic: Category structure on nat


view this post on Zulip Adam Topaz (Aug 05 2020 at 19:03):

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

example : category  := by apply_instance

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

view this post on Zulip Kevin Buzzard (Aug 05 2020 at 19:04):

what are your imports?

view this post on Zulip Bhavik Mehta (Aug 05 2020 at 19:04):

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

view this post on Zulip Adam Topaz (Aug 05 2020 at 19:05):

Just category_theory.category

view this post on Zulip 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.

view this post on Zulip 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₂

view this post on Zulip 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 α
-/

view this post on Zulip 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.

view this post on Zulip Bhavik Mehta (Aug 05 2020 at 19:10):

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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Aug 05 2020 at 19:11):

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

view this post on Zulip Adam Topaz (Aug 05 2020 at 19:12):

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

view this post on Zulip Adam Topaz (Aug 05 2020 at 19:12):

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

view this post on Zulip Adam Topaz (Aug 05 2020 at 19:12):

What's the best way to say this?

view this post on Zulip Adam Topaz (Aug 05 2020 at 19:15):

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

view this post on Zulip Bhavik Mehta (Aug 05 2020 at 19:15):

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

view this post on Zulip 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"

view this post on Zulip Adam Topaz (Aug 05 2020 at 19:16):

No.

view this post on Zulip Adam Topaz (Aug 05 2020 at 19:16):

You can have many many morphisms.

view this post on Zulip Bhavik Mehta (Aug 05 2020 at 19:16):

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

view this post on Zulip Adam Topaz (Aug 05 2020 at 19:16):

Yeah, exactly.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Aug 05 2020 at 19:20):

Sounds good. What import do I need for binary_fan?

view this post on Zulip Bhavik Mehta (Aug 05 2020 at 19:20):

ct.limits.shapes.binary_products

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Aug 05 2020 at 23:57):

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

view this post on Zulip 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 }

view this post on Zulip Reid Barton (Aug 06 2020 at 00:03):

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

view this post on Zulip 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