assign properties to TorsAb

Author: ScriptRaccoon

databases/catdat/data/003_category-property-assignments/TorsAb.sql

@@ -0,0 +1,75 @@
+INSERT INTO category_property_assignments (
+	category_id,
+	property_id,
+	is_satisfied,
+	reason
+)
+VALUES
+(
+	'TorsAb',
+	'locally small',
+	TRUE,
+	'There is a forgetful functor $\mathbf{TorsAb} \to \mathbf{Ab}$ and $\mathbf{Ab}$ is locally small.'
+),
+(
+	'TorsAb',
+	'cocomplete',
+	TRUE,
+	'The embedding $\mathbf{TorsAb} \hookrightarrow \mathbf{Ab}$ is closed under colimits and $\mathbf{Ab}$ is cocomplete.'
+),
+(
+	'TorsAb',
+	'complete',
+	TRUE,
+	'The embedding $\mathbf{TorsAb} \hookrightarrow \mathbf{Ab}$ has a right adjoint, sending an abelian group $A$ to its torsion subgroup $T(A)$. Since $\mathbf{Ab}$ is complete, $\mathbf{TorsAb}$ is complete as well. The limit of a diagram of torsion abelian groups is the torsion subgroup of the limit of the underlying abelian groups. Notice that the torsion subgroup is not required in the case of equalizers, since a subgroup of a torsion abelian group is already torsion. Also, a \emph{finite} product of torsion abelian groups is already torsion.'
+),
+(
+	'TorsAb',
+	'preadditive',
+	TRUE,
+	'It is a full subcategory of the preadditive category $\mathbf{Ab}$.'
+),
+(
+	'TorsAb',
+	'normal',
+	TRUE,
+	'If $f : A \to B$ is a monomorphism, it is injective (see below). In $\mathbf{Ab}$ it is then the kernel of $B \to B/f(A)$. Since $B/f(A)$ is torsion, it is also the kernel in $\mathbf{TorsAb}$.'
+),
+(
+	'TorsAb',
+	'conormal',
+	TRUE,
+	'If $f : A \to B$ is an epimorphism, it is surjective (see below). In $\mathbf{Ab}$ it is then the cokernel of its kernel $K \hookrightarrow A$. Since $K$ is torsion, it is also the cokernel in $\mathbf{TorsAb}$.'
+),
+(
+	'TorsAb',
+	'finitely accessible',
+	TRUE,
+	'We already know that (filtered) colimits exist and are preserved by the forgetful functor to $\mathbf{Ab}$. Every torsion abelian group is the filtered colimit of its finitely generated subgroups (which are finite). These are finitely presentable in $\mathbf{Ab}$, hence also in $\mathbf{TorsAb}$.'
+),
+(
+	'TorsAb',
+	'skeletal',
+	FALSE,
+	'This is trivial.'
+),
+(
+	'TorsAb',
+	'split abelian',
+	FALSE,
+	'The sequence $0 \to \mathbb{Z}/2 \to \mathbb{Z}/4 \to \mathbb{Z}/2 \to 0$ does not split.'
+),
+(
+	'TorsAb',
+	'CSP',
+	FALSE,
+	'The canonical homomorphism $\bigoplus_{n \geq 0} \mathbb{Z}/2 \to T(\prod_{n \geq 0} \mathbb{Z}/2)$ is not surjective, since the torsion element $(1,1,\dotsc)$ does not lie in the image. Hence, it is no epimorphism.'
+),
+(
+	'TorsAb',
+	'locally strongly finitely presentable',
+	FALSE,
+	'Assume that it is locally strongly finitely presentable, and therefore the category of algebras of a multi-sorted finitary algebraic theory. For each sort $s$ let $F_s$ be the free algebra on one generator of sort $s$. One of them must be non-trivial, since otherwise the category would be thin. So assume $F_s \neq 0$. It is finitely presentable, hence a finite abelian group, and regular projective. Any direct summand will have the same properties. So we find that some $\mathbb{Z}/p^k$ (with $k \geq 1$ and $p$ prime) is regular projective. However, the exact sequence in $\mathbf{TorsAb}$
+	$$0 \to \mathbb{Z}/p \to \mathbb{Z}/p^{k+1} \to \mathbb{Z}/p^k \to 0$$
+	does not split.'
+);

databases/catdat/data/005_special-objects/002_initial_objects.sql

@@ -55,6 +55,7 @@ VALUES
 ('sSet', 'simplicial set $X$ with $X_n = \varnothing$'),
 ('Top', 'empty space'),
 ('Top*', 'singleton space with the unique base point'),
+('TorsAb', 'trivial group'),
 ('TorsFreeAb', 'trivial group'),
 ('Vect', 'trivial vector space'),
 ('walking_commutative_square', '$a$'),

databases/catdat/data/005_special-objects/003_terminal_objects.sql

@@ -52,6 +52,7 @@ VALUES
 ('sSet', 'simplicial set $X$ with $X_n = 1$'),
 ('Top', 'singleton space'),
 ('Top*', 'singleton space with the unique base point'),
