Input all categorical data via YAML files (WIP)

databases/catdat/data_yaml/categories/0.yaml

@@ -0,0 +1,56 @@
+id: '0'
+name: empty category
+notation: $\0$
+objects: no objects
+morphisms: no morphisms
+description: This is the category with no objects and no morphisms. It is the initial object in the category of small categories.
+nlab_link: https://ncatlab.org/nlab/show/empty+category
+
+tags:
+  - finite
+  - thin
+
+related_categories:
+  - '1'
+
+satisfied_properties:
+  - property_id: preadditive
+    reason: This is vacuously true.
+
+  - property_id: discrete
+    reason: This is trivial.
+
+  - property_id: binary products
+    reason: This is vacuously true.
+
+  - property_id: finite
+    reason: This is trivial.
+
+  - property_id: small
+    reason: This is trivial.
+
+  - property_id: multi-algebraic
+    reason: The terminal category $\1$ becomes an FPC-sketch by selecting the unique empty cone and cocone. Then, a $\Set$-valued model of this sketch is a functor $\1 \to \Set$ sending the unique object to a terminal and initial object, which never exists. Hence, $\0$ is the category of models of this FPC-sketch.
+
+unsatisfied_properties:
+  - property_id: inhabited
+    reason: This is trivial.
+
+special_objects: {}
+
+special_morphisms:
+  isomorphisms:
+    description: none
+    reason: This is trivial.
+  monomorphisms:
+    description: none
+    reason: This is trivial.
+  epimorphisms:
+    description: none
+    reason: This is trivial.
+  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_yaml/categories/1.yaml

@@ -0,0 +1,58 @@
+id: '1'
+name: trivial category
+notation: $\1$
+objects: a single object $0$
+morphisms: only the identity morphism
+description: This is the simplest category, consisting of a single object $0$ and its identity morphism $0 \to 0$. A concrete representation is the full subcategory of $\Set$ consisting of the empty set. It is the terminal object in the category of small categories.
+nlab_link: https://ncatlab.org/nlab/show/terminal+category
+
+tags:
+  - finite
+  - single object
+  - thin
+
+related_categories:
+  - '0'
+  - '2'
+
+satisfied_properties:
+  - property_id: trivial
+    reason: This is trivial.
+
+  - property_id: finite
+    reason: This is trivial.
+
+  - property_id: small
+    reason: This is trivial.
+
+  - property_id: discrete
+    reason: This is trivial.
+
+unsatisfied_properties: []
+
+special_objects:
+  initial object:
+    description: the unique object
+  terminal object:
+    description: the unique object
+  coproducts:
+    description: $0 \sqcup 0 = 0$
+  products:
+    description: $0 \times 0$
+
+special_morphisms:
+  isomorphisms:
+    description: every morphism
+    reason: This is trivial.
+  monomorphisms:
+    description: every morphism
+    reason: This is trivial.
+  epimorphisms:
+    description: every morphism
+    reason: This is clear since it is discrete.
+  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_yaml/categories/2.yaml

@@ -0,0 +1,52 @@
+id: '2'
+name: discrete category on two objects
+notation: $\2$
+objects: two objects $0$ and $1$
+morphisms: only the two identity morphisms
+description: A concrete representation is the full subcategory of $\CRing$ consisting of the two fields $\IF_2$ and $\IF_3$.
+
+tags:
+  - finite
+  - thin
+
+related_categories:
+  - '1'
+
+satisfied_properties:
+  - property_id: discrete
+    reason: This is trivial.
+
+  - property_id: finite
+    reason: This is trivial.
+
+  - property_id: small
+    reason: This is trivial.
+
+  - property_id: inhabited
+    reason: This is trivial.
+
+  - property_id: multi-algebraic
+    reason: There is an FPC-sketch whose $\Set$-model is precisely a pair $(X,Y)$ of sets such that the coproduct $X+Y$ is a singleton. Any $\Set$-model of such a sketch is isomorphic to either $(\varnothing, 1)$ or $(1, \varnothing)$, hence the category of models is equivalent to $\2$.
+
+unsatisfied_properties:
+  - property_id: connected
+    reason: The objects $0$, $1$ have no zig-zag path between them.
+
+special_objects: {}
+
+special_morphisms:
+  isomorphisms:
+    description: every morphism
+    reason: This is trivial.
+  monomorphisms:
+    description: every morphism
+    reason: This is trivial.
+  epimorphisms:
+    description: every morphism
+    reason: This is clear since it is discrete.
+  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_yaml/categories/Ab.yaml

