Show functors on category detail page, and improve functor notation

databases/catdat/data/functors/power_set_contravariant.yaml

@@ -1,9 +1,9 @@
 id: power_set_contravariant
 name: contravariant power set functor
-notation: $\Hom(-,2)$
+notation: $P_{\forall}$
 source: Set_op
 target: Set
-description: 'This functor maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced preimage operator $f^* : P(Y) \to P(X)$. It is isomorphic to the representable functor $\Hom(-,2) : \Set^{\op} \to \Set$.'
+description: 'This functor $P_{\forall}$ maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced preimage operator $f^* : P(Y) \to P(X)$.'
 nlab_link: https://ncatlab.org/nlab/show/power+set
 
 tags:
@@ -26,13 +26,13 @@ satisfied_properties:
 
   - property: right adjoint
     proof: >-
-      The functor $P : \Set^{\op} \to \Set$ is right adjoint to $P^{\op} : \Set \to \Set^{\op}$ since
+      The functor $P_{\forall} : \Set^{\op} \to \Set$ is right adjoint to $P_{\forall}^{\op} : \Set \to \Set^{\op}$ since
       $$\Hom_{\Set}(X,P(Y)) \cong P(X \times Y) \cong \Hom_{\Set}(Y,P(X)) = \Hom_{\Set^{\op}}(P(X),Y).$$
     check_redundancy: false
 
   - property: preserves reflexive coequalizers
     proof: >-
-      This is contained in the proof of Theorem 2.2.7 (monadicity of $P$ for an elementary topos) in <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, but we include a direct proof here for the sake of completeness, and also since we want the system to deduce monadicity automatically.
+      This is contained in the proof of Theorem 2.2.7 (monadicity of $P_{\forall}$ for an elementary topos) in <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, but we include a direct proof here for the sake of completeness, and also since we want the system to deduce monadicity automatically.
 
       Let $f,g : X \rightrightarrows Y$ be two maps with a common retraction $r : Y \to X$, i.e. $rf = rg = \id_X$. Let $i : E \hookrightarrow X$ be their equalizer. We need to show that $i^* : P(X) \to P(E)$ is a coequalizer of $f^*,g^* : P(Y) \rightrightarrows P(X)$. First, $i^*$ is surjective since $i$ is injective, which implies that $A = i^*(i_*(A))$ for all $A \subseteq E$. Hence, $i^*$ is the quotient of $P(X)$ by the equivalence relation $\sim_1$ defined by $A \sim_1 B \iff i^*(A) = i^*(B)$, i.e. $A \cap E = B \cap E$. The coequalizer of $f^*,g^*$ is the quotient of $P(X)$ by the smallest equivalence relation $\sim_2$ satisfying $f^*(C) \sim_2 g^*(C)$ for all $C \subseteq Y$. We need to show that these equivalence relations coincide.
 

databases/catdat/data/functors/power_set_covariant.yaml

@@ -1,9 +1,9 @@
 id: power_set_covariant
 name: covariant power set functor
-notation: $P$
+notation: $P_{\exists}$
 source: Set
 target: Set
-description: 'This functor maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced image operator $f_* : P(X) \to P(Y)$.'
+description: 'This functor $P_{\exists}$ maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced image operator $f_* : P(X) \to P(Y)$.'
 nlab_link: https://ncatlab.org/nlab/show/power+set
 
 tags:
@@ -17,7 +17,7 @@ satisfied_properties:
     proof: 'Let $f,g : X \rightrightarrows Y$ be two maps with $f_* = g_* : P(X) \rightrightarrows P(Y)$. Then $\{f(x)\} = f_*(\{x\}) = g_*(\{x\}) = \{g(x)\}$ and hence $f(x) = g(x)$ for all $x \in X$.'
 
   - property: preserves epimorphisms
-    proof: 'If $f : X \to Y$ is surjective, then $f_* \circ f^* = \id_{P(Y)}$, so that $f^*$ is surjective.'
+    proof: 'If $f : X \to Y$ is surjective, then $f_* \circ f^* = \id_{P(Y)}$, so that $f_*$ is surjective.'
 
   - property: preserves monomorphisms
     proof: 'If $f : X \to Y$ is injective, then $f^* \circ f_* = \id_{P(X)}$, so that $f_*$ is injective.'
