Show stored morphisms on category detail page

database/data/categories/FreeAb.yaml

@@ -82,8 +82,8 @@ special_morphisms:
     description: 'homomorphisms $f : A \to B$ with the property that $f(A)$ is not contained in a proper direct summand of $B$'
     proof: 'Let $f : A \to B$ be a morphism of free abelian groups such that $f(A)$ is not contained in a proper direct summand of $B$. Then $f$ is an epimorphism: If $t : B \to C$ is a morphism with $t \circ f = 0$, we want to show $t = 0$. Since the image of $t$ is free abelian (as a subgroup of $B$), we may assume that $t$ is surjective. Since $C$ is free, $t$ splits, so its kernel $K$ is a direct summand of $B$ (Splitting Lemma). It contains $f(A)$ because of $t \circ f = 0$. By assumption, $K = B$, so that $t = 0$. Conversely, assume that $f : A \to B$ is an epimorphism, and that $f(A)$ is contained in a direct summand $K$ of $B$. Let $L$ be a complement of $B$ (which is free abelian) and let $p : B \to L$ be the projection. Then $t \circ f = 0$, so $t = 0$. But then $L = 0$, which means $K = B$.'
   regular monomorphisms:
-    description: 'injective homomorphisms $f : A \to B$ with the property that $B/f(A)$ is free abelian'
-    proof: 'If $f$ is injective and $B/f(A)$ is free abelian, then $f$ is a kernel of the projection $B \to B/f(A)$. Conversely, if $f$ is a kernel of some homomorphism $g : B \to C$ of free abelian groups, by applying $\Hom(\IZ,-)$ we see that it is also the kernel in $\Ab$. In particular, $f$ is injective, and the quotient $B/f(A)$ embeds into $C$ and is therefore free abelian.'
+    description: 'injective homomorphisms $f : A \to B$ with the property that $B/f(A)$ is free abelian (which are automatically split monomorphisms)'
+    proof: 'If $f$ is injective and $B/f(A)$ is free abelian, then $f$ is a kernel of the projection $B \to B/f(A)$. Since $B/f(A)$ is free abelian, the sequence $0 \to A \to B \to B/f(A) \to 0$ splits, so by the splitting lemma, $f$ is a split monomorphism. Conversely, if $f$ is a kernel of some homomorphism $g : B \to C$ of free abelian groups, by applying $\Hom(\IZ,-)$ we see that it is also the kernel in $\Ab$. In particular, $f$ is injective, and the quotient $B/f(A)$ embeds into $C$ and is therefore free abelian.'
   regular epimorphisms:
-    description: surjective homomorphisms
-    proof: See the proof above that $\FreeAb$ is regular.
+    description: surjective homomorphisms (which are automatically split epimorphisms)
+    proof: Regular homomorphisms coincide with surjective homomorphisms by the proof above that $\FreeAb$ is regular. They are automatically split because their codomain is free abelian.

src/lib/commons/types.ts

@@ -134,7 +134,8 @@ export type CategorySpecificDisplay = {
 	morphisms: string
 	special_objects: SpecialObject[]
 	special_morphisms: SpecialMorphism[]
-	functors: StructureShort[]
+	stored_functors: StructureShort[]
+	stored_morphisms: StructureShort[]
 }
 
 export type FunctorSpecificDisplay = {

src/lib/server/fetchers/category.ts

@@ -39,7 +39,7 @@ export function fetch_category(id: string) {
 		)
 		.all(id)
 
-	const functors = db
+	const stored_functors = db
 		.prepare<[string, string], StructureShort>(
 			`SELECT f.id, s.name
 			FROM functors f
@@ -49,12 +49,23 @@ export function fetch_category(id: string) {
 		)
 		.all(id, id)
 
+	const stored_morphisms = db
+		.prepare<[string], StructureShort>(
+			`SELECT m.id, s.name
+			FROM morphisms m
+			INNER JOIN structures s ON s.id = m.id
+			WHERE m.category = ?
+			ORDER BY lower(s.name)`
+		)
+		.all(id)
+
 	return {
 		type: 'category' as const,
 		...category,
 		special_objects,
 		special_morphisms,
-		functors
+		stored_functors,
+		stored_morphisms
 	}
 }
 

src/pages/CategoryDetailPage.svelte

@@ -59,18 +59,35 @@
 	{/snippet}
 
 	{#snippet footer()}
-		{#if data.functors.length}
+		{#if data.stored_functors.length}
 			<section>
 				<h3>Functors</h3>
 
 				<p class="hint">
-					{pluralize(data.functors.length, {
-						one: 'There is 1 functor',
-						other: 'There are {count} functors'
+					The database has stored
+					{pluralize(data.stored_functors.length, {
+						one: '{count} functor',
+						other: '{count} functors'
 					})}
 					whose (co-)domain is the {data.structure.name}.
 				</p>
-				<StructureList structures={data.functors} type="functor" />
+				<StructureList structures={data.stored_functors} type="functor" />
+			</section>
+		{/if}
+
+		{#if data.stored_morphisms.length}
+			<section>
+				<h3>Morphisms</h3>
+
+				<p class="hint">
+					The database has stored
+					{pluralize(data.stored_morphisms.length, {
+						one: '{count} morphism',
+						other: '{count} morphisms'
+					})}
+					in the {data.structure.name}.
+				</p>
+				<StructureList structures={data.stored_morphisms} type="morphism" />
 			</section>
 		{/if}
 	{/snippet}

tests/categories.spec.ts

@@ -312,3 +312,21 @@ test('user sees functors associated with the given category', async ({ page }) =
 		})
 	).toBeVisible()
 })
+
+test('user sees morphisms stored for the given category', async ({ page }) => {
+	await page.goto('/category/Grp', { waitUntil: 'networkidle' })
+
+	await expect(
+		page.getByRole('link', {
+			name: 'embedding of A3 into S3',
+			exact: true
+		})
+	).toBeVisible()
+
+	await expect(
+		page.getByRole('link', {
+			name: 'identity map of a group',
+			exact: true
+		})
+	).toBeVisible()
+})