@@ -0,0 +1,66 @@
+id: Ab
+name: category of abelian groups
+notation: $\Ab$
+objects: abelian groups
+morphisms: group homomorphisms
+description: This is the prototype of an abelian category.
+nlab_link: https://ncatlab.org/nlab/show/Ab
+
+tags:
+  - algebra
+
+related_categories:
+  - CMon
+  - FinAb
+  - FreeAb
+  - Grp
+  - R-Mod
+  - TorsAb
+  - TorsFreeAb
+
+satisfied_properties:
+  - property_id: locally small
+    reason: There is a forgetful functor $\Ab \to \Set$ and $\Set$ is locally small.
+
+  - property_id: abelian
+    reason: This is standard, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. VIII.
+
+  - property_id: finitary algebraic
+    reason: Take the algebraic theory of a commutative group.
+
+unsatisfied_properties:
+  - property_id: split abelian
+    reason: "The short exact sequence $0 \\xrightarrow{} \\IZ \\xrightarrow{p} \\IZ \\xrightarrow{} \\IZ/p \\xrightarrow{} 0$ does not split. "
+
+  - property_id: skeletal
+    reason: This is trivial.
+
+  - property_id: CSP
+    reason: The canonical homomorphism $\bigoplus_{n \geq 0} \IZ \to \prod_{n \geq 0} \IZ$ is not surjective, hence no epimorphism.
+
+special_objects:
+  initial object:
+    description: trivial group
+  terminal object:
+    description: trivial group
+  coproducts:
+    description: direct sums
+  products:
+    description: direct products with pointwise operations
+
+special_morphisms:
+  isomorphisms:
+    description: bijective homomorphisms
+    reason: This characterization holds in every algebraic category.
+  monomorphisms:
+    description: injective homomorphisms
+    reason: "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."
+  epimorphisms:
+    description: surjective homomorphisms
+    reason: "For the non-trivial direction, if $f : A \\to B$ is an epimorphism, then $p \\circ f = 0$ for the projection  $p : B \\to B/f(A)$ implies that $p = 0$, so that $B = f(A)$."
+  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_yaml/categories/Ab_fg.yaml

@@ -0,0 +1,72 @@
+id: Ab_fg
+name: category of finitely generated abelian groups
+notation: $\Ab_{\fg}$
+objects: finitely generated abelian groups
+morphisms: group homomorphisms
+nlab_link: https://ncatlab.org/nlab/show/finitely+generated+module
+
+tags:
+  - algebra
+
+related_categories:
+  - Ab
+  - FinAb
+
+satisfied_properties:
+  - property_id: locally small
+    reason: There is a forgetful functor $\FinAb \to \Set$ and $\Set$ is locally small.
+
+  - property_id: essentially countable
+    reason: Every finitely generated abelian group is isomorphic to a group of the form $\IZ^n / U$, where $n \in \IN$ and $U$ is a subgroup of $\IZ^n$. Since $\IZ^n$ is Noetherian as a $\IZ$-module, $U$ is finitely generated, hence the category $\Ab_\fg$ has only countably many objects up to isomorphism. Furthermore, for any objects $A \cong \IZ^n / U$ and $B \cong \IZ^m / T$, the hom-set $\Hom(A,B)$ is countable. Indeed, precomposition with the quotient map yields an injection $\Hom(A,B) \hookrightarrow \Hom(\IZ^n, B) \cong B^n$, and $B^n$ is countable.
+
+  - property_id: abelian
+    reason: This follows from the fact for abelian groups and the fact that subgroups of finitely generated abelian groups are also finitely generated.
+
+  - property_id: generator
+    reason: The group $\IZ$ is a generator since it represents the forgetful functor to $\Set$.
+
+  - property_id: ℵ₁-accessible
+    reason: The inclusion $\Ab_{\fg} \hookrightarrow \Ab$ is closed under $\aleph_1$-filtered colimits by <a href="https://mathoverflow.net/questions/400763/">MO/400763</a>. In particular, $\Ab_{\fg}$ has $\aleph_1$-filtered colimits. Since $\Ab_{\fg}$ is essentially small, there is a set $G$ such that every f.g. abelian group is isomorphic to one in $G$. So trivially it is also a $\aleph_1$-filtered colimit of such objects (take the constant diagram). Finally, every object is $\Ab_{\fg} = \Ab_{\fp}$ is finitely presentable in $\Ab$ and hence also in $\Ab_{\fg}$, a fortiori $\aleph_1$-presentable.
+
+unsatisfied_properties:
+  - property_id: small
+    reason: Even the collection of trivial groups is not small.
+
+  - property_id: cogenerator
+    reason: Let $Q$ be a finitely generated abelian group. By their well-known classification, we have $Q = F \oplus T$ for a free abelian group $F$ and a finite abelian group $T$. Let $p$ be a prime number which does not divide the order of $T$. Then $\Hom(\IZ/p, Q) = 0$, but $\IZ/p \neq 0$. Therefore, $Q$ is no cogenerator.
+
+  - property_id: split abelian
+    reason: The short exact sequence $0 \xrightarrow{} \IZ \xrightarrow{p} \IZ \xrightarrow{} \IZ/p \xrightarrow{} 0$ does not split.
+
+  - property_id: skeletal
+    reason: This is trivial.
+
+  - property_id: countable
+    reason: This is trivial.
+
+special_objects:
+  initial object:
+    description: trivial group
+  terminal object:
+    description: trivial group
+  coproducts:
+    description: '[finite case] direct sum'
+  products:
+    description: '[finite case] direct products'
+
+special_morphisms:
+  isomorphisms:
+    description: bijective homomorphisms
+    reason: This follows exactly as for abelian groups.
+  monomorphisms:
+    description: injective homomorphisms
+    reason: "Let $f : A \\to B$ be a monomorphism of finitely generated abelian groups. Let $a \\in A$ be in the kernel of $a$. Then we may view $a$ as a morphism $a : \\IZ \\to A$ with $f \\circ a = 0$, and $\\IZ$ is finitely generated. Hence, $a = 0$."
+  epimorphisms:
+    description: surjective homomorphisms
+    reason: Use the same proof as for abelian groups.
+  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_yaml/categories/Alg(R).yaml

