diff --git a/.vscode/settings.json b/.vscode/settings.json
index 9074afb3b..89fdf748c 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -88,6 +88,7 @@
"coreflexivity",
"coregular",
"corelations",
+ "corestrict",
"corestriction",
"corestricts",
"cosifted",
@@ -201,6 +202,8 @@
"Rosicky",
"saft",
"Schapira",
+ "semigroup",
+ "semigroups",
"semisimple",
"setoid",
"Sheafifiable",
@@ -214,6 +217,7 @@
"subposet",
"subproset",
"subscheme",
+ "subsemigroup",
"subsheaf",
"summands",
"suprema",
diff --git a/databases/catdat/data/001_categories/002_algebra.sql b/databases/catdat/data/001_categories/002_algebra.sql
index e10e6b4c1..9d6344f72 100644
--- a/databases/catdat/data/001_categories/002_algebra.sql
+++ b/databases/catdat/data/001_categories/002_algebra.sql
@@ -26,6 +26,15 @@ VALUES
'This is the prototype of a finitary algebraic category.',
'https://ncatlab.org/nlab/show/Grp'
),
+(
+ 'SemiGrp',
+ 'category of semigroups',
+ '$\SemiGrp$',
+ 'semigroups, i.e. sets equipped with an associative binary operation',
+ 'maps preserving the binary operation',
+ 'In contrast to monoids, semigroups do not need to have a neutral element, and in fact, they can be empty. This small difference has a huge impact on the categorical properties. For example, we do not have a zero object anymore.',
+ 'https://ncatlab.org/nlab/show/semigroup'
+),
(
'Vect',
'category of vector spaces',
diff --git a/databases/catdat/data/001_categories/100_related-categories.sql b/databases/catdat/data/001_categories/100_related-categories.sql
index 2b76e80aa..d8c69d678 100644
--- a/databases/catdat/data/001_categories/100_related-categories.sql
+++ b/databases/catdat/data/001_categories/100_related-categories.sql
@@ -61,6 +61,7 @@ VALUES
('Grp', 'FinGrp'),
('Grp', 'Ab'),
('Grp', 'Mon'),
+('Grp', 'SemiGrp'),
('FinGrp', 'Grp'),
('FinGrp', 'FinAb'),
('Haus', 'Top'),
@@ -86,6 +87,7 @@ VALUES
('Mon', 'CMon'),
('Mon', 'Grp'),
('Mon', 'Cat'),
+('Mon', 'SemiGrp'),
('N', 'N_oo'),
('N', 'On'),
('N', 'Z_div'),
@@ -110,6 +112,8 @@ VALUES
('Rng', 'Ring'),
('Sch', 'LRS'),
('Sch', 'Z'),
+('SemiGrp', 'Mon'),
+('SemiGrp', 'Grp'),
('Set_c', 'Set'),
('Set_c', 'FinSet'),
('Set_f', 'Set'),
diff --git a/databases/catdat/data/001_categories/200_category-tags.sql b/databases/catdat/data/001_categories/200_category-tags.sql
index f9d97dab0..95dfde10f 100644
--- a/databases/catdat/data/001_categories/200_category-tags.sql
+++ b/databases/catdat/data/001_categories/200_category-tags.sql
@@ -74,6 +74,7 @@ VALUES
('Ring', 'algebra'),
('Rng', 'algebra'),
('Sch', 'algebraic geometry'),
+('SemiGrp', 'algebra'),
('Set_c', 'set theory'),
('Set_f', 'set theory'),
('Set', 'set theory'),
diff --git a/databases/catdat/data/003_category-property-assignments/SemiGrp.sql b/databases/catdat/data/003_category-property-assignments/SemiGrp.sql
new file mode 100644
index 000000000..f88654504
--- /dev/null
+++ b/databases/catdat/data/003_category-property-assignments/SemiGrp.sql
@@ -0,0 +1,134 @@
+INSERT INTO category_property_assignments (
+ category_id,
+ property_id,
+ is_satisfied,
+ reason
+)
+VALUES
+(
+ 'SemiGrp',
+ 'locally small',
+ TRUE,
+ 'There is a forgetful functor $\SemiGrp \to \Set$ and $\Set$ is locally small.'
+),
+(
+ 'SemiGrp',
+ 'finitary algebraic',
+ TRUE,
+ 'Take the algebraic theory of a semigroup.'
+),
+(
+ 'SemiGrp',
+ 'strict initial object',
+ TRUE,
+ 'This is because the initial object is the empty semigroup, and a non-empty set has no map to an empty set.'
+),
+(
+ 'SemiGrp',
+ 'disjoint coproducts',
+ TRUE,
+ 'This follows easily from the concrete description of coproducts as (a variant of) free products.'
+),
+(
+ 'SemiGrp',
+ 'cocartesian cofiltered limits',
+ TRUE,
+ 'We need to prove that for two cofiltered diagram of semigroups $(B_i)$, $(C_i)$ the canonical map
+ $$\textstyle \alpha : \lim_i B_i + \lim_i C_i \to \lim_i (B_i + C_i)$$
+ is an isomorphism, i.e. bijective. The underlying set of the coproduct $B_i + C_i$ is identified with the disjoint union of sets of the form
+ $$B_i \times C_i \times B_i \times \cdots \times C_i$$
+ with any positive product length, starting and ending either with $B_i$ or $C_i$. Moreover, $\lim_i$ commutes with arbitrary coproducts in $\Set$, and of course also with products. This shows that $\alpha$ is bijective.'
+),
+(
+ 'SemiGrp',
+ 'skeletal',
+ FALSE,
+ 'This is trivial.'
+),
+(
+ 'SemiGrp',
+ 'balanced',
+ FALSE,
+ 'The inclusion of additive semigroups $\IN \hookrightarrow \IZ$ is a counterexample. Indeed, if $f,g : \IZ \to G$ are semigroup homomorphisms which agree on $\IN$, the element $e := f(0) = g(0)$ provides a neutral element for $eGe$, which therefore becomes a monoid, and $f,g$ corestrict to monoid homomorphisms $f,g : \IZ \to eGe$ which agree on $\IN$. And we already know that $f = g$ in that case (inverses are uniquely determined).
+ Another example can be found in MO/510431.'
+),
+(
+ 'SemiGrp',
+ 'Malcev',
+ FALSE,
+ 'Consider the subsemigroup $\{(a,b) : a \leq b \}$ of $\IN^2$ under addition.'
+),
+(
+ 'SemiGrp',
+ 'co-Malcev',
+ FALSE,
+ 'See MO/509552: Consider the forgetful functor $U : \SemiGrp \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) := \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by the free semigroup on a single generator and $R$ by the free semigroup on two generators $x,y$ subject to the relation $xy=x^2$. It is clear that $R$ is reflexive, but not symmetric.'
+),
+(
+ 'SemiGrp',
+ 'semi-strongly connected',
+ FALSE,
+ 'Let us first remark that every non-empty finite semigroup $A$ has an idempotent element $e$, and then $B \to A$, $x \mapsto e$ does define a semigroup homomorphism for any $B$. Therefore, counterexamples need to be infinite and also without idempotent elements.
+ Let $A$ be the set of positive rational numbers of the form $m/2^n$ (with $m > 0$, $n \geq 0$), and let $B$ be the set of positive rational numbers of the form $m/3^n$ (with $m > 0$, $n \geq 0$). Both are semigroups under addition. The element $1 \in A$ is $2^\infty$-divisible, meaning that for every $n \geq 0$ there is some $a \in A$ with $1 = 2^n \cdot a$. But $B$ has no $2^\infty$-divisible element. Hence, there is no semigroup homomorphism $A \to B$. Likewise, there is no semigroup homomorphism $B \to A$.'
+),
+(
+ -- TODO: find a variant of the lemma missing_cogenerating_sets (or missing_cogenerator) which handles this.
+ 'SemiGrp',
+ 'cogenerating set',
+ FALSE,
+ 'The proof is similar to the proof for $\Grp$. Assume that there is a cogenerating set $S$. There is an infinite simple group $G$ larger than all the semigroups in $S$ (such as an alternating group). Since $\id_G, 1 : G \rightrightarrows G$ are different, there is a semigroup $H \in S$ and a homomorphism of semigroups $f : G \to H$ with $f \neq f \circ 1$. Then
+ $$N := \{g \in G : f(g) = f(1)\}$$
+ is a normal subgroup of $G$. It is proper, and hence trivial. But then $f$ is injective, which is a contradiction.'
+),
+(
+ 'SemiGrp',
+ 'cofiltered-limit-stable epimorphisms',
+ FALSE,
+ 'We already know that $\Set$ does not have this property (by this result). Now apply the contrapositive of the dual of this lemma to the functor $\Set \to \SemiGrp$ that equips a set with the multiplication $a \cdot b := a$.'
+),
+(
+ 'SemiGrp',
+ 'effective cocongruences',
+ FALSE,
+ 'The proof is similar to $\Mon$, i.e. we adapt the counterexample from MO/510744. Namely, consider the semigroups
+ $$\begin{align*} X & := \langle p \mid p^2 = p \rangle,\\
+ E & := \langle p, q \mid p^2 = p,\, q^2 = q,\, pq = q,\, qp = p \rangle,
+ \end{align*}$$
+ whose underlying sets are $\{p\}$ and $\{p,q\}$, respectively. Then $X$ represents the functor sending a semigroup $A$ to its idempotents, and $E$ represents the relation on idempotents $a, b$ of $A$ that $ab = b$, $ba = a$. It is easy to check that this defines an equivalence relation (see MO/510744 for details). Since $p \ne q$ in $E$, the equalizer of the two maps $X \rightrightarrows E$ is the empty semigroup. Therefore, if $E$ were effective, it would be isomorphic to the coproduct $X \sqcup X$, whose underlying set consists of non-empty words in $p,q$ with $p,q$ strictly alternating. In particular, in this coproduct, $pq \ne q$.'
+),
+(
+ 'SemiGrp',
+ 'natural numbers object',
+ FALSE,
+ 'Assume that a natural numbers object exists. Then by this result, for every semigroup $A$ the natural homomorphism
+ $$\textstyle\alpha : \coprod_{n \geq 0} A \to A \times \coprod_{n \geq 0} 1$$
+ is a split monomorphism. But this is not true: For each $n \geq 0$ let $A_n$ denote a copy of $A$. The elements of the coproduct in $\alpha$''s domain have a unique representation as
+ $$x_{n_1} * \cdots * x_{n_s}$$
+ with $x_i \in A_i$ and $n_i \neq n_{i+1}$, and we have
+ $$\alpha(x_{n_1} * \cdots * x_{n_s}) = (x_{n_1} \cdots x_{n_s}, n_1 * \cdots * n_s).$$
+ In particular, if $A$ has two non-equal commuting elements $x,y$ (for example, if $A$ is any non-trivial monoid), we have
+ $$\alpha(y_0 x_0) = \alpha(x_0 y_0),$$
+ showing that $\alpha$ is not injective.'
+),
+(
+ 'SemiGrp',
+ 'coregular',
+ FALSE,
+ 'We will find a regular monomorphism $\iota : F \to M$ of semigroups and a homomorphism $F \to K$ such that $K \to K \sqcup_F M$ is not injective. It is similar to our example for $\Mon$. Consider these semigroups defined by generators and relations:
+ $$\begin{align*}
+ F & := \langle a,b,c,d \rangle \\
+ M & := \langle a,b,c,d,s : as = c, \, bs = d \rangle \cong \langle a,b,s \rangle \\
+ K & := \langle x,c,d \rangle \\
+ N & := \langle a,b,c,d,s_0,s_1 : as_i = c, \, bs_i = d \rangle \\
+ & \cong \langle a,b,s_0,s_1 : a s_0 = a s_1, \, b s_0 = b s_1 \rangle \\
+ \end{align*}$$
+ There is a canonical homomorphism $\iota : F \to M$, which is the equalizer of the two canonical homomorphisms $M \rightrightarrows N$ defined by $s \mapsto s_i$. We define $F \to K$ by $a \mapsto x$, $b \mapsto x$, $c \mapsto c$, $d \mapsto d$. Then
+ $$K \sqcup_F M \cong \langle x,c,d,s : x s = c,\, x s = d \rangle$$
+ shows that $c,d \in K$ have the same image in the pushout.'
+),
+(
+ 'SemiGrp',
+ 'regular subobject classifier',
+ FALSE,
+ 'Assume that a regular subobject classifier $\Omega$ exists in $\SemiGrp$. The universal regular monomorphism $\top : 1 \to \Omega$ corresponds to an idempotent element $e \in \Omega$. It follows that $e \Omega e$ is a monoid with neutral element $e$. We claim that it is a regular subobject classifier in $\Mon$, which we know does not exist. Indeed, let $\iota : A \to B$ be a regular monomorphism of monoids. Since the forgetful functor $\Mon \to \SemiGrp$ preserves limits, we can also see $\iota$ as a regular monomorphism of semigroups. Hence, there is a unique homomorphism of semigroups $f : B \to \Omega$ with $\iota(A) = \{b \in B : f(b) = e\}$. Since $1 \in \iota(A)$, we have $f(1) = e$. Then $f$ corresponds to a homomorphism of monoids $f : B \to e \Omega e$ with kernel $\iota$, which proves our claim.'
+);
\ No newline at end of file
diff --git a/databases/catdat/data/005_special-objects/002_initial_objects.sql b/databases/catdat/data/005_special-objects/002_initial_objects.sql
index 29b8868f5..763f583dd 100644
--- a/databases/catdat/data/005_special-objects/002_initial_objects.sql
+++ b/databases/catdat/data/005_special-objects/002_initial_objects.sql
@@ -44,6 +44,7 @@ VALUES
('Ring', 'ring of integers'),
('Rng', 'trivial ring'),
('Sch', 'empty scheme'),
+('SemiGrp', 'empty semigroup'),
('Set_c', 'empty set'),
('Set_f', 'empty set'),
('Set', 'empty set'),
diff --git a/databases/catdat/data/005_special-objects/003_terminal_objects.sql b/databases/catdat/data/005_special-objects/003_terminal_objects.sql
index 4f8841015..9f95331ba 100644
--- a/databases/catdat/data/005_special-objects/003_terminal_objects.sql
+++ b/databases/catdat/data/005_special-objects/003_terminal_objects.sql
@@ -41,6 +41,7 @@ VALUES
('Ring', 'zero ring'),
('Rng', 'zero ring'),
('Sch', '$\Spec(\IZ)$'),
+('SemiGrp', 'trivial semigroup'),
('Set_c', 'singleton set'),
('Set', 'singleton set'),
('Set*', 'singleton pointed set'),
diff --git a/databases/catdat/data/005_special-objects/004_coproducts.sql b/databases/catdat/data/005_special-objects/004_coproducts.sql
index dd74e850c..fae68b39f 100644
--- a/databases/catdat/data/005_special-objects/004_coproducts.sql
+++ b/databases/catdat/data/005_special-objects/004_coproducts.sql
@@ -37,6 +37,7 @@ VALUES
('Ring', 'see MSE/625874'),
('Rng', 'see MSE/4975797'),
('Sch', 'disjoint union with the product sheaf'),
+('SemiGrp', 'similar to free products of monoids, but where the empty word is not allowed, and of course we do (and can) not demand that the factors are $\neq 1$'),
('Set', 'disjoint union'),
('Set*', 'wedge sum, aka one-point union'),
('SetxSet', 'component-wise disjoint union'),
diff --git a/databases/catdat/data/005_special-objects/005_products.sql b/databases/catdat/data/005_special-objects/005_products.sql
index 92fcb6c44..091fd6f9a 100644
--- a/databases/catdat/data/005_special-objects/005_products.sql
+++ b/databases/catdat/data/005_special-objects/005_products.sql
@@ -33,6 +33,7 @@ VALUES
('Rel', 'disjoint unions (!)'),
('Ring', 'direct products with pointwise operations'),
('Rng', 'direct products with pointwise operations'),
+('SemiGrp', 'direct products with pointwise operations'),
('Set', 'direct products with pointwise operations'),
('Set*', 'direct products with pointwise operations'),
('Setne', 'direct products'),
diff --git a/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql b/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql
index e7e9e0904..e61b24d06 100644
--- a/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql
+++ b/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql
@@ -255,6 +255,11 @@ VALUES
'pairs $(f,f^{\sharp})$ consisting of a homeomorphism $f$ and an isomorphism of sheaves $f^{\sharp}$',
'This is easy.'
),
+(
+ 'SemiGrp',
+ 'bijective ring homomorphisms',
+ 'This characterization holds in every algebraic category.'
+),
(
'Set_c',
'bijective maps',
diff --git a/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql b/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql
index f143a1b2c..e09446576 100644
--- a/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql
+++ b/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql
@@ -245,6 +245,11 @@ VALUES
'injective rng homomorphisms',
'This holds in every finitary algebraic category: the forgetful functor to $\Set$ is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.'
),
+(
+ 'SemiGrp',
+ 'injective semigroup homomorphisms',
+ 'This holds in every finitary algebraic category: the forgetful functor to $\Set$ is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.'
+),
(
'Set_c',
'injective maps',
diff --git a/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql b/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql
index 8e92bc6ce..342e6cbaa 100644
--- a/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql
+++ b/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql
@@ -231,6 +231,11 @@ VALUES
'A relation $R : A \to B$ is an epimorphism iff the map $R^* : P(B) \to P(A)$ defined by $S \mapsto \{a \in A : \exists \, b \in S: (a,b) \in R \}$ is injective.',
'See MSE/350716.'
),
+(
+ 'SemiGrp',
+ 'A semigroup homomorphism $f : T \to S$ is an epimorphism iff $S$ equals the dominion of $U := f(T) \subseteq S$, meaning that for every $s \in S$ there are $u_1,\dotsc,u_{m+1} \in U$, $v_1,\dotsc,v_m \in U$, $x_1,\dotsc,x_m \in S$ and $y_1,\dotsc,y_m \in S$ such that $s = x_1 u_1$, $u_1 = v_1 y_1$, $x_{i-1} v_{i-1} = x_i u_i$, $u_i y_{i-1} = v_i y_i$, $x_m v_m = u_{m+1}$ and $u_{m+1} y_m = s$.',
+ 'This is Isbell''s zigzag Theorem, see references there.'
+),
(
'Set_c',
'surjective maps',
diff --git a/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql b/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql
index 44e0ec907..89cbf7c72 100644
--- a/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql
+++ b/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql
@@ -180,6 +180,11 @@ VALUES
'surjective homomorphisms',
'This holds in every finitary algebraic category.'
),
+(
+ 'SemiGrp',
+ 'surjective homomorphisms',
+ 'This holds in every finitary algebraic category.'
+),
(
'Set_c',
'same as epimorphisms',
diff --git a/databases/catdat/data/009_lemmas/001_lemmas.sql b/databases/catdat/data/009_lemmas/001_lemmas.sql
index 8dd7794a6..68f874000 100644
--- a/databases/catdat/data/009_lemmas/001_lemmas.sql
+++ b/databases/catdat/data/009_lemmas/001_lemmas.sql
@@ -160,5 +160,28 @@ INSERT INTO lemmas (
Now if this congruence is the kernel pair of $h : A+X \to Z$ in $A \backslash \C$, then $E$ is the kernel pair of $h \circ i_2 : X \to Z$ in $\C$. Namely, if we have two generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $h \circ i_2 \circ x_1 = h \circ i_2 \circ x_2$, then we can construct a map pair
$$\id_A + x_1,\, \id_A + x_2 : A+T \rightrightarrows A+X$$
in $A \backslash \C$ with $h \circ (\id_A + x_1) = h \circ (\id_A + x_2)$. Therefore, $\id_A + x_1, \id_A + x_2$ factors through $A+E$ in $A \backslash \C$, so $x_1, x_2$ factors through $A+E$ in $\C$; and using disjoint coproducts, we may conclude $x_1, x_2$ factors through $E$.'
+),
+(
+ 'nno_distributive_criterion',
+ 'Natural number objects indicate distributivity',
+ 'Let $\C$ be a category with finite products, arbitrary copowers (denoted $\otimes$), and a natural numbers object $1 \xrightarrow{z} N \xrightarrow{s} N$. Then there is an isomorphism $N \cong \IN \otimes 1$, and for every object $A$ the natural morphism
+ $$\alpha : \IN \otimes A \to A \times (\IN \otimes 1)$$
+ is a split monomorphism.',
+ 'We will use generalized elements extensively. In particular, for every element $a \in A$ and $n \in \IN$ there is an element $n \otimes a \in \IN \otimes A$, formally defined by the $n$th coproduct inclusion. The morphism $\alpha$ is defined by
+ $$\alpha(n \otimes a) = (a , n \otimes 1).$$
+ In any category with finite products and arbitrary copowers, we can construct the non-parameterized NNO $\IN \otimes 1$ with the element $0 \otimes 1 \in \IN \otimes 1$ and the map
+ $$s : \IN \otimes 1 \to \IN \otimes 1, \quad s(n \otimes 1) := (n+1) \otimes 1.$$
+ Its universal property states that it is initial in the category of pairs $1 \xrightarrow{x_0} X \xrightarrow{r} X$. Hence, it is unique up to isomorphism. Since by assumption $1 \xrightarrow{z} N \xrightarrow{s} N$ is a full, parameterized NNO, it is also a non-parameterized NNO and therefore isomorphic to the one described. We will assume w.l.o.g. that it is equal to it and continue to work with $N = \IN \otimes 1$.
+ Next, we apply the (parameterized) universal property of the NNO to the diagram
+ $$A \xrightarrow{f} \IN \otimes A \xrightarrow{g} \IN \otimes A$$
+ defined by $f(a) := 0 \otimes a$ and $g(n \otimes a) := (n+1) \otimes a$. It tells us that there is a map
+ $$\Phi : A \times N \to \IN \otimes A$$
+ with
+ $$\Phi(a,0 \otimes 1) = 0 \otimes a, \quad \Phi(a, s(m)) = g(\Phi(a,m)).$$
+ For $m := n \otimes 1 \in N$ (where $n \in \IN$) the second equation reads
+ $$\Phi(a, (n+1) \otimes 1) = g(\Phi(a, n \otimes 1)).$$
+ By classical induction on $n \in \IN$ it follows that
+ $$\Phi(a, n \otimes 1) = n \otimes a,$$
+ which exactly means $\Phi \circ \alpha = \id_{\IN \otimes A}$.'
);
diff --git a/src/lib/server/macros.ts b/src/lib/server/macros.ts
index f6c1356d8..e01b47a72 100644
--- a/src/lib/server/macros.ts
+++ b/src/lib/server/macros.ts
@@ -97,4 +97,5 @@ export const MACROS = {
'\\RS': '\\mathbf{RS}',
'\\CoAlg': '\\mathbf{CoAlg}',
'\\Cone': '\\mathbf{Cone}',
+ '\\SemiGrp': '\\mathbf{SemiGrp}',
}