Assign properties

ykawase5048 · ykawase5048 · commit 3e0da5eba4a7 · 2026-04-12T08:30:14.000+09:00
diff --git a/database/data/004_property-assignments/0.sql b/database/data/004_property-assignments/0.sql
@@ -29,6 +29,12 @@ VALUES
 	TRUE,
 	'This is trivial.'
 ),
+(
+	'0',
+	'multialgebraic',
+	TRUE,
+	'The terminal category $\mathbf{1}$ becomes an FPC-sketch by selecting the unique empty cone and cocone. Then, a $\mathbf{Set}$-valued model of this sketch is a functor $\mathbf{1} \to \mathbf{Set}$ sending the unique object to a terminal and initial object, which never exists. Hence, $\mathbf{0}$ is the category of models of this FPC-sketch.'
+),
 (
 	'0',
 	'inhabited',
diff --git a/database/data/004_property-assignments/2.sql b/database/data/004_property-assignments/2.sql
@@ -23,6 +23,12 @@ VALUES
 	TRUE,
 	'This is trivial.'
 ),
+(
+	'2',
+	'multialgebraic',
+	TRUE,
+	'There is an FPC-sketch whose $\mathbf{Set}$-model is precisely a pair $(X,Y)$ of sets such that the coproduct $X+Y$ is a singleton. Any $\mathbf{Set}$-model of such a sketch is isomorphic to either $(\varnothing, 1)$ or $(1, \varnothing)$, hence the category of models is equivalent to $\mathbf{2}$.'
+),
 (
 	'2',
 	'connected',
diff --git a/database/data/004_property-assignments/Ab_fg.sql b/database/data/004_property-assignments/Ab_fg.sql
@@ -64,4 +64,10 @@ VALUES
 	'skeletal',
 	FALSE,
 	'This is trivial.'
+),
+(
+	'Ab_fg',
+	'countable',
+	FALSE,
+	'This is trivial.'
 );
diff --git a/database/data/004_property-assignments/B.sql b/database/data/004_property-assignments/B.sql
@@ -13,7 +13,7 @@ VALUES
 ),
 (
 	'B',
-	'essentially small',
+	'essentially countable',
 	TRUE,
 	'Every finite set is isomorphic to some $[n] = \{1,\dotsc,n\}$ for some $n \in \mathbb{N}$.'
 ),
@@ -58,4 +58,16 @@ VALUES
 	'skeletal',
 	FALSE,
 	'This is trivial.'
+),
+(
+	'B',
+	'multiterminal object',
+	FALSE,
+	'This is trivial.'
+),
+(
+	'B',
+	'countable',
+	FALSE,
+	'This is trivial.'
 );
diff --git a/database/data/004_property-assignments/BN.sql b/database/data/004_property-assignments/BN.sql
@@ -11,6 +11,12 @@ VALUES
 	TRUE,
 	'This is trivial.'
 ),
+(
+	'BN',
+	'countable',
+	TRUE,
+	'This is trivial.'
+),
 (
 	'BN',
 	'strongly connected',
diff --git a/database/data/004_property-assignments/FI.sql b/database/data/004_property-assignments/FI.sql
@@ -25,7 +25,7 @@ VALUES
 ),
 (
 	'FI',
-	'essentially small',
+	'essentially countable',
 	TRUE,
 	'Every finite set is isomorphic to some $[n] = \{1,\dotsc,n\}$ for some $n \in \mathbb{N}$.'
 ),
@@ -118,4 +118,10 @@ VALUES
 	'strongly connected',
 	FALSE,
 	'There is no map from a non-empty set to the empty set.'
+),
+(
+	'FI',
+	'countable',
+	FALSE,
+	'This is trivial.'
 );
diff --git a/database/data/004_property-assignments/FS.sql b/database/data/004_property-assignments/FS.sql
@@ -13,7 +13,7 @@ VALUES
 ),
 (
 	'FS',
-	'essentially small',
+	'essentially countable',
 	TRUE,
 	'Every finite set is isomorphic to some $[n] = \{1,\dotsc,n\}$ for some $n \in \mathbb{N}$.'
 ),
