Improve context section on content pages

content/aleph1-filtered-colimits-in-deloopings.md

@@ -3,7 +3,7 @@ title: ℵ₁-filtered colimits in deloopings
 description: We give a detailed proof that the delooping of the monoid of natural numbers, and likewise the delooping of the large monoid of ordinal numbers, has colimits indexed by ℵ₁-filtered categories.
 ---
 
-# $\aleph_1$-filtered colimits in deloopings
+## $\aleph_1$-filtered colimits in deloopings
 
 Every (possibly large) monoid $M$ induces a category $BM$ with just one object. We will show that this category has $\aleph_1$-filtered colimits in the cases $M = \IN$ and $M = \On$ (both respect to addition).
 

content/inclusion-functors.md

@@ -3,7 +3,7 @@ title: Inclusion functors
 description: We gather results about inclusion functors
 ---
 
-# Inclusion functors
+## Inclusion functors
 
 ::: Lemma 1
 Let $\D$ be category that has an extremal cogenerator $Q$. Let $\C \subseteq \D$ be a full subcategory that contains $Q$. Then the inclusion functor $U : \C \hookrightarrow \D$ preserves all colimits that exist in $\C$ and in $\D$. In particular, if $\D$ is cocomplete, $U$ is cocontinuous.

content/sifted-colimits-in-groupoids.md

@@ -5,7 +5,7 @@ description: A description of sifted colimits in groupoids, yielding a proof tha
 
 ## Sifted colimits in groupoids
 
-While the combination of [this result](http://localhost:5173/category-implication/groupoid_consequence) and [this result](http://localhost:5173/category-implication/sifted_colimits_criterion) already implies that groupoids have sifted colimits, we can make these colimits more explicit and also prove their existence without using any non-trivial theorem. We also do this in a more general setting.
+While the combination of [this result](/category-implication/groupoid_consequence) and [this result](/category-implication/sifted_colimits_criterion) already implies that groupoids have sifted colimits, we can make these colimits more explicit and also prove their existence without using any non-trivial theorem. We also do this in a more general setting.
 
 Let $D : \I \to \C$ be a [sifted](/category-property/sifted) diagram in a category and $i_0 \in \I$. We call $D$ _constant after_ $i_0$ when for all morphisms $i_0 \to i$ the morphism $D(i_0) \to D(i)$ is an isomorphism. Of course, in a groupoid, this is satisfied for every $i_0 \in \I$. If such an object $i_0$ exists, we call $D$ _eventually constant_.
 

content/thin_algebraic_categories.md

@@ -5,9 +5,17 @@ description: A proof that the only thin algebraic categories are the terminal an
 
 ## Algebraic categories are "never" thin
 
+<!--
+TODO: Currently, this lemma is not used anymore
+(because of the results on extremal generators).
+Evaluate later if we want to remove it.
+-->
+
 ::: Lemma
 Let $\C$ be a [thin](/category-property/thin) and [one-sorted finitary algebraic](/category-property/one-sorted_finitary_algebraic) category. Then $\C \simeq 1$ or $\C \simeq I$, where $I$ is the walking morphism.
 :::
 
 _Proof._
 Let $F : \Set \to \C$ denote the free algebra functor. Every object $A \in \C$ admits a regular epimorphism $F(X) \twoheadrightarrow A$ for some set $X$. But since $\C$ is thin, every regular epimorphism must be an isomorphism. Thus, $A \cong F(X)$. 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 $\C$ is thin). If $F(1) \cong 0$, then every object is isomorphic to the initial object $0$, and hence $\C$ is trivial. If not, then $\C$ has exactly two objects up to isomorphism, $0$ and $F(1)$, there is a morphism $0 \to F(1)$, but no morphism $F(1) \to 0$. Since $\C$ is thin, we conclude $\C \simeq I$. <span class="qed">$\square$</span>
+
+Remark: Another proof is possible by using the Lemma [here](/content/thin_extremal_generator).

content/thin_extremal_generator.md

@@ -3,7 +3,7 @@ title: Thin Category with an Extremal Generator
 description: A result restricting which thin categories can have an extremal generator
 ---
 