+('TorsAb', 'trivial group'),
 ('TorsFreeAb', 'trivial group'),
 ('Vect', 'trivial vector space'),
 ('walking_commutative_square', '$d$'),

databases/catdat/data/005_special-objects/004_coproducts.sql

@@ -45,6 +45,7 @@ VALUES
 ('sSet', 'pointwise disjoint union'),
 ('Top', 'disjoint union with the disjoint union topology'),
 ('Top*', 'wedge sum, aka one-point union'),
+('TorsAb', 'direct sums'),
 ('TorsFreeAb', 'direct sums'),
 ('Vect', 'direct sums'),
 ('walking_commutative_square', '$b \sqcup c = d$, $a \sqcup x = x$, $d \sqcup x = d$, $x \sqcup x = x$'),

databases/catdat/data/005_special-objects/005_products.sql

@@ -42,6 +42,7 @@ VALUES
 ('sSet', 'pointwise defined direct product'),
 ('Top', 'direct product with the <a href="https://en.wikipedia.org/wiki/Product_topology" target="_blank">product topology</a>'),
 ('Top*', 'direct product with the <a href="https://en.wikipedia.org/wiki/Product_topology" target="_blank">product topology</a> and the obvious base point'),
+('TorsAb', 'torsion subgroup of the direct product'),
 ('TorsFreeAb', 'direct products'),
 ('Vect', 'direct products with pointwise operations'),
 ('walking_commutative_square', '$b \times c = a$, $x \times x = x$, $a \times x = a$, $d \times x = x$'),

databases/catdat/data/006_special-morphisms/002_isomorphisms.sql

@@ -315,6 +315,11 @@ VALUES
 	'pointed homeomorphisms',
 	'This is easy.'
 ),
+(
+	'TorsAb',
+	'bijective group homomorphisms',
+	'This is easy.'
+),
 (
 	'TorsFreeAb',
 	'bijective group homomorphisms',

databases/catdat/data/006_special-morphisms/003_monomorphisms.sql

@@ -305,6 +305,11 @@ VALUES
 	'injective pointed continuous maps',
 	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the discrete two-point space), hence preserves monomorphisms.'
 ),
+(
+	'TorsAb',
+	'injective group homomorphisms',
+	'For the non-trivial direction, assume $f : A \to B$ is a monomorphism and $a \in A$ satisfies $f(a)=0$. Choose $n \geq 1$ with $n a = 0$. Then $a$ corresponds to a homomorphism of torsion abelian groups $\tilde{a} : \mathbb{Z}/n \to A$ satisfying $f \circ \tilde{a} = 0$. Hence, $\tilde{a} = 0$, which means $a = 0$.'
+),
 (
 	'TorsFreeAb',
 	'injective group homomorphisms',

databases/catdat/data/006_special-morphisms/004_epimorphisms.sql

@@ -291,6 +291,11 @@ VALUES
 	'surjective pointed continuous maps',
 	'For the non-trivial direction: The forgetful functor $\mathbf{Top}_* \to \mathbf{Top}$ preserves pushouts and hence also epimorphisms, and we already know the epimorphisms in $\mathbf{Top}$.'
 ),
+(
+	'TorsAb',
+	'surjective homomorphisms',
+	'For the non-trivial direction, assume that $f : A \to B$ is an epimorphism. The projection $q : B \to B/f(A)$ satisfies $q \circ f = 0$ and hence $q = 0$, so that $B=f(A)$.'
+),
 (
 	'TorsFreeAb',
 	'homomorphisms $f : A \to B$ such that $B/f(A)$ is a torsion group',

databases/catdat/data/006_special-morphisms/005_regular-monomorphisms.sql

@@ -225,6 +225,11 @@ VALUES
     'embeddings',
     'Equalizers are embeddings by their construction. Conversely, if $f : X \to Y$ is an embedding, then $f$ is the equalizer of the two characteristic maps $\chi_Y, \chi_{f(X)} : Y \to \{0,1\}$, where $\{0,1\}$ carries the indiscrete topology and $1$ is the base point.'
 ),
+(
+    'TorsAb',
+    'same as monomorphisms',
+    'This is because the category is mono-regular.'
+),
 (
 	'TorsFreeAb',
 	'injective group homomorphisms $i : A \to B$ such that $B/i(A)$ is torsion-free, i.e., $i$ is the inclusion of a <i>saturated subgroup</i>',

databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql

@@ -240,6 +240,11 @@ VALUES
     'surjective pointed quotient maps',
     'Regular epimorphisms are surjective pointed quotient maps by the explicit construction of coequalizers. Conversely, if $q : X \to Y$ is a surjective pointed quotient map, then one checks that $q$ is the coequalizer of its kernel pair $X \times_Y X \rightrightarrows X$: This is true for the underlying pointed sets, and continuity of the induced morphism follows since $q$ is a quotient map.' 
 ),
+(
+    'TorsAb',
+    'same as epimorphisms',
+    'This is because the category is epi-regular.'
+),
 (
 	'TorsFreeAb',
 	'surjective group homomorphisms',