Write property instead of property_id in YAML files

databases/catdat/data/categories/0.yaml

@@ -14,26 +14,26 @@ related_categories:
   - '1'
 
 satisfied_properties:
-  - property_id: discrete
+  - property: discrete
     reason: This is trivial.
 
-  - property_id: binary products
+  - property: binary products
     reason: This is vacuously true.
 
-  - property_id: finite
+  - property: finite
     reason: This is trivial.
 
-  - property_id: small
+  - property: small
     reason: This is trivial.
 
-  - property_id: preadditive
+  - property: preadditive
     reason: This is vacuously true.
 
-  - property_id: multi-algebraic
+  - property: 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
+  - property: inhabited
     reason: This is trivial.
 
 special_objects: {}

databases/catdat/data/categories/1.yaml

@@ -16,16 +16,16 @@ related_categories:
   - '2'
 
 satisfied_properties:
-  - property_id: trivial
+  - property: trivial
     reason: This is trivial.
 
-  - property_id: finite
+  - property: finite
     reason: This is trivial.
 
-  - property_id: small
+  - property: small
     reason: This is trivial.
 
-  - property_id: discrete
+  - property: discrete
     reason: This is trivial.
 
 unsatisfied_properties: []

databases/catdat/data/categories/2.yaml

@@ -14,23 +14,23 @@ related_categories:
   - '1'
 
 satisfied_properties:
-  - property_id: discrete
+  - property: discrete
     reason: This is trivial.
 
-  - property_id: finite
+  - property: finite
     reason: This is trivial.
 
-  - property_id: small
+  - property: small
     reason: This is trivial.
 
-  - property_id: inhabited
+  - property: inhabited
     reason: This is trivial.
 
-  - property_id: multi-algebraic
+  - property: 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
+  - property: connected
     reason: The objects $0$, $1$ have no zig-zag path between them.
 
 special_objects: {}

databases/catdat/data/categories/Ab.yaml

@@ -20,23 +20,23 @@ related_categories:
   - TorsFreeAb
 
 satisfied_properties:
-  - property_id: locally small
+  - property: locally small
     reason: There is a forgetful functor $\Ab \to \Set$ and $\Set$ is locally small.
 
-  - property_id: abelian
+  - property: 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
+  - property: finitary algebraic
     reason: Take the algebraic theory of a commutative group.
 
 unsatisfied_properties:
-  - property_id: skeletal
+  - property: skeletal
     reason: This is trivial.
 
-  - property_id: split abelian
+  - property: split abelian
     reason: The short exact sequence $0 \xrightarrow{} \IZ \xrightarrow{p} \IZ \xrightarrow{} \IZ/p \xrightarrow{} 0$ does not split.
 
-  - property_id: CSP
+  - property: CSP
     reason: The canonical homomorphism $\bigoplus_{n \geq 0} \IZ \to \prod_{n \geq 0} \IZ$ is not surjective, hence no epimorphism.
 
 special_objects:

databases/catdat/data/categories/Ab_fg.yaml

@@ -14,38 +14,38 @@ related_categories:
   - FinAb
 
 satisfied_properties:
-  - property_id: locally small
+  - property: locally small
     reason: There is a forgetful functor $\FinAb \to \Set$ and $\Set$ is locally small.
 
-  - property_id: abelian
+  - property: 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
+  - property: generator
     reason: The group $\IZ$ is a generator since it represents the forgetful functor to $\Set$.
 
-  - property_id: essentially countable
+  - property: 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: ℵ₁-accessible
+  - property: ℵ₁-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
+  - property: small
     reason: Even the collection of trivial groups is not small.
 
-  - property_id: locally finite
+  - property: locally finite
     reason: The group $\Hom(\IZ,\IZ) \cong \IZ$ is not finite.
 
-  - property_id: skeletal
+  - property: skeletal
     reason: This is trivial.
 
-  - property_id: countable
+  - property: countable
     reason: This is trivial.
 
-  - property_id: split abelian
+  - property: split abelian
     reason: The short exact sequence $0 \xrightarrow{} \IZ \xrightarrow{p} \IZ \xrightarrow{} \IZ/p \xrightarrow{} 0$ does not split.
 
-  - property_id: cogenerator
+  - property: 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.
 
 special_objects:

databases/catdat/data/categories/Alg(R).yaml

@@ -15,56 +15,56 @@ related_categories:
   - Ring
 
 satisfied_properties:
-  - property_id: locally small
+  - property: locally small
     reason: There is a forgetful functor $\Alg(R) \to \Set$ and $\Set$ is locally small.
 