@@ -53,6 +53,12 @@ VALUES
 	TRUE,
 	'If $f : X \to Y$ is a surjective map of finite sets, it is the coequalizer of the two projections $p_1, p_2 : X \times_Y X \rightrightarrows X$ in $\mathbf{FinSet}$, but also in $\mathbf{FS}$. Notice that $p_1,p_2$ are surjective. Even though $X \times_Y X$ is not a pullback in $\mathbf{FS}$, we can use this finite set here.'
 ),
+(
+	'FS',
+	'multiterminal object',
+	TRUE,
+	'The empty set and a singleton give a multiterminal object.'
+),
 (
 	'FS',
 	'small',
@@ -116,4 +122,16 @@ VALUES
 	but
 	$(E_1 \vee E_2) \wedge (E_1 \vee E_3) = \top \wedge \top = \top$.
 	<p>*For thin categories, the properties codistributive and distributive <a href="/category-implication/distributive_duality">are equivalent</a>.'
+),
+(
+	'FS',
+	'multiinitial object',
+	FALSE,
+	'This is trivial.'
+),
+(
+	'FS',
+	'countable',
+	FALSE,
+	'This is trivial.'
 );
diff --git a/database/data/004_property-assignments/FinAb.sql b/database/data/004_property-assignments/FinAb.sql
@@ -13,7 +13,7 @@ VALUES
 ),
 (
 	'FinAb',
-	'essentially small',
+	'essentially countable',
 	TRUE,
 	'The underlying set of a finite structure can be chosen to be a subset of $\mathbb{N}$.'
 ),
@@ -58,4 +58,10 @@ VALUES
 	'skeletal',
 	FALSE,
 	'There are many trivial and hence isomorphic groups which are not equal.'
+),
+(
+	'FinAb',
+	'countable',
+	FALSE,
+	'This is trivial.'
 );
diff --git a/database/data/004_property-assignments/FinGrp.sql b/database/data/004_property-assignments/FinGrp.sql
@@ -19,7 +19,7 @@ VALUES
 ),
 (
 	'FinGrp',
-	'essentially small',
+	'essentially countable',
 	TRUE,
 	'The underlying set of a finite structure can be chosen to be a subset of $\mathbb{N}$.'
 ),
@@ -100,4 +100,10 @@ VALUES
 	'sequential colimits',
 	FALSE,
 	'Let $G$ be a non-trivial finite group. We prove that the sequence of homomorphisms $1 \to G \to G^2 \to G^3 \to \cdots$ defined by $(x_1,\dotsc,x_n) \mapsto (x_1,\dotsc,x_n,1)$ has no colimit. Assume that $(G^n \to C)_{n \in \mathbb{N}}$ is a colimit. If $m \in \mathbb{N}$ is fixed, we have homomorphisms $G^n \to G^m$ for $n \in \mathbb{N}$ defined as the inclusion for $n \leq m$ and as the projection for $n \geq m$. They are compatible, hence yield a homomorphism $C \to G^m$. By construction, $G^m \to C \to G^m$ is the identity. In particular, $C \to G^m$ is surjective. But then $C$ has at least $2^m$ elements, for every $m$, which is a contradiction.'
+),
+(
+	'FinGrp',
+	'countable',
+	FALSE,
+	'This is trivial.'
 );
diff --git a/database/data/004_property-assignments/FinOrd.sql b/database/data/004_property-assignments/FinOrd.sql
@@ -61,7 +61,7 @@ VALUES
 ),
 (
 	'FinOrd',
-	'essentially small',
+	'essentially countable',
 	TRUE,
 	'Every finite ordered set is isomorphic to $\{0 < \cdots < n-1 \}$ for some $n \in \mathbb{N}$.'
 ),
@@ -124,4 +124,10 @@ VALUES
 	'one-way',
 	FALSE,
 	'There are three different order-preserving maps $\{0 < 1\} \to \{0 < 1\}$.'
+),
+(
+	'FinOrd',
+	'countable',
+	FALSE,
+	'This is trivial.'
 );
diff --git a/database/data/004_property-assignments/FinSet.sql b/database/data/004_property-assignments/FinSet.sql
@@ -13,7 +13,7 @@ VALUES
 ),
 (
 	'FinSet',
-	'essentially small',
+	'essentially countable',
 	TRUE,
 	'Every finite set is isomorphic to some $[n] = \{1,\dotsc,n\}$ for some $n \in \mathbb{N}$.'
 ),