@@ -49,13 +49,13 @@ unsatisfied_properties:
   - property: preserves reflexive coequalizers
     proof: >-
       Consider the two maps $f,g : \IN \times \{0,1\} \rightrightarrows \IN$ defined by $f(n,i)=n$, $g(n,0)=n$, and $g(n,1)=n+1$. They form a reflexive pair with common section $n \mapsto (n,0)$. Their coequalizer is the quotient of $\IN$ by the equivalence relation generated by $n \sim n+1$, which collapses everything to a single point. Thus, the unique map $p : \IN \to \{\ast\}$ is a coequalizer of $f,g$.
-      The induced map $P(p) : P(\IN) \to P(\{\ast\}) = \{\varnothing,\{\ast\}\}$ sends $\varnothing$ to $\varnothing$ and every non-empty subset to $\{\ast\}$. In particular, all non-empty subsets of $\IN$ have the same image.
+      The induced map $p_* : P(\IN) \to P(\{\ast\}) = \{\varnothing,\{\ast\}\}$ sends $\varnothing$ to $\varnothing$ and every non-empty subset to $\{\ast\}$. In particular, all non-empty subsets of $\IN$ have the same image.
 
-      Next, we compute the coequalizer of $P(f),P(g) : P(\IN \times \{0,1\}) \rightrightarrows P(\IN)$. Identify $P(\IN \times \{0,1\})$ with $P(\IN) \times P(\IN)$. Under this identification, $P(f)$ sends a pair of subsets $(A,B)$ to $A \cup B$, while $P(g)$ sends it to $A \cup (B+1)$.
+      Next, we compute the coequalizer of $f_*, g_* : P(\IN \times \{0,1\}) \rightrightarrows P(\IN)$. Identify $P(\IN \times \{0,1\})$ with $P(\IN) \times P(\IN)$. Under this identification, $f_*$ sends a pair of subsets $(A,B)$ to $A \cup B$, while $g_*$ sends it to $A \cup (B+1)$.
 
       The coequalizer is the quotient of $P(\IN)$ by the equivalence relation generated by
       $$A \cup B \sim A \cup (B+1).$$
-      This generated equivalence relation is the transitive closure of the symmetric closure. From this it follows that a finite subset is equivalent only to finite subsets. In particular, $\{0\}$ and $\IN$ are not equivalent, i.e. they do not have the same image in the coequalizer. Therefore, $P(p)$ cannot be the coequalizer.
+      This generated equivalence relation is the transitive closure of the symmetric closure. From this it follows that a finite subset is equivalent only to finite subsets. In particular, $\{0\}$ and $\IN$ are not equivalent, i.e. they do not have the same image in the coequalizer. Therefore, $p_*$ cannot be the coequalizer.
 
   - property: preserves equalizers
     proof: 'Any pair of distinct surjective maps $f,g : X \rightrightarrows Y$ provides a counterexample: Their equalizer $E$ is a proper subset of $X$, so that $P(E)$ cannot contain $X$. But $f_*(X) = Y = g_*(X)$ shows that $X$ is contained in the equalizer of $f_*,g_* : P(X) \rightrightarrows P(Y)$.'

src/lib/server/fetchers/category.ts

