Add the category of countable groups

.cspell.json

@@ -151,6 +151,7 @@
 		"Lawvere",
 		"libsql",
 		"Lindelöf",
+		"Lodha",
 		"Makkai",
 		"Malcev",
 		"Mathoverflow",

databases/catdat/data/categories/FinGrp.yaml

@@ -12,6 +12,7 @@ tags:
 related_categories:
   - FinAb
   - Grp
+  - Grp_c
 
 satisfied_properties:
   - property_id: locally small
@@ -47,7 +48,7 @@ satisfied_properties:
 
 unsatisfied_properties:
   - property_id: normal
-    reason: Every non-normal subgroup of a finite group provides a counterexample.
+    reason: Every non-normal subgroup of a finite group (such as $C_2 \hookrightarrow S_3$) provides a counterexample.
 
   - property_id: cogenerator
     reason: 'We apply <a href="/lemma/missing_cogenerator">this lemma</a> to the collection of finite simple groups: Any non-trivial homomorphism from a finite simple group to a finite group must be injective, and for every $n \in \IN$ there is a finite simple group of size $\geq n$ (for example, the alternating group on $n+5$ elements).'

databases/catdat/data/categories/Grp.yaml

@@ -10,8 +10,9 @@ tags:
   - algebra
 
 related_categories:
-  - Ab
   - FinGrp
+  - Grp_c
+  - Ab
   - Mon
   - SemiGrp
 

databases/catdat/data/categories/Grp_c.yaml

