diff --git a/subgroups.tex b/subgroups.tex index 6cf3821..556dbe5 100644 --- a/subgroups.tex +++ b/subgroups.tex @@ -85,8 +85,18 @@ \subsection{Subgroups as monomorphisms} \begin{lemma} \label{lem:setofsubgroups} Let $G$ be a group and $(H,i_H,!),(H',i_{H'},!):\typemono_G$ be two monomorphisms into $G$. The identity type $(H,i_H,!)\eqto{}(H',i_{H'},!)$ is equivalent to - \marginnote{$$\xymatrix{H\ar[rr]^f_\simeq\ar[dr]_{i_H}&&H'\ar[dl]^{i_{H'}}\\ - &G&}$$} + \marginnote{ + \[ + \begin{tikzpicture}[scale=1.5] + \path (-1,0) node (H) {$H$} + (1,0) node (H') {$H'$} + (0,-1) node (G) {$G$}; + \draw[->] (H) -- node[above] {$f$} node[below] {$\simeq$} (H'); + \draw[->] (H) -- node[below left] {$i_H$} (G); + \draw[->] (H') -- node[below right] {$i_{H'}$} (G); + \end{tikzpicture} + \] + } $$\sum_{f:\Hom(H,H')}\isEq(\US f)\times (i_{H'}\eqto{}i_H f)$$ and is a proposition. In particular, the type $\typemono_G$ of monomorphisms into $G$ is a set. \end{lemma}