@@ -10,42 +10,51 @@ import { error } from '@sveltejs/kit'
 
 export function fetch_category(id: string) {
 	const { results, err } = batch<
-		[CategorySpecificDisplay, SpecialObject, SpecialMorphism]
+		[CategorySpecificDisplay, SpecialObject, SpecialMorphism, StructureShort]
 	>([
 		// specific information for the category
 		sql`
-                SELECT c.objects, c.morphisms
-                FROM categories c
-                WHERE c.id = ${id}
-            `,
+			SELECT c.objects, c.morphisms
+			FROM categories c
+			WHERE c.id = ${id}
+		`,
 		// special objects
 		sql`
-                SELECT s.type, s.description
-                FROM special_objects s
-                INNER JOIN special_object_types t ON t.type = s.type
-                WHERE s.category_id = ${id}
-                ORDER BY t.id
-            `,
+			SELECT s.type, s.description
+			FROM special_objects s
+			INNER JOIN special_object_types t ON t.type = s.type
+			WHERE s.category_id = ${id}
+			ORDER BY t.id
+		`,
 		// special morphisms
 		sql`
-                SELECT t.type, s.description, s.proof
-                FROM special_morphism_types t
-                LEFT JOIN special_morphisms s
-                    ON s.type = t.type AND s.category_id = ${id}
-                ORDER BY t.id
-            `,
+			SELECT t.type, s.description, s.proof
+			FROM special_morphism_types t
+			LEFT JOIN special_morphisms s
+				ON s.type = t.type AND s.category_id = ${id}
+			ORDER BY t.id
+		`,
+		// functors whose source or target is the current category
+		sql`
+			SELECT f.id, s.name
+			FROM functors f
+			INNER JOIN structures s ON s.id = f.id
+			WHERE f.source = ${id} OR f.target = ${id}
+			ORDER BY lower(s.name)
+		`,
 	])
 
 	if (err) error(500, 'Could not load category')
 
-	const [categories, special_objects, special_morphisms] = results
+	const [categories, special_objects, special_morphisms, functors] = results
 
 	if (!categories.length) error(404, `Could not find category with ID '${id}'`)
 
 	return {
 		...categories[0],
 		special_objects,
 		special_morphisms,
+		functors,
 	}
 }
 

src/lib/server/utils.ts

@@ -34,3 +34,11 @@ export function cache_page(event: RequestEvent) {
 	// shared cache for 30min
 	event.setHeaders({ 'cache-control': 'public, max-age=0, s-maxage=1800' })
 }
+
+export function strip_math(s: string) {
+	return s.replaceAll('$', '')
+}
+
+export function add_math(s: string) {
+	return `$${s}$`
+}

src/pages/StructureDetailPage.svelte

@@ -30,6 +30,7 @@
 		comments: CommentObject[]
 		definition?: Snippet
 		specials?: Snippet
+		footer?: Snippet
 	}
 
 	let {
@@ -45,6 +46,7 @@
 		comments,
 		definition,
 		specials,
+		footer,
 	}: Props = $props()
 </script>
 
@@ -118,6 +120,8 @@
 
 <CommentList {comments} />
 
+{@render footer?.()}
+
 <SuggestionForm />
 
 <style>

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

@@ -3,6 +3,8 @@
 	import { faQuestion } from '@fortawesome/free-solid-svg-icons'
 	import Fa from 'svelte-fa'
 	import StructureDetailPage from '$pages/StructureDetailPage.svelte'
+	import StructureList from '$components/StructureList.svelte'
+	import { pluralize } from '$lib/client/utils.js'
 
 	let { data } = $props()
 </script>
@@ -52,4 +54,21 @@
 			</ul>
 		</section>
 	{/snippet}
+
+	{#snippet footer()}
+		{#if data.category.functors.length}
+			<section>
+				<h3>Functors</h3>
+
+				<p class="hint">
+					{pluralize(data.category.functors.length, {
+						one: 'There is 1 functor',
+						other: 'There are {count} functors',
+					})}
+					whose source or target is the {data.structure.name}.
+				</p>
+				<StructureList structures={data.category.functors} type="functor" />
+			</section>
+		{/if}
+	{/snippet}
 </StructureDetailPage>

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

@@ -1,6 +1,7 @@
 import { fetch_functor } from '$lib/server/fetchers/functor'
 import { fetch_structure } from '$lib/server/fetchers/structure'
 import { render_nested_formulas } from '$lib/server/formulas'
+import { add_math, strip_math } from '$lib/server/utils'
 
 export const load = (event) => {
 	const id = event.params.id
@@ -19,6 +20,11 @@ export const load = (event) => {
 
 	const functor = fetch_functor(id)
 
+	// functors are notated as F : C -> D
+	structure.notation = add_math(
+		`${strip_math(structure.notation)}: ${strip_math(functor.source_notation)} \\to ${strip_math(functor.target_notation)}`,
+	)
+
 	return render_nested_formulas({
 		structure,
 		functor,