3
$\begingroup$

An object K in a category C is called a generator if, for all pairs of morphisms f, g : A → B between arbitrary objects A and B, f = g iff ∀e : K → A. f ◦ e = g ◦ e.

Source: http://events.cs.bham.ac.uk/mgs2012/lectures/ReddyNotes.pdf (Page 7, Definition 3)

Can someone help me break down the meaning of this definition?

for all pairs of morphisms f, g : A → B between arbitrary types A and B

A morphism can be thought of as a a mapping from one type to another?

f and g are morphisms from type A to type B?

f = g iff ∀e : K → A. ...

Morphism f is equivalent to morphism g if and only if for the morphism type K to type A

f ◦ e = g ◦ e

e applied to f is equivalent to e applied to g

Is my interpretation of this correct?

The number of steps in this definition blows my mind, can anyone help me visualize the entire definition?

$\endgroup$
  • 1
    $\begingroup$ This question is probably better suited to math.stackexchange. $\endgroup$ – cody Jul 12 '16 at 15:25
  • $\begingroup$ I am a developer and would like an answer in terms I can relate to, so I will leave this here for a while to see if anyone here can answer. Otherwise, I'll move it. $\endgroup$ – Ben Jul 12 '16 at 15:32
  • $\begingroup$ The title you have chosen is not well suited to representing your question. Please take some time to improve it; we have collected some advice here. Thank you! $\endgroup$ – Raphael Jul 12 '16 at 21:26
6
$\begingroup$

The most obvious intuition comes from the notion of well pointed categories. A well pointed category is simply a category $\cal C$ in which the final object $1$ exists and is a generator for $\cal C$. This means that for every $f,g:A \rightarrow B$, $$ f = g \ \Leftrightarrow \forall p:1\rightarrow A, f\circ p = g\circ p$$

Note that $\circ$ is composition and not application! In haskell you would define:

f `comp` g = \x -> f (g x)

In programmatic notation the definition of well-pointedness gives

f == g iff for all p : () -> A, f `comp` p == g `comp` p

or unfolding the definitions

f == g iff for all p : () -> A, \x:() -> f (p x) == \x:() -> g (p x)

if we assume that the only inhabitant of () is in fact () (which is not the case in haskell, btw), then we get

f == g iff for all p : () -> A, \_ -> f (p ()) == \_ -> g (p ())

assuming extentionality (functions are equal if they are equal on all arguments)

f == g iff for all p, f (p ()) == g (p ())

Now the crucial observation, is that in "reasonable" categories, like $\mathrm{Set}$, morphisms $1\rightarrow A$ can be identified with elements of $A$ which gives

f == g iff for all x : A, f x == g x

which is obviously true in $\mathrm{Set}$ (this is exactly extentionality). Now note that "elements of an object of $\cal C$" doesn't even make sense in a general category, where objects are just "things" that can have morphisms into or out of them.

So the notion of well-pointedness says 2 things:

  1. It's reasonable to treat morphisms $1\rightarrow A$ as "elements" of the object $A$
  2. Extensionality holds.

It's reasonable to generalize this notion by replacing the terminal object $1$ by some arbitrary object $K$.


Now it might be useful to see a category where this doesn't hold (i.e. a category that is not well-pointed) just to see where this intuition can fail.

The simplest example I know of is the category of groups and group morphisms $\mathrm{Grp}$. Here the terminal (and initial) object $1$ is the group $\{e\}$ with a single element $e$, which is the unit for that group, and the operation $e*e=e$.

Because group morphisms must send $e$ to $e_G$ (the unit of $G$), there is always exactly 1 morphism $1\rightarrow G$ for any group $G$, namely, $\phi(e)=e_G$.

But now take any 2 distinct morphisms $f,g:\mathbb{Z}\rightarrow \mathbb{Z}$, for example $f(n) = n$ and $g(n) = 2\cdot n$.

It's not true that $f = g$ iff $\forall p : 1\rightarrow \mathbb{Z}, f\circ p = g\circ p$. Indeed there is only one $p$, namely $\phi$ from above, and $f\circ \phi(e) = g\circ \phi(e) = e_{\mathbb{Z}} = 0$. But $f \neq g$!

So $\mathrm{Grp}$ is not well-pointed, and it's not useful to treat morphisms $1\rightarrow G$ as points of $G$. However, in this case, there happens to be a generating object $K\neq 1$, so the generalization is useful after all! I'll leave it as an exercise to figure out what $K$ is...


I'll try to answer the questions more directly.

A morphism can be thought of as a a mapping from one type to another?

Sort of. It's a good intuition, but you shouldn't think that it always makes sense to talk about elements of type $A$, unless you're working in a well-pointed category as explained above..

Morphism f is equivalent to morphism g if and only if for the morphism type K to type A

It's equal rather than equivalent (though computer scientists tend to define equality in a much stricter sense than category theorists, e.g. by syntactic equality).

Also, it's "if and only if for every morphism from K to A", in general you can have many morphisms in K -> A

e applied to f is equivalent to e applied to g

Composition (written $\circ$) is not application! I've tried to break it down above.

The number of steps in this definition blows my mind, can anyone help me visualize the entire definition?

Category theory often offers very abstract definitions, and it's useful to work through examples and basic lemmas yourself to gain intuition.

However, if this helps, in the $\mathrm{Hask}$ category with types as objects and total programs of type A -> B as morphisms between A and B, the unit type () is a generator, as I tried to explain above.

$\endgroup$
  • $\begingroup$ I'm sure this is correct but it is way above my understanding. I'd be grateful if you could address the questions in my posting directly? $\endgroup$ – Ben Jul 12 '16 at 18:36
  • $\begingroup$ @BenAston Your ultimate question was, "can anyone help me visualize the entire definition?" That's arguably a very broad question, but it seems that's what cody has attempted to answer. $\endgroup$ – Raphael Jul 12 '16 at 21:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.