Add properties: core-thin + gaunt

databases/catdat/data/003_properties/005_morphism-behavior.sql

@@ -121,4 +121,25 @@ VALUES
 	NULL,
 	'filtered-colimit-stable monomorphisms',
 	TRUE 
-);
+),
+(
+	'core-thin',
+	'is',
+	'A category is <i>core-thin</i> if it satisfies the following equivalent conditions:
+	<ol>
+		<li>Its <a href="https://ncatlab.org/nlab/show/core+groupoid" target="_blank">core</a> is thin.</li>
+		<li>Parallel isomorphisms are equal.</li>
+		<li>Every automorphism is the identity.</li>
+	</ol>',
+	'https://ncatlab.org/nlab/show/gaunt+category',
+	'core-thin',
+	TRUE
+),
+(
+	'gaunt',
+	'is',
+	'A category is <i>gaunt</i> when every isomorphism $f : A \to B$ must be the identity (in particular, $A = B$). This is the "skeletal variant" of being core-thin.',
+	'https://ncatlab.org/nlab/show/gaunt+category',
+	'gaunt',
+	FALSE
+);

databases/catdat/data/003_properties/100_related-properties.sql

@@ -138,7 +138,9 @@ VALUES
 ('strict initial object', 'initial object'),
 ('strict terminal object', 'terminal object'),
 ('discrete', 'essentially discrete'),
+('discrete', 'thin'),
 ('essentially discrete', 'discrete'),
+('essentially discrete', 'thin'),
 ('finite', 'essentially finite'),
 ('finite', 'small'),
 ('finite', 'countable'),
@@ -292,8 +294,18 @@ VALUES
 ('direct', 'skeletal'),
 ('inverse', 'one-way'),
 ('inverse', 'skeletal'),
+('skeletal', 'gaunt'),
+('gaunt', 'skeletal'),
+('gaunt', 'one-way'),
+('gaunt', 'core-thin'),
+('core-thin', 'thin'),
+('core-thin', 'one-way'),
+('core-thin', 'gaunt'),
+('thin', 'core-thin'),
+('thin', 'discrete'),
 ('one-way', 'direct'),
 ('one-way', 'inverse'),
+('one-way', 'core-thin'),
 ('powers', 'products'),
 ('powers', 'countable powers'),
 ('powers', 'finite powers'),

databases/catdat/data/004_property-assignments/BN.sql

