2
$\begingroup$

I'm trying to show that the categories $\mathcal{P}(X)$ and $Sub(X)$ are equivalent.

According to Steve Awodey's "Category Theory" I need to find two functors

  • $ E: \mathcal{P}(X) \to Sub(X)$
  • $F: Sub(X) \to \mathcal{P}(X)$

and a pair of natural isomorphisms

  • $\alpha: 1_{\mathcal{P}(X)} \overset{\sim}{\to} F \circ E$
  • $\beta: 1_{Sub(X)}: \overset{\sim}{\to} E \circ F$

I believe I've constructed E and F correctly on the objects. On object $Y \in \mathcal{P}(X)$ I define $E(Y) = \lambda y. y$, and since $Y$ is a subset of $X$ this has the type $Y \to X$ as required.

On object $f \in Sub(X)$ I define $E(f) = \lbrace f(x) \mid x \in \mathsf{dom}(f) \rbrace \subseteq X$ as required.

I'm not sure how I define the functors on morphisms in both cases though.

Edit: I forgot to define $Sub(X)$, so here's a definition:

The objects in $Sub(X)$ are monomorphisms $m$ with $cod(m) = X$ and the given two objects $m$ and $m'$ an arrow in $Sub(X)$ is $f: m \to m'$ such that $m = m' \circ f$. Hopefully that clears things up.

$\endgroup$
  • 1
    $\begingroup$ You'll have to be more specific - it is not clear how $\mathcal{Sub}(X)$ is defined differently from $\mathcal{P}(X)$. $\endgroup$ – Thomas Andrews Apr 27 '15 at 21:25
  • $\begingroup$ Oh sorry. I've added a definition in an edit now $\endgroup$ – Michael Apr 27 '15 at 21:30
  • 1
    $\begingroup$ I think you can work less. If you prove that one of your functors is full, faithfull and essentially surjective on objects you're done. $\endgroup$ – Abellan Apr 27 '15 at 21:50
1
$\begingroup$

Well, what are the arrows in $P(X)$?
I assume it is the poset category, ie. the arrows are just the inclusions $Y_1\subseteq Y_2$.

Basically $E$ is the identity, also on arrows: for $Y_1\subseteq Y_2\subseteq X$, $\ E$ maps it to the identical inclusions $Y_1\hookrightarrow Y_2\hookrightarrow X$.

On the other hand, for an $f:m\to m'$, i.e. $m=m'\circ f$, first prove that $f$ is also a monomorphism, then take its image and map all these into $X$ by $m'$.

| cite | improve this answer | |
$\endgroup$

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.