Epi-Mono decomposition for groups

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

Creative Commons Attribution Share Alike 4.0 International

375 stars 22 forks source link

Epi-Mono decomposition for groups #136

Open marcbezem opened 2 years ago

marcbezem commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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$.