@@ -49,9 +49,9 @@ VALUES
 ),
 (
 	'BN',
-	'skeletal',
+	'gaunt',
 	TRUE,
-	'There is just one object.'
+	'This is because $0$ is the only natural number with an additive inverse.'
 ),
 (
 	'BN',

databases/catdat/data/004_property-assignments/BOn.sql

@@ -43,9 +43,9 @@ VALUES
 ),
 (
 	'BOn',
-	'skeletal',
+	'gaunt',
 	TRUE,
-	'There is just one object.'
+	'This is because $0$ is the only ordinal number with an additive inverse.'
 ),
 (
 	'BOn',

databases/catdat/data/004_property-assignments/Delta.sql

@@ -5,12 +5,6 @@ INSERT INTO category_property_assignments (
 	reason
 )
 VALUES
-(
-    'Delta',
-    'skeletal',
-    TRUE,
-    'If $[n] \to [m]$ is a bijection, then $n+1 = m+1$ by comparing the sizes, hence $n=m$.'
-),
 (
     'Delta',
     'countable',
@@ -53,6 +47,18 @@ VALUES
     TRUE,
     'The ordered set $[0] = \{0\}$ is a generator.'
 ),
+(
+    'Delta',
+    'skeletal',
+    TRUE,
+    'If $f : [n] \to [m]$ is an isomorphism, then $n + 1 = m + 1$ by comparing the cardinalities, hence $n = m$.'
+),
+(
+    'Delta',
+    'core-thin',
+    TRUE,
+    'The category $\mathbf{FinOrd} \setminus \{\varnothing\}$ is core-thin because already $\mathbf{FinOrd}$ is core-thin (see its <a href="/category/FinOrd">category page</a>).'
+),
 (
     'Delta',
     'mono-regular',
@@ -75,12 +81,6 @@ VALUES
     <p>$\begin{array}{ccccc} X & \xleftarrow{x_0} & [0] & \xrightarrow{y} & Y \\ \parallel && \phantom{ {\footnotesize 0}} \downarrow {\footnotesize 0} && \parallel \\ X & \xleftarrow{f} & [1] & \xrightarrow{g} & Y \\ \parallel && \phantom{ {\footnotesize 1}} \uparrow  {\footnotesize 1} && \parallel \\ X & \xleftarrow{x_1} & [0] & \xrightarrow{y} & Y \end{array}$</p>
     This shows that the choice of $x \in X$ does not matter, and for $y \in Y$ the proof is the same.'
 ),
-(
-    'Delta',
-    'coquotients of cocongruences',
-    TRUE,
-    'The simplex category has the special property that every isomorphism $[n] \to [n]$ is the identity. Thus, every cosymmetric corelation $f, g : [m] \rightrightarrows [n]$ must satisfy $f = g$. Then the identity provides an equalizer.'
-),
 (
     'Delta',
     'strict terminal object',

databases/catdat/data/004_property-assignments/FI.sql

@@ -115,9 +115,9 @@ VALUES
 ),
 (
 	'FI',
-	'one-way',
+	'core-thin',
 	FALSE,
-	'Already the full subcategory of <a href="/category/B">finite sets and bijections</a> is not one-way.'
+	'Its core is the <a href="/category/B">category of finite sets and bijections</a>, which we know is not thin.'
 ),
 (
 	'FI',

databases/catdat/data/004_property-assignments/FS.sql

@@ -109,9 +109,9 @@ VALUES
 ),
 (
 	'FS',
-	'one-way',
+	'core-thin',
 	FALSE,
-	'Already the full subcategory of <a href="/category/B">finite sets and bijections</a> is not one-way.'
+	'Its core is the <a href="/category/B">category of finite sets and bijections</a>, which we know is not thin.'
 ),
 (
 	'FS',

databases/catdat/data/004_property-assignments/FinOrd.sql

@@ -71,6 +71,12 @@ VALUES
 	TRUE,
 	'There is a forgetful functor $\mathbf{FinOrd} \to \mathbf{Set}$ and $\mathbf{Set}$ is locally small.'
 ),
+(
+	'FinOrd',
+	'core-thin',
+	TRUE,
+	'Let $f : \{1 < \cdots < n \} \to \{1 < \cdots < n \}$ be an automorphism. Then $f(i)$ is the smallest element not contained in $\{f(j) : j < i\}$. From this one can deduce $f(i)=i$ by induction.'
+),
 (
 	'FinOrd',
 	'small',

databases/catdat/data/004_property-assignments/Fld.sql

@@ -79,9 +79,9 @@ VALUES
 ),
 (
 	'Fld',
-	'one-way',
+	'core-thin',
 	FALSE,
-	'Consider the endomorphism $\mathbb{Q}(X) \to \mathbb{Q}(X)$, $X \mapsto X^2$.'
+	'If this category was core-thin, Galois theory would not exist. Specifically, the conjugation $\mathbb{C} \to \mathbb{C}$, $z \mapsto \overline{z}$ is a non-trivial automorphism.'
 ),
 (
 	'Fld',

databases/catdat/data/004_property-assignments/walking_idempotent.sql

@@ -25,9 +25,9 @@ VALUES
 ),
 (
 	'walking_idempotent',
-	'skeletal',
+	'gaunt',
 	TRUE,
-	'There is just one object.'
+	'This is obvious.'
 ),
 (
     'walking_idempotent',

databases/catdat/data/005_implications/004_morphism-behavior-implications.sql

@@ -126,17 +126,17 @@ VALUES
 	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 every two morphisms $Y \rightrightarrows X$ are the same.',
+	'one-way_implies_core-thin',
+	'["one-way"]',
+	'["core-thin"]',
+	'This is trivial.',
 	FALSE
 ),
 (
-	'one-way_groupoids',
-	'["one-way", "groupoid"]',
+	'core-thin_products_thin',
+	'["core-thin", "binary powers"]',
 	'["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$.',
+	'Let $X$ be any object. The swap $\tau : X \times X \to X \times X$ is an automorphism, hence 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 every two morphisms $Y \rightrightarrows X$ are the same.',
 	FALSE
 ),
 (
@@ -166,4 +166,25 @@ VALUES
 	'["filtered-colimit-stable monomorphisms"]',
 	'This is trivial.',
 	FALSE
+),
+(
+	'thin_groupoids',
+	'["groupoid", "core-thin"]',
+	'["thin"]',
+	'This is trivial.',
+	FALSE
+),
+(
+	'core-hin_quotients',
+	'["core-thin"]',
+	'["quotients of congruences"]',
+	'If $p_1, p_2 : E \rightrightarrows X$ is a congruence, the symmetry morphism $s : E \to E$ is an automorphism of $E$, hence equal to $\mathrm{id}_E$ by assumption. But then $p_1 = p_2 \circ s = p_2$, and simply $\mathrm{id}_X$ is a coequalizer.',
+	FALSE
+),
+(
+	'gaunt_characterization',
+	'["gaunt"]',
+	'["skeletal", "core-thin"]',
+	'This is trivial.',
+	TRUE
 );

databases/catdat/data/005_implications/008_topos-theory-implications.sql

@@ -213,7 +213,7 @@ VALUES
 	'nno_terminal',
 	'["natural numbers object", "strict terminal object"]',
 	'["one-way"]',
-	'By assumption, $z : 1 \to N$ is an isomorphism. Therefore, the terminal object $1$ is a NNO with $z = \mathrm{id}_1$ and $s = \mathrm{id}_1$. This precisely means that for all $f : A \to X$ and $g : X \to X$ there is a unique $\Phi : A \to X$ with $\Phi = f$ and $\Phi = g \circ \Phi$. In other words, we have $f = g \circ f$, and therefore $g = \mathrm{id}_X$ (take $f = \mathrm{id}_X$), which proves the claim. (From here one can <a href="/category-implication/one-way_products_thin">further deduce</a> that the category is thin.)',
+	'By assumption, $z : 1 \to N$ is an isomorphism. Therefore, the terminal object $1$ is a NNO with $z = \mathrm{id}_1$ and $s = \mathrm{id}_1$. This precisely means that for all $f : A \to X$ and $g : X \to X$ there is a unique $\Phi : A \to X$ with $\Phi = f$ and $\Phi = g \circ \Phi$. In other words, we have $f = g \circ f$, and therefore $g = \mathrm{id}_X$ (take $f = \mathrm{id}_X$), which proves the claim. (From here one can further deduce that the category is thin.)',
 	FALSE
 ),
 (

databases/catdat/scripts/expected-data/Ab.json

@@ -151,5 +151,7 @@
 	"countably codistributive": false,
 	"CSP": false,
 	"cofiltered-limit-stable epimorphisms": false,
-	"exact cofiltered limits": false
+	"exact cofiltered limits": false,
+	"gaunt": false,
+	"core-thin": false
 }

databases/catdat/scripts/expected-data/Set.json

@@ -151,5 +151,7 @@
 	"CIP": false,
 	"CSP": false,
 	"cofiltered-limit-stable epimorphisms": false,
-	"exact cofiltered limits": false
+	"exact cofiltered limits": false,
+	"gaunt": false,
+	"core-thin": false
 }

databases/catdat/scripts/expected-data/Top.json

@@ -151,5 +151,7 @@
 	"CIP": false,
 	"CSP": false,
 	"cofiltered-limit-stable epimorphisms": false,
-	"exact cofiltered limits": false
+	"exact cofiltered limits": false,
+	"gaunt": false,
+	"core-thin": false
 }