Add new properties: direct, inverse, one-way

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$',

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'),

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 <i>direct</i> if it contains no infinite sequence of non-identity morphisms of the form
+	<p>$\cdots \to A_2 \to A_1 \to A_0.$</p>
+	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 <i>inverse</i> if its dual is direct, i.e., if it contains no infinite sequence of non-identity morphisms of the form
+	<p>$A_0 \to A_1 \to A_2 \to \cdots.$</p>',
+	'https://ncatlab.org/nlab/show/inverse+category',
+	'direct',
+	FALSE
+),
+(
+	'one-way',
+	'is',
+	'A category is <i>one-way</i> if every endomorphism in it is equal to the identity.',
+	'https://ncatlab.org/nlab/show/one-way+category',
+	'one-way',
+	TRUE
 );

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');
+('reflexive coequalizers', 'sifted colimits'),
+('direct', 'one-way'),
+('direct', 'skeletal'),
+('inverse', 'one-way'),
+('inverse', 'skeletal'),
+('one-way', 'direct'),
+('one-way', 'inverse');

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.'
 );

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.'
+);

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 <a href="/category/B">finite sets and bijections</a> is not one-way.'
 );

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 <a href="/category/B">finite sets and bijections</a> is not one-way.'
 );
+

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\}$.'
 );

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 <a href="/category-implication/distributive_criterion">here</a>). 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$.'
 );

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$.'
+);

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$.'
 );

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$.'
+);

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$.'
+);

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 <a href="/category/1">trivial category</a>. The slice category over $1$ is the <a href="/category/walking_morphism">walking morphism</a>. Finally, the slice category over $2$ ist the <a href="/category/walking_commutative_square">walking commutative square</a>. All of these are cartesian closed, see their pages for details.'
 ),
+(
+	'walking_fork',
+	'one-way',
+	TRUE,
+	'This is trivial.'
+),
 (
 	'walking_fork',
 	'terminal object',

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',

database/data/005_implications/001_limits-colimits-existence-implications.sql

@@ -97,7 +97,6 @@ VALUES
 	'This is trivial.',
 	FALSE
 ),
-
 (
 	'complete_characterization',
 	'["complete"]',

database/data/005_implications/004_morphism-behavior-implications.sql

@@ -103,4 +103,67 @@ 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 <a href="https://ncatlab.org/nlab/show/direct+category#direct_versus_oneway_categories" target="_blank">nLab</a> 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
+),
+(
+	'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
+),
+(
+	'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
 );

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
 );

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
 }

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
 }

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
 }