@@ -70,4 +70,10 @@ VALUES
 	'Malcev',
 	FALSE,
 	'There are lots of non-symmetric reflexive relations.'
+),
+(
+	'FinSet',
+	'countable',
+	FALSE,
+	'This is trivial.'
 );
diff --git a/database/data/004_property-assignments/Fld.sql b/database/data/004_property-assignments/Fld.sql
@@ -11,18 +11,6 @@ VALUES
 	TRUE,
 	'There is a forgetful functor $\mathbf{Fld} \to \mathbf{Set}$ and $\mathbf{Set}$ is locally small.'
 ),
-(
-	'Fld',
-	'directed colimits',
-	TRUE,
-	'Consider a directed diagram $(F_i)$ of fields and take the colimit $F$ in the category of commutative rings. Now one checks that $F$ is a field as well, and the universal property remains true for fields.'
-),
-(
-	'Fld',
-	'connected limits',
-	TRUE,
-	'Consider a connected diagram $(F_i)$ of fields and take the limit $F$ in the category of commutative rings. Now one checks that $F$ is a field as well, and the universal property remains true for fields. Namely, $1 = 0$ in $F$ would imply that $1 = 0$ in each $F_i$ and hence, since the diagram is connected, in some $F_i$, which is a contradiction. And if $x \in F$ is non-zero, then all components $x_i$ are non-zero and hence invertible: Choose some $j$ such that $x_j$ is non-zero. Since there is a zig zag path of morphisms between $i$ and $j$ in the index category, which get mapped to field homomorphisms which are injective, it follows that $x_i$ is non-zero.'
-),
 (
 	'Fld',
 	'inhabited',
@@ -35,12 +23,6 @@ VALUES
 	TRUE,
 	'It is well-known that every field homomorphism is injective and hence a monomorphism.'
 ),
-(
-	'Fld',
-	'well-powered',
-	TRUE,
-	'The subfields of a given field form a set.'
-),
 (
 	'Fld',
 	'well-copowered',
@@ -49,9 +31,9 @@ VALUES
 ),
 (
 	'Fld',
-	'generating set',
+	'multialgebraic',
 	TRUE,
-	'The fields $Q(\mathbb{Z}[X]/\mathfrak{p})$, where $\mathfrak{p}$ runs through all prime ideals of the polynomial ring, provide a generating set. This is because for every element $a \in K$ of a field $K$ there is a prime ideal $\mathfrak{p}$ with a homomorphism $Q(\mathbb{Z}[X]/\mathfrak{p}) \to K$ mapping $[X]$ to $a$: There is a homomorphism $\mathbb{Z}[X] \to K$ mapping $X \mapsto a$. Let $\mathfrak{p}$ be its kernel. Then it extends to a field homomorphism as desired.'
+	'See Eg. 4.3(1) in <a href="http://www.tac.mta.ca/tac/volumes/8/n3/8-03abs.html" target="_blank">[AR01]</a>.'
 ),
 (
 	'Fld',
@@ -83,12 +65,6 @@ VALUES
 	FALSE,
 	'Assume that there is a cogenerating set $S$. Take a field $F$ which is larger than all the fields in $S$ and admits a non-trivial automorphism (for example, a field of rational functions). Then there is no field homomorphism $F \to Q$ for $Q \in S$. Since $S$ cogenerates, this means that every two homomorphisms $F \rightrightarrows F$ are equal, a contradiction.'
 ),
