# Injective Representables

by Nicolas Wu

Posted on 7 April 2011

Tags: Category Theory

In this article I’ll show how the injective and surjective properties of a function have a nice relationship with the injectivity of the corresponding representable functors, and how the right cancellative definition of surjection can be derived from the standard one. This is a fairly trivial discussion about a simple observation, so don’t expect anything spectacular.

The definition of injectivity is usually given in the following terms,
where a function is injective when it is *left cancellative*:

his injective iff ∀f,g⋅h.f=h.g⇒f=g

Surjectivity can be described in similar terms, where
a function is surjective when it is *right cancellative*:

his surjective iff ∀f,g⋅f.h=g.h⇒f=g

While these two definitions show the similarity between the injective and surjective properties, this definition of surjectivity isn’t the standard one. The standard definition goes as follows:

his surjective iff ∀y⋅ ∃x⋅hx=y

I don’t like this definition, since I don’t find it easy to work with in proofs, and it doesn’t show the relationship between surjections and injections well.

## Representables

The representables, or Hom-functors, are functions from arrows to arrows in a category.
These functions come in two flavours, the covariant representable, and the
contravariant representable.
Given objects *S* and *T* in a category *ℂ*, we write *ℂ*(*S*,*T*) denote the set
of all arrows from *S* to *T*.

### Covariant Representable

Given a function *h* : *X* → *Y*, the covariant representable, *ℂ*(*S*,−) is defined as:

```
S,—) :: (X -> Y) -> ℂ(S, X) -> ℂ(S, Y)
ℂ(S,—) h f = h . f ℂ(
```

As shorthand for the above, we usually slot the argument *h* into the dash:

`S, h) = ℂ(S,—) h ℂ(`

### Contravariant Representable

Given a function *h* : *X* → *Y*, the contravariant representable, *ℂ*(−,*T*) is defined as:

```
T) :: (X -> Y) -> ℂ(X, T) -> ℂ(Y, T)
ℂ(—,T) h f = f . h ℂ(—,
```

Again, we use the following shorthand, where we slot *h* into the dash:

`T) = ℂ(—,T) h ℂ(h, `

One feature of these representables that I like particularly is that they give rise to a clean correspondence between injectivity and surjectivity.

## Injectivity

The injective Representables give rise to a nice model for injective functions.

### Injective Covariant Reperesentable

The following property holds of covariant representables:

ℂ(S,h) is injective iffhis injective.

#### Proof

First we show that if *h* is injective then *ℂ*(*S*,*h*) is injective:

```
S, h) f == ℂ(S, h) g
ℂ(== {- definition ℂ(S, h) -}
. f == h . g
h => {- injective h -}
== g f
```

Then we show that if *ℂ*(*S*,*h*) is injective then *h* is injective:

```
. f == h . g
h == {- definition ℂ(S, h) -}
S, h) f == ℂ(S, h) g
ℂ(=> {- injective ℂ(S, h) -}
== g f
```

### Injective Contravariant Reperesentable

Here’s a property of the contravariant representable functor:

ℂ(h,S) is injective iffhis surjective.

#### Proof

We work with the contrapositive to show that
if *h* is surjective, then *ℂ*(*h*,*S*) is injective:

```
f ≠ g== {- definition inequality -}
. f y ≠ g y
∃ y == {- surjective h -}
. f (h x) ≠ g (h x)
∃ x == {- definition inequality -}
. h ≠ g . h
f == {- definition ℂ(h, S) -}
S) f ≠ ℂ(h, S) g ℂ(h,
```

Finally we show that if *h* is not surjective, then *ℂ*(*h*,*S*) is not injective:

```
let h 0 = 0 {- h : {0} -> {0,1} -}
let f 0 = 0, f 1 = 0
let g 0 = 0, g 1 = 1
```

then

```
. h = g . h
f == {- definition ℂ(h, S) -}
S) f = ℂ(h, S) g ℂ(h,
```

but

` f ≠ g`

Sadly, I don’t like this part of the proof, since it involves finding a counterexample
to the injectivity of *ℂ*(*h*,*S*) when *h* is not surjective, and I prefer
constructive proofs.
Nevertheless, we’ve shown that *ℂ*(*h*,*S*) is injective iff *h* is surjective, which gives us
the right cancellative definition of surjection.