From 89cb460833e34a43fa4a764e1ca913d2bf1895cf Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 3 Apr 2026 12:41:22 +0200 Subject: [PATCH 1/6] adjust some tags --- database/data/002_tags/002_category-tags.sql | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/database/data/002_tags/002_category-tags.sql b/database/data/002_tags/002_category-tags.sql index 7bb43550..d51b9023 100644 --- a/database/data/002_tags/002_category-tags.sql +++ b/database/data/002_tags/002_category-tags.sql @@ -5,6 +5,7 @@ VALUES ('0', 'thin'), ('1', 'tiny'), ('1', 'well-behaved'), +('1', 'single object'), ('1', 'thin'), ('2', 'tiny'), ('2', 'badly-behaved'), @@ -144,14 +145,16 @@ VALUES ('walking_commutative_square', 'category theory'), ('walking_commutative_square', 'thin'), ('walking_composable_pair', 'tiny'), -('walking_composable_pair', 'badly-behaved'), +('walking_composable_pair', 'well-behaved'), ('walking_composable_pair', 'category theory'), +('walking_composable_pair', 'thin'), ('walking_fork', 'tiny'), ('walking_fork', 'badly-behaved'), ('walking_fork', 'category theory'), ('walking_isomorphism', 'tiny'), ('walking_isomorphism', 'well-behaved'), ('walking_isomorphism', 'category theory'), +('walking_isomorphism', 'thin'), ('walking_morphism', 'tiny'), ('walking_morphism', 'well-behaved'), ('walking_morphism', 'category theory'), From cfa4a9d9015f5c66c04869223f16ce3f2931a894 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 3 Apr 2026 15:31:59 +0200 Subject: [PATCH 2/6] shorter name --- database/data/001_categories/007_tiny.sql | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/data/001_categories/007_tiny.sql b/database/data/001_categories/007_tiny.sql index 28f8c10e..f4cc0ed0 100644 --- a/database/data/001_categories/007_tiny.sql +++ b/database/data/001_categories/007_tiny.sql @@ -51,7 +51,7 @@ VALUES ), ( 'walking_pair', - 'walking parallel pair of morphisms', + 'walking parallel pair', '$\{0 \rightrightarrows 1 \}$', 'two objects $0$ and $1$', 'the two identities and two parallel morphisms from $0$ to $1$', From ae52a46ba0deefc9b0b8d90574df53cdb56642ac Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 3 Apr 2026 13:10:41 +0200 Subject: [PATCH 3/6] add easy result about thin categories --- .../006_trivial-categories-implications.sql | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/database/data/005_implications/006_trivial-categories-implications.sql b/database/data/005_implications/006_trivial-categories-implications.sql index 815243b2..c97f339c 100644 --- a/database/data/005_implications/006_trivial-categories-implications.sql +++ b/database/data/005_implications/006_trivial-categories-implications.sql @@ -96,4 +96,11 @@ VALUES '["regular"]', 'In a thin category, regular epimorphisms are isomorphisms, and the rest is clear as well.', FALSE +), +( + 'thin_zero_trivial', + '["thin", "zero morphisms", "inhabited"]', + '["trivial"]', + 'This is easy.', + FALSE ); \ No newline at end of file From 12453cbb0579ba234c0b35ddda0530cce0d49f8e Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 3 Apr 2026 13:20:32 +0200 Subject: [PATCH 4/6] add properties: direct, inverse, one-way --- .../003_properties/005_morphism-behavior.sql | 27 ++++++++++++ .../003_properties/100_related_properties.sql | 8 +++- database/data/004_property-assignments/BN.sql | 6 +++ .../data/004_property-assignments/BOn.sql | 8 +++- database/data/004_property-assignments/FI.sql | 6 +++ database/data/004_property-assignments/FS.sql | 7 ++++ .../data/004_property-assignments/FinOrd.sql | 6 +++ .../data/004_property-assignments/Fld.sql | 6 +++ database/data/004_property-assignments/N.sql | 14 ++++++- .../data/004_property-assignments/N_oo.sql | 12 ++++++ database/data/004_property-assignments/On.sql | 14 ++++++- .../real_interval.sql | 14 ++++++- .../004_property-assignments/walking_fork.sql | 6 +++ .../004_property-assignments/walking_pair.sql | 6 +++ .../004_morphism-behavior-implications.sql | 42 +++++++++++++++++++ scripts/expected-data/Ab.json | 5 ++- scripts/expected-data/Set.json | 5 ++- scripts/expected-data/Top.json | 5 ++- 18 files changed, 189 insertions(+), 8 deletions(-) diff --git a/database/data/003_properties/005_morphism-behavior.sql b/database/data/003_properties/005_morphism-behavior.sql index cff7f028..a628bc65 100644 --- a/database/data/003_properties/005_morphism-behavior.sql +++ b/database/data/003_properties/005_morphism-behavior.sql @@ -62,4 +62,31 @@ VALUES 'https://ncatlab.org/nlab/show/balanced+category', 'balanced', TRUE +), +( + 'direct', + 'is', + 'A category is direct if it contains no infinite sequence of non-identity morphisms of the form +

$\cdots \to A_2 \to A_1 \to A_0.$

+ For example, a poset is direct iff it is well-founded.', + 'https://ncatlab.org/nlab/show/direct+category', + 'inverse', + FALSE +), +( + 'inverse', + 'is', + 'A category is inverse if its dual is direct, i.e., if it contains no infinite sequence of non-identity morphisms of the form +

$A_0 \to A_1 \to A_2 \to \cdots.$

', + 'https://ncatlab.org/nlab/show/inverse+category', + 'direct', + FALSE +), +( + 'one-way', + 'is', + 'A category is one-way if every endomorphism in it is equal to the identity.', + 'https://ncatlab.org/nlab/show/one-way+category', + 'one-way', + TRUE ); \ No newline at end of file diff --git a/database/data/003_properties/100_related_properties.sql b/database/data/003_properties/100_related_properties.sql index 54a83fad..0be4728b 100644 --- a/database/data/003_properties/100_related_properties.sql +++ b/database/data/003_properties/100_related_properties.sql @@ -187,4 +187,10 @@ VALUES ('coreflexive equalizers', 'equalizers'), ('coreflexive equalizers', 'cosifted limits'), ('reflexive coequalizers', 'coequalizers'), -('reflexive coequalizers', 'sifted colimits'); \ No newline at end of file +('reflexive coequalizers', 'sifted colimits'), +('direct', 'one-way'), +('direct', 'skeletal'), +('inverse', 'one-way'), +('inverse', 'skeletal'), +('one-way', 'direct'), +('one-way', 'inverse'); \ No newline at end of file diff --git a/database/data/004_property-assignments/BN.sql b/database/data/004_property-assignments/BN.sql index 6b03039b..b7965990 100644 --- a/database/data/004_property-assignments/BN.sql +++ b/database/data/004_property-assignments/BN.sql @@ -70,4 +70,10 @@ VALUES 'sequential limits', FALSE, 'Assume that the sequence $\cdots \xrightarrow{1} \bullet \xrightarrow{1} \bullet \xrightarrow{1} \bullet$ has a limit. This is a (universal) sequence of natural numbers $n_0,n_1,\dotsc$ satisfying $n_i = n_{i+1} + 1$. But then $n_i = n_0 - i$, and in particular $n_{n_0 + 1} = - 1$, a contradiction.' +), +( + 'BN', + 'one-way', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/BOn.sql b/database/data/004_property-assignments/BOn.sql index 30631aef..00cc3bf5 100644 --- a/database/data/004_property-assignments/BOn.sql +++ b/database/data/004_property-assignments/BOn.sql @@ -118,4 +118,10 @@ VALUES 'pushouts', FALSE, 'Assume that $1,\omega$ have a pushout. This is a (universal) pair of ordinals $\alpha,\beta$ with $\alpha + 1 = \beta + \omega$. But $\beta + \omega$ is a limit ordinal, while $\alpha + 1$ is not.' -); +), +( + 'BOn', + 'one-way', + FALSE, + 'This is trivial.' +); \ No newline at end of file diff --git a/database/data/004_property-assignments/FI.sql b/database/data/004_property-assignments/FI.sql index 83425741..6a8a73c0 100644 --- a/database/data/004_property-assignments/FI.sql +++ b/database/data/004_property-assignments/FI.sql @@ -100,4 +100,10 @@ VALUES 'skeletal', FALSE, 'This is trivial.' +), +( + 'FI', + 'one-way', + FALSE, + 'Already the full subcategory of finite sets and bijections is not one-way.' ); diff --git a/database/data/004_property-assignments/FS.sql b/database/data/004_property-assignments/FS.sql index 74481a36..280e4188 100644 --- a/database/data/004_property-assignments/FS.sql +++ b/database/data/004_property-assignments/FS.sql @@ -94,4 +94,11 @@ VALUES 'skeletal', FALSE, 'This is trivial.' +), +( + 'FS', + 'one-way', + FALSE, + 'Already the full subcategory of finite sets and bijections is not one-way.' ); + diff --git a/database/data/004_property-assignments/FinOrd.sql b/database/data/004_property-assignments/FinOrd.sql index 94dc7e8c..97ad17d1 100644 --- a/database/data/004_property-assignments/FinOrd.sql +++ b/database/data/004_property-assignments/FinOrd.sql @@ -118,4 +118,10 @@ VALUES 'essentially finite', FALSE, 'This is trivial.' +), +( + 'FinOrd', + 'one-way', + FALSE, + 'There are three different order-preserving maps $\{0 < 1\} \to \{0 < 1\}$.' ); diff --git a/database/data/004_property-assignments/Fld.sql b/database/data/004_property-assignments/Fld.sql index 52a4fe7a..2b5490b0 100644 --- a/database/data/004_property-assignments/Fld.sql +++ b/database/data/004_property-assignments/Fld.sql @@ -100,4 +100,10 @@ VALUES 'locally cartesian closed', FALSE, 'Assume that $K$ is a field such that $\mathbf{Fld} / K$ is cartesian closed. This slice category is equivalent to the poset of subfields of $K$. This poset is a lattice, and our assumption implies that it is distributive (see here). But this is quite rare: Consider $K = \mathbb{Q}(\sqrt{2}, \sqrt{3})$. By Galois theory, the lattice of subfields is isomorphic to the diamond lattice $M_3$ which is not distributive. Specifically, $(\mathbb{Q}(\sqrt{2}) \wedge \mathbb{Q}(\sqrt{6})) \vee (\mathbb{Q}(\sqrt{3}) \wedge \mathbb{Q}(\sqrt{6})) = \mathbb{Q} \vee \mathbb{Q} = \mathbb{Q}$, while $(\mathbb{Q}(\sqrt{2}) \vee \mathbb{Q}(\sqrt{3})) \wedge \mathbb{Q}(\sqrt{6}) = \mathbb{Q}(\sqrt{2},\sqrt{3}) \wedge \mathbb{Q}(\sqrt{6}) = \mathbb{Q}(\sqrt{6})$.' +), +( + 'Fld', + 'one-way', + FALSE, + 'Consider the endomorphism $\mathbb{Q}(X) \to \mathbb{Q}(X)$, $X \mapsto X^2$.' ); diff --git a/database/data/004_property-assignments/N.sql b/database/data/004_property-assignments/N.sql index e1d27e97..883604c0 100644 --- a/database/data/004_property-assignments/N.sql +++ b/database/data/004_property-assignments/N.sql @@ -47,6 +47,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'N', + 'direct', + TRUE, + 'This is because the natural numbers with respect to $<$ are well-founded.' +), ( 'N', 'countable coproducts', @@ -58,4 +64,10 @@ VALUES 'essentially finite', FALSE, 'This is trivial.' -); +), +( + 'N', + 'inverse', + FALSE, + 'Consider the strictly increasing sequence $0 < 1 < 2 < \cdots$.' +); \ No newline at end of file diff --git a/database/data/004_property-assignments/N_oo.sql b/database/data/004_property-assignments/N_oo.sql index 98d39bb3..1f6a8814 100644 --- a/database/data/004_property-assignments/N_oo.sql +++ b/database/data/004_property-assignments/N_oo.sql @@ -23,6 +23,12 @@ VALUES TRUE, 'The relation $\leq$ is antisymmetric.' ), +( + 'N_oo', + 'direct', + TRUE, + 'This is because the natural numbers with $\infty$ with respect to $<$ are well-founded.' +), ( 'N_oo', 'infinitary distributive', @@ -58,4 +64,10 @@ VALUES 'self-dual', FALSE, 'This is because every upper set is infinite, but every lower set is finite.' +), +( + 'N_oo', + 'inverse', + FALSE, + 'Consider the strictly increasing sequence $0 < 1 < 2 < \cdots$.' ); diff --git a/database/data/004_property-assignments/On.sql b/database/data/004_property-assignments/On.sql index db0f7e26..9f313b92 100644 --- a/database/data/004_property-assignments/On.sql +++ b/database/data/004_property-assignments/On.sql @@ -53,6 +53,12 @@ VALUES TRUE, 'It is well-known that for ordinals $\alpha,\beta$ we have $\alpha \leq \beta$ or $\beta \leq \alpha$.' ), +( + 'On', + 'direct', + TRUE, + 'This is because the ordinal numbers with respect to $<$ are well-founded (by definition).' +), ( 'On', 'terminal object', @@ -64,4 +70,10 @@ VALUES 'well-copowered', FALSE, 'The "quotients" of $0$ are all ordinals.' -); +), +( + 'On', + 'inverse', + FALSE, + 'Consider the strictly increasing sequence $0 < 1 < 2 < \cdots$.' +); \ No newline at end of file diff --git a/database/data/004_property-assignments/real_interval.sql b/database/data/004_property-assignments/real_interval.sql index 8965e30d..d2bc8f3c 100644 --- a/database/data/004_property-assignments/real_interval.sql +++ b/database/data/004_property-assignments/real_interval.sql @@ -46,4 +46,16 @@ VALUES 'locally finitely presentable', FALSE, 'It suffices to prove that $0$ (the initial object) is the only finitely presentable object. If $s > 0$, then $s = \sup_{n \in \mathbb{N}, \, s \geq 1/n } (s - 1/n)$, but there is no $n$ with $s \leq s - 1/n$.' -); +), +( + 'real_interval', + 'direct', + FALSE, + 'Consider the strictly decreasing sequence $1/2^n$ for $n \geq 0$.' +), +( + 'real_interval', + 'inverse', + FALSE, + 'Consider the strictly increasing sequence $1 - 1/2^n$ for $n \geq 0$.' +); \ No newline at end of file diff --git a/database/data/004_property-assignments/walking_fork.sql b/database/data/004_property-assignments/walking_fork.sql index 1b7606cf..f6d17a9e 100644 --- a/database/data/004_property-assignments/walking_fork.sql +++ b/database/data/004_property-assignments/walking_fork.sql @@ -65,6 +65,12 @@ VALUES TRUE, 'We need to check that every slice category is cartesian closed. The slice category over $0$ is the trivial category. The slice category over $1$ is the walking morphism. Finally, the slice category over $2$ ist the walking commutative square. All of these are cartesian closed, see their pages for details.' ), +( + 'walking_fork', + 'one-way', + TRUE, + 'This is trivial.' +), ( 'walking_fork', 'terminal object', diff --git a/database/data/004_property-assignments/walking_pair.sql b/database/data/004_property-assignments/walking_pair.sql index 24739ad9..9933374e 100644 --- a/database/data/004_property-assignments/walking_pair.sql +++ b/database/data/004_property-assignments/walking_pair.sql @@ -47,6 +47,12 @@ VALUES TRUE, 'The two objects are not isomorphic.' ), +( + 'walking_pair', + 'one-way', + TRUE, + 'This is trivial.' +), ( 'walking_pair', 'initial object', diff --git a/database/data/005_implications/004_morphism-behavior-implications.sql b/database/data/005_implications/004_morphism-behavior-implications.sql index fb5c7b66..2f499af5 100644 --- a/database/data/005_implications/004_morphism-behavior-implications.sql +++ b/database/data/005_implications/004_morphism-behavior-implications.sql @@ -103,4 +103,46 @@ VALUES '["balanced"]', 'Any regular monomorphism that is an epimorphism must be an isomorphism.', FALSE +), +( + 'direct_implies_one-way', + '["direct"]', + '["one-way", "skeletal"]', + 'The category is one-way since any non-identity endomorphism yields an infinite sequence of equal non-identity morphisms. The category is skeletal since any non-identity isomorphism $f : A \to B$ yields the infinite sequence $\dotsc,f^{-1},f,f^{-1},f$.', + FALSE +), +( + 'thin_implies_one-way', + '["thin"]', + '["one-way"]', + 'This is trivial.', + FALSE +), +( + 'one-way_zero', + '["zero morphisms", "one-way"]', + '["thin"]', + 'If $f,g : A \rightrightarrows B$ are two morphisms, then since $0_{B,B} = \mathrm{id}_B$ we have $f = 0_{B,B} \circ f = 0_{A,B} = 0_{B,B} \circ g = g$.', + FALSE +), +( + 'direct_criterion', + '["skeletal", "one-way", "finite"]', + '["direct"]', + 'See the nLab for a proof.', + FALSE +), +( + 'one-way_products_thin', + '["one-way", "binary products"]', + '["thin"]', + 'Let $X$ be any object. The swap $\tau : X \times X \to X \times X$ is equal to the identity. It follows that the projections $p_1,p_2 : X \times X \rightrightarrows X$ are the same. And this means that all morphisms $Y \rightrightarrows X$ are the same.', + FALSE +), +( + 'one-way_groupoids', + '["one-way", "groupoid"]', + '["thin"]', + 'If $f,g : A \rightrightarrows B$ are two morphisms, then $f^{-1} \circ g : A \to A$ must be the identity, so that $f = g$.', + FALSE ); \ No newline at end of file diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index 22729543..c3f85cb0 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -100,5 +100,8 @@ "coextensive": false, "infinitary coextensive": false, "lextensive": false, - "regular subobject classifier": false + "regular subobject classifier": false, + "direct": false, + "inverse": false, + "one-way": false } diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index 6b3c478e..c7abbb3d 100644 --- a/scripts/expected-data/Set.json +++ b/scripts/expected-data/Set.json @@ -100,5 +100,8 @@ "coextensive": false, "infinitary coextensive": false, "unital": false, - "counital": false + "counital": false, + "direct": false, + "inverse": false, + "one-way": false } diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index b45a5321..a46fa11e 100644 --- a/scripts/expected-data/Top.json +++ b/scripts/expected-data/Top.json @@ -100,5 +100,8 @@ "co-Malcev": false, "unital": false, "counital": false, - "locally strongly finitely presentable": false + "locally strongly finitely presentable": false, + "direct": false, + "inverse": false, + "one-way": false } From 4de3a7b13c16fa417c6e13dc17ecef8d313c136d Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 3 Apr 2026 14:19:12 +0200 Subject: [PATCH 5/6] add more results on direct categories --- .../004_morphism-behavior-implications.sql | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/database/data/005_implications/004_morphism-behavior-implications.sql b/database/data/005_implications/004_morphism-behavior-implications.sql index 2f499af5..f68c5215 100644 --- a/database/data/005_implications/004_morphism-behavior-implications.sql +++ b/database/data/005_implications/004_morphism-behavior-implications.sql @@ -145,4 +145,18 @@ VALUES '["thin"]', 'If $f,g : A \rightrightarrows B$ are two morphisms, then $f^{-1} \circ g : A \to A$ must be the identity, so that $f = g$.', FALSE +), +( + 'discrete_implies_direct', + '["discrete"]', + '["direct"]', + 'This is trivial.', + FALSE +), +( + 'direct_implies_sequential_limits', + '["direct"]', + '["sequential limits"]', + 'Assume that $\cdots \to A_2 \to A_1 \to A_0$ is a sequence of morphisms. We will prove that almost all of them are identities, so that the sequence is eventually constant and the limit exists. Assume the opposite, i.e. that there are infinitely many $A_k \to A_{k-1}$ which are not the identity. Pick some $n_1$ such that $A_{n_1} \to A_{n_1 - 1}$ is not the identity, and let $n_0 := n_1 - 1$. If $A_{n_i} \to A_{n_{i-1}}$ has been constructed, there is some $n_{i+1} > n_i$ such that the composite $A_{n_{i+1}} \to A_{n_i}$ is not the identity, because otherwise it would follow inductively that all $A_{k+1} \to A_k$, $k \geq n_i$ would be identities, which would contradict our infiniteness assumption. This way we construct an infinite sequence of non-identity morphisms $A_{n_{i+1}} \to A_{n_i}$, a contradiction.', + FALSE ); \ No newline at end of file From ee4f8d66e195567f2bfd0bf03cc7a5d2915b88b3 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 3 Apr 2026 15:22:02 +0200 Subject: [PATCH 6/6] add result on one-way categories --- .../001_limits-colimits-existence-implications.sql | 1 - .../004_morphism-behavior-implications.sql | 7 +++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index c2fb9c86..c076abf8 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -97,7 +97,6 @@ VALUES 'This is trivial.', FALSE ), - ( 'complete_characterization', '["complete"]', diff --git a/database/data/005_implications/004_morphism-behavior-implications.sql b/database/data/005_implications/004_morphism-behavior-implications.sql index f68c5215..9be52baa 100644 --- a/database/data/005_implications/004_morphism-behavior-implications.sql +++ b/database/data/005_implications/004_morphism-behavior-implications.sql @@ -159,4 +159,11 @@ VALUES '["sequential limits"]', 'Assume that $\cdots \to A_2 \to A_1 \to A_0$ is a sequence of morphisms. We will prove that almost all of them are identities, so that the sequence is eventually constant and the limit exists. Assume the opposite, i.e. that there are infinitely many $A_k \to A_{k-1}$ which are not the identity. Pick some $n_1$ such that $A_{n_1} \to A_{n_1 - 1}$ is not the identity, and let $n_0 := n_1 - 1$. If $A_{n_i} \to A_{n_{i-1}}$ has been constructed, there is some $n_{i+1} > n_i$ such that the composite $A_{n_{i+1}} \to A_{n_i}$ is not the identity, because otherwise it would follow inductively that all $A_{k+1} \to A_k$, $k \geq n_i$ would be identities, which would contradict our infiniteness assumption. This way we construct an infinite sequence of non-identity morphisms $A_{n_{i+1}} \to A_{n_i}$, a contradiction.', FALSE +), +( + 'one-way_reflexive', + '["one-way"]', + '["reflexive coequalizers"]', + 'Every reflexive pair is equal: If $f s = g s = \mathrm{id}$, then since $s f = \mathrm{id}$ (one-way), we must have $f = s^{-1}$, and likewise $g = s^{-1}$.', + FALSE ); \ No newline at end of file