-(
-	'Fld',
-	'essentially small',
-	FALSE,
-	'Consider function fields in any number of variables.'
-),
 (
 	'Fld',
 	'skeletal',
@@ -112,4 +88,10 @@ VALUES
 	'binary powers',
 	FALSE,
 	'Assume that the product $P := \mathbb{Q}(\sqrt{2}) \times \mathbb{Q}(\sqrt{2})$ exists. This field is isomorphic to a subfield of $\mathbb{Q}(\sqrt{2})$, hence $P \cong \mathbb{Q}$ or $P \cong \mathbb{Q}(\sqrt{2})$. In the first case, the two projections $P \rightrightarrows \mathbb{Q}(\sqrt{2})$ must be equal, which means that every two homomorphisms $K \rightrightarrows \mathbb{Q}(\sqrt{2})$ are equal, which is absurd (take $K = \mathbb{Q}(\sqrt{2})$ and its two automorphisms). In the second case, the projections induce for every field $K$ a bijection $\mathrm{Hom}(K,\mathbb{Q}(\sqrt{2})) \cong \mathrm{Hom}(K,\mathbb{Q}(\sqrt{2}))^2$, which however fails for $K = \mathbb{Q}(\sqrt{2})$: the left hand side has $2$ elements, the right hand side has $4$ elements. A more general result about products in $\mathbf{Fld}$ can be found at <a href="https://math.stackexchange.com/questions/359352" target="_blank">MSE/359352</a>.'
+),
+(
+	'Fld',
+	'multiterminal object',
+	FALSE,
+	'Every field has a non-trivial extension, for instance, the rational function field over itself in one variable. Hence, a multiterminal object never exists.'
 );
diff --git a/database/data/004_property-assignments/Man.sql b/database/data/004_property-assignments/Man.sql
@@ -119,4 +119,10 @@ VALUES
 	'sequential colimits',
 	FALSE,
 	'Assume that the sequence of inclusions $i_n : \mathbb{R}^n \hookrightarrow \mathbb{R}^{n+1}$, $(x_1,\dotsc,x_n) \mapsto (x_1,\dotsc,x_n,0)$ (for $n \geq 1$) has a colimit $M$ in $\mathbf{Man}$. Let $0 \in M$ denote the image of $0 \in \mathbb{R}^1$. Let $k \geq 1$. We define smooth maps $f_n : \mathbb{R}^n \to \mathbb{R}^k$ as follows: For $n \leq k$ it is the inclusion $(x_1,\dotsc,x_n) \mapsto (x_1,\dotsc,x_n,0,\dotsc,0)$. For $n \geq k$ it is the projection $(x_1,\dotsc,x_n) \mapsto (x_1,\dotsc,x_k)$. These maps are compatible with the inclusions $i_n$, hence extend to a smooth map $M \to \mathbb{R}^k$. By construction, $\mathbb{R}^k \to M \to \mathbb{R}^k$ is the identity. Hence, for the tangent spaces also $T_0(\mathbb{R}^k) \to T_0(M) \to T_0(\mathbb{R}^k)$ is the identity, showing that $\dim T_0(M) \geq k$. Since this holds for all $k$, but $T_0(M)$ is finite-dimensional, we have a contradiction.'
+),
+(
+	'Man',
+	'countable',
+	FALSE,
+	'This is trivial.'
 );
diff --git a/database/data/004_property-assignments/N.sql b/database/data/004_property-assignments/N.sql
@@ -53,6 +53,12 @@ VALUES
 	TRUE,
 	'This is because the natural numbers with respect to $<$ are well-founded.'
 ),
+(
+	'N',
+	'countable',
+	TRUE,
+	'This is trivial.'
+),
 (
 	'N',
 	'countable coproducts',
diff --git a/database/data/004_property-assignments/N_oo.sql b/database/data/004_property-assignments/N_oo.sql
@@ -11,6 +11,12 @@ VALUES
 	TRUE,
 	'This is trivial.'
 ),
