Learning category theory, how do define a certain poset cat?

Stream: maths

[metakuntyyy]

So I always wanted to understand category theory better. I recently stumbled upon the following interesting category where the objects are natural numbers and the morphisms are arrows a->b iff a is less than b.

So Homs are defined as $\{\star\}$ if $a\le b$ and $\emptyset$ otherwise

However I fail to define the category and the errors lean gives me are bespoke.

import Mathlib

open CategoryTheory

def NatCat := ℕ

def srcTgt (a b :NatCat) : Option (Unit) :=by
  rw[NatCat] at a
  rw[NatCat] at b
  exact if a ≤ b then Option.some (Unit.unit) else Option.none

instance : SmallCategory NatCat where
  Hom R S := PLift.up (srcTgt R S)
  id R := sorry
  comp R S := sorry

It's likely I'm doing something stupid, I just don't see what it is. I don't even know how best to define the arrows.

[Ben Eltschig]

the Hom field expects something of type Type, you're giving it something of type PLift (Option Unit) - so it's no wonder it fails, the types just don't match up

[Ben Eltschig]

something like Hom n m := PLift (n.le m) should work though

[metakuntyyy]

Nope, still doesn't work.

import Mathlib

open CategoryTheory

def NatCat := ℕ

def natVal (R: NatCat) : ℕ := by
  rw[NatCat] at R
  exact R

def srcTgt (a b :NatCat) : Option (Unit) :=by
  rw[NatCat] at a
  rw[NatCat] at b
  exact if a ≤ b then Option.some (Unit.unit) else Option.none

instance : SmallCategory NatCat where
  Hom R S := PLift.up ((natVal R).le (natVal S))
  id R := sorry
  comp R S := sorry

[Ben Eltschig]

PLift takes a term of type Prop to a term of type Type, 'PLift.up' takes a term of type P : Prop to a term of type PLift P

[Ben Eltschig]

you need something of type Type, so you want the former, not the latter

[metakuntyyy]

Ah, now it works.

[Ben Eltschig]

docs#Preorder.smallCategory should be exactly this construction btw

[metakuntyyy]

Well thanks, it worked.

import Mathlib

open CategoryTheory

def NatCat := ℕ

def natVal (R: NatCat) : ℕ := by
  rw[NatCat] at R
  exact R

instance : SmallCategory NatCat where
  Hom R S := PLift ((natVal R).le (natVal S))
  id R := by
    let x := natVal R
    have h : x.le x := Nat.le.refl
    exact PLift.up h
  comp R S := by
    let r := PLift.down R
    let s := PLift.down S
    let hh := Nat.le_trans r s
    exact PLift.up hh

[metakuntyyy]

Ah, it's good that my independent calculation matches the mathlib definition, very happy with that.

[metakuntyyy]

It's really weird to think of morphisms as wrappers around propositions, because my original thought was to just assign it the ordered pair $\{ (x,y) ~\vert~ x \le y \}$

[metakuntyyy]

I have one question remaining. Can I somehow introduce the witnesses X,Y,Z to the context?
image.png
Intro does not seem to work. Can I destructure R,S?

[Ben Eltschig]

they are implicit arguments - so you can introduce them with names by writing comp {X Y Z} R S instead of comp R S

[metakuntyyy]

Thank you very much for the help. It was immensely useful.