From 33888decd3f6e49f5e7c0004897f048c9ac7efbc Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 13 Aug 2026 20:09:28 +0200 Subject: [PATCH 1/5] refactor and extend context display on content pages --- src/lib/server/fetchers/content.ts | 72 ++++++++++++------------- src/routes/content/[id]/+page.svelte | 80 +++++++++++++--------------- 2 files changed, 73 insertions(+), 79 deletions(-) diff --git a/src/lib/server/fetchers/content.ts b/src/lib/server/fetchers/content.ts index c70f0754..e5d2429c 100644 --- a/src/lib/server/fetchers/content.ts +++ b/src/lib/server/fetchers/content.ts @@ -1,54 +1,52 @@ -import type { PropertyShort, StructureShort } from '$lib/commons/types' +import type { PropertyShort, StructureShort, StructureType } from '$lib/commons/types' import { db } from '$lib/server/db' 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> = {} - 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> = {} + + for (const { type, ...property } of properties) { + properties_by_type[type] ??= [] + properties_by_type[type].push(property) + } + + const implications = db + .prepare<[string], { id: string; type: StructureType }>( + `SELECT id, type FROM implications + WHERE proof LIKE '%/content/' || ? || '%'` ) .all(content_id) - return { categories, category_properties, category_implications, functors, morphisms } + const implications_by_type: Partial> = {} + + for (const { id, type } of implications) { + implications_by_type[type] ??= [] + implications_by_type[type].push({ id }) + } + + return { structures_by_type, properties_by_type, implications_by_type } } diff --git a/src/routes/content/[id]/+page.svelte b/src/routes/content/[id]/+page.svelte index d397ef18..8c3422d5 100644 --- a/src/routes/content/[id]/+page.svelte +++ b/src/routes/content/[id]/+page.svelte @@ -1,10 +1,18 @@ @@ -13,48 +21,36 @@ {@html data.html} - - -{#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}

Context

- {#if data.categories.length > 0} -

This page is referenced by the following categories.

- - - {/if} - - {#if data.category_properties.length > 0} -

- This page is referenced by the following properties of categories. -

- - - {/if} - - {#if data.category_implications.length > 0} -

This page is referenced by the following implications.

- -
    - {#each data.category_implications as { id }} -
  • - {id} -
    • - {/each} -
- {/if} - - {#if data.functors.length > 0} -

This page is referenced by the following functors.

- - - {/if} - - {#if data.morphisms.length > 0} -

This page is referenced by the following morphisms.

- - - {/if} + {#each STRUCTURE_TYPES as type} + {#if data.structures_by_type?.[type]?.length} +

This page is referenced by the following {PLURALS[type]}.

+ + {/if} + + {#if data.properties_by_type?.[type]?.length} +

+ This page is referenced by the following properties of {PLURALS[type]}. +

+ + + {/if} + + {#if data.implications_by_type?.[type]?.length} +

+ This page is referenced by the following {remove_underscores(type)} implications. +

+ +
    + {#each data.implications_by_type[type] as { id }} + +
  • {id}
    • + {/each} +
+ {/if} + {/each} {/if} From 7a4b47708b1628fa113be9a82dc516369d9e5375 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 13 Aug 2026 20:19:36 +0200 Subject: [PATCH 2/5] improve display of implication references --- src/lib/server/fetchers/content.ts | 31 +++++++++++++++++++++------- src/routes/content/[id]/+page.svelte | 10 +++------ 2 files changed, 27 insertions(+), 14 deletions(-) diff --git a/src/lib/server/fetchers/content.ts b/src/lib/server/fetchers/content.ts index e5d2429c..42c4b4d2 100644 --- a/src/lib/server/fetchers/content.ts +++ b/src/lib/server/fetchers/content.ts @@ -1,5 +1,12 @@ -import type { PropertyShort, StructureShort, StructureType } 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) { const structures = db @@ -35,17 +42,27 @@ export function fetch_content_references(content_id: string) { } const implications = db - .prepare<[string], { id: string; type: StructureType }>( - `SELECT id, type FROM implications - WHERE proof LIKE '%/content/' || ? || '%'` + .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) - const implications_by_type: Partial> = {} + const implications_by_type: Partial> = {} - for (const { id, type } of implications) { + for (const { type, ...rest } of implications) { implications_by_type[type] ??= [] - implications_by_type[type].push({ id }) + implications_by_type[type].push(display_implication(rest)) } return { structures_by_type, properties_by_type, implications_by_type } diff --git a/src/routes/content/[id]/+page.svelte b/src/routes/content/[id]/+page.svelte index 8c3422d5..7296ce4a 100644 --- a/src/routes/content/[id]/+page.svelte +++ b/src/routes/content/[id]/+page.svelte @@ -2,9 +2,10 @@ import MetaData from '$components/MetaData.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 { remove_underscores } from '$shared/utils.js' + import ImplicationList from '$components/ImplicationList.svelte' let { data } = $props() @@ -43,12 +44,7 @@ This page is referenced by the following {remove_underscores(type)} implications.

-
    - {#each data.implications_by_type[type] as { id }} - -
  • {id}
    • - {/each} -
+ {/if} {/each} {/if} From 09798f02ce52c5a9d5750022fa722705586fd1f3 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 13 Aug 2026 21:59:38 +0200 Subject: [PATCH 3/5] fix links --- content/sifted-colimits-in-groupoids.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/sifted-colimits-in-groupoids.md b/content/sifted-colimits-in-groupoids.md index 49d54803..cc6c2530 100644 --- a/content/sifted-colimits-in-groupoids.md +++ b/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_. From c9e97dda73d07c6b36bf9ab5a9361cd7b1c84fab Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 13 Aug 2026 22:03:26 +0200 Subject: [PATCH 4/5] content page headings must be h2 --- content/aleph1-filtered-colimits-in-deloopings.md | 2 +- content/inclusion-functors.md | 2 +- content/thin_extremal_generator.md | 2 +- content/topos-with-generator.md | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/content/aleph1-filtered-colimits-in-deloopings.md b/content/aleph1-filtered-colimits-in-deloopings.md index 8d9d8174..d9ad3311 100644 --- a/content/aleph1-filtered-colimits-in-deloopings.md +++ b/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). diff --git a/content/inclusion-functors.md b/content/inclusion-functors.md index ed67b1b9..8cd2c071 100644 --- a/content/inclusion-functors.md +++ b/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. diff --git a/content/thin_extremal_generator.md b/content/thin_extremal_generator.md index efdc3f0b..f1a47f1c 100644 --- a/content/thin_extremal_generator.md +++ b/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. diff --git a/content/topos-with-generator.md b/content/topos-with-generator.md index 841b8244..475336ce 100644 --- a/content/topos-with-generator.md +++ b/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. From a433a195e8f76a7e2a4fb8118784594cfd663808 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 13 Aug 2026 22:27:31 +0200 Subject: [PATCH 5/5] the result on thin algebraic categories is deprecated --- content/thin_algebraic_categories.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/content/thin_algebraic_categories.md b/content/thin_algebraic_categories.md index d707a87a..b57fb19c 100644 --- a/content/thin_algebraic_categories.md +++ b/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 + + ::: 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$. $\square$ + +Remark: Another proof is possible by using the Lemma [here](/content/thin_extremal_generator).