-  - property_id: finitary algebraic
+  - property: finitary algebraic
     reason: Take the algebraic theory of an $R$-algebra.
 
-  - property_id: strict terminal object
+  - property: 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: disjoint finite products
+  - property: disjoint finite products
     reason: One can take the same proof as for <a href="/category/Ring">$\Ring$</a>.
 
-  - property_id: Malcev
+  - property: Malcev
     reason: This follows in the same way as for <a href="/category/Grp">$\Grp$</a>, 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>.
 
 unsatisfied_properties:
-  - property_id: skeletal
+  - property: skeletal
     reason: This is trivial.
 
-  - property_id: balanced
+  - property: 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: semi-strongly connected
+  - property: semi-strongly connected
     reason: This is because already the full subcategory <a href="/category/CAlg(R)">$\CAlg(R)$</a> of commutative algebras is not semi-strongly connected.
 
-  - property_id: cogenerating set
+  - property: 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
+  - property: 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: co-Malcev
+  - property: 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
+  - property: coregular
     reason: 'We just need to tweak the proof for <a href="/category/Ring">$\Ring$</a>. 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
+  - property: regular quotient object classifier
     reason: We may copy the proof for <a href="/category/CAlg(R)">$\CRing$</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
+  - property: 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
+  - property: cofiltered-limit-stable epimorphisms
     reason: We already know that <a href="/category/CRing">$\CAlg(R)$</a> 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
+  - property: 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:

databases/catdat/data/categories/B.yaml

@@ -15,38 +15,38 @@ related_categories:
   - FS
 
 satisfied_properties:
-  - property_id: locally small
+  - property: locally small
     reason: There is a forgetful functor $\IB \to \Set$ and $\Set$ is locally small.
 
-  - property_id: locally finite
+  - property: locally finite
     reason: There is a faithful functor $\IB \to \FinSet$ and <a href="/category/FinSet">$\FinSet$</a> is locally finite.
 
-  - property_id: inhabited
+  - property: inhabited
     reason: This is trivial.
 
-  - property_id: groupoid
+  - property: groupoid
     reason: This is trivial.
 
-  - property_id: essentially countable
+  - property: essentially countable
     reason: Every finite set is isomorphic to some $\{1,\dotsc,n\}$ for some $n \in \IN$.
 
 unsatisfied_properties:
-  - property_id: small
+  - property: small
     reason: Even the collection of singletons is not small.
 
-  - property_id: skeletal
+  - property: skeletal
     reason: This is trivial.
 
-  - property_id: generator
+  - property: generator
     reason: This is trivial.
 
-  - property_id: essentially finite
+  - property: essentially finite
     reason: This is trivial.
 
-  - property_id: countable
+  - property: countable
     reason: This is trivial.
 
-  - property_id: connected
+  - property: connected
     reason: For every $n \geq 0$ there is a connected component of sets of size $n$.
 
 special_objects: {}

databases/catdat/data/categories/BG_c.yaml

@@ -16,26 +16,26 @@ related_categories:
   - BN
 
 satisfied_properties:
-  - property_id: small
+  - property: small
     reason: This is trivial.
 
-  - property_id: groupoid
+  - property: groupoid
     reason: This is trivial.
 
-  - property_id: connected
+  - property: connected
     reason: This is trivial.
 
-  - property_id: skeletal
+  - property: skeletal
     reason: There is just one object.
 
-  - property_id: generator
+  - property: generator
     reason: The unique object is a generator for trivial reasons.
 
-  - property_id: countable
+  - property: countable
     reason: This is because $G$ is countable.
 
 unsatisfied_properties:
-  - property_id: locally finite
+  - property: locally finite
     reason: This is because we choose $G$ to be infinite.
 
 special_objects: {}

databases/catdat/data/categories/BG_f.yaml

@@ -17,26 +17,26 @@ related_categories:
   - BN
 
 satisfied_properties:
-  - property_id: finite
+  - property: finite
     reason: This is trivial.
 
-  - property_id: small
+  - property: small
     reason: This is trivial.
 
-  - property_id: groupoid
+  - property: groupoid
     reason: This is trivial.
 
-  - property_id: connected
+  - property: connected
     reason: This is trivial.
 
-  - property_id: skeletal
+  - property: skeletal
     reason: There is just one object.
 
-  - property_id: generator
+  - property: generator
     reason: The unique object is a generator for trivial reasons.
 
 unsatisfied_properties:
-  - property_id: trivial
+  - property: trivial
     reason: This is trivial.
 
 special_objects: {}