Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 11 additions & 1 deletion databases/catdat/data/001_categories/002_algebra.sql
Original file line number Diff line number Diff line change
Expand Up @@ -196,10 +196,20 @@ VALUES
'$\TorsFreeAb$',
'torsion-free abelian groups',
'group homomorphisms',
'This is a typical example of a well-behaved additive category which is <i>not</i> abelian.',
'This is a typical example of a well-behaved additive category which is <i>not</i> abelian. It contains the category of free abelian groups.',
'https://ncatlab.org/nlab/show/torsion-free+module',
NULL
),
(
'TorsAb',
'category of torsion abelian groups',
'$\TorsAb$',
'torsion abelian groups',
'group homomorphisms',
'This is a Grothendieck abelian category containing all finite abelian groups.',
'https://ncatlab.org/nlab/show/torsion+subgroup',
NULL
),
(
'Cat',
'category of small categories',
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ VALUES
('Ab', 'R-Mod'),
('Ab', 'FreeAb'),
('Ab', 'TorsFreeAb'),
('Ab', 'TorsAb'),
('Ab_fg', 'Ab'),
('Ab_fg', 'FinAb'),
('Alg(R)', 'CAlg(R)'),
Expand Down Expand Up @@ -47,6 +48,7 @@ VALUES
('FinAb', 'Ab'),
('FinAb', 'Ab_fg'),
('FinAb', 'FinGrp'),
('FinAb', 'TorsAb'),
('FinOrd', 'FinSet'),
('FinOrd', 'Pos'),
('FinOrd', 'Delta'),
Expand Down Expand Up @@ -137,6 +139,10 @@ VALUES
('Top*', 'Set*'),
('TorsFreeAb', 'Ab'),
('TorsFreeAb', 'FreeAb'),
('TorsFreeAb', 'TorsAb'),
('TorsAb', 'TorsFreeAb'),
('TorsAb', 'Ab'),
('TorsAb', 'FinAb'),
('Vect', 'R-Mod'),
('Vect', 'R-Mod_div'),
('Z', 'Sch'),
Expand Down
1 change: 1 addition & 0 deletions databases/catdat/data/001_categories/200_category-tags.sql
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,7 @@ VALUES
('Top', 'topology'),
('Top*', 'topology'),
('TorsFreeAb', 'algebra'),
('TorsAb', 'algebra'),
('Vect', 'algebra'),
('walking_commutative_square', 'finite'),
('walking_commutative_square', 'category theory'),
Expand Down
75 changes: 75 additions & 0 deletions databases/catdat/data/003_category-property-assignments/TorsAb.sql
Original file line number Diff line number Diff line change
@@ -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 $\TorsAb \to \Ab$ and $\Ab$ is locally small.'
),
(
'TorsAb',
'cocomplete',
TRUE,
'The embedding $\TorsAb \hookrightarrow \Ab$ is closed under colimits and $\Ab$ is cocomplete.'
),
(
'TorsAb',
'complete',
TRUE,
'The embedding $\TorsAb \hookrightarrow \Ab$ has a right adjoint, sending an abelian group $A$ to its torsion subgroup $T(A)$. Since $\Ab$ is complete, $\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 <i>finite</i> product of torsion abelian groups is already torsion.'
),
(
'TorsAb',
'preadditive',
TRUE,
'It is a full subcategory of the preadditive category $\Ab$.'
),
(
'TorsAb',
'normal',
TRUE,
'If $f : A \to B$ is a monomorphism, it is injective (see below). In $\Ab$ it is then the kernel of $B \to B/f(A)$. Since $B/f(A)$ is torsion, it is also the kernel in $\TorsAb$.'
),
(
'TorsAb',
'conormal',
TRUE,
'If $f : A \to B$ is an epimorphism, it is surjective (see below). In $\Ab$ it is then the cokernel of its kernel $K \hookrightarrow A$. Since $K$ is torsion, it is also the cokernel in $\TorsAb$.'
),
(
'TorsAb',
'finitely accessible',
TRUE,
'We already know that (filtered) colimits exist and are preserved by the forgetful functor to $\Ab$. Every torsion abelian group is the filtered colimit of its finitely generated subgroups (which are finite). These are finitely presentable in $\Ab$, hence also in $\TorsAb$.'
),
(
'TorsAb',
'skeletal',
FALSE,
'This is trivial.'
),
(
'TorsAb',
'split abelian',
FALSE,
'The sequence $0 \to \IZ/2 \to \IZ/4 \to \IZ/2 \to 0$ does not split.'
),
(
'TorsAb',
'CSP',
FALSE,
'The canonical homomorphism $\bigoplus_{n \geq 0} \IZ/2 \to T(\prod_{n \geq 0} \IZ/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 $\IZ/p^k$ (with $k \geq 1$ and $p$ prime) is regular projective. However, the exact sequence in $\TorsAb$
$$0 \to \IZ/p \to \IZ/p^{k+1} \to \IZ/p^k \to 0$$
does not split.'
);
Original file line number Diff line number Diff line change
Expand Up @@ -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$'),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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$'),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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$'),
Expand Down
1 change: 1 addition & 0 deletions databases/catdat/data/005_special-objects/005_products.sql
Original file line number Diff line number Diff line change
Expand Up @@ -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$'),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -315,6 +315,11 @@ VALUES
'pointed homeomorphisms',
'This is easy.'
),
(
'TorsAb',
'bijective group homomorphisms',
'This is easy.'
),
(
'TorsFreeAb',
'bijective group homomorphisms',
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -305,6 +305,11 @@ VALUES
'injective pointed continuous maps',
'For the non-trivial direction, the forgetful functor to $\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} : \IZ/n \to A$ satisfying $f \circ \tilde{a} = 0$. Hence, $\tilde{a} = 0$, which means $a = 0$.'
),
(
'TorsFreeAb',
'injective group homomorphisms',
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -291,6 +291,11 @@ VALUES
'surjective pointed continuous maps',
'For the non-trivial direction: The forgetful functor $\Top_* \to \Top$ preserves pushouts and hence also epimorphisms, and we already know the epimorphisms in $\Top$.'
),
(
'TorsAb',
'surjective homomorphisms',
'Clearly, surjective homomorphisms are epimorphisms. The converse follows since the forgetful functor $\TorsAb \to \Ab$ has a right adjoint, hence preserves epimorphisms.'
),
(
'TorsFreeAb',
'homomorphisms $f : A \to B$ such that $B/f(A)$ is a torsion group',
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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>',
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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',
Expand Down
1 change: 1 addition & 0 deletions src/lib/server/macros.ts
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,7 @@ export const MACROS = {
'\\FinGrp': '\\mathbf{FinGrp}',
'\\FreeAb': '\\mathbf{FreeAb}',
'\\TorsFreeAb': '\\mathbf{TorsFreeAb}',
'\\TorsAb': '\\mathbf{TorsAb}',
'\\Cat': '\\mathbf{Cat}',
'\\Ban': '\\mathbf{Ban}',
'\\Meas': '\\mathbf{Meas}',
Expand Down