@@ -0,0 +1,89 @@
+id: Alg(R)
+name: category of algebras
+notation: $\Alg(R)$
+objects: algebras over a commutative ring $R \neq 0$
+morphisms: maps preserving the ring and module structure
+description: This is a generalization of the category of rings, which we get for $R = \IZ$. We assume our rings (and algebras) to be unital. For $R = 0$ we would get the trivial category, which is why we exclude this here.
+nlab_link: https://ncatlab.org/nlab/show/Alg
+
+tags:
+  - algebra
+
+related_categories:
+  - CAlg(R)
+  - R-Mod
+  - Ring
+
+satisfied_properties:
+  - property_id: locally small
+    reason: There is a forgetful functor $\Alg(R) \to \Set$ and $\Set$ is locally small.
+
+  - property_id: finitary algebraic
+    reason: Take the algebraic theory of an $R$-algebra.
+
+  - property_id: strict terminal object
+    reason: "If $f : 0 \\to A$ is an algebra homomorphism, then $A$ satisfies $1=f(1)=f(0)=0$, so that $A=0$."
+
+  - property_id: Malcev
+    reason: This follows in the same way as for groups, see also Example 2.2.5 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>.
+
+  - property_id: disjoint finite products
+    reason: One can take the same proof as for $\Ring$.
+
+unsatisfied_properties:
+  - property_id: balanced
+    reason: Take a prime ideal $P \subseteq R$ and consider the $R$-algebra $A := R/P$ (which is an integral domain). Then the inclusion $A \hookrightarrow Q(A)$ is a counterexample.
+
+  - property_id: skeletal
+    reason: This is trivial.
+
+  - property_id: cogenerating set
+    reason: 'We apply <a href="/lemma/missing_cogenerating_sets">this lemma</a> to the collection of $R$-algebras which are fields: If $F$ is an $R$-algebra that is also a field and $A$ is a non-trivial $R$-algebra, any algebra homomorphism $F \to A$ is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables over some residue field of $R$ has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).'
+
+  - property_id: codistributive
+    reason: 'If $\sqcup$ denotes the coproduct of $R$-algebras (see <a href="https://math.stackexchange.com/questions/625874" target="_blank">MSE/625874</a> for their description) and $A$ is an $R$-algebra, the canonical morphism $A \sqcup R^2 \to (A \sqcup R)^2 = A^2$ is usually no isomorphism. For example, for $A = R[X]$ the coproduct on the LHS is not commutative, it has the algebra presentation $\langle X,E : E^2=E \rangle$.'
+
+  - property_id: semi-strongly connected
+    reason: This is because already the full subcategory $\CAlg(R)$ of commutative algebras is not semi-strongly connected, see <a href="/category/CAlg(R)">its category page</a> for details.
+
+  - property_id: co-Malcev
+    reason: 'See <a href="https://mathoverflow.net/questions/509552">MO/509552</a>: Consider the forgetful functor $U : \Alg(R) \to \Set$ and the relation $S \subseteq U^2$ defined by $S(A) := \{(a,b) \in U(A)^2 : ab = a^2\}$. Both are representable: $U$ by $R[X]$ and $S$ by $R \langle X,Y \rangle / \langle XY-X^2 \rangle$. It is clear that $S$ is reflexive, but not symmetric.'
+
+  - property_id: coregular
+    reason: 'We just need to tweak the proof for $\Ring$. Since $R \neq 0$, there is an infinite field $K$ with a homomorphism $R \to K$. Since $K$ is infinite, we may choose some $\lambda \in K \setminus \{0,1\}$. Let $B := M_2(K)$ and $A := K \times K$. Then $A \to B$, $(x,y) \mapsto \diag(x,y)$ is a regular monomorphism: A direct calculation shows that a matrix is diagonal iff it commutes with $M := \bigl(\begin{smallmatrix} 1 & 0 \\ 0 & \lambda \end{smallmatrix}\bigr)$, so that $A \to B$ is the equalizer of the identity $B \to B$ and the conjugation $B \to B$, $X \mapsto M X M^{-1}$. Consider the homomorphism $A \to K$, $(a,b) \mapsto a$. We claim that $K \to K \sqcup_A B$ is not a monomorphism, because in fact, the pushout $K \sqcup_A B$ is zero: Since $A \to K$ is surjective with kernel $0 \times K$, the pushout is $B/\langle 0 \times K \rangle$, which is $0$ because $B$ is simple (<a href="https://math.stackexchange.com/questions/22629" target="_blank">proof</a>) or via a direct calculation with elementary matrices.'
+
+  - property_id: regular quotient object classifier
+    reason: We may copy the proof for the <a href="/category/CAlg(R)">category of commutative algebras</a> (since the proof there did not use that $P$ is commutative). Alternatively, any regular quotient object classifier in $\Alg(R)$ would produce one in $\CAlg(R)$ by <a href="/lemma/subobject_classifiers_coreflection">this lemma</a> (dualized).
+
+  - property_id: cocartesian cofiltered limits
+    reason: |-
+      Consider the ring $A = R[X]$ and the sequence of rings $B_n = R[Y]/(Y^{n+1})$ with projections $B_{n+1} \to B_n$, whose limit is $R[[Y]]$. Every element in the coproduct of rings $R[X] \sqcup R[[Y]]$ has a finite "free product" length. Now consider the elements
+      	$$w_n = (1 + XY) (1+XY^2) \cdots (1+X Y^n) \in A \sqcup B_n.$$
+      	Because of $w_n \equiv w_{n-1} \bmod Y^n$ these form an element $w \in \lim_n (A \sqcup B_n)$. Expanding $w_n$, the longest term is $XY XY^2 \cdots X Y^n$ of "free product" length $2n$, which is unbounded.
+
+  - property_id: cofiltered-limit-stable epimorphisms
+    reason: We already know that $\CAlg(R)$ does not have this property. Now apply the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by <a href="https://math.stackexchange.com/questions/5133488" target="_blank">MSE/5133488</a>.
+
+  - property_id: effective cocongruences
+    reason: 'The counterexample is similar to the one for <a href="/category/Ring">$\Ring$</a>: Let $X := R[p] / (p^2-p)$ with cocongruence $E := R \langle p, q \rangle / (p^2-p, q^2-q, pq-q, qp-p)$.'
+
+special_objects:
+  initial object:
+    description: $R$
+  terminal object:
+    description: trivial algebra
+  coproducts:
+    description: see <a href="https://math.stackexchange.com/questions/625874" target="_blank">MSE/625874</a>
+  products:
+    description: direct products with pointwise operations
+
+special_morphisms:
+  isomorphisms:
+    description: bijective ring homomorphisms
+    reason: This characterization holds in every algebraic category.
+  monomorphisms:
+    description: injective ring homomorphisms
+    reason: "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."
+  regular epimorphisms:
+    description: surjective homomorphisms
+    reason: This holds in every finitary algebraic category.