Epi-Mono decomposition for groups

[marcbezem]

The title refers to \cref{con:im}, currently Construction 5.3.11.

• Wouldn't we also need for \circ to be an equivalence that the constructed equivalence (j,q) is unique? We prove this in \cref{thm:n-im-univ-prop}, currently Theorem 3.10.17.
• If yes, then I think we also need that the pointing path of the equivalence (j,q) is unique. Perhaps this is easy because in 5.3 we are dealing with groupoids? We don't do that (yet) in 3.10.
• Do we need the universal property of the n-image for pointed maps for n>0?
• Minor: in the indented text block in the implementation of \cref{con:im}: qj ---> jq; in footnote 4: qx ---> q(x).

[DanGrayson]

I don't understand all of what you say, but it seems to me that the proof currently addresses uniqueness. And since the basepoint of the middle object is obtained by applying p to the basepoint of X, the identity between the images preserves basepoints.

[marcbezem]

The question in the first point came up when I tried to understand why $\circ$ is an equivalence. The problem is the third argument $\alpha$. If, for example, the image has a non-trivial auto-equivalence $e$ such that $ep = p$ and $je = j$, then $jep = jp$, and composition would not be an equivalence. (Here I mean $p$ and $j$ as in the image factorization.) So it seems essential that we prove in Theorem 3.10.17 that $e$ is unique. We do this by cancelling the $n$-connected map $p$ on the right: $ep = p$ implies $e = id$.