Free Walking Arrow Category

Stream: mathlib4

[Sina Hazratpour 𓃵]

Is the free walking arrow category $\mathbb{2}$ defined somewhere in mathlib? It is a very useful thing to have around.

[Markus Himmel]

We don't have a special definition for it, but Fin 2 (which has a category instance because it is a preorder) should do the job.

[Sina Hazratpour 𓃵]

Good suggestion! So far, I've been using WithTerminal Unit which is not too bad, but I think Fin 2 is better.

[Sina Hazratpour 𓃵]

I guess one advantage of WithTerminal Unit is that it is already in mathlib that the inclusion of Unit to WithTerminal Unit is full and faithful -- something I need -- whereas for Fin 1 to Fin 2 one has to prove it anew?

[Adam Topaz]

There should be a fully faithful functor associated to an ordered embedding.

[Markus Himmel]

Yes, but mainly because mathlib is missing the two necessary instances:

import Mathlib

open CategoryTheory

instance {C : Type*} [Category C] [Quiver.IsThin C] {D : Type*} [Category D] (F : C ⥤ D) : Faithful F where

section

variable {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (f : X ↪o Y)

instance : Full (f.monotone.functor) where
  preimage {x y} h := homOfLE (f.map_rel_iff.1 h.le)

end

example : Full (Fin.succEmb 1).monotone.functor := inferInstance
example : Faithful (Fin.succEmb 1).monotone.functor := inferInstance