Inversion on an internal groupoid

44 Views Asked by At

Let $\mathcal{C}$ be a category with pullbacks, with $\mathscr{G}=({\bf Ob}_\mathscr{G},{\bf Hom}_\mathscr{G},cod,dom,{\bf 1}, \circ_{\mathscr{G}},-^{-1})$ an internal groupoid in $\mathcal{C}$. I'm trying to see that $-^{-1}\circ-^{-1}=1_{{\bf Hom}_\mathscr{G}}$, and the best I've got so far is the following somewhat ugly series of identities:

$$1_{{\bf Hom}_\mathscr{G}}=p_0\circ\langle1_{{\bf Hom}_\mathscr{G}},dom\rangle=\circ_\mathscr{G}\circ(1_{{\bf Hom}_\mathscr{C}}\times_{{\bf Ob}_\mathscr{C}}{\bf 1})\circ\langle1_{{\bf Hom}_\mathscr{G}},dom\rangle$$

$$=\circ_\mathscr{G}\circ(1_{{\bf Hom}_\mathscr{C}}\times_{{\bf Ob}_\mathscr{C}}{\bf 1})\circ\langle1_{{\bf Hom}_\mathscr{G}},dom\circ-^{-1}\circ-^{-1}\rangle=\circ_\mathscr{G}\circ\langle1_{{\bf Hom}_\mathscr{G}},{\bf 1}\circ dom\circ-^{-1}\circ-^{-1}\rangle$$

$$=\circ_\mathscr{G}\circ\langle1_{{\bf Hom}_\mathscr{G}},\circ_\mathscr{G}\circ\langle-^{-1},1_{{\bf Hom}_\mathscr{G}}\rangle\circ-^{-1}\circ-^{-1}\rangle=\circ_\mathscr{G}\circ\langle\circ_\mathscr{G}\circ\langle1_{{\bf Hom}_\mathscr{G}},-^{-1}\rangle,-^{-1}\circ-^{-1}\rangle$$ $$=\circ_\mathscr{G}\circ\langle{\bf 1}\circ cod,-^{-1}\circ-^{-1}\rangle=\circ_\mathscr{G}\circ\langle{\bf 1}\circ cod\circ-^{-1}\circ-^{-1},-^{-1}\circ-^{-1}\rangle$$

$$=\circ_\mathscr{G}\circ\langle{\bf 1}\circ cod,1_{{\bf Hom}_\mathscr{G}}\rangle\circ-^{-1}\circ-^{-1}=1_{{\bf Hom}_\mathscr{G}}\circ-^{-1}\circ-^{-1}=-^{-1}\circ-^{-1}.$$

These were obtained by staring at the following simpler identities for a sufficiently long time:

$$f=f\circ1_{dom(f)}=f\circ(f^{-1}\circ(f^{-1})^{-1})=(f\circ f^{-1})\circ(f^{-1})^{-1}=1_{cod((f^{-1})^{-1})}\circ(f^{-1})^{-1}=(f^{-1})^{-1}.$$

I've begun the diagram chase to verify that this all shakes out, however this strikes me as a very cumbersome proof for something I'd think was simple and trivial to show -- the authors of the book I'm working through that mention this fact in passing seem to think so as well.

Is there a simpler proof that I've missed, perhaps obtained by Yoneda embedding $\mathcal{C}$ and considering ${\bf Hom}_\mathcal{C}(-,{\bf Hom}_\mathscr{G}):\mathcal{C}^{op}\to{\bf Set}$ or something along these lines?