@@ -0,0 +1,115 @@
+id: Grp_c
+name: category of countable groups
+notation: $\Grp_\c$
+objects: countable groups
+morphisms: group homomorphisms
+description: A group is called countable if its underlying set is countable. In particular, every finite group is countable, but also every finitely generated group is countable.
+nlab_link: null
+
+tags:
+  - algebra
+
+related_categories:
+  - Grp
+  - FinGrp
+  - Set_c
+
+satisfied_properties:
+  - property_id: locally small
+    reason: There is an embedding $\Grp_\c \hookrightarrow \Grp$ and $\Grp$ is locally small.
+
+  - property_id: essentially small
+    reason: Every countable group is isomorphic to a group whose underlying set is a subset of $\IN$.
+
+  - property_id: pointed
+    reason: The trivial group is countable and is a zero object.
+
+  - property_id: generator
+    reason: The countable group $\IZ$ is a generator because it represents the forgetful functor $\Grp_\c \to \Set$.
+
+  - property_id: finite products
+    reason: This is because <a href="/category/Grp">$\Grp$</a> has finite (in fact, all) products, and $\Grp_\c \hookrightarrow \Grp$ is closed under finite products. This is because a finite product of countable sets is again countable.
+    check_redundancy: false
+
+  - property_id: equalizers
+    reason: One can use the same construction as in <a href="/category/Grp">$\Grp$</a> since a subgroup of a countable group is again countable.
+    check_redundancy: false
+
+  - property_id: coequalizers
+    reason: One can use the same construction as in <a href="/category/Grp">$\Grp$</a> since a quotient of a countable group is again countable.
+
+  - property_id: countable coproducts
+    reason: This is because <a href="/category/Grp">$\Grp$</a> has countable (in fact, all) coproducts, and $\Grp_\c \hookrightarrow \Grp$ is closed under countable coproducts. This is because a countable union of countable sets is again countable.
+
+  - property_id: mono-regular
+    reason: 'This can be deduced from the corresponding property of <a href="/category/Grp">$\Grp$</a> as follows: Let $i : K \hookrightarrow G$ be a monomorphism in $\Grp_\c$, i.e. an injective homomorphism of countable groups. Since $\Grp$ is mono-regular, there is a group $H$ and two homomorphisms $f,g : G \rightrightarrows H$ with $i = \eq(f,g)$. Let $H'' \subseteq H$ be the subgroup generated by $\im(f) \cup \im(g)$. Since $G$ is countable, $H''$ is countable as well, and $f,g$ corestrict to homomorphisms $f'', g'' : G \rightrightarrows H''$. Hence, $i = \eq(f'',g'')$.'
+
+  - property_id: conormal
+    reason: 'If $f : G \to H$ is an epimorphism in $\Grp_\c$, i.e. a surjective homomorphism of countable groups, then $f$ is the cokernel of $K \hookrightarrow G$ in $\Grp$, where $K$ is the kernel of $f$. Since $K$ is countable, it is also the cokernel in $\Grp_\c$.'
+
+  - property_id: Malcev
+    reason: We can use the same proof as for <a href="/category/Grp">$\Grp$</a>.
+
+  - property_id: regular
+    reason: We already know that the category is finitely complete, and that it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks.
+
+  - property_id: effective congruences
+    reason: 'A congruence on a countable group $G$ has the form $\{(g,h) \in G^2 : g^{-1} h \in N \}$ for some normal subgroup $N \subseteq G$. It is the kernel pair of the projection $p : G \twoheadrightarrow G/N$ in $\Grp$, but also in $\Grp_\c$ since $G/N$ is countable.'
+
+  - property_id: effective cocongruences
+    reason: 'Let $G + G \twoheadrightarrow H$ be a cocongruence in $\Grp_\c$. Since $\Grp_\c \hookrightarrow \Grp$ is closed under finite colimits, this is the same as a cocongruence in $\Grp$ where $G,H \in \Grp$ happen to be countable groups. Since we already know that <a href="/category/Grp">$\Grp$</a> has effective cocongruences, the cocongruence is the cokernel pair of some homomorphism of groups $K \to H$. If $K'' \subseteq H$ denotes the image of $K$, it is then also the cokernel pair of the inclusion $K'' \hookrightarrow H$, and $K''$ is countable.'
+
+unsatisfied_properties:
+  - property_id: skeletal
+    reason: This is trivial.
+
+  - property_id: small
+    reason: Even the collection of all trivial groups is not a set.
+
+  - property_id: normal
+    reason: Every non-normal subgroup of a countable group (such as $C_2 \hookrightarrow S_3$) provides a counterexample.
+
+  - property_id: counital
+    reason: The canonical morphism $F_2 = \IZ \sqcup \IZ \to \IZ \times \IZ$ is not a monomorphism since $F_2$ is not abelian.
+
+  - property_id: countable powers
+    reason: Since the forgetful functor $\Grp_\c \to \Set$ is representable, it preserves products. Therefore, if the power $\IZ^{\IN}$ exists in $\Grp_\c$, its underlying set must be the ordinary cartesian product, which however is uncountable.
+
+  - property_id: regular quotient object classifier
+    reason: We can copy the proof from <a href="/category/Grp">$\Grp$</a>.
+
+  - property_id: coregular
+    reason: Pushouts of injective homomorphisms between countable groups do not need to be injective, see <a href="https://math.stackexchange.com/questions/5088032" target="_blank">MSE/5088032</a>.
+
+  - property_id: cogenerator
+    reason: 'Assume that a cogenerator $Q$ exists in $\Grp_\c$. There are only countably many finitely generated subgroups of $Q$. But there are continuum many finitely generated simple groups; this follows from Corollary 1.5 in <a href="https://arxiv.org/abs/1807.06478" target="_blank">Finitely generated infinite simple groups of homeomorphisms of the real line</a> by J. Hyde and Y. Lodha. Hence, there is a finitely generated (and hence countable) simple group $H$ which does not embed into $Q$. Since $H$ is simple, any homomorphism $H \to Q$ must be trivial then. But then $\id_H, 1 : H \rightrightarrows H$ are not separated by a homomorphism $H \to Q$.'
+
+  - property_id: ℵ₁-accessible
+    reason: 'We can almost copy the proof from <a href="/category/Set_c">$\Set_\c$</a> to show that $\Grp_\c$ does not have $\aleph_1$-filtered colimits: Fix an uncountable set $X$, let $P_\c(X)$ be the poset of countable subsets of $X$, which is $\aleph_1$-filtered, and consider the functor $P_\c(X) \to \Grp_\c$ taking a subset $Y \subseteq X$ to the free group $F(Y)$. The colimit of this diagram in $\Grp$ is given by $F(X)$ itself, so if $G$ were a colimit in $\Grp_\c$, then $\Hom(G, C_2) \cong \Hom(F(X),C_2) \cong \{0,1\}^X$. But the former has cardinality at most $2^{\aleph_0}$ and the latter has cardinality $2^{\card(X)}$, so we have obtained a contradiction if we pick $X$ large enough (e.g. $\card(X)=2^{\aleph_0}$).'
+
+special_objects:
+  initial object:
+    description: trivial group
+  terminal object:
+    description: trivial group
+  coproducts:
+    description: '[countable case] free products'
+  products:
+    description: '[finite case] direct products with pointwise operations'
+
+special_morphisms:
+  isomorphisms:
+    description: bijective homomorphisms
+    reason: This is easy.
+  monomorphisms:
+    description: injective homomorphisms
+    reason: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the countable group $\IZ$), hence preserves monomorphisms.
+  epimorphisms:
+    description: surjective homomorphisms
+    reason: 'For the non-trivial direction, if $f : G \to H$ is an epimorphism, we may factor it as $G \to f(G) \to H$, and $f(G) \to H$ is still an epimorphism, but also an inclusion and hence a monomorphism. Since we already know that the category is mono-regular, $f(G) \to H$ must be an isomorphism.'
+  regular monomorphisms:
+    description: same as monomorphisms
+    reason: This is because the category is mono-regular.
+  regular epimorphisms:
+    description: same as epimorphisms
+    reason: This is because the category is epi-regular.

databases/catdat/data/categories/Set_c.yaml

@@ -12,6 +12,7 @@ tags:
 related_categories:
   - FinSet
   - Set
+  - Grp_c
 
 satisfied_properties:
   - property_id: locally small

databases/catdat/data/macros.yaml

@@ -51,6 +51,7 @@
 \supp: \operatorname{supp}
 \Coexp: \operatorname{Coexp}
 \inc: \operatorname{inc}
+\eq: \operatorname{eq}
 
 # categories
 \Set: \mathbf{Set}