diff --git a/database/data/categories/FreeAb.yaml b/database/data/categories/FreeAb.yaml index 475dcb2f..ab65e1fd 100644 --- a/database/data/categories/FreeAb.yaml +++ b/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. diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index d11008fb..6dfc6a01 100644 --- a/src/lib/commons/types.ts +++ b/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 = { diff --git a/src/lib/server/fetchers/category.ts b/src/lib/server/fetchers/category.ts index 175c1f0d..4d9ff7bd 100644 --- a/src/lib/server/fetchers/category.ts +++ b/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 } } diff --git a/src/pages/CategoryDetailPage.svelte b/src/pages/CategoryDetailPage.svelte index 8a5047c0..c1a98c32 100644 --- a/src/pages/CategoryDetailPage.svelte +++ b/src/pages/CategoryDetailPage.svelte @@ -59,18 +59,35 @@ {/snippet} {#snippet footer()} - {#if data.functors.length} + {#if data.stored_functors.length}

Functors

- {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}.

- + +
+ {/if} + + {#if data.stored_morphisms.length} +
+

Morphisms

+ +

+ The database has stored + {pluralize(data.stored_morphisms.length, { + one: '{count} morphism', + other: '{count} morphisms' + })} + in the {data.structure.name}. +

+
{/if} {/snippet} diff --git a/tests/categories.spec.ts b/tests/categories.spec.ts index 0d0defe9..1b1bfa01 100644 --- a/tests/categories.spec.ts +++ b/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() +})