All kinds of lattices

Posted on 2019-07-23 by Oleg Grenrus

This post contains excerpts from a PDF "post" I have written. It looks way better in PDF.

Partial ordered set, or poset for short is well used example in category theory books. Yet, posets are not too familiar for an average CT-curious Haskeller, yet they are easy to visualise! Let’s do exactly that, and mention elementery bits of category theory. In particular, I’ll scan over the six first chapters of Category Theory by Steve Awodey, repeating related definitions and poset examples.1


Definition (Awodey 1.1) A category consist of the following data

  • Objects: A, B, C, \ldots

  • Arrows: f, g, h, \ldots

  • For each arrow f, there are given objects

    \mathrm{dom}(f), \qquad \mathrm{cod}(f)

    called the domain and codomain of f. We write

    f : A \to B

    to indicate that A = \mathrm{dom}(f) and B = \mathrm{cod}(f).

  • Given arrows f : A \to B and g : B \to C, that is, with

    \mathrm{cod}(f) = \mathrm{dom}(g)

    there is given an arrow

    g \circ f : A \to C

    called the composite of f and g.

  • For each object A, there is given an arrow

    1_A : A \to A

    called the identity arrow of A.

  • Associativity:

    h \circ (g \circ f) = (h \circ g) \circ f

    for all f : A \to B, g : B \to C, h : C \to D.

  • Unit:

    f \circ 1_A = f = 1_B \circ f

    for all f : A \to B.

We’ll see how Category type-class is related later, in later section.


Before proceeding, we’ll answer a question: is there a category with posets as objects? Yes, it’s called \mathbf{Pos}! What are the arrows in this category? An arrow from a poset A to a poset B is a function

m : A \to B

that is monotone, in the sense that, for all a, a&39; \in A,

a \le_A a&39; \qquad\text{implies}\qquad m(a) \le_B m(a&39;).

We need to know that 1_A : A \to A is monotone, and also that if f : A \to B and g : B \to C are monotone, then g \circ f : A \to C is monotone. That holds, check!

Recall, posets are categories, so monotone functions are "mappings" between categories. A "homomorphism2 of categories" is called a functor.

Definition (Awodey 1.2) A functor

F : \mathbf{C} \to \mathbf{D}

between categories \mathbf{C} and \mathbf{D} is a mapping of objects to objects and arrows to arrows, in such a way that

  • F (f : A \to B) = F(f) : F(A) \to F(B),

  • F(1_A) = 1_{F(A)},

  • F(g \circ f) = F(g) \circ F(f).

That is, F preserves domains and codomains, identity arrows, and composition. A functor F : \mathbf{C} \to \mathbf{D} thus gives a sort of "picture" – perhaps distorted – of \mathbf{C} in \mathbf{D}.

The  version looks quite different:

class Functor f where
  fmap :: (a -> b) -> f a -> f b

There is a mismatch of a notation of category theory, and what can be written as code. In CT notation F acts both on objects and arrows. In  f acts on objects, and fmap f acts on arrows. Substituting above, id and . into definition of functor, will also give familiar laws

fmap id       = id
fmap (g . f)  = fmap g . fmap f

However,  Functor-class is only for functors from a pseudo-category \mathbf{Hask} to itself, where f, a mapping from types to types is a type-constructor, not arbitrary type family. Functor is a very special case of category theoretical variant.

With small posets, like Bool and M2 we can visualise a monotone function, a functor. Let’s consider a function

f :: Bool -> M2
f True   = M2i
f False  = M2o
Graph of f :: Bool -> M2
Graph of f :: Bool -> M2

The graph of f is on [fig:f-bool-to-m2]. Dotted and dashed lines are arrows in Bool and M2 respectively. We can see on figure, that f indeed gives a picture of Bool in M2.

In  we have only written a mapping of objects, True and False. The mapping of arrows is something we need to check, to be able to claim that f is a functor, and therefore a monotone function. The other way around, there are mappings from Bool to M2 which aren’t monotone, and aren’t functors.

In this section we went backwards. More principal approach would been to first consider functors between poset categories. The monotonicity requirement is implied by first functor requirement. This is a power of category theory. When you look for something, category theory tells you which properties it should have. Once you find something which satisfies the requirements, you know that it’s the right one (up to an isomorphism).

Exponential lattices with M2 are pretty. ZHO -> M2 ([fig:zho2m2]) has nice planar graph. . Yet the final stress test is (ZHO -> ZHO) -> ZHO, or \mathtt{ZHO}^{\mathtt{ZHO}^\mathtt{ZHO}} is on [fig:big]. A beautiful monster.

ZHO -> M2 lattice
ZHO -> M2 lattice
(ZHO -> ZHO) -> ZHO lattice
(ZHO -> ZHO) -> ZHO lattice

  1. If you want to learn category theory, getting a book is a small investment. Your public or university library probably have a copy.

  2. morphism preserving the structure

Site proudly generated by Hakyll