Support comments on undecidable properties

databases/catdat/data/000_setup/001_clear.sql

@@ -36,4 +36,6 @@ DELETE FROM functor_implication_source_assumptions;
 DELETE FROM functor_implication_target_assumptions;
 DELETE FROM functor_implications;
 
+DELETE FROM category_property_comments;
+
 PRAGMA foreign_keys = ON;

databases/catdat/data/001_categories/300_comments.sql

@@ -40,10 +40,6 @@ VALUES
     'Sh(X,Ab)',
     'It is likely that neither of the currently remaining unknown properties (finitary algebraic, locally ℵ₁-presentable, CSP, etc.) are satisfied for a <i>generic</i> space $X$, but we need to make this precise by adding additional requirements to $X$. Maybe we need to create separate entries for specific spaces $X$.'
 ),
-(
-    'M-Set',
-    'If this category is semi-strongly connected depends on the choice of $M$. For $M = 1$ it is, for $M = \mathbb{Z}$ it is not. In general, if $G$ is a group, then $G{-}\mathbf{Set}$ is semi-strongly connected if and only if for all subgroups $H,K \subseteq G$, $H$ is subconjugated to $K$ or $K$ is subconjugated to $H$. If $G$ is abelian, this means that the poset of subgroups is linear, in which case $G$ is either isomorphic to $\mathbb{Z}/p^n$ or to $\mathbb{Z}/p^{\infty}$ for a prime $p$. See also <a href="https://math.stackexchange.com/questions/5129804" target="_blank">MSE/5129804</a>.'
-),
 (
     'Meas',
     'The thread <a href="https://math.stackexchange.com/questions/5024471/">MSE/5024471</a> asks for the finitely presentable objects of this category.'

databases/catdat/data/003_category-property-assignments/FreeAb.sql

@@ -84,4 +84,12 @@ VALUES
 	'sequential colimits',
 	FALSE,
 	'See <a href="https://mathoverflow.net/questions/509715" target="_blank">MO/509715</a>.'
+);
+
+INSERT INTO category_property_comments (category_id, property_id, comment)
+VALUES
+(
+    'FreeAb',
+    'accessible',
+    'The question if this category is accessible is undecidable in ZFC. See <a href="https://math.stackexchange.com/questions/720885" target="_blank">MSE/720885</a>.'
 );

databases/catdat/data/003_category-property-assignments/M-Set.sql

@@ -41,3 +41,11 @@ VALUES
 	FALSE,
 	'We know that $\mathbf{Set}$ does not have this property. Now use the contrapositive of the dual of <a href="/lemma/filtered-monos">this lemma</a> applied to the functor $\mathbf{Set} \to M{-}\mathbf{Set}$ that equips a set with the trivial $M$-action.'
 );
+
+INSERT INTO category_property_comments (category_id, property_id, comment)
+VALUES
+(
+    'M-Set',
+	'semi-strongly connected',
+    'If this category is semi-strongly connected depends on the choice of $M$. For $M = 1$ it is, for $M = \mathbb{Z}$ it is not. In general, if $G$ is a group, then $G{-}\mathbf{Set}$ is semi-strongly connected if and only if for all subgroups $H,K \subseteq G$, $H$ is subconjugated to $K$ or $K$ is subconjugated to $H$. If $G$ is abelian, this means that the poset of subgroups is linear, in which case $G$ is either isomorphic to $\mathbb{Z}/p^n$ or to $\mathbb{Z}/p^{\infty}$ for a prime $p$. See also <a href="https://math.stackexchange.com/questions/5129804" target="_blank">MSE/5129804</a>.'
+);

databases/catdat/migrations/015_property_comments.sql

@@ -0,0 +1,8 @@
+CREATE TABLE category_property_comments (
+    category_id TEXT NOT NULL,
+    property_id TEXT NOT NULL,
+    comment TEXT NOT NULL,
+    PRIMARY KEY (category_id, property_id),
+    FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE,
+    FOREIGN KEY (property_id) REFERENCES category_properties (id) ON DELETE CASCADE
+);

src/components/PropertyList.svelte

@@ -9,16 +9,17 @@
 			reason?: string | null
 		}[]
 		type?: 'category' | 'functor'
+		reason_heading?: string
 	}
 
-	let { properties, type = 'category' }: Props = $props()
+	let { properties, type = 'category', reason_heading }: Props = $props()
 </script>
 
 {#if properties.length}
 	<ul>
 		{#each properties as { id, relation, reason }}
 			<li>
-				<TextWithReason {reason}>
+				<TextWithReason {reason} heading={reason_heading}>
 					{relation}
 					<a href={get_property_url(id, type)}>{id}</a>
 				</TextWithReason>

src/components/TextWithReason.svelte

@@ -7,17 +7,18 @@
 	type Props = {
 		children: Snippet
 		reason?: string | null
+		heading?: string
 	}
 
-	let { children, reason }: Props = $props()
+	let { children, reason, heading = 'Reason' }: Props = $props()
 
 	const id = $props.id()
 
 	function show_reason(e: MouseEvent) {
 		e.stopPropagation()
 		show_popup({
 			id,
-			heading: 'Reason',
+			heading,
 			text: reason!,
 		})
 	}

src/routes/category/[id]/+page.server.ts

@@ -88,8 +88,11 @@ export const load = async (event) => {
 		sql`
 			SELECT
 				p.id,
-				p.relation
+				p.relation,
+				c.comment as reason
 			FROM category_properties p
+			LEFT JOIN category_property_comments c
+			ON c.category_id = ${id} AND c.property_id = p.id
 			WHERE NOT EXISTS (
 				SELECT 1 FROM category_property_assignments
 				WHERE category_id = ${id} AND property_id = p.id

src/routes/category/[id]/+page.svelte

@@ -149,7 +149,7 @@
 		</p>
 	{/if}
 
-	<PropertyList properties={data.unknown_properties} />
+	<PropertyList properties={data.unknown_properties} reason_heading="Comment" />
 </section>
 
 <section>