diff --git a/.cspell.json b/.cspell.json
index 50979502..158edf39 100644
--- a/.cspell.json
+++ b/.cspell.json
@@ -110,6 +110,7 @@
"cosymmetry",
"cotransitive",
"cotransitivity",
+ "counit",
"counital",
"delooping",
"deloopings",
diff --git a/databases/catdat/data/functors/enveloping_group.yaml b/databases/catdat/data/functors/enveloping_group.yaml
new file mode 100644
index 00000000..45812add
--- /dev/null
+++ b/databases/catdat/data/functors/enveloping_group.yaml
@@ -0,0 +1,54 @@
+id: enveloping_group
+name: enveloping group functor
+notation: $F_{\Mon,\Grp}$
+source: Mon
+target: Grp
+description: 'This functor maps a monoid $M$ to the group $F(M)$ that is equipped with a universal homomorphism $i_M : M \to F(M)$. It is called the (universal) enveloping group or the group completion of $M$; in the commutative case, it is known as the Grothendieck group of $M$. As a possible construction of $F(M)$, take the free group on generators $\underline{m}$ for $m \in M$ subject to the relations $\underline{1} = 1$ and $\underline{m \cdot n} = \underline{m} \cdot \underline{n}$.'
+nlab_link: https://ncatlab.org/nlab/show/free+functor
+
+tags:
+ - algebra
+ - free
+
+related_functors:
+ - free_group
+
+satisfied_properties:
+ - property: left adjoint
+ proof: 'By definition, this functor is left adjoint to the forgetful functor $U_{\Grp,\Mon} : \Grp \to \Mon$.'
+
+ - property: essentially surjective
+ proof: 'In fact, the counit of the adjunction $F \circ U_{\Grp,\Mon} \to \id_{\Grp}$ is an isomorphism since the right adjoint $U_{\Grp,\Mon}$ is fully faithful (Prop. 3.4 at the nLab).'
+
+ - property: preserves finite products
+ proof: >-
+ Since $F(1)=1$, we only need to consider binary products. The canonical homomorphism
+ $$\alpha : F(M \times N) \to F(M) \times F(N)$$
+ is defined by $p_i \alpha = F(p_i)$ and satisfies
+ $$\alpha(i_{M \times N}(m,n)) = (i_M(m),i_N(n)).$$
+ We construct an inverse homomorphism
+ $$\beta : F(M) \times F(N) \to F(M \times N)$$
+ as follows.
+ The two canonical homomorphisms $M \rightarrow M \times N \leftarrow N$ induce homomorphisms $F(M) \rightarrow F(M \times N) \leftarrow F(N)$. We claim that for every pair of elements $x \in F(M)$, $y \in F(N)$, their images in $F(M \times N)$ commute. Notice that $x$ is a product of elements of the form $i_M(m)$ or $i_M(m)^{-1}$ for $m \in M$, and likewise $y$ is a product of elements of the form $i_N(n)$ or $i_N(n)^{-1}$ for $n \in N$. Thus, by standard arguments from group theory, it suffices to prove that the images of $i_M(m)$ and $i_N(n)$ commute in $F(M \times N)$. This follows since the images of $m$ and $n$ in $M \times N$ commute.
+ Therefore, the two homomorphisms induce a homomorphism $\beta : F(M) \times F(N) \to F(M \times N)$. It is characterized by
+ $$\beta(i_M(m),1) = i_{M \times N}(m,1),\quad \beta(1,i_N(n)) = i_{M \times N}(1,n).$$
+ It is straightforward to check that it is inverse to $\alpha$ by arguing with the generators in both groups.
+
+unsatisfied_properties:
+ - property: faithful
+ proof: 'Take any non-trivial monoid $M$ with an absorbing element, such as $(\IN,\cdot,1)$. Its enveloping group is trivial. Hence, $\id_M,1 : M \rightrightarrows M$ provide a counterexample.'
+
+ - property: full
+ proof: 'We have $F(\IN) = \IZ$ (w.r.t. addition). The homomorphism $\IZ \to \IZ$, $x \mapsto -x$ is not induced by a homomorphism $\IN \to \IN$.'
+
+ - property: preserves monomorphisms
+ proof: 'Consider the monoid $N = \langle a,b,c : ab = ac \rangle_{\Mon}$ and the free monoid $M = \langle b,c \rangle_{\Mon}$. The canonical homomorphism $M \to N$ is injective. However, $F(M) = \langle b,c \rangle_{\Grp}$ (free group), and $b,c$ become identified in $F(N) \cong \langle a,b,c : b = c \rangle_{\Grp}$ since we may cancel $a$, so that $F(M) \to F(N)$ is not injective.'
+
+ - property: preserves products
+ proof: >-
+ We will find a family of monoids $(M_n)_{n \in \IN}$ such that the canonical homomorphism
+ $$\textstyle \alpha : F(\prod_{n \in \IN} M_n) \to \prod_{n \in \IN} F(M_n)$$
+ is not an isomorphism. We first remark that this is true for commutative monoids, so a counterexample must be non-commutative.
+ For $n \in \IN$ let $M_n$ be the free monoid on two generators $a,b$. Then $F(M_n)$ is the free group on these generators. Define $g = (g_n)_{n \in \IN} \in \prod_{n \in \IN} F(M_n)$ by $g_n \coloneqq (a b^{-1})^n$. Assume that $g$ has a preimage under $\alpha$. It is a finite product $X_1 \cdots X_L$, where either $X_i \in \prod_{i \in \IN} M_n$ or $X_i^{-1} \in \prod_{i \in \IN} M_n$, and $L \in \IN$ is a fixed length. For sufficiently large $n \in \IN$ let $x_i \coloneqq \pi_n(X_i) \in M_n \cup M_n^{-1}$, so that
+ $$(a b^{-1})^n = x_1 \cdots x_L.$$
+ Each $x_i$ is either a "completely positive" word (such as $a^2 b^3 a$) in $a,b$ or a "completely negative" word in $a,b$ (such as $b^{-1} a^{-1} b^{-2}$). The normal form of $x_1 \cdots x_L$ can therefore have at most $L$ alternations between positive and negative letters. But $(a b^{-1})^n = a b^{-1} \cdots a b^{-1}$ is in normal form and has $2n$ such alternations. It follows that $2n \leq L$. Since $n$ was arbitrary, this is a contradiction.
diff --git a/databases/catdat/data/functors/forget_abelian.yaml b/databases/catdat/data/functors/forget_abelian.yaml
index 59a2ff1c..d834a8a8 100644
--- a/databases/catdat/data/functors/forget_abelian.yaml
+++ b/databases/catdat/data/functors/forget_abelian.yaml
@@ -13,6 +13,7 @@ tags:
related_functors:
- forget_group
+ - forget_inverses
satisfied_properties:
- property: full
diff --git a/databases/catdat/data/functors/forget_inverses.yaml b/databases/catdat/data/functors/forget_inverses.yaml
new file mode 100644
index 00000000..468c8f1c
--- /dev/null
+++ b/databases/catdat/data/functors/forget_inverses.yaml
@@ -0,0 +1,32 @@
+id: forget_inverses
+name: forgetful functor from groups to monoids
+notation: $U_{\Grp,\Mon}$
+source: Grp
+target: Mon
+description: This functor maps a group to its underlying monoid. We view groups as structured sets $(X,m,e,i)$ (consisting of a set, a multiplication, a neutral element, and an inverse operation), and monoids as structured sets $(X,m,e)$. This forgetful functor precisely maps $(X,m,e,i)$ to $(X,m,e)$. From this point of view, it does not merely forget a property; it forgets an operation. This perspective is useful in contexts where the inverse operation is no longer reducible to a property, for example, the forgetful functor from topological groups to topological monoids.
+nlab_link: https://ncatlab.org/nlab/show/forgetful+functor
+left_adjoint: enveloping_group
+
+tags:
+ - algebra
+ - forgetful
+
+related_functors:
+ - forget_abelian
+
+satisfied_properties:
+ - property: faithful
+ proof: This is trivial.
+
+ - property: full
+ proof: It is a standard fact from group theory that a multiplicative map already preserves inverses.
+
+ - property: right adjoint
+ proof: Every forgetful functor between algebraic categories is a right adjoint. This functor is right adjoint to the enveloping group functor $\Mon \to \Grp$.
+
+ - property: left adjoint
+ proof: 'This functor is left adjoint to the functor $(-)^{\times} : \Mon \to \Grp$ that sends a monoid $M$ to its group of units $M^{\times} \coloneqq \{(a,b) \in M^2 : ab = ba = 1 \}$. In fact, if $M$ is a monoid and $G$ is a group, there is a bijection $\Hom(U_{\Grp,\Mon}(G),M) \to \Hom(G,M^{\times})$ given by mapping $\varphi$ to $g \mapsto (\varphi(g),\varphi(g^{-1}))$.'
+
+unsatisfied_properties:
+ - property: essentially surjective
+ proof: This is trivial.
diff --git a/databases/catdat/data/functors/group_units.yaml b/databases/catdat/data/functors/group_units.yaml
new file mode 100644
index 00000000..8efc64cf
--- /dev/null
+++ b/databases/catdat/data/functors/group_units.yaml
@@ -0,0 +1,56 @@
+id: group_units
+name: group of units functor
+notation: $(-)^{\times}$
+source: Mon
+target: Grp
+description: This functor maps a monoid $M$ to its group of units $M^{\times}$, consisting of pairs $(a,b) \in M^2$ satisfying $ab=ba=1$. Equivalently, it takes the submonoid of invertible elements of $M$, equipped with the inverse operation.
+nlab_link: https://ncatlab.org/nlab/show/group+of+units
+left_adjoint: forget_inverses
+
+tags:
+ - algebra
+
+related_functors: []
+
+satisfied_properties:
+ - property: essentially surjective
+ proof: If $G$ is a group, then $G$ is isomorphic to its group of units.
+
+ - property: right adjoint
+ proof: This functor is right adjoint to the forgetful functor $\Grp \to \Mon$.
+
+ - property: finitary
+ proof: 'There is a direct way to prove this, but here is an abstract argument: Since the forgetful functor $\Grp \to \Set$ is conservative and finitary, it suffices to prove that the composition $\Mon \to \Set$, which maps a monoid to its set of units, is finitary. This functor is represented by the monoid $\langle x,y : xy = yx = 1 \rangle \cong \IZ$. It has a finite presentation and hence is finitely presentable in the categorical sense (Corollary 3.13 in Adamek-Rosicky).'
+
+ - property: preserves coproducts
+ proof: >-
+ We need to prove that for every family of monoids $(M_i)_{i \in I}$ the canonical map
+ $$\textstyle \coprod_{i \in I} M_i^{\times} \to \bigl(\coprod_{i \in I} M_i\bigr)^{\times}$$
+ is an isomorphism. Notice that coproducts of monoids and groups have the same element structure; they are free products. From this, it follows immediately that the map is injective. For surjectivity, assume that $x = x_1 \cdots x_n$ and $y = y_1 \cdots y_m$ are reduced words in $\coprod_{i \in I} M_i$ with $xy = 1$ and $yx = 1$. We will prove by induction on $n$ that $n = m$ and that each $x_j$ is a unit in the corresponding monoid $M_{i_j}$.
+
+ If $n = 0$, i.e. $x = 1$, then we have $y = 1$, so $m = 0$, and the claim is true.
+
+ Let $n \geq 1$. The product $xy= x_1 \cdots x_n y_1 \cdots y_m$ would be in reduced form if $x_n$ and $y_1$ belong to different monoids; likewise, if they belong to the same monoid but $x_n y_1 \neq 1$. In that case, its free product length would be $n + m \geq 1$, so it could not evaluate to $1$. Thus, $x_n$ and $y_1$ necessarily belong to the same monoid, say $M_k$, and satisfy $x_n y_1 = 1$ in $M_k$. In particular, this implies that $m \geq 1$.
+
+ Next, consider the shorter elements $\tilde{x} \coloneqq x_1 \cdots x_{n-1}$ and $\tilde{y} \coloneqq y_2 \cdots y_m$, which are still in reduced form. Since $x_n y_1 = 1$, it follows that $1 = xy = \tilde{x} \tilde{y}$. On the other hand,
+ $$\tilde{y}\tilde{x} = (x_n y_1) \tilde{y} \tilde{x} (x_n y_1) = x_n (y x) y_1 = x_n y_1 = 1.$$
+ Thus, by the induction hypothesis applied to the pair $(\tilde{x},\tilde{y})$, all $x_1,\dotsc,x_{n-1}$ are units and $n-1 = m-1$, hence $n = m$. Moreover,
+ $$1 = y x = y_1 (\tilde{y} \tilde{x}) x_n = y_1 x_n,$$
+ which shows that $1 = y_1 x_n$ in $M_k$. Combined with $x_n y_1 = 1$, this shows that $x_n$ is a unit as well.
+
+unsatisfied_properties:
+ - property: conservative
+ proof: If $M$ is the free monoid on one generator (i.e. $\IN$ w.r.t. addition), then $M^{\times}$ is trivial, but $M$ is not. Hence, the unique homomorphism $1 \to M$ provides a counterexample.
+
+ - property: faithful
+ proof: If $M$ is the free monoid on one generator (i.e. $\IN$ w.r.t. addition), then $M^{\times}$ is trivial, but $M$ is not. Hence, the identity $M \to M$ and the trivial homomorphism $M \to M$ have the same image under the functor, but they are not equal.
+
+ - property: full
+ proof: Let $M$ be a monoid and $G \subseteq M$ be its group of units. Then the identity $M^{\times} \to G^{\times} = G$ is in the image of the functor iff there is a homomorphism $M \to G$ that extends the identity on $G$, i.e. a retraction of $G \subseteq M$. If $M$ has an absorbing element, then its image in $G$ would be an absorbing element, forcing $G$ to be trivial. However, the monoid $(\IZ,\cdot,1)$, for example, has an absorbing element and a non-trivial group of units $\{\pm 1\}$.
+
+ - property: preserves coequalizers
+ proof: >-
+ Let $M$ be the free monoid on two generators $x,y$. Consider the homomorphism $\varphi : M \to M$ defined by $\varphi(x)=xy$, $\varphi(y)=yx$. Also consider the trivial homomorphism $\psi : M \to M$, $m \mapsto 1$. The coequalizer of these in $\Mon$ is $\langle x,y : xy=yx=1 \rangle \cong \IZ$, whose group of units is again $\IZ$. However, since $M^{\times}$ is trivial, the coequalizer of $\varphi^{\times},\psi^{\times} : M^{\times} \rightrightarrows M^{\times}$ in $\Grp$ is the trivial group.
+
+ - property: preserves epimorphisms
+ proof: The inclusion $\IN \hookrightarrow \IZ$ is an epimorphism of monoids. It is mapped to the trivial homomorphism $\{0\} \hookrightarrow \IZ$, which is not an epimorphism of groups.