+(
+	'N_oo',
+	'countable',
+	TRUE,
+	'This is trivial.'
+),
 (
 	'N_oo',
 	'coproducts',
diff --git a/database/data/004_property-assignments/Set_op.sql b/database/data/004_property-assignments/Set_op.sql
@@ -7,7 +7,7 @@ INSERT INTO category_property_assignments (
 VALUES
 (
 	'Set_op',
-	'locally presentable',
+	'accessible',
 	FALSE,
 	'This follows from the fact that the opposite category of a complete accessible large category is never accessible. See <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>, Thm. 3.4.3.'
 );
diff --git a/database/data/004_property-assignments/Setne.sql b/database/data/004_property-assignments/Setne.sql
@@ -83,6 +83,24 @@ VALUES
 	TRUE,
 	'Use constant maps.'
 ),
+(
+	'Setne',
+	'generalized variety',
+	TRUE,
+	'Since the inclusion $\mathbf{Set}_{\neq \varnothing} \hookrightarrow \mathbf{Set}$ is closed under non-empty colimits, it is also closed under sifted colimits. Therefore, non-empty finite sets are still strongly finitely presentable in $\mathbf{Set}_{\neq \varnothing}$, and every non-empty set is written as a small sifted colimit of them.'
+),
+(
+	'Setne',
+	'finitely accessible',
+	TRUE,
+	'Since the inclusion $\mathbf{Set}_{\neq \varnothing} \hookrightarrow \mathbf{Set}$ is closed under non-empty colimits, it is also closed under filtered colimits. Therefore, non-empty finite sets are still finitely presentable in $\mathbf{Set}_{\neq \varnothing}$, and every non-empty set is written as a small filtered colimit of them.'
+),
+(
+	'Setne',
+	'multilimits',
+	TRUE,
+	'Let $D$ be a diagram in $\mathbf{Set}_{\neq \varnothing}$, and let $L$ be a limit of $D$ in $\mathbf{Set}$. If $L$ is non-empty, it gives a limit in $\mathbf{Set}_{\neq \varnothing}$ as well. If $L$ is the empty set, there is no cone over $D$ in $\mathbf{Set}_{\neq \varnothing}$; hence the empty set of cone gives a multilimit of $D$ in $\mathbf{Set}_{\neq \varnothing}$.'
+),
 (
 	'Setne',
 	'sequential limits',
diff --git a/database/data/004_property-assignments/Sp.sql b/database/data/004_property-assignments/Sp.sql
@@ -64,4 +64,10 @@ VALUES
 	'generator',
 	FALSE,
 	'Assume that a generator $G$ exists. For $n \geq 0$ let $F_n$ be the combinatorial species of sets of cardinality $\neq n$: $F_n(A) = \varnothing$ when $A$ has cardinality $n$, otherwise $F_n(A) = \{A\}$. There are two different morphisms $F_n \rightrightarrows F_n \sqcup F_n$. Hence, there must be at least one morphism $G \to F_n$. If $A$ has cardinality $n$, this implies $G(A) = \varnothing$. Since this holds for all $n$, $G$ is the initial object. But this is clearly no generator (it would mean that the category is thin).'
+),
+(
+	'Sp',
+	'essentially countable',
+	FALSE,
+	'Any function $f\colon\mathbb{N} \to \mathbb{N}$ can be regarded as a combinatorial species with trivial actions, and distinct functions yield non-isomorphic species.'
 );
diff --git a/database/data/004_property-assignments/Top.sql b/database/data/004_property-assignments/Top.sql
@@ -118,4 +118,10 @@ VALUES
 	'co-Malcev',
 	FALSE,
 	'See <a href="https://mathoverflow.net/questions/509548" target="_blank">MO/509548</a>. We can also phrase the proof as follows: Consider the forgetful functor $U : \mathbf{Top} \to \mathbf{Set}$ and the relation $R \subseteq U^2$ defined by $R(X) := \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the singleton and $R$ by the Sierpinski space. It is clear that $R$ is reflexive, but not symmetric.'
+),
+(
+	'Top',
+	'coaccessible',
+	FALSE,
+	'Assume $\mathbf{Top}$ is coaccessible. Let $p\colon S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\mathbf{Set}$, is coaccessible by Prop. 4.7 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>. However, since $\mathbf{Set}$ is not coaccessible, this is a contradiction.'
 );
diff --git a/database/data/004_property-assignments/Z_div.sql b/database/data/004_property-assignments/Z_div.sql
@@ -11,6 +11,12 @@ VALUES
 	TRUE,
 	'This is trivial.'
 ),
+(
+	'Z_div',
+	'countable',
+	TRUE,
+	'This is trivial.'
+),
 (
 	'Z_div',
 	'products',
diff --git a/database/data/004_property-assignments/real_interval.sql b/database/data/004_property-assignments/real_interval.sql
@@ -37,7 +37,7 @@ VALUES
 ),
 (
 	'real_interval',
-	'essentially finite',
+	'essentially countable',
 	FALSE,
 	'This is trivial.'
 ),
diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json
diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json
diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json