-# Thin Category with an Extremal Generator
+## Thin Category with an Extremal Generator
 
 ::: Lemma
 Suppose $G$ is an object of a thin category. Then $G$ is an extremal generator if and only if for every object $X$, either $X \cong G$ or every morphism with codomain $X$ is an isomorphism.

content/topos-with-generator.md

@@ -3,7 +3,7 @@ title: Topos with a Generator
 description: An elementary topos with a generator has at most two subterminal objects
 ---
 
-# Topos with a Generator
+## Topos with a Generator
 
 ::: Lemma
 Suppose a category is coregular, and it has disjoint finite coproducts, a terminal object, and a generator. Then every regular subterminal object (i.e. an object $X$ such that the unique morphism $X \to 1$ is a regular monomorphism) is either initial or terminal.

src/lib/server/fetchers/content.ts

@@ -1,54 +1,69 @@
-import type { PropertyShort, StructureShort } from '$lib/commons/types'
+import type {
+	ImplicationDB,
+	ImplicationDisplay,
+	PropertyShort,
+	StructureShort,
+	StructureType
+} from '$lib/commons/types'
 import { db } from '$lib/server/db'
+import { display_implication } from '../transforms'
 
 export function fetch_content_references(content_id: string) {
-	// TODO: make this more systematic
-
-	const categories = db
-		.prepare<[string], StructureShort>(
-			`SELECT DISTINCT s.id, s.name
+	const structures = db
+		.prepare<[string], StructureShort & { type: StructureType }>(
+			`SELECT DISTINCT s.id, s.name, s.type
 	        FROM property_assignments pa
 	        INNER JOIN structures s ON s.id = pa.structure_id
-	        WHERE pa.type = 'category'
-	        AND pa.proof LIKE '%/content/' || ? || '%'`
+	        WHERE pa.proof LIKE '%/content/' || ? || '%'
+			ORDER BY s.name`
 		)
 		.all(content_id)
 
-	const functors = db
-		.prepare<[string], StructureShort>(
-			`SELECT DISTINCT s.id, s.name
-	        FROM property_assignments pa
-	        INNER JOIN structures s ON s.id = pa.structure_id
-	        WHERE pa.type = 'functor'
-	        AND pa.proof LIKE '%/content/' || ? || '%'`
-		)
-		.all(content_id)
+	const structures_by_type: Partial<Record<StructureType, StructureShort[]>> = {}
 
-	const morphisms = db
-		.prepare<[string], StructureShort>(
-			`SELECT DISTINCT s.id, s.name
-	        FROM property_assignments pa
-	        INNER JOIN structures s ON s.id = pa.structure_id
-	        WHERE pa.type = 'morphism'
-	        AND pa.proof LIKE '%/content/' || ? || '%'`
-		)
-		.all(content_id)
+	for (const { type, ...structure } of structures) {
+		structures_by_type[type] ??= []
+		structures_by_type[type].push(structure)
+	}
 
-	const category_properties = db
-		.prepare<[string], PropertyShort>(
-			`SELECT id, relation FROM properties
-            WHERE type = 'category'
-            AND description LIKE '%/content/' || ? || '%'`
+	const properties = db
+		.prepare<[string], PropertyShort & { type: StructureType }>(
+			`SELECT id, relation, type FROM properties
+            WHERE description LIKE '%/content/' || ? || '%'
+			ORDER BY lower(id)`
 		)
 		.all(content_id)
 
-	const category_implications = db
-		.prepare<[string], { id: string }>(
-			`SELECT id FROM implications
-            WHERE type = 'category'
-            AND proof LIKE '%/content/' || ? || '%'`
+	const properties_by_type: Partial<Record<StructureType, PropertyShort[]>> = {}
+
+	for (const { type, ...property } of properties) {
+		properties_by_type[type] ??= []
+		properties_by_type[type].push(property)
+	}
+
+	const implications = db
+		.prepare<[string], ImplicationDB & { type: StructureType }>(
+			`SELECT
+				id,
+				type,
+				is_equivalence,
+				is_deduced,
+				proof,
+				assumptions,
+				conclusions,
+				mapped_assumptions
+			FROM implications_view
+			WHERE proof LIKE '%/content/' || ? || '%'
+			ORDER BY lower(assumptions) || ' ' || lower(conclusions)`
 		)
 		.all(content_id)
 
-	return { categories, category_properties, category_implications, functors, morphisms }
+	const implications_by_type: Partial<Record<StructureType, ImplicationDisplay[]>> = {}
+
+	for (const { type, ...rest } of implications) {
+		implications_by_type[type] ??= []
+		implications_by_type[type].push(display_implication(rest))
+	}
+
+	return { structures_by_type, properties_by_type, implications_by_type }
 }

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

@@ -1,10 +1,19 @@
 <script lang="ts">
-	import StructureList from '$components/StructureList.svelte'
 	import MetaData from '$components/MetaData.svelte'
-	import PropertyList from '$components/PropertyList.svelte'
 	import SuggestionForm from '$components/SuggestionForm.svelte'
+	import { PLURALS, STRUCTURE_TYPES } from '$shared/config'
+	import { remove_underscores } from '$shared/utils'
+	import StructureList from '$components/StructureList.svelte'
+	import PropertyList from '$components/PropertyList.svelte'
+	import ImplicationList from '$components/ImplicationList.svelte'
 
 	let { data } = $props()
+
+	let has_context = $derived(
+		Object.keys(data.structures_by_type).length ||
+			Object.keys(data.properties_by_type).length ||
+			Object.keys(data.implications_by_type).length
+	)
 </script>
 
 <MetaData title={data.meta_data.title} description={data.meta_data.description} />
@@ -13,48 +22,31 @@
 	{@html data.html}
 </div>
 
-<!-- TODO: make this more systematic -->
-
-{#if data.categories.length > 0 || data.category_properties.length > 0 || data.category_implications.length > 0 || data.functors.length > 0 || data.morphisms.length > 0}
+{#if has_context}
 	<h3>Context</h3>
 
-	{#if data.categories.length > 0}
-		<p class="hint">This page is referenced by the following categories.</p>
-
-		<StructureList structures={data.categories} type="category" />
-	{/if}
-
-	{#if data.category_properties.length > 0}
-		<p class="hint">
-			This page is referenced by the following properties of categories.
-		</p>
-
-		<PropertyList properties={data.category_properties} type="category" />
-	{/if}
-
-	{#if data.category_implications.length > 0}
-		<p class="hint">This page is referenced by the following implications.</p>
-
-		<ul class="with-margins">
-			{#each data.category_implications as { id }}
-				<li>
-					<a href="/category-implication/{id}">{id}</a>
-				</li>
-			{/each}
-		</ul>
-	{/if}
+	{#each STRUCTURE_TYPES as type}
+		{#if data.structures_by_type?.[type]?.length}
+			<p class="hint">This page is referenced by the following {PLURALS[type]}.</p>
+			<StructureList structures={data.structures_by_type[type]} {type} />
+		{/if}
 
-	{#if data.functors.length > 0}
-		<p class="hint">This page is referenced by the following functors.</p>
+		{#if data.properties_by_type?.[type]?.length}
+			<p class="hint">
+				This page is referenced by the following properties of {PLURALS[type]}.
+			</p>
 
-		<StructureList structures={data.functors} type="functor" />
-	{/if}
+			<PropertyList properties={data.properties_by_type[type]} {type} />
+		{/if}
 
-	{#if data.morphisms.length > 0}
-		<p class="hint">This page is referenced by the following morphisms.</p>
+		{#if data.implications_by_type?.[type]?.length}
+			<p class="hint">
+				This page is referenced by the following {remove_underscores(type)} implications.
+			</p>
 
-		<StructureList structures={data.morphisms} type="morphism" />
-	{/if}
+			<ImplicationList implications={data.implications_by_type[type]} {type} />
+		{/if}
+	{/each}
 {/if}
 
 <SuggestionForm />