complete data for walking composable pair

Author: ScriptRaccoon

database/data/007_category-satisfied-properties.sql

@@ -778,8 +778,8 @@ VALUES
 	),
 	(
 		'walking_composable_pair',
-		'products',
-		'trivial'
+		'locally finitely presentable',
+		'We get coproducts by taking the supremum inside $\{0 < 1 < 2\}$. The objects $0,1,2$ are finitely presentable for trivial reasons.'
 	),
 	(
 		'walking_composable_pair',

database/data/008_category-unsatisfied-properties.sql

@@ -606,7 +606,6 @@ VALUES
 		'trivial',
 		'trivial'
 	),
-
 	(
 		'walking_pair',
 		'initial object',
@@ -637,6 +636,16 @@ VALUES
 		'skeletal',
 		'The two objects are isomorphic, but different.'
 	),
+	-- (
+	-- 	'walking_composable_pair',
+	-- 	'zero morphisms',
+	-- 	'There is no morphism $1 \to 0$.'
+	-- ),
+	(
+		'walking_composable_pair',
+		'finitary algebraic',
+		'More generally, let $\mathcal{C}$ be a thin finitary algebraic category. Let $F : \mathbf{Set} \to \mathcal{C}$ denote the free algebra functor. Every object $A \in \mathcal{C}$ admits a regular epimorphism $F(X) \to A$ for some set $X$. But since $\mathcal{C}$ is left cancellative, every regular epimorphism must be an isomorphism. Also, $F(X)$ is a coproduct of copies of $F(1)$, which means it is either the initial object $0$ or $F(1)$ itself (since $\mathcal{C}$ is thin). This shows that $\mathcal{C}$ must have at most $2$ objects up to isomorphism. In fact, either $\mathcal{C}$ is trivial or equivalent to the <a href="/category/walking_morphism">interval category</a> $\{0 \to 1\}$ (which <i>is</i> finitary algebraic).'
+	),
 
 	-- geometric categories
 	(

database/data/012_initial_objects.sql

@@ -49,5 +49,6 @@ VALUES
 ('walking_isomorphism', 'initial object', 'both objects'),
 ('walking_morphism', 'initial object', '$0$'),
 ('Z', 'initial object', 'constant functor with value $\emptyset$'),
-('Zdiv', 'initial object', '$1$');
+('Zdiv', 'initial object', '$1$'),
+('walking_composable_pair', 'initial object', '$0$');
 

database/data/013_terminal_objects.sql

@@ -47,4 +47,5 @@ VALUES
 ('walking_isomorphism', 'terminal object', 'both objects'),
 ('walking_morphism', 'terminal object', '$1$'),
 ('Z', 'terminal object', 'constant functor with value $1$'),
-('Zdiv', 'terminal object', '$0$');
+('Zdiv', 'terminal object', '$0$'),
+('walking_composable_pair', 'terminal object', '$2$');

database/data/014_coproducts.sql

@@ -40,6 +40,7 @@ VALUES
 ('Vect', 'coproducts', 'direct sums'),
 ('walking_isomorphism', 'coproducts', '$0 \sqcup 0 = 0$'),
 ('walking_morphism', 'coproducts', '$0 \sqcup x = x$, $1 \sqcup x = 1$'),
+('walking_composable_pair', 'coproducts', 'supremum taken in $\{0 < 1 < 2\}$'),
 ('Z', 'coproducts', 'pointwise disjoint union'),
 ('Zdiv', 'coproducts', 'the least common multiple, can be $0$ for infinite families'),
 -- only finite and countable coproducts

database/data/015_products.sql

@@ -37,6 +37,7 @@ VALUES
 ('Vect', 'products', 'direct products with pointwise operations'),
 ('walking_isomorphism', 'products', '$0 \times 0 = 0$'),
 ('walking_morphism', 'products', '$0 \times x = 0$, $1 \times x = x$'),
+('walking_composable_pair', 'products', 'infimum taken in $\{0 < 1 < 2\}$'),
 ('Z', 'products', 'pointwise defined direct product'),
 ('Zdiv', 'products', 'greatest common divisor'),
 -- only finite and countable products

database/data/017_isomorphisms.sql

@@ -132,6 +132,12 @@ VALUES
 		'the two identities',
 		'trivial'
 	),
+	(
+		'walking_composable_pair',
+		'isomorphisms',
+		'the three identities',
+		'trivial'
+	),
 	(
 		'M-Set',
 		'isomorphisms',

database/data/018_monomorphisms.sql

@@ -130,7 +130,13 @@ VALUES
 		'walking_morphism',
 		'monomorphisms',
 		'every morphism',
-		'trivial'
+		'It is a thin category.'
+	),
+	(
+		'walking_composable_pair',
+		'monomorphisms',
+		'every morphism',
+		'It is a thin category.'
 	),
 	(
 		'M-Set',

database/data/019_epimorphisms.sql

@@ -95,6 +95,12 @@ VALUES
 		'every morphism',
 		'It is a thin category.'
 	),
+	(
+		'walking_composable_pair',
+		'epimorphisms',
+		'every morphism',
+		'It is a thin category.'
+	),
 	(
 		'M-Set',
 		'epimorphisms',