From 95c7ca1d07e99a09dd325bc2b83df3249d15f654 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 14 Aug 2026 17:37:39 +0200 Subject: [PATCH 1/8] introduce `structure_map_assignments` table; rework queries --- database/schema/001_structures.sql | 21 +++++ database/schema/007_functors.sql | 13 +-- database/schema/008_morphisms.sql | 17 ---- .../009_symmetric-monoidal-categories.sql | 17 ---- .../scripts/restrict-functor-properties.ts | 9 +- .../scripts/restrict-morphism-properties.ts | 19 ++-- database/scripts/seed.ts | 70 +++++++++++--- database/scripts/utils/structures.ts | 92 +++++++++---------- src/lib/commons/types.ts | 24 ++--- src/lib/server/fetchers/category.ts | 49 ++++------ src/lib/server/fetchers/functor.ts | 87 +++++++++++++----- src/lib/server/fetchers/morphism.ts | 30 +++--- .../fetchers/symmetric_monoidal_category.ts | 33 ++++--- src/pages/FunctorDetailPage.svelte | 18 ++-- src/pages/MorphismDetailPage.svelte | 4 +- ...SymmetricMonoidalCategoryDetailPage.svelte | 4 +- src/routes/[type]/[id]/+page.server.ts | 2 +- 17 files changed, 290 insertions(+), 219 deletions(-) delete mode 100644 database/schema/008_morphisms.sql delete mode 100644 database/schema/009_symmetric-monoidal-categories.sql diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index cf73970a7..6b4a9d748 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -19,6 +19,10 @@ CREATE TABLE structure_maps ( FOREIGN KEY (mapped_type) REFERENCES structure_types (type) ON DELETE CASCADE ); +-- TODO: add the boolean field "required" to the structure_maps table. +-- For example, the domain of a functor is required, +-- but its left adjoint is not. + INSERT INTO structure_maps (map, type, mapped_type) VALUES @@ -26,6 +30,9 @@ VALUES ('codomain', 'functor', 'category'), ('category', 'morphism', 'category'), ('underlying_category', 'symmetric_monoidal_category', 'category'); +-- TODO: make left_adjoint a structure_map (with required = FALSE) +-- TODO: perhaps make dual a structure_map (with required = FALSE) +-- TODO: perhaps also "parent" CREATE TABLE structures ( id TEXT PRIMARY KEY, @@ -80,4 +87,18 @@ CREATE TABLE structure_tag_assignments ( PRIMARY KEY (structure_id, type, tag), FOREIGN KEY (structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE, FOREIGN KEY (tag, type) REFERENCES structure_tags (tag, type) ON DELETE CASCADE +); + +CREATE TABLE structure_map_assignments ( + map TEXT NOT NULL, + type TEXT NOT NULL, + mapped_type TEXT NOT NULL, + structure_id TEXT NOT NULL, + mapped_structure_id TEXT NOT NULL, + FOREIGN KEY (map, type, mapped_type) + REFERENCES structure_maps (map, type, mapped_type) ON DELETE CASCADE, + FOREIGN KEY (structure_id, type) + REFERENCES structures (id, type) ON DELETE CASCADE, + FOREIGN KEY (mapped_structure_id, mapped_type) + REFERENCES structures (id, type) ON DELETE CASCADE ); \ No newline at end of file diff --git a/database/schema/007_functors.sql b/database/schema/007_functors.sql index 982d01210..e6340dac5 100644 --- a/database/schema/007_functors.sql +++ b/database/schema/007_functors.sql @@ -1,17 +1,14 @@ CREATE TABLE functors ( id TEXT PRIMARY KEY, - domain TEXT NOT NULL, - codomain TEXT NOT NULL, left_adjoint TEXT, - UNIQUE (id, domain, codomain), FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE, - FOREIGN KEY (domain) REFERENCES categories (id) ON DELETE CASCADE, - FOREIGN KEY (codomain) REFERENCES categories (id) ON DELETE CASCADE, - FOREIGN KEY (left_adjoint, codomain, domain) - REFERENCES functors (id, domain, codomain) - ON DELETE CASCADE + FOREIGN KEY (left_adjoint) REFERENCES structures (id) ON DELETE CASCADE ); +-- TODO: bring back check that left_adjoint has correct domain and codomain +-- TODO: move this feature to the structure_maps table +-- TODO: check that the left_adjoint is a functor + CREATE TRIGGER trg_functor_type_check BEFORE INSERT ON functors BEGIN diff --git a/database/schema/008_morphisms.sql b/database/schema/008_morphisms.sql deleted file mode 100644 index dfc9ea414..000000000 --- a/database/schema/008_morphisms.sql +++ /dev/null @@ -1,17 +0,0 @@ -CREATE TABLE morphisms ( - id TEXT PRIMARY KEY, - category TEXT NOT NULL, - FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE, - FOREIGN KEY (category) REFERENCES categories (id) ON DELETE CASCADE -); - -CREATE TRIGGER trg_morphism_type_check -BEFORE INSERT ON morphisms -BEGIN - SELECT - CASE - WHEN - (SELECT type FROM structures WHERE id = NEW.id) != 'morphism' - THEN RAISE(ABORT, 'Morphisms must have type "morphism"') - END; -END; \ No newline at end of file diff --git a/database/schema/009_symmetric-monoidal-categories.sql b/database/schema/009_symmetric-monoidal-categories.sql deleted file mode 100644 index b9ceab78e..000000000 --- a/database/schema/009_symmetric-monoidal-categories.sql +++ /dev/null @@ -1,17 +0,0 @@ -CREATE TABLE symmetric_monoidal_categories ( - id TEXT PRIMARY KEY, - underlying_category TEXT NOT NULL, - FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE, - FOREIGN KEY (underlying_category) REFERENCES categories (id) ON DELETE CASCADE -); - -CREATE TRIGGER trg_symmetric_monoidal_category_type_check -BEFORE INSERT ON symmetric_monoidal_categories -BEGIN - SELECT - CASE - WHEN - (SELECT type FROM structures WHERE id = NEW.id) != 'symmetric_monoidal_category' - THEN RAISE(ABORT, 'Symmetric monoidal categories must have type "symmetric_monoidal_category"') - END; -END; \ No newline at end of file diff --git a/database/scripts/restrict-functor-properties.ts b/database/scripts/restrict-functor-properties.ts index 0fd26e37b..5a8fbed22 100644 --- a/database/scripts/restrict-functor-properties.ts +++ b/database/scripts/restrict-functor-properties.ts @@ -29,15 +29,18 @@ function restrict_representable_functors() { check_redundancy ) SELECT - f.id, + a.structure_id, 'representable', 'functor', FALSE, 'The codomain is not $\\Set$.', TRUE, FALSE - FROM functors f - WHERE f.codomain <> 'Set' + FROM structure_map_assignments a + WHERE + a.type = 'functor' + AND a.map = 'codomain' + AND a.mapped_structure_id <> 'Set' ON CONFLICT (structure_id, property_id) DO UPDATE SET proof = excluded.proof, diff --git a/database/scripts/restrict-morphism-properties.ts b/database/scripts/restrict-morphism-properties.ts index cdde6fdc9..13eb177b7 100644 --- a/database/scripts/restrict-morphism-properties.ts +++ b/database/scripts/restrict-morphism-properties.ts @@ -6,6 +6,7 @@ const db = get_client({ readonly: false }) /** * Ensures that certain properties of morphisms are only satisfied * when the ambient categories have certain properties. + * TODO: rework this once we have category_conclusions */ export function restrict_morphism_properties() { restrict_normal_morphisms('mono') @@ -31,21 +32,23 @@ function restrict_normal_morphisms(variant: 'mono' | 'epi') { check_redundancy ) SELECT - m.id, + sa.structure_id, ?, 'morphism', FALSE, 'The ' || c.name || ' has no zero morphisms.', TRUE, FALSE - FROM morphisms m + FROM structure_map_assignments sa + INNER JOIN structures c + ON c.id = sa.mapped_structure_id INNER JOIN property_assignments a - ON a.structure_id = m.category - INNER JOIN structures c - ON c.id = m.category - WHERE a.type = 'category' - AND a.property_id = 'zero morphisms' - AND a.is_satisfied = FALSE + ON a.structure_id = c.id + WHERE + sa.type = 'morphism' + AND sa.map = 'category' + AND a.property_id = 'zero morphisms' + AND a.is_satisfied = FALSE ON CONFLICT (structure_id, property_id) DO UPDATE SET proof = excluded.proof, diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index f475f8347..cef8835e9 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -108,6 +108,7 @@ function clear_all_tables() { db.prepare(`DELETE FROM relations`).run() db.prepare(`DELETE FROM structures`).run() + db.prepare(`DELETE FROM structure_map_assignments`).run() }) try { @@ -246,6 +247,9 @@ function seed_structures({ ) VALUES (?, ?, ?, ?)` ) + // TODO: loop over structure_maps here + // and fill the structure_map_assignments table + function insert_structure(structure: T) { const properties_are_disjoint = are_disjoint( [ @@ -350,30 +354,72 @@ function insert_category(category: CategoryYaml) { * Inserts the data of a functor that is specific to functors. */ function insert_functor(functor: FunctorYaml) { - db.prepare( - `INSERT INTO functors (id, domain, codomain, left_adjoint) - VALUES (?, ?, ?, ?)` - ).run(functor.id, functor.domain, functor.codomain, functor.left_adjoint || null) + // TODO: refactor into optional structure_map_assignment + if (functor.left_adjoint) { + db.prepare(`INSERT INTO functors (id, left_adjoint) VALUES (?, ?)`).run( + functor.id, + functor.left_adjoint + ) + } + + // TODO: unify this + const insert_mapped = db.prepare( + `INSERT INTO structure_map_assignments ( + map, + type, + mapped_type, + structure_id, + mapped_structure_id + ) + VALUES (?, ?, ?, ?, ?)` + ) + + insert_mapped.run('domain', 'functor', 'category', functor.id, functor.domain) + insert_mapped.run('codomain', 'functor', 'category', functor.id, functor.codomain) } /** * Inserts the data of a morphism that is specific to morphisms. */ function insert_morphism(morphism: MorphismYaml) { - db.prepare( - `INSERT INTO morphisms (id, category) - VALUES (?, ?)` - ).run(morphism.id, morphism.category) + // TODO: unify this + const insert_mapped = db.prepare( + `INSERT INTO structure_map_assignments ( + map, + type, + mapped_type, + structure_id, + mapped_structure_id + ) + VALUES (?, ?, ?, ?, ?)` + ) + + insert_mapped.run('category', 'morphism', 'category', morphism.id, morphism.category) } /** * Inserts the data of a symmetric monoidal category that is specific to symmetric monoidal categories. */ function insert_symmetric_monoidal_category(s: SymmetricMonoidalCategoryYaml) { - db.prepare( - `INSERT INTO symmetric_monoidal_categories (id, underlying_category) - VALUES (?, ?)` - ).run(s.id, s.underlying_category) + // TODO: unify this + const insert_mapped = db.prepare( + `INSERT INTO structure_map_assignments ( + map, + type, + mapped_type, + structure_id, + mapped_structure_id + ) + VALUES (?, ?, ?, ?, ?)` + ) + + insert_mapped.run( + 'underlying_category', + 'symmetric_monoidal_category', + 'category', + s.id, + s.underlying_category + ) } /** diff --git a/database/scripts/utils/structures.ts b/database/scripts/utils/structures.ts index 88978aaba..8d3e5d9a5 100644 --- a/database/scripts/utils/structures.ts +++ b/database/scripts/utils/structures.ts @@ -11,67 +11,61 @@ export type StructureMeta = { associated_satisfied_properties?: Partial>> } -/** - * Dictionary associating to every structure type the name of the table. - */ -const TABLES: Record = { - category: 'categories', - functor: 'functors', - morphism: 'morphisms', - symmetric_monoidal_category: 'symmetric_monoidal_categories' -} - /** * Returns the list of stored categorical structures of a given type. * For structures with structure maps (e.g. functors), the associated * satisfied properties are retrieved as well. */ export function get_structures(db: Database, type: StructureType): StructureMeta[] { - const structures = db - .prepare<[StructureType], StructureMeta>( - `SELECT - s.id, - s.name, - s.dual_structure_id AS dual - FROM structures s - WHERE s.type = ? - ORDER BY lower(s.name)` - ) - .all(type) - - const structure_maps = db - .prepare<[StructureType], string>( - `SELECT map - FROM structure_maps - WHERE type = ?` + const structures_raw = db + .prepare< + [StructureType], + { + id: string + name: string + dual: string | null + properties: string + } + >( + `WITH mapped_properties AS ( + SELECT + s.id, + s.name, + s.dual_structure_id AS dual, + m.map, + json_group_array(a.property_id) AS props + FROM structures s + LEFT JOIN structure_map_assignments m + ON m.structure_id = s.id + LEFT JOIN property_assignments a + ON a.structure_id = m.mapped_structure_id + AND a.is_satisfied = TRUE + WHERE s.type = ? + GROUP BY s.id, m.map + ) + SELECT + id, name, dual, + json_group_object(map, props) AS properties + FROM mapped_properties + GROUP BY id + ORDER BY id` ) - .pluck() .all(type) - if (!structure_maps.length) return structures - - const add_associated_properties = db.transaction(() => { - for (const map of structure_maps) { - const prop_query = db - .prepare<[string], string>( - `SELECT property_id FROM property_assignments - INNER JOIN ${TABLES[type]} t ON t.id = ? - WHERE structure_id = t.${map} - AND is_satisfied = TRUE` - ) - .pluck() + return structures_raw.map((s) => { + const { id, name, dual, properties } = s + const parsed_properties = JSON.parse(properties) as Partial< + Record + > - for (const structure of structures) { - structure.associated_satisfied_properties ??= {} - const props = prop_query.all(structure.id) - structure.associated_satisfied_properties[map] = new Set(props) - } + const associated_satisfied_properties: Partial>> = {} + for (const [map, props] of Object.entries(parsed_properties)) { + if (!props) continue + associated_satisfied_properties[map] = new Set(JSON.parse(props)) } - }) - add_associated_properties() - - return structures + return { id, name, dual, associated_satisfied_properties } + }) } /** diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 35710c3d4..fb9be8b2c 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -145,28 +145,16 @@ export type CategorySpecificDisplay = { } export type FunctorSpecificDisplay = { - domain: string - domain_name: string - domain_notation: string - codomain: string - codomain_name: string - codomain_notation: string - left_adjoint: string | null - left_adjoint_name: string | null - left_adjoint_notation: string | null - right_adjoint: string | null - right_adjoint_name: string | null - right_adjoint_notation: string | null + domain: RelatedStructure + codomain: RelatedStructure + left_adjoint?: RelatedStructure + right_adjoint?: RelatedStructure } export type MorphismSpecificDisplay = { - category: string - category_name: string - category_notation: string + category: RelatedStructure } export type SymmetricMonoidalCategorySpecificDisplay = { - underlying_category: string - underlying_category_name: string - underlying_category_notation: string + underlying_category: RelatedStructure } diff --git a/src/lib/server/fetchers/category.ts b/src/lib/server/fetchers/category.ts index cc30693a6..374d7a66d 100644 --- a/src/lib/server/fetchers/category.ts +++ b/src/lib/server/fetchers/category.ts @@ -2,7 +2,8 @@ import type { CategoryDefinition, SpecialMorphism, SpecialObject, - StructureShort + StructureShort, + StructureType } from '$lib/commons/types' import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' @@ -39,37 +40,25 @@ export function fetch_category(id: string) { ) .all(id) - // TODO: make this more systematic by looping over the structure_maps + // TODO: make this more systematic - const stored_functors = db - .prepare<[string, string], StructureShort>( - `SELECT f.id, s.name - FROM functors f - INNER JOIN structures s ON s.id = f.id - WHERE f.domain = ? OR f.codomain = ? - ORDER BY lower(s.name)` - ) - .all(id, id) + const get_stored_structures = db.prepare<[string, StructureType], StructureShort>( + `SELECT DISTINCT s.id, s.name + FROM structure_map_assignments a + INNER JOIN structures s + ON s.id = a.structure_id + WHERE + a.mapped_structure_id = ? + AND a.type = ? + ORDER BY lower(s.name)` + ) - 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) - - const stored_symmetric_monoidal_categories = db - .prepare<[string], StructureShort>( - `SELECT c.id, s.name - FROM symmetric_monoidal_categories c - INNER JOIN structures s ON s.id = c.id - WHERE c.underlying_category = ? - ORDER BY lower(s.name)` - ) - .all(id) + const stored_functors = get_stored_structures.all(id, 'functor') + const stored_morphisms = get_stored_structures.all(id, 'morphism') + const stored_symmetric_monoidal_categories = get_stored_structures.all( + id, + 'symmetric_monoidal_category' + ) return { type: 'category' as const, diff --git a/src/lib/server/fetchers/functor.ts b/src/lib/server/fetchers/functor.ts index 7645f72d2..4e7599a18 100644 --- a/src/lib/server/fetchers/functor.ts +++ b/src/lib/server/fetchers/functor.ts @@ -1,34 +1,77 @@ -import type { FunctorSpecificDisplay } from '$lib/commons/types' +import type { RelatedStructure } from '$lib/commons/types' import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' export function fetch_functor(id: string) { - const functor = db - .prepare<[string], FunctorSpecificDisplay>( + // TODO: refactor this function + + const domain = db + .prepare<[string], RelatedStructure>( + `SELECT + s.id, + s.name, + s.notation + FROM structure_map_assignments a + INNER JOIN structures s + ON s.id = a.mapped_structure_id + WHERE + a.type = 'functor' + AND a.structure_id = ? + AND a.map = 'domain'` + ) + .get(id) + + if (!domain) error(404, `No domain found for functor with ID ${id}`) + + const codomain = db + .prepare<[string], RelatedStructure>( `SELECT - f.domain, - f.codomain, - domain.name AS domain_name, - domain.notation AS domain_notation, - codomain.name AS codomain_name, - codomain.notation AS codomain_notation, - la.id AS left_adjoint, - la.name AS left_adjoint_name, - la.notation AS left_adjoint_notation, - ra.id AS right_adjoint, - ra.name AS right_adjoint_name, - ra.notation AS right_adjoint_notation + s.id, + s.name, + s.notation + FROM structure_map_assignments a + INNER JOIN structures s + ON s.id = a.mapped_structure_id + WHERE + a.type = 'functor' + AND a.structure_id = ? + AND a.map = 'codomain'` + ) + .get(id) + + if (!codomain) error(404, `No codomain found for functor with ID ${id}`) + + const left_adjoint = db + .prepare<[string], RelatedStructure>( + `SELECT + s.id, + s.name, + s.notation FROM functors f - INNER JOIN structures AS domain ON domain.id = f.domain - INNER JOIN structures AS codomain ON codomain.id = f.codomain - LEFT JOIN structures AS la ON la.id = f.left_adjoint - LEFT JOIN functors AS rf ON rf.left_adjoint = f.id - LEFT JOIN structures AS ra ON ra.id = rf.id + INNER JOIN structures s + ON s.id = f.left_adjoint WHERE f.id = ?` ) .get(id) - if (!functor) error(404, `Could not find functor with ID '${id}'`) + const right_adjoint = db + .prepare<[string], RelatedStructure>( + `SELECT + s.id, + s.name, + s.notation + FROM functors f + INNER JOIN structures s + ON s.id = f.id + WHERE f.left_adjoint = ?` + ) + .get(id) - return { type: 'functor' as const, ...functor } + return { + type: 'functor' as const, + domain, + codomain, + left_adjoint, + right_adjoint + } } diff --git a/src/lib/server/fetchers/morphism.ts b/src/lib/server/fetchers/morphism.ts index 8aacbf9a8..a44eff627 100644 --- a/src/lib/server/fetchers/morphism.ts +++ b/src/lib/server/fetchers/morphism.ts @@ -1,21 +1,29 @@ -import type { MorphismSpecificDisplay } from '$lib/commons/types' +import type { RelatedStructure } from '$lib/commons/types' import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' export function fetch_morphism(id: string) { - const morphism = db - .prepare<[string], MorphismSpecificDisplay>( + // TODO: generalize this to all structures + + const category = db + .prepare<[string], RelatedStructure>( `SELECT - c.id AS category, - c.name AS category_name, - c.notation AS category_notation - FROM morphisms m - INNER JOIN structures AS c ON c.id = m.category - WHERE m.id = ?` + s.id, + s.name, + s.notation + FROM structure_map_assignments a + INNER JOIN structures s + ON s.id = a.mapped_structure_id + WHERE + a.type = 'morphism' + AND a.structure_id = ? + AND a.map = 'category'` ) .get(id) - if (!morphism) error(404, `Could not find morphism with ID '${id}'`) + if (!category) { + error(404, `Could not find the category of the morphism with ID '${id}'`) + } - return { type: 'morphism' as const, ...morphism } + return { type: 'morphism' as const, category } } diff --git a/src/lib/server/fetchers/symmetric_monoidal_category.ts b/src/lib/server/fetchers/symmetric_monoidal_category.ts index 89cb454c3..3551410dd 100644 --- a/src/lib/server/fetchers/symmetric_monoidal_category.ts +++ b/src/lib/server/fetchers/symmetric_monoidal_category.ts @@ -1,21 +1,32 @@ -import type { SymmetricMonoidalCategorySpecificDisplay } from '$lib/commons/types' +import type { RelatedStructure } from '$lib/commons/types' import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' export function fetch_symmetric_monoidal_category(id: string) { - const s = db - .prepare<[string], SymmetricMonoidalCategorySpecificDisplay>( + // TODO: generalize this + + const underlying_category = db + .prepare<[string], RelatedStructure>( `SELECT - c.id AS underlying_category, - c.name AS underlying_category_name, - c.notation AS underlying_category_notation - FROM symmetric_monoidal_categories s - INNER JOIN structures AS c ON c.id = s.underlying_category - WHERE s.id = ?` + s.id, + s.name, + s.notation + FROM structure_map_assignments a + INNER JOIN structures s + ON s.id = a.mapped_structure_id + WHERE + a.type = 'symmetric_monoidal_category' + AND a.structure_id = ? + AND a.map = 'underlying_category'` ) .get(id) - if (!s) error(404, `Could not find symmetric monoidal category with ID '${id}'`) + if (!underlying_category) { + error( + 404, + `No underlying category found for symmetric monoidal category with ID ${id}` + ) + } - return { type: 'symmetric_monoidal_category' as const, ...s } + return { type: 'symmetric_monoidal_category' as const, underlying_category } } diff --git a/src/pages/FunctorDetailPage.svelte b/src/pages/FunctorDetailPage.svelte index c944f9238..a69eaa9d8 100644 --- a/src/pages/FunctorDetailPage.svelte +++ b/src/pages/FunctorDetailPage.svelte @@ -8,25 +8,27 @@ + + {#snippet definition()}
  • Domain: - {data.domain_name} + {data.domain.name}
  • Codomain: - {data.codomain_name} + {data.codomain.name}
    • {#if data.left_adjoint}
  • Left adjoint functor: - {@html data.left_adjoint_notation} + {@html data.left_adjoint.notation}
    • {/if} @@ -35,10 +37,10 @@
  • Right adjoint functor: - {@html data.right_adjoint_notation} + {@html data.right_adjoint.notation}
    • {/if} diff --git a/src/pages/MorphismDetailPage.svelte b/src/pages/MorphismDetailPage.svelte index fc15a3b83..75fdef181 100644 --- a/src/pages/MorphismDetailPage.svelte +++ b/src/pages/MorphismDetailPage.svelte @@ -11,8 +11,8 @@ {#snippet definition()}
  • Category: - - {data.category_name} + + {data.category.name}
    • {/snippet} diff --git a/src/pages/SymmetricMonoidalCategoryDetailPage.svelte b/src/pages/SymmetricMonoidalCategoryDetailPage.svelte index 6213f9c07..204394e00 100644 --- a/src/pages/SymmetricMonoidalCategoryDetailPage.svelte +++ b/src/pages/SymmetricMonoidalCategoryDetailPage.svelte @@ -14,8 +14,8 @@ {#snippet definition()}
  • Underlying category: - - {data.underlying_category_name} + + {data.underlying_category.name}
    • {/snippet} diff --git a/src/routes/[type]/[id]/+page.server.ts b/src/routes/[type]/[id]/+page.server.ts index 58af8b25c..2a97faace 100644 --- a/src/routes/[type]/[id]/+page.server.ts +++ b/src/routes/[type]/[id]/+page.server.ts @@ -27,7 +27,7 @@ export const load = (event) => { if (special_structure_data.type === 'functor') { structure_data.structure.notation = add_math( - `${strip_math(structure_data.structure.notation)}: ${strip_math(special_structure_data.domain_notation)} \\to ${strip_math(special_structure_data.codomain_notation)}` + `${strip_math(structure_data.structure.notation)}: ${strip_math(special_structure_data.domain.notation)} \\to ${strip_math(special_structure_data.codomain.notation)}` ) } From dae19364bc605a687f2e188a844d45b077c8ce86 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 14 Aug 2026 19:19:40 +0200 Subject: [PATCH 2/8] unify seeding step for structures --- database/scripts/seed.ts | 92 ++++++++-------------------- database/scripts/utils/seed.types.ts | 10 --- 2 files changed, 25 insertions(+), 77 deletions(-) diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index cef8835e9..1ae74e4eb 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -8,9 +8,7 @@ import type { FunctorYaml, SpecialMorphismRuleYaml, StructureYaml, - PropertyYaml, - MorphismYaml, - SymmetricMonoidalCategoryYaml + PropertyYaml } from './utils/seed.types' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' import { STRUCTURE_TYPES, type StructureType, PLURALS } from '$shared/config' @@ -43,7 +41,7 @@ function seed() { seed_properties({ type: 'morphism', folder: 'morphism-properties' }) seed_implications({ type: 'morphism', folder: 'morphism-implications' }) - seed_structures({ type: 'morphism', folder: 'morphisms', extra: insert_morphism }) + seed_structures({ type: 'morphism', folder: 'morphisms' }) seed_properties({ type: 'symmetric_monoidal_category', @@ -55,8 +53,7 @@ function seed() { }) seed_structures({ type: 'symmetric_monoidal_category', - folder: 'symmetric_monoidal_categories', - extra: insert_symmetric_monoidal_category + folder: 'symmetric_monoidal_categories' }) } @@ -211,6 +208,13 @@ function seed_structures({ folder: string extra?: (structure: T) => void }) { + const structure_maps = db + .prepare<[StructureType], { map: keyof T; mapped_type: StructureType }>( + `SELECT map, mapped_type + FROM structure_maps WHERE type = ?` + ) + .all(type) + const structure_insert = db.prepare( `INSERT INTO structures ( id, type, name, notation, description, nlab_link, @@ -247,8 +251,11 @@ function seed_structures({ ) VALUES (?, ?, ?, ?)` ) - // TODO: loop over structure_maps here - // and fill the structure_map_assignments table + const structure_map_assignment_insert = db.prepare( + `INSERT INTO structure_map_assignments ( + map, type, mapped_type, structure_id, mapped_structure_id + ) VALUES (?, ?, ?, ?, ?)` + ) function insert_structure(structure: T) { const properties_are_disjoint = are_disjoint( @@ -276,6 +283,16 @@ function seed_structures({ structure.parent || null ) + for (const { map, mapped_type } of structure_maps) { + structure_map_assignment_insert.run( + map, + type, + mapped_type, + structure.id, + structure[map] + ) + } + if (!structure.tags.length) { console.error(`❌ Structure "${structure.id}" has no tags`) process.exit(1) @@ -361,65 +378,6 @@ function insert_functor(functor: FunctorYaml) { functor.left_adjoint ) } - - // TODO: unify this - const insert_mapped = db.prepare( - `INSERT INTO structure_map_assignments ( - map, - type, - mapped_type, - structure_id, - mapped_structure_id - ) - VALUES (?, ?, ?, ?, ?)` - ) - - insert_mapped.run('domain', 'functor', 'category', functor.id, functor.domain) - insert_mapped.run('codomain', 'functor', 'category', functor.id, functor.codomain) -} - -/** - * Inserts the data of a morphism that is specific to morphisms. - */ -function insert_morphism(morphism: MorphismYaml) { - // TODO: unify this - const insert_mapped = db.prepare( - `INSERT INTO structure_map_assignments ( - map, - type, - mapped_type, - structure_id, - mapped_structure_id - ) - VALUES (?, ?, ?, ?, ?)` - ) - - insert_mapped.run('category', 'morphism', 'category', morphism.id, morphism.category) -} - -/** - * Inserts the data of a symmetric monoidal category that is specific to symmetric monoidal categories. - */ -function insert_symmetric_monoidal_category(s: SymmetricMonoidalCategoryYaml) { - // TODO: unify this - const insert_mapped = db.prepare( - `INSERT INTO structure_map_assignments ( - map, - type, - mapped_type, - structure_id, - mapped_structure_id - ) - VALUES (?, ?, ?, ?, ?)` - ) - - insert_mapped.run( - 'underlying_category', - 'symmetric_monoidal_category', - 'category', - s.id, - s.underlying_category - ) } /** diff --git a/database/scripts/utils/seed.types.ts b/database/scripts/utils/seed.types.ts index dfc372d82..8cde2d586 100644 --- a/database/scripts/utils/seed.types.ts +++ b/database/scripts/utils/seed.types.ts @@ -71,19 +71,9 @@ export type CategoryYaml = StructureYaml & { } export type FunctorYaml = StructureYaml & { - domain: string - codomain: string left_adjoint: string | null } -export type MorphismYaml = StructureYaml & { - category: string -} - -export type SymmetricMonoidalCategoryYaml = StructureYaml & { - underlying_category: string -} - export type PropertyYaml = { id: string relation: string From afe0bee02a6c6e9ac2d15ad8e1a96954afce8b7f Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 14 Aug 2026 19:41:57 +0200 Subject: [PATCH 3/8] move adjoint functors to the `structure_map_assignments` table, support optional entries --- database/schema/001_structures.sql | 20 +++++++++-------- database/schema/007_functors.sql | 21 ------------------ database/scripts/seed.ts | 32 +++++++++------------------- database/scripts/utils/seed.types.ts | 4 ---- src/lib/server/fetchers/functor.ts | 18 ++++++++++------ 5 files changed, 33 insertions(+), 62 deletions(-) delete mode 100644 database/schema/007_functors.sql diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index 6b4a9d748..85a6b4867 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -13,26 +13,28 @@ CREATE TABLE structure_maps ( map TEXT NOT NULL, type TEXT NOT NULL, mapped_type TEXT NOT NULL, + required INTEGER NOT NULL + CHECK (required in (TRUE, FALSE)), PRIMARY KEY (map, type, mapped_type), UNIQUE (map, type), FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE CASCADE, FOREIGN KEY (mapped_type) REFERENCES structure_types (type) ON DELETE CASCADE ); --- TODO: add the boolean field "required" to the structure_maps table. --- For example, the domain of a functor is required, --- but its left adjoint is not. +-- TODO: check somewhere that the required fields are indeed filled for every structure. INSERT INTO structure_maps - (map, type, mapped_type) + (map, type, mapped_type, required) VALUES - ('domain', 'functor', 'category'), - ('codomain', 'functor', 'category'), - ('category', 'morphism', 'category'), - ('underlying_category', 'symmetric_monoidal_category', 'category'); --- TODO: make left_adjoint a structure_map (with required = FALSE) + ('domain', 'functor', 'category', TRUE), + ('codomain', 'functor', 'category', TRUE), + ('category', 'morphism', 'category', TRUE), + ('underlying_category', 'symmetric_monoidal_category', 'category', TRUE), + ('left_adjoint', 'functor', 'functor', FALSE); + -- TODO: perhaps make dual a structure_map (with required = FALSE) -- TODO: perhaps also "parent" +-- TODO: check that domain and codomain of functor match CREATE TABLE structures ( id TEXT PRIMARY KEY, diff --git a/database/schema/007_functors.sql b/database/schema/007_functors.sql deleted file mode 100644 index e6340dac5..000000000 --- a/database/schema/007_functors.sql +++ /dev/null @@ -1,21 +0,0 @@ -CREATE TABLE functors ( - id TEXT PRIMARY KEY, - left_adjoint TEXT, - FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE, - FOREIGN KEY (left_adjoint) REFERENCES structures (id) ON DELETE CASCADE -); - --- TODO: bring back check that left_adjoint has correct domain and codomain --- TODO: move this feature to the structure_maps table --- TODO: check that the left_adjoint is a functor - -CREATE TRIGGER trg_functor_type_check -BEFORE INSERT ON functors -BEGIN - SELECT - CASE - WHEN - (SELECT type FROM structures WHERE id = NEW.id) != 'functor' - THEN RAISE(ABORT, 'Functors must have type "functor"') - END; -END; \ No newline at end of file diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index 1ae74e4eb..3adccbe4d 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -5,7 +5,6 @@ import type { CategoryYaml, ConfigYaml, ImplicationYaml, - FunctorYaml, SpecialMorphismRuleYaml, StructureYaml, PropertyYaml @@ -37,7 +36,7 @@ function seed() { seed_properties({ type: 'functor', folder: 'functor-properties' }) seed_implications({ type: 'functor', folder: 'functor-implications' }) - seed_structures({ type: 'functor', folder: 'functors', extra: insert_functor }) + seed_structures({ type: 'functor', folder: 'functors' }) seed_properties({ type: 'morphism', folder: 'morphism-properties' }) seed_implications({ type: 'morphism', folder: 'morphism-implications' }) @@ -284,13 +283,15 @@ function seed_structures({ ) for (const { map, mapped_type } of structure_maps) { - structure_map_assignment_insert.run( - map, - type, - mapped_type, - structure.id, - structure[map] - ) + if (structure[map]) { + structure_map_assignment_insert.run( + map, + type, + mapped_type, + structure.id, + structure[map] + ) + } } if (!structure.tags.length) { @@ -367,19 +368,6 @@ function insert_category(category: CategoryYaml) { } } -/** - * Inserts the data of a functor that is specific to functors. - */ -function insert_functor(functor: FunctorYaml) { - // TODO: refactor into optional structure_map_assignment - if (functor.left_adjoint) { - db.prepare(`INSERT INTO functors (id, left_adjoint) VALUES (?, ?)`).run( - functor.id, - functor.left_adjoint - ) - } -} - /** * Seeds all properties of a given type from YAML files. */ diff --git a/database/scripts/utils/seed.types.ts b/database/scripts/utils/seed.types.ts index 8cde2d586..1846f6305 100644 --- a/database/scripts/utils/seed.types.ts +++ b/database/scripts/utils/seed.types.ts @@ -70,10 +70,6 @@ export type CategoryYaml = StructureYaml & { special_morphisms: Record } -export type FunctorYaml = StructureYaml & { - left_adjoint: string | null -} - export type PropertyYaml = { id: string relation: string diff --git a/src/lib/server/fetchers/functor.ts b/src/lib/server/fetchers/functor.ts index 4e7599a18..a2509b606 100644 --- a/src/lib/server/fetchers/functor.ts +++ b/src/lib/server/fetchers/functor.ts @@ -47,10 +47,13 @@ export function fetch_functor(id: string) { s.id, s.name, s.notation - FROM functors f + FROM structure_map_assignments a INNER JOIN structures s - ON s.id = f.left_adjoint - WHERE f.id = ?` + ON s.id = a.mapped_structure_id + WHERE + a.type = 'functor' + AND a.structure_id = ? + AND a.map = 'left_adjoint'` ) .get(id) @@ -60,10 +63,13 @@ export function fetch_functor(id: string) { s.id, s.name, s.notation - FROM functors f + FROM structure_map_assignments a INNER JOIN structures s - ON s.id = f.id - WHERE f.left_adjoint = ?` + ON s.id = a.structure_id + WHERE + a.type = 'functor' + AND a.mapped_structure_id = ? + AND a.map = 'left_adjoint'` ) .get(id) From e702946d5d022494219733217dd735983452059e Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 14 Aug 2026 20:18:11 +0200 Subject: [PATCH 4/8] unify display of structures on structure detail page that refer to the current one --- src/components/StructuresBasedOn.svelte | 31 ++++++++++++++ src/lib/commons/types.ts | 6 +-- src/lib/server/fetchers/category.ts | 28 +------------ src/lib/server/fetchers/content.ts | 3 +- src/lib/server/fetchers/structure.ts | 25 +++++++++++ src/pages/CategoryDetailPage.svelte | 56 ------------------------- src/pages/StructureDetailPage.svelte | 10 +++-- 7 files changed, 69 insertions(+), 90 deletions(-) create mode 100644 src/components/StructuresBasedOn.svelte diff --git a/src/components/StructuresBasedOn.svelte b/src/components/StructuresBasedOn.svelte new file mode 100644 index 000000000..2eb1320f6 --- /dev/null +++ b/src/components/StructuresBasedOn.svelte @@ -0,0 +1,31 @@ + + +{#each STRUCTURE_TYPES as type} + {@const structures = structures_based_on[type]} + {#if structures && structures.length > 0} +

    {capitalize(PLURALS[type])}

    + +

    + The database stores {structures.length} + {pluralize(structures.length, { + one: remove_underscores(type), + other: PLURALS[type] + })} + based on the {structure_name}. +

    + + + {/if} +{/each} diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index fb9be8b2c..8698087b9 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -9,6 +9,8 @@ export type StructureShort = { name: string } +export type StructureShortDictionary = Partial> + export type RelatedStructure = StructureShort & { notation: string } export type StructureDisplay = { @@ -124,6 +126,7 @@ export type StructureDetails = { type: StructureType structure: StructureDisplay related_structures: RelatedStructure[] + structures_based_on: StructureShortDictionary children: RelatedStructure[] tags: string[] satisfied_properties: PropertyAssignmentDisplay[] @@ -139,9 +142,6 @@ export type CategorySpecificDisplay = { morphisms: string special_objects: SpecialObject[] special_morphisms: SpecialMorphism[] - stored_functors: StructureShort[] - stored_morphisms: StructureShort[] - stored_symmetric_monoidal_categories: StructureShort[] } export type FunctorSpecificDisplay = { diff --git a/src/lib/server/fetchers/category.ts b/src/lib/server/fetchers/category.ts index 374d7a66d..7ac4fe7cc 100644 --- a/src/lib/server/fetchers/category.ts +++ b/src/lib/server/fetchers/category.ts @@ -2,8 +2,7 @@ import type { CategoryDefinition, SpecialMorphism, SpecialObject, - StructureShort, - StructureType + StructureShort } from '$lib/commons/types' import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' @@ -40,34 +39,11 @@ export function fetch_category(id: string) { ) .all(id) - // TODO: make this more systematic - - const get_stored_structures = db.prepare<[string, StructureType], StructureShort>( - `SELECT DISTINCT s.id, s.name - FROM structure_map_assignments a - INNER JOIN structures s - ON s.id = a.structure_id - WHERE - a.mapped_structure_id = ? - AND a.type = ? - ORDER BY lower(s.name)` - ) - - const stored_functors = get_stored_structures.all(id, 'functor') - const stored_morphisms = get_stored_structures.all(id, 'morphism') - const stored_symmetric_monoidal_categories = get_stored_structures.all( - id, - 'symmetric_monoidal_category' - ) - return { type: 'category' as const, ...category, special_objects, - special_morphisms, - stored_functors, - stored_morphisms, - stored_symmetric_monoidal_categories + special_morphisms } } diff --git a/src/lib/server/fetchers/content.ts b/src/lib/server/fetchers/content.ts index 42c4b4d22..aa719517d 100644 --- a/src/lib/server/fetchers/content.ts +++ b/src/lib/server/fetchers/content.ts @@ -3,6 +3,7 @@ import type { ImplicationDisplay, PropertyShort, StructureShort, + StructureShortDictionary, StructureType } from '$lib/commons/types' import { db } from '$lib/server/db' @@ -19,7 +20,7 @@ export function fetch_content_references(content_id: string) { ) .all(content_id) - const structures_by_type: Partial> = {} + const structures_by_type: StructureShortDictionary = {} for (const { type, ...structure } of structures) { structures_by_type[type] ??= [] diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts index b4727cb33..b2c50b5a0 100644 --- a/src/lib/server/fetchers/structure.ts +++ b/src/lib/server/fetchers/structure.ts @@ -6,6 +6,7 @@ import type { StructureDetails, StructureDisplay, StructureShort, + StructureShortDictionary, StructureType } from '$lib/commons/types' import { error } from '@sveltejs/kit' @@ -51,6 +52,29 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai ) .all(id) + const list_structures_based_on = db + .prepare<[string], StructureShort & { type: StructureType }>( + `SELECT DISTINCT s.id, s.name, a.type + FROM structure_map_assignments a + INNER JOIN structures s + ON s.id = a.structure_id + INNER JOIN structure_maps m + ON + m.map = a.map + AND m.type = a.type + AND m.mapped_type = a.mapped_type + WHERE a.mapped_structure_id = ? AND m.required = TRUE + ORDER BY a.type, lower(s.name)` + ) + .all(id) + + const structures_based_on: StructureShortDictionary = {} + + for (const { id, name, type } of list_structures_based_on) { + structures_based_on[type] ??= [] + structures_based_on[type].push({ id, name }) + } + const children = db .prepare<[string], RelatedStructure>( `SELECT s.id, s.name, s.notation @@ -147,6 +171,7 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai structure, children, related_structures, + structures_based_on, tags, satisfied_properties, unsatisfied_properties, diff --git a/src/pages/CategoryDetailPage.svelte b/src/pages/CategoryDetailPage.svelte index 9e8c8a9cf..5f58f804a 100644 --- a/src/pages/CategoryDetailPage.svelte +++ b/src/pages/CategoryDetailPage.svelte @@ -1,7 +1,5 @@ @@ -143,7 +145,7 @@ -{@render footer?.()} + From 53c4900f4c19dba3d39abc25e0b6f4fe7a65537c Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 14 Aug 2026 22:33:11 +0200 Subject: [PATCH 5/8] add right_adjoint as separate structure map --- database/data/functors/abelianization.yaml | 1 + database/data/functors/binary_coproduct_sets.yaml | 1 + database/data/functors/binary_product_sets.yaml | 1 + database/data/functors/brauer_group.yaml | 1 + database/data/functors/continuous-functions.yaml | 1 + database/data/functors/countable_copower_sets.yaml | 1 + database/data/functors/diagonal_sets.yaml | 1 + database/data/functors/discrete_topology.yaml | 1 + database/data/functors/doubling_sets.yaml | 1 + database/data/functors/empty_sets.yaml | 1 + database/data/functors/enveloping_group.yaml | 1 + database/data/functors/forget_abelian.yaml | 1 + database/data/functors/forget_addition.yaml | 1 + database/data/functors/forget_commutative.yaml | 1 + database/data/functors/forget_finite.yaml | 1 + database/data/functors/forget_finite_abelian_group.yaml | 1 + database/data/functors/forget_finite_group.yaml | 1 + database/data/functors/forget_group.yaml | 1 + database/data/functors/forget_group_pointed.yaml | 1 + database/data/functors/forget_hausdorff.yaml | 1 + database/data/functors/forget_inverses.yaml | 1 + database/data/functors/forget_ring.yaml | 1 + database/data/functors/forget_topology.yaml | 1 + database/data/functors/forget_torsion.yaml | 1 + database/data/functors/forget_torsion_free.yaml | 1 + database/data/functors/forget_vector.yaml | 1 + database/data/functors/free_group.yaml | 1 + database/data/functors/group_units.yaml | 1 + database/data/functors/id_Set.yaml | 1 + database/data/functors/inclusion_ordinals.yaml | 1 + database/data/functors/indiscrete_topology.yaml | 1 + database/data/functors/modulo-p.yaml | 1 + database/data/functors/monoid_ring.yaml | 1 + database/data/functors/morphism_endpoints_inclusion.yaml | 1 + database/data/functors/nerve.yaml | 1 + database/data/functors/opposite_category.yaml | 1 + database/data/functors/opposite_monoid.yaml | 1 + database/data/functors/p-torsion.yaml | 1 + database/data/functors/pi_0.yaml | 1 + database/data/functors/pi_1.yaml | 1 + database/data/functors/power_set_contravariant.yaml | 1 + database/data/functors/power_set_covariant.yaml | 1 + database/data/functors/rational_product.yaml | 1 + database/data/functors/ring_idempotents.yaml | 1 + database/data/functors/sequences_sets.yaml | 1 + database/data/functors/simple_group_probing.yaml | 1 + database/data/functors/span_endpoints_inclusion.yaml | 1 + database/data/functors/squaring_sets.yaml | 1 + database/data/functors/stone-cech-compactification.yaml | 1 + database/data/functors/torsion.yaml | 1 + database/data/functors/trivial_BG.yaml | 1 + database/data/functors/trivial_Idem.yaml | 1 + database/data/functors/trivial_groups.yaml | 1 + database/data/functors/trivial_sets.yaml | 1 + .../data/functors/walking_isomorphism_object_inclusion.yaml | 1 + database/data/functors/walking_morphism_representation.yaml | 1 + database/schema/001_structures.sql | 4 +++- src/lib/server/fetchers/functor.ts | 6 +++--- 58 files changed, 62 insertions(+), 4 deletions(-) diff --git a/database/data/functors/abelianization.yaml b/database/data/functors/abelianization.yaml index 2bd138246..a20bd0f44 100644 --- a/database/data/functors/abelianization.yaml +++ b/database/data/functors/abelianization.yaml @@ -6,6 +6,7 @@ codomain: Ab description: This functor maps a group $G$ to its abelianization $G^{\ab} \coloneqq G/[G,G]$. nlab_link: https://ncatlab.org/nlab/show/abelianization left_adjoint: null +right_adjoint: forget_abelian tags: - algebra diff --git a/database/data/functors/binary_coproduct_sets.yaml b/database/data/functors/binary_coproduct_sets.yaml index e2866b182..05d01e848 100644 --- a/database/data/functors/binary_coproduct_sets.yaml +++ b/database/data/functors/binary_coproduct_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a pair of sets $(X,Y)$ to their coproduct $X + Y$. It is an example of a right-invertible left adjoint functor which is not a reflector. nlab_link: null left_adjoint: null +right_adjoint: diagonal_sets tags: - set theory diff --git a/database/data/functors/binary_product_sets.yaml b/database/data/functors/binary_product_sets.yaml index 00ba6d450..b4639bbe9 100644 --- a/database/data/functors/binary_product_sets.yaml +++ b/database/data/functors/binary_product_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a pair of sets $(X,Y)$ to their product $X \times Y$. It is an example of a right-invertible right adjoint functor which is not a coreflector. nlab_link: null left_adjoint: diagonal_sets +right_adjoint: null tags: - set theory diff --git a/database/data/functors/brauer_group.yaml b/database/data/functors/brauer_group.yaml index 10636f298..9888bc89c 100644 --- a/database/data/functors/brauer_group.yaml +++ b/database/data/functors/brauer_group.yaml @@ -6,6 +6,7 @@ codomain: Ab description: The Brauer group $\Br(K)$ of a field $K$ consists of equivalence classes of central simple algebras over $K$, where $A \sim B$ iff $A \otimes_K M_n(K) \cong B \otimes_K M_n(K)$ for some $n \geq 0$. The group structure is given by $[A] \cdot [B] \coloneqq [A \otimes_K B]$, $1 \coloneqq [K]$ and $[A]^{-1} \coloneqq [A^{\op}]$. A homomorphism $K \to L$ induces the homomorphism $\Br(K) \to \Br(L)$ defined by $[A] \mapsto [A \otimes_K L]$. nlab_link: https://ncatlab.org/nlab/show/Brauer+group left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/continuous-functions.yaml b/database/data/functors/continuous-functions.yaml index 20a1942de..75a0322dc 100644 --- a/database/data/functors/continuous-functions.yaml +++ b/database/data/functors/continuous-functions.yaml @@ -6,6 +6,7 @@ codomain: CAlg(R) # TODO: specify that R is IR description: 'This functor maps a topological space $X$ to the commutative $\IR$-algebra $C(X)$ of continuous functions $X \to \IR$. A continuous map $f : X \to Y$ is mapped to the algebra homomorphism $f^* : C(Y) \to C(X)$, $u \mapsto u \circ f$.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - topology diff --git a/database/data/functors/countable_copower_sets.yaml b/database/data/functors/countable_copower_sets.yaml index bd01ca6c3..a75a9cda8 100644 --- a/database/data/functors/countable_copower_sets.yaml +++ b/database/data/functors/countable_copower_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a set $X$ to the product $\IN \times X$, which can also be seen as the copower $\IN \otimes X = \coprod_{n \in \IN} X$. It is an example of a polynomial functor. nlab_link: null left_adjoint: null +right_adjoint: sequences_sets tags: - set theory diff --git a/database/data/functors/diagonal_sets.yaml b/database/data/functors/diagonal_sets.yaml index 87ce3358e..72fc8410e 100644 --- a/database/data/functors/diagonal_sets.yaml +++ b/database/data/functors/diagonal_sets.yaml @@ -6,6 +6,7 @@ codomain: SetxSet description: 'Every category $\C$ has a (binary) diagonal functor $\Delta : \C \to \C^2$, $X \mapsto (X,X)$. Here, we specify that $\C$ is the category of sets.' nlab_link: https://ncatlab.org/nlab/show/diagonal+functor left_adjoint: binary_coproduct_sets +right_adjoint: binary_product_sets tags: - set theory diff --git a/database/data/functors/discrete_topology.yaml b/database/data/functors/discrete_topology.yaml index 398260266..79a914b45 100644 --- a/database/data/functors/discrete_topology.yaml +++ b/database/data/functors/discrete_topology.yaml @@ -6,6 +6,7 @@ codomain: Top description: This functor maps a set $X$ to the discrete topological space $D(X) \coloneqq (X, P(X))$ in which every subset is open. It is a typical example of a fully faithful functor that preserves finite but does not preserve infinite products. nlab_link: https://ncatlab.org/nlab/show/discrete+and+indiscrete+topology left_adjoint: null +right_adjoint: forget_topology tags: - topology diff --git a/database/data/functors/doubling_sets.yaml b/database/data/functors/doubling_sets.yaml index 56727bfd3..79e27eea9 100644 --- a/database/data/functors/doubling_sets.yaml +++ b/database/data/functors/doubling_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a set $X$ to its double $2 X \coloneqq X + X$. It is a simple example of a polynomial functor. nlab_link: null left_adjoint: null +right_adjoint: squaring_sets tags: - set theory diff --git a/database/data/functors/empty_sets.yaml b/database/data/functors/empty_sets.yaml index b6cbaddf2..6a20120e7 100644 --- a/database/data/functors/empty_sets.yaml +++ b/database/data/functors/empty_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: 'Every category $\C$ has a unique functor $!_{\C} : \varnothing \to \C$. Here, we specify $\C = \Set$, but most of the properties do not depend on the choice of $\C$, as long as $\C$ is non-empty. This is the simplest example of a functor to $\Set$ that is both continuous and cocontinuous, but is neither representable nor a left or right adjoint.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - set theory diff --git a/database/data/functors/enveloping_group.yaml b/database/data/functors/enveloping_group.yaml index d0204fab2..260df85bd 100644 --- a/database/data/functors/enveloping_group.yaml +++ b/database/data/functors/enveloping_group.yaml @@ -6,6 +6,7 @@ codomain: Grp description: 'This functor maps a monoid $M$ to the group $F(M)$ that is equipped with a universal homomorphism $i_M : M \to F(M)$. It is called the (universal) enveloping group or the group completion of $M$; in the commutative case, it is known as the Grothendieck group of $M$. As a possible construction of $F(M)$, take the free group on generators $\underline{m}$ for $m \in M$ subject to the relations $\underline{1} = 1$ and $\underline{m \cdot n} = \underline{m} \cdot \underline{n}$.' nlab_link: https://ncatlab.org/nlab/show/free+functor left_adjoint: null +right_adjoint: forget_inverses tags: - algebra diff --git a/database/data/functors/forget_abelian.yaml b/database/data/functors/forget_abelian.yaml index b4d36e898..77c3f8c3d 100644 --- a/database/data/functors/forget_abelian.yaml +++ b/database/data/functors/forget_abelian.yaml @@ -6,6 +6,7 @@ codomain: Grp description: This functor maps an abelian group to itself, considered merely as a group. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: abelianization +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_addition.yaml b/database/data/functors/forget_addition.yaml index a954e4a82..778b44d9a 100644 --- a/database/data/functors/forget_addition.yaml +++ b/database/data/functors/forget_addition.yaml @@ -6,6 +6,7 @@ codomain: Mon description: This functor maps a ring to its underlying multiplicative monoid, which as "forgotten" the addition of the ring. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: monoid_ring +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_commutative.yaml b/database/data/functors/forget_commutative.yaml index 0e50c8b45..fe2a22415 100644 --- a/database/data/functors/forget_commutative.yaml +++ b/database/data/functors/forget_commutative.yaml @@ -6,6 +6,7 @@ codomain: Ring description: This is the inclusion functor $\CRing \hookrightarrow \Ring$ that maps a commutative ring to itself, regarded merely as a ring. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null # TODO: add the left adjoint to the database +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_finite.yaml b/database/data/functors/forget_finite.yaml index 9996e27cc..cd6f87e34 100644 --- a/database/data/functors/forget_finite.yaml +++ b/database/data/functors/forget_finite.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor is the inclusion functor $\FinSet \hookrightarrow \Set$ mapping a finite set to itself. It can also be regarded as a forgetful functor since it makes finite sets "forget" their finiteness. The functor is a basic example of a representable functor which is not a right adjoint. nlab_link: null left_adjoint: null +right_adjoint: null tags: - set theory diff --git a/database/data/functors/forget_finite_abelian_group.yaml b/database/data/functors/forget_finite_abelian_group.yaml index 4afaac996..649147eb1 100644 --- a/database/data/functors/forget_finite_abelian_group.yaml +++ b/database/data/functors/forget_finite_abelian_group.yaml @@ -6,6 +6,7 @@ codomain: Ab description: 'This is the inclusion functor $\FinAb \hookrightarrow \Ab$ that maps a finite abelian group to itself, regarded as an abelian group that has "forgotten" that it is finite. It provides an example of a fully faithful functor that is neither finitary nor cofinitary.' nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_finite_group.yaml b/database/data/functors/forget_finite_group.yaml index 0d87d5de4..55b235457 100644 --- a/database/data/functors/forget_finite_group.yaml +++ b/database/data/functors/forget_finite_group.yaml @@ -6,6 +6,7 @@ codomain: Grp description: 'This is the inclusion functor $\FinGrp \hookrightarrow \Grp$. It can also be viewed as a forgetful functor that forgets the property of being finite. Among other things, it provides an example of a fully faithful functor that is neither finitary nor cofinitary.' nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_group.yaml b/database/data/functors/forget_group.yaml index e88b3777d..50fead21b 100644 --- a/database/data/functors/forget_group.yaml +++ b/database/data/functors/forget_group.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a group $G$ to its underlying set $U_{\Grp}(G)$. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: free_group +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_group_pointed.yaml b/database/data/functors/forget_group_pointed.yaml index 776ca0ebe..bb5141854 100644 --- a/database/data/functors/forget_group_pointed.yaml +++ b/database/data/functors/forget_group_pointed.yaml @@ -6,6 +6,7 @@ codomain: Set_* description: This functor maps a group $G$ to its underlying pointed set $U_{\Grp,\Set_*}(G)$, whose base point is the identity element of $G$. It is an example of an essentially surjective functor which is not right-invertible. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_hausdorff.yaml b/database/data/functors/forget_hausdorff.yaml index 5cd125196..a4b70c6cb 100644 --- a/database/data/functors/forget_hausdorff.yaml +++ b/database/data/functors/forget_hausdorff.yaml @@ -6,6 +6,7 @@ codomain: Top description: This is the inclusion functor $\Haus \hookrightarrow \Top$ that maps a Hausdorff space to itself. It can also be viewed as a forgetful functor, since Hausdorff spaces "forget" that they are Hausdorff. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null # TODO: add the Hausdorff reflection functor +right_adjoint: null tags: - topology diff --git a/database/data/functors/forget_inverses.yaml b/database/data/functors/forget_inverses.yaml index be8d4a8ee..f25cfbc02 100644 --- a/database/data/functors/forget_inverses.yaml +++ b/database/data/functors/forget_inverses.yaml @@ -6,6 +6,7 @@ codomain: Mon description: This functor maps a group to its underlying monoid. We view groups as structured sets $(X,m,e,i)$ (consisting of a set, a multiplication, a neutral element, and an inverse operation), and monoids as structured sets $(X,m,e)$. This forgetful functor precisely maps $(X,m,e,i)$ to $(X,m,e)$. From this point of view, it does not merely forget a property; it forgets an operation. This perspective is useful in contexts where the inverse operation is no longer reducible to a property, for example, the forgetful functor from topological groups to topological monoids. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: enveloping_group +right_adjoint: group_units tags: - algebra diff --git a/database/data/functors/forget_ring.yaml b/database/data/functors/forget_ring.yaml index 36ac92478..5199e2b25 100644 --- a/database/data/functors/forget_ring.yaml +++ b/database/data/functors/forget_ring.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a ring $R$ to its underlying set $U_{\Ring}(R)$. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_topology.yaml b/database/data/functors/forget_topology.yaml index 3cd74fd04..d5e9eb59a 100644 --- a/database/data/functors/forget_topology.yaml +++ b/database/data/functors/forget_topology.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a topological space $X$ to its underlying set $U_{\Top}(X)$. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: discrete_topology +right_adjoint: indiscrete_topology tags: - topology diff --git a/database/data/functors/forget_torsion.yaml b/database/data/functors/forget_torsion.yaml index 1cc5bd192..adbcfa047 100644 --- a/database/data/functors/forget_torsion.yaml +++ b/database/data/functors/forget_torsion.yaml @@ -6,6 +6,7 @@ codomain: Ab description: 'This is the inclusion functor $\TorsAb \hookrightarrow \Ab$. It can also be viewed as a forgetful functor that forgets the property of being torsion. It is a typical example of a fully faithful functor that preserves finite products but does not preserve infinite products.' nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null # we only have the torsion functor Ab -> Ab in the database, not Ab -> TorsAb +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_torsion_free.yaml b/database/data/functors/forget_torsion_free.yaml index 5c4a3e619..c52066873 100644 --- a/database/data/functors/forget_torsion_free.yaml +++ b/database/data/functors/forget_torsion_free.yaml @@ -6,6 +6,7 @@ codomain: Ab description: 'This is the inclusion functor $\TorsFreeAb \hookrightarrow \Ab$. It can also be seen as a forgetful functor which forgets the property of being torsion-free. The functor provides a typical example of a fully faithful functor that does not preserve coequalizers and does not preserve epimorphisms.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_vector.yaml b/database/data/functors/forget_vector.yaml index bfa2df0ff..6923a81d9 100644 --- a/database/data/functors/forget_vector.yaml +++ b/database/data/functors/forget_vector.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a vector space $V$ (over a fixed field $K$) to its underlying set $U_{\Vect}(V)$. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/free_group.yaml b/database/data/functors/free_group.yaml index 89d47b9a8..d08c7edba 100644 --- a/database/data/functors/free_group.yaml +++ b/database/data/functors/free_group.yaml @@ -6,6 +6,7 @@ codomain: Grp description: This functor maps a set $X$ to the free group $F_{\Grp}(X)$ on that set. In the proofs, we abbreviate $F \coloneqq F_{\Grp}$. nlab_link: https://ncatlab.org/nlab/show/free+functor left_adjoint: null +right_adjoint: forget_group tags: - algebra diff --git a/database/data/functors/group_units.yaml b/database/data/functors/group_units.yaml index ad6f6312b..b8329db92 100644 --- a/database/data/functors/group_units.yaml +++ b/database/data/functors/group_units.yaml @@ -6,6 +6,7 @@ codomain: Grp description: This functor maps a monoid $M$ to its group of units $M^{\times}$, consisting of pairs $(a,b) \in M^2$ satisfying $ab=ba=1$. Equivalently, it takes the submonoid of invertible elements of $M$, equipped with the inverse operation. nlab_link: https://ncatlab.org/nlab/show/group+of+units left_adjoint: forget_inverses +right_adjoint: null tags: - algebra diff --git a/database/data/functors/id_Set.yaml b/database/data/functors/id_Set.yaml index 607ae5945..fd8a13b72 100644 --- a/database/data/functors/id_Set.yaml +++ b/database/data/functors/id_Set.yaml @@ -6,6 +6,7 @@ codomain: Set description: 'Every category $\C$ has an identity functor $\id_{\C} : \C \to \C$. Here, we specify that $\C$ is the category of sets.' nlab_link: https://ncatlab.org/nlab/show/identity+functor left_adjoint: id_Set +right_adjoint: id_Set tags: - set theory diff --git a/database/data/functors/inclusion_ordinals.yaml b/database/data/functors/inclusion_ordinals.yaml index 2e7c98554..3c7d64990 100644 --- a/database/data/functors/inclusion_ordinals.yaml +++ b/database/data/functors/inclusion_ordinals.yaml @@ -6,6 +6,7 @@ codomain: On description: 'This is the inclusion map from the partially ordered set $(\IN \cup \{\infty\},\leq)$ (considered as a thin category as usual) into the partially ordered collection $(\On,\leq)$, where we map $\infty$ to the ordinal $\omega$. It is an example of a functor that preserves binary products, but not terminal objects.' nlab_link: https://ncatlab.org/nlab/show/identity+functor left_adjoint: null +right_adjoint: null tags: - set theory diff --git a/database/data/functors/indiscrete_topology.yaml b/database/data/functors/indiscrete_topology.yaml index 31593840f..ebda9939b 100644 --- a/database/data/functors/indiscrete_topology.yaml +++ b/database/data/functors/indiscrete_topology.yaml @@ -6,6 +6,7 @@ codomain: Top description: This functor maps a set $X$ to the indiscrete topological space $I(X) \coloneqq (X, \{\varnothing,X\})$ in which only the empty set and $X$ are open. nlab_link: https://ncatlab.org/nlab/show/discrete+and+indiscrete+topology left_adjoint: forget_topology +right_adjoint: null tags: - topology diff --git a/database/data/functors/modulo-p.yaml b/database/data/functors/modulo-p.yaml index 74b4bc9ef..7c6789a07 100644 --- a/database/data/functors/modulo-p.yaml +++ b/database/data/functors/modulo-p.yaml @@ -6,6 +6,7 @@ codomain: Ab description: This functor maps an abelian group $A$ to the quotient $T^p(A) \coloneqq A/pA$, where $p$ is a fixed prime number. This group can also be represented as $A \otimes \IZ/p$. nlab_link: null left_adjoint: null +right_adjoint: p-torsion tags: - algebra diff --git a/database/data/functors/monoid_ring.yaml b/database/data/functors/monoid_ring.yaml index 673b5ca35..c3f7a35e9 100644 --- a/database/data/functors/monoid_ring.yaml +++ b/database/data/functors/monoid_ring.yaml @@ -6,6 +6,7 @@ codomain: Ring description: This functor maps a monoid $M$ to the monoid ring $\IZ[M]$, which consists of finite sums of elements in $M$. nlab_link: https://ncatlab.org/nlab/show/group+algebra left_adjoint: null +right_adjoint: forget_addition tags: - algebra diff --git a/database/data/functors/morphism_endpoints_inclusion.yaml b/database/data/functors/morphism_endpoints_inclusion.yaml index 6bb78f1d0..0de43353f 100644 --- a/database/data/functors/morphism_endpoints_inclusion.yaml +++ b/database/data/functors/morphism_endpoints_inclusion.yaml @@ -6,6 +6,7 @@ codomain: walking_morphism description: This is the functor that embeds the discrete category $\{0,1\}$ into the walking morphism $\{0 \to 1\}$. It provides an example of a faithful functor that is full on isomorphisms but not full. nlab_link: null left_adjoint: null +right_adjoint: null tags: - category theory diff --git a/database/data/functors/nerve.yaml b/database/data/functors/nerve.yaml index c827c6736..9c13396d0 100644 --- a/database/data/functors/nerve.yaml +++ b/database/data/functors/nerve.yaml @@ -6,6 +6,7 @@ codomain: sSet description: The nerve of a small category $\C$ is the simplicial set $N(\C)$ whose $n$-simplices are chains of morphisms $X_0 \to \cdots \to X_n$. Among other things, it provides an example of a fully faithful functor that does not preserve regular epimorphisms. nlab_link: https://ncatlab.org/nlab/show/nerve left_adjoint: null +right_adjoint: null tags: - category theory diff --git a/database/data/functors/opposite_category.yaml b/database/data/functors/opposite_category.yaml index 6532ff0da..508c338f0 100644 --- a/database/data/functors/opposite_category.yaml +++ b/database/data/functors/opposite_category.yaml @@ -6,6 +6,7 @@ codomain: Cat description: 'This functor maps a small category $\C$ to its opposite category $\C^{\op}$ and a functor $F : \C \to \D$ to the opposite functor $F^{\op} : \C^{\op} \to \D^{\op}$.' nlab_link: https://ncatlab.org/nlab/show/opposite+category left_adjoint: opposite_category +right_adjoint: opposite_category tags: - category theory diff --git a/database/data/functors/opposite_monoid.yaml b/database/data/functors/opposite_monoid.yaml index d9837087d..5b0ca1360 100644 --- a/database/data/functors/opposite_monoid.yaml +++ b/database/data/functors/opposite_monoid.yaml @@ -6,6 +6,7 @@ codomain: Mon description: 'This functor maps a monoid $M$ to its opposite monoid $M^{\op}$ which has the multiplication $a *^{\op} b \coloneqq a * b$. A monoid homomorphism $f : M \to N$ is also a monoid homomorphism $f^{\op} : M^{\op} \to N^{\op}$.' nlab_link: https://ncatlab.org/nlab/show/opposite+magma left_adjoint: opposite_monoid +right_adjoint: opposite_monoid tags: - algebra diff --git a/database/data/functors/p-torsion.yaml b/database/data/functors/p-torsion.yaml index 26a4c043d..00e54523f 100644 --- a/database/data/functors/p-torsion.yaml +++ b/database/data/functors/p-torsion.yaml @@ -9,6 +9,7 @@ description: >- where $p$ is a fixed prime number. This group can also be represented as $\HomInternal(\IZ/p,A)$. nlab_link: null left_adjoint: modulo-p +right_adjoint: null tags: - algebra diff --git a/database/data/functors/pi_0.yaml b/database/data/functors/pi_0.yaml index 32fa83bea..509a2aa18 100644 --- a/database/data/functors/pi_0.yaml +++ b/database/data/functors/pi_0.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a topological space $X$ to its set $\pi_0(X)$ of path components. Thus, $\pi_0(X) = U(X) / {\sim}$, where $U(X)$ is the underlying set and $x \sim y$ when there is a path from $x$ to $y$. nlab_link: https://ncatlab.org/nlab/show/connected+space left_adjoint: null +right_adjoint: null tags: - topology diff --git a/database/data/functors/pi_1.yaml b/database/data/functors/pi_1.yaml index b5295d99b..33768be6b 100644 --- a/database/data/functors/pi_1.yaml +++ b/database/data/functors/pi_1.yaml @@ -6,6 +6,7 @@ codomain: Grp description: The fundamental group $\pi_1(X,x_0)$ of a pointed topological space $(X,x_0)$ is the group of homotopy classes of loops at $x_0$. The group operation is concatenation of paths. For example, we have $\pi_1(S^1,1) \cong \IZ$ (see Hatcher's Algebraic Topology, Theorem 1.7). nlab_link: https://ncatlab.org/nlab/show/fundamental+group left_adjoint: null +right_adjoint: null tags: - topology diff --git a/database/data/functors/power_set_contravariant.yaml b/database/data/functors/power_set_contravariant.yaml index 4a020b963..f0f6599d8 100644 --- a/database/data/functors/power_set_contravariant.yaml +++ b/database/data/functors/power_set_contravariant.yaml @@ -6,6 +6,7 @@ codomain: 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 left_adjoint: null +right_adjoint: null tags: - set theory diff --git a/database/data/functors/power_set_covariant.yaml b/database/data/functors/power_set_covariant.yaml index 1533afd21..31f11461e 100644 --- a/database/data/functors/power_set_covariant.yaml +++ b/database/data/functors/power_set_covariant.yaml @@ -6,6 +6,7 @@ codomain: Set 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 left_adjoint: null +right_adjoint: null tags: - set theory diff --git a/database/data/functors/rational_product.yaml b/database/data/functors/rational_product.yaml index 9be781954..a0ab1bea9 100644 --- a/database/data/functors/rational_product.yaml +++ b/database/data/functors/rational_product.yaml @@ -6,6 +6,7 @@ codomain: Top description: This functor maps a topological space $X$ to the topological space $X \times \IQ$, where $\IQ \subseteq \IR$ carries the usual topology. It is a typical example of a functor that preserves epimorphisms but not regular epimorphisms. nlab_link: null left_adjoint: null +right_adjoint: null tags: - topology diff --git a/database/data/functors/ring_idempotents.yaml b/database/data/functors/ring_idempotents.yaml index 510453c04..cd7bb6f68 100644 --- a/database/data/functors/ring_idempotents.yaml +++ b/database/data/functors/ring_idempotents.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor sends a ring $R$ to its set $\Id(R)$ of idempotent elements. A ring homomorphism $R \to S$ restricts to a map $\Id(R) \to \Id(S)$. Among other things, it provides an example of a representable functor that does not preserve regular epimorphisms. nlab_link: null left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/sequences_sets.yaml b/database/data/functors/sequences_sets.yaml index ea1427914..ec7363fdb 100644 --- a/database/data/functors/sequences_sets.yaml +++ b/database/data/functors/sequences_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a set $X$ to the countable power $X^{\IN}$, i.e. the set of sequences in $X$. It is an example of a polynomial functor. It is also an example of a monadic functor for which the crude monadicity theorem does not apply. nlab_link: null left_adjoint: countable_copower_sets +right_adjoint: null tags: - set theory diff --git a/database/data/functors/simple_group_probing.yaml b/database/data/functors/simple_group_probing.yaml index 1643e8cb8..60edf66e0 100644 --- a/database/data/functors/simple_group_probing.yaml +++ b/database/data/functors/simple_group_probing.yaml @@ -12,6 +12,7 @@ description: >- This is the canonical example of a continuous functor $\Grp \to \Set$ that is not representable, and not a right adjoint. nlab_link: null left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/span_endpoints_inclusion.yaml b/database/data/functors/span_endpoints_inclusion.yaml index f4ad455e7..6a82fd1a7 100644 --- a/database/data/functors/span_endpoints_inclusion.yaml +++ b/database/data/functors/span_endpoints_inclusion.yaml @@ -6,6 +6,7 @@ codomain: walking_span description: This is the functor that embeds the discrete category $\{1,2\}$ into the walking span $\{1 \leftarrow 0 \rightarrow 2\}$. Among other things, it provides an example of a fully faithful functor which is not left-invertible. nlab_link: null left_adjoint: null +right_adjoint: null tags: - category theory diff --git a/database/data/functors/squaring_sets.yaml b/database/data/functors/squaring_sets.yaml index e95e558a9..59b1a4898 100644 --- a/database/data/functors/squaring_sets.yaml +++ b/database/data/functors/squaring_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a set $X$ to its square $X^2$. It is a simple example of a polynomial functor. nlab_link: null left_adjoint: doubling_sets +right_adjoint: null tags: - set theory diff --git a/database/data/functors/stone-cech-compactification.yaml b/database/data/functors/stone-cech-compactification.yaml index 165f1443b..9b43842e2 100644 --- a/database/data/functors/stone-cech-compactification.yaml +++ b/database/data/functors/stone-cech-compactification.yaml @@ -9,6 +9,7 @@ description: >- Among other things, this functor provides an example of a reflector that does not preserve binary products. nlab_link: https://ncatlab.org/nlab/show/Stone-%C4%8Cech+compactification left_adjoint: null +right_adjoint: null tags: - topology diff --git a/database/data/functors/torsion.yaml b/database/data/functors/torsion.yaml index 50f0778ba..3fab4b8fe 100644 --- a/database/data/functors/torsion.yaml +++ b/database/data/functors/torsion.yaml @@ -8,6 +8,7 @@ description: >- $$T(A) \coloneqq \{a \in A : \exists n \geq 1 \, (na = 0)\}.$$ nlab_link: https://ncatlab.org/nlab/show/torsion+subgroup left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/trivial_BG.yaml b/database/data/functors/trivial_BG.yaml index 205035760..51582aed3 100644 --- a/database/data/functors/trivial_BG.yaml +++ b/database/data/functors/trivial_BG.yaml @@ -6,6 +6,7 @@ codomain: '1' description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the delooping of a non-trivial group $G$. It is a basic example of a conservative functor which is not faithful.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/trivial_Idem.yaml b/database/data/functors/trivial_Idem.yaml index af27dd9bc..1c31eb27b 100644 --- a/database/data/functors/trivial_Idem.yaml +++ b/database/data/functors/trivial_Idem.yaml @@ -6,6 +6,7 @@ codomain: '1' description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the walking idempotent. It is a basic example of an essentially injective functor which is not conservative.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - category theory diff --git a/database/data/functors/trivial_groups.yaml b/database/data/functors/trivial_groups.yaml index 112e6d358..0d40eb32a 100644 --- a/database/data/functors/trivial_groups.yaml +++ b/database/data/functors/trivial_groups.yaml @@ -6,6 +6,7 @@ codomain: '1' description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of groups. It is a basic example of a full functor which is not faithful.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/trivial_sets.yaml b/database/data/functors/trivial_sets.yaml index aaa860557..86e3226d1 100644 --- a/database/data/functors/trivial_sets.yaml +++ b/database/data/functors/trivial_sets.yaml @@ -6,6 +6,7 @@ codomain: '1' description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of sets.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - set theory diff --git a/database/data/functors/walking_isomorphism_object_inclusion.yaml b/database/data/functors/walking_isomorphism_object_inclusion.yaml index 8955508cb..2a504dbd1 100644 --- a/database/data/functors/walking_isomorphism_object_inclusion.yaml +++ b/database/data/functors/walking_isomorphism_object_inclusion.yaml @@ -6,6 +6,7 @@ codomain: walking_isomorphism description: 'This is the natural embedding of the trivial category with a single object $0$ into the walking isomorphism given by two objects $0,1$ and an isomorphism $0 \to 1$. This is the simplest example of an equivalence of categories which is not an isomorphism.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - category theory diff --git a/database/data/functors/walking_morphism_representation.yaml b/database/data/functors/walking_morphism_representation.yaml index 0a7acf257..2691d2b36 100644 --- a/database/data/functors/walking_morphism_representation.yaml +++ b/database/data/functors/walking_morphism_representation.yaml @@ -6,6 +6,7 @@ codomain: Set description: This is the functor $I \to \Set$ that maps the universal morphism $0 \to 1$ to the unique map $\varnothing \to \{*\}$ in $\Set$. It provides a very simple example of a functor that preserves coequalizers (and hence regular epimorphisms) but does not preserve epimorphisms. nlab_link: null left_adjoint: null +right_adjoint: null tags: - category theory diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index 85a6b4867..7d40a0ca4 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -30,11 +30,13 @@ VALUES ('codomain', 'functor', 'category', TRUE), ('category', 'morphism', 'category', TRUE), ('underlying_category', 'symmetric_monoidal_category', 'category', TRUE), - ('left_adjoint', 'functor', 'functor', FALSE); + ('left_adjoint', 'functor', 'functor', FALSE), + ('right_adjoint', 'functor', 'functor', FALSE); -- TODO: perhaps make dual a structure_map (with required = FALSE) -- TODO: perhaps also "parent" -- TODO: check that domain and codomain of functor match +-- TODO: check that right_adjoint and left_adjoint are symmetric CREATE TABLE structures ( id TEXT PRIMARY KEY, diff --git a/src/lib/server/fetchers/functor.ts b/src/lib/server/fetchers/functor.ts index a2509b606..7f829d069 100644 --- a/src/lib/server/fetchers/functor.ts +++ b/src/lib/server/fetchers/functor.ts @@ -65,11 +65,11 @@ export function fetch_functor(id: string) { s.notation FROM structure_map_assignments a INNER JOIN structures s - ON s.id = a.structure_id + ON s.id = a.mapped_structure_id WHERE a.type = 'functor' - AND a.mapped_structure_id = ? - AND a.map = 'left_adjoint'` + AND a.structure_id = ? + AND a.map = 'right_adjoint'` ) .get(id) From 2d4b8985d522167005ff0eb9d29d90ae96beb38a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 14 Aug 2026 23:21:57 +0200 Subject: [PATCH 6/8] add tests for adjoint functor relationships --- database/schema/001_structures.sql | 2 - database/scripts/test.ts | 145 +++++++++++++++++++++++++++++ 2 files changed, 145 insertions(+), 2 deletions(-) diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index 7d40a0ca4..c1f5fb737 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -35,8 +35,6 @@ VALUES -- TODO: perhaps make dual a structure_map (with required = FALSE) -- TODO: perhaps also "parent" --- TODO: check that domain and codomain of functor match --- TODO: check that right_adjoint and left_adjoint are symmetric CREATE TABLE structures ( id TEXT PRIMARY KEY, diff --git a/database/scripts/test.ts b/database/scripts/test.ts index 76e6b5b02..ef4b35326 100644 --- a/database/scripts/test.ts +++ b/database/scripts/test.ts @@ -53,6 +53,7 @@ function execute_tests() { { forget_vector: forget_vector_expected }, 'functor' ) + test_adjoint_functor_relationships() devlog('\n--- Test morphisms ---') @@ -300,3 +301,147 @@ function check_link_targets_exist() { devlog(`✅ Link targets exist`) } + +/** + * Tests for functors that if L is left adjoint to R, + * then R is right adjoint to L, and vice versa. + * Also tests dom(L)=cod(R) and cod(L)=dom(R). + */ +function test_adjoint_functor_relationships() { + const asymmetric_right_pairs = db + .prepare< + never[], + { + right_1: string + left: string + right_2: string | null + } + >( + `SELECT + sm1.structure_id AS right_1, + sm1.mapped_structure_id AS left, + sm2.mapped_structure_id AS right_2 + FROM structure_map_assignments sm1 + LEFT JOIN structure_map_assignments sm2 + ON + sm2.type = 'functor' + AND sm2.structure_id = sm1.mapped_structure_id + AND sm2.map = 'right_adjoint' + WHERE + sm1.type = 'functor' + AND sm1.map = 'left_adjoint' + AND (right_2 IS NULL OR right_2 <> right_1)` + ) + .all() + + for (const { right_1, left, right_2 } of asymmetric_right_pairs) { + console.error( + `❌ The functor ${left} is left adjoint to ${right_1}, but ${right_2} is right adjoint to ${left}` + ) + } + + const asymmetric_left_pairs = db + .prepare< + never[], + { + left_1: string + right: string + left_2: string | null + } + >( + `SELECT + sm1.structure_id AS left_1, + sm1.mapped_structure_id AS right, + sm2.mapped_structure_id AS left_2 + FROM structure_map_assignments sm1 + LEFT JOIN structure_map_assignments sm2 + ON + sm2.type = 'functor' + AND sm2.structure_id = sm1.mapped_structure_id + AND sm2.map = 'left_adjoint' + WHERE + sm1.type = 'functor' + AND sm1.map = 'right_adjoint' + AND (left_2 IS NULL OR left_2 <> left_1)` + ) + .all() + + for (const { left_1, right, left_2 } of asymmetric_left_pairs) { + console.error( + `❌ The functor ${right} is right adjoint to ${left_1}, but ${left_2} is left adjoint to ${right}` + ) + } + + const incorrect_codomain_pairs = db + .prepare( + `SELECT + sm.structure_id AS functor, + sm.mapped_structure_id AS left_adjoint, + dom.mapped_structure_id AS functor_domain, + adj_cod.mapped_structure_id AS left_adjoint_codomain + FROM + structure_map_assignments sm + INNER JOIN structure_map_assignments dom + ON + dom.map = 'domain' + AND dom.type = 'functor' + AND dom.structure_id = sm.structure_id + INNER JOIN structure_map_assignments adj_cod + ON + adj_cod.map = 'codomain' + AND adj_cod.type = 'functor' + AND adj_cod.structure_id = sm.mapped_structure_id + WHERE sm.map = 'left_adjoint' + AND functor_domain <> left_adjoint_codomain + ` + ) + .all() + + for (const { functor, left_adjoint } of incorrect_codomain_pairs) { + console.error( + `❌ The functor ${left_adjoint}, the left adjoint of ${functor}, does not have the correct codomain` + ) + } + + const incorrect_domain_pairs = db + .prepare( + `SELECT + sm.structure_id AS functor, + sm.mapped_structure_id AS left_adjoint, + cod.mapped_structure_id AS functor_codomain, + adj_dom.mapped_structure_id AS left_adjoint_domain + FROM + structure_map_assignments sm + INNER JOIN structure_map_assignments cod + ON + cod.map = 'codomain' + AND cod.type = 'functor' + AND cod.structure_id = sm.structure_id + INNER JOIN structure_map_assignments adj_dom + ON + adj_dom.map = 'domain' + AND adj_dom.type = 'functor' + AND adj_dom.structure_id = sm.mapped_structure_id + WHERE sm.map = 'left_adjoint' + AND functor_codomain <> left_adjoint_domain + ` + ) + .all() + + for (const { functor, left_adjoint } of incorrect_domain_pairs) { + console.error( + `❌ The functor ${left_adjoint}, the left adjoint of ${functor}, does not have the correct domain` + ) + } + + if ( + asymmetric_right_pairs.length > 0 || + asymmetric_left_pairs.length > 0 || + incorrect_codomain_pairs.length > 0 || + incorrect_domain_pairs.length > 0 + ) { + throw new Error(`❌ Invalid adjoint functor relationships detected`) + } + + console.info('✅ Adjoint relationships are symmetric') +} From a9f103d94e320bde4ac24ea3b4d5ab0f11c6d2c3 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 15 Aug 2026 08:25:07 +0200 Subject: [PATCH 7/8] unify fetching of associated structures; remove obsolete components --- src/lib/commons/types.ts | 21 ++--- src/lib/server/fetchers/functor.ts | 83 ------------------- src/lib/server/fetchers/morphism.ts | 29 ------- src/lib/server/fetchers/structure.ts | 19 ++++- .../fetchers/symmetric_monoidal_category.ts | 32 ------- src/lib/server/transforms.ts | 15 +++- src/pages/FunctorDetailPage.svelte | 48 ----------- src/pages/MorphismDetailPage.svelte | 19 ----- src/pages/StructureDetailPage.svelte | 12 ++- ...SymmetricMonoidalCategoryDetailPage.svelte | 22 ----- src/routes/[type]/[id]/+page.server.ts | 20 +---- src/routes/[type]/[id]/+page.svelte | 23 +---- 12 files changed, 54 insertions(+), 289 deletions(-) delete mode 100644 src/lib/server/fetchers/functor.ts delete mode 100644 src/lib/server/fetchers/morphism.ts delete mode 100644 src/lib/server/fetchers/symmetric_monoidal_category.ts delete mode 100644 src/pages/FunctorDetailPage.svelte delete mode 100644 src/pages/MorphismDetailPage.svelte delete mode 100644 src/pages/SymmetricMonoidalCategoryDetailPage.svelte diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 8698087b9..5b9826228 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -13,6 +13,11 @@ export type StructureShortDictionary = Partial( - `SELECT - s.id, - s.name, - s.notation - FROM structure_map_assignments a - INNER JOIN structures s - ON s.id = a.mapped_structure_id - WHERE - a.type = 'functor' - AND a.structure_id = ? - AND a.map = 'domain'` - ) - .get(id) - - if (!domain) error(404, `No domain found for functor with ID ${id}`) - - const codomain = db - .prepare<[string], RelatedStructure>( - `SELECT - s.id, - s.name, - s.notation - FROM structure_map_assignments a - INNER JOIN structures s - ON s.id = a.mapped_structure_id - WHERE - a.type = 'functor' - AND a.structure_id = ? - AND a.map = 'codomain'` - ) - .get(id) - - if (!codomain) error(404, `No codomain found for functor with ID ${id}`) - - const left_adjoint = db - .prepare<[string], RelatedStructure>( - `SELECT - s.id, - s.name, - s.notation - FROM structure_map_assignments a - INNER JOIN structures s - ON s.id = a.mapped_structure_id - WHERE - a.type = 'functor' - AND a.structure_id = ? - AND a.map = 'left_adjoint'` - ) - .get(id) - - const right_adjoint = db - .prepare<[string], RelatedStructure>( - `SELECT - s.id, - s.name, - s.notation - FROM structure_map_assignments a - INNER JOIN structures s - ON s.id = a.mapped_structure_id - WHERE - a.type = 'functor' - AND a.structure_id = ? - AND a.map = 'right_adjoint'` - ) - .get(id) - - return { - type: 'functor' as const, - domain, - codomain, - left_adjoint, - right_adjoint - } -} diff --git a/src/lib/server/fetchers/morphism.ts b/src/lib/server/fetchers/morphism.ts deleted file mode 100644 index a44eff627..000000000 --- a/src/lib/server/fetchers/morphism.ts +++ /dev/null @@ -1,29 +0,0 @@ -import type { RelatedStructure } from '$lib/commons/types' -import { db } from '$lib/server/db' -import { error } from '@sveltejs/kit' - -export function fetch_morphism(id: string) { - // TODO: generalize this to all structures - - const category = db - .prepare<[string], RelatedStructure>( - `SELECT - s.id, - s.name, - s.notation - FROM structure_map_assignments a - INNER JOIN structures s - ON s.id = a.mapped_structure_id - WHERE - a.type = 'morphism' - AND a.structure_id = ? - AND a.map = 'category'` - ) - .get(id) - - if (!category) { - error(404, `Could not find the category of the morphism with ID '${id}'`) - } - - return { type: 'morphism' as const, category } -} diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts index b2c50b5a0..8e1edf07b 100644 --- a/src/lib/server/fetchers/structure.ts +++ b/src/lib/server/fetchers/structure.ts @@ -7,7 +7,8 @@ import type { StructureDisplay, StructureShort, StructureShortDictionary, - StructureType + StructureType, + AssociatedStructure } from '$lib/commons/types' import { error } from '@sveltejs/kit' import { db } from '$lib/server/db' @@ -39,6 +40,21 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai error(404, `Could not find ${type} with ID '${id}'`) } + const associated_structures = db + .prepare<[string], AssociatedStructure>( + `SELECT + s.id, + s.name, + s.notation, + a.map, + a.mapped_type + FROM structure_map_assignments a + INNER JOIN structures s + ON s.id = a.mapped_structure_id + WHERE a.structure_id = ?` + ) + .all(id) + const related_structures = db .prepare<[string], RelatedStructure>( `SELECT @@ -171,6 +187,7 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai structure, children, related_structures, + associated_structures, structures_based_on, tags, satisfied_properties, diff --git a/src/lib/server/fetchers/symmetric_monoidal_category.ts b/src/lib/server/fetchers/symmetric_monoidal_category.ts deleted file mode 100644 index 3551410dd..000000000 --- a/src/lib/server/fetchers/symmetric_monoidal_category.ts +++ /dev/null @@ -1,32 +0,0 @@ -import type { RelatedStructure } from '$lib/commons/types' -import { db } from '$lib/server/db' -import { error } from '@sveltejs/kit' - -export function fetch_symmetric_monoidal_category(id: string) { - // TODO: generalize this - - const underlying_category = db - .prepare<[string], RelatedStructure>( - `SELECT - s.id, - s.name, - s.notation - FROM structure_map_assignments a - INNER JOIN structures s - ON s.id = a.mapped_structure_id - WHERE - a.type = 'symmetric_monoidal_category' - AND a.structure_id = ? - AND a.map = 'underlying_category'` - ) - .get(id) - - if (!underlying_category) { - error( - 404, - `No underlying category found for symmetric monoidal category with ID ${id}` - ) - } - - return { type: 'symmetric_monoidal_category' as const, underlying_category } -} diff --git a/src/lib/server/transforms.ts b/src/lib/server/transforms.ts index 46ca3ab6f..4bd9b07a3 100644 --- a/src/lib/server/transforms.ts +++ b/src/lib/server/transforms.ts @@ -4,9 +4,10 @@ import type { PropertyAssignmentDB, PropertyAssignmentDisplay, ImplicationDB, - ImplicationDisplay + ImplicationDisplay, + StructureDetails } from '$lib/commons/types' -import { parse_nested_json_set } from '$shared/utils' +import { add_math, parse_nested_json_set, strip_math } from '$shared/utils' export function display_property(property: PropertyDB): PropertyDisplay { return { @@ -41,3 +42,13 @@ export function display_implication(implication: ImplicationDB): ImplicationDisp mapped_assumptions: parse_nested_json_set(implication.mapped_assumptions) } } + +export function adjust_functor_notation(functor: StructureDetails) { + const domain = functor.associated_structures.find((s) => s.map == 'domain') + const codomain = functor.associated_structures.find((s) => s.map == 'codomain') + if (!domain || !codomain) return + + functor.structure.notation = add_math( + `${strip_math(functor.structure.notation)}: ${strip_math(domain.notation)} \\to ${strip_math(codomain.notation)}` + ) +} diff --git a/src/pages/FunctorDetailPage.svelte b/src/pages/FunctorDetailPage.svelte deleted file mode 100644 index a69eaa9d8..000000000 --- a/src/pages/FunctorDetailPage.svelte +++ /dev/null @@ -1,48 +0,0 @@ - - - - - - {#snippet definition()} -
  • - Domain: - {data.domain.name} -
    • - -
  • - Codomain: - {data.codomain.name} -
    • - - {#if data.left_adjoint} -
  • - Left adjoint functor: - - {@html data.left_adjoint.notation} - -
    • - {/if} - - {#if data.right_adjoint} -
  • - Right adjoint functor: - - {@html data.right_adjoint.notation} - -
    • - {/if} - {/snippet} -     diff --git a/src/pages/MorphismDetailPage.svelte b/src/pages/MorphismDetailPage.svelte deleted file mode 100644 index 75fdef181..000000000 --- a/src/pages/MorphismDetailPage.svelte +++ /dev/null @@ -1,19 +0,0 @@ - - - - {#snippet definition()} -
  • - Category: - - {data.category.name} - -
    • - {/snippet} -     diff --git a/src/pages/StructureDetailPage.svelte b/src/pages/StructureDetailPage.svelte index 00c3bb87a..716bf3ae9 100644 --- a/src/pages/StructureDetailPage.svelte +++ b/src/pages/StructureDetailPage.svelte @@ -8,6 +8,7 @@ import StructuresBasedOn from '$components/StructuresBasedOn.svelte' import { PLURALS } from '$shared/config' import type { + AssociatedStructure, CommentObject, PropertyAssignmentDisplay, PropertyShort, @@ -18,11 +19,12 @@ StructureType } from '$lib/commons/types' import type { Snippet } from 'svelte' - import { remove_underscores } from '$shared/utils' + import { capitalize, remove_underscores } from '$shared/utils' type Props = { type: StructureType structure: StructureDisplay + associated_structures: AssociatedStructure[] related_structures: RelatedStructure[] structures_based_on: StructureShortDictionary children: RelatedStructure[] @@ -40,6 +42,7 @@ let { type, structure, + associated_structures, related_structures, structures_based_on, children, @@ -70,6 +73,13 @@ {@render definition?.()} + {#each associated_structures as a} +
  • + {capitalize(remove_underscores(a.map))}: + {a.name} +
    • + {/each} + {#if structure.parent}
  • Parent: diff --git a/src/pages/SymmetricMonoidalCategoryDetailPage.svelte b/src/pages/SymmetricMonoidalCategoryDetailPage.svelte deleted file mode 100644 index 204394e00..000000000 --- a/src/pages/SymmetricMonoidalCategoryDetailPage.svelte +++ /dev/null @@ -1,22 +0,0 @@ - - - - {#snippet definition()} -
  • - Underlying category: - - {data.underlying_category.name} - -
    • - {/snippet} -     diff --git a/src/routes/[type]/[id]/+page.server.ts b/src/routes/[type]/[id]/+page.server.ts index 2a97faace..73d2ace54 100644 --- a/src/routes/[type]/[id]/+page.server.ts +++ b/src/routes/[type]/[id]/+page.server.ts @@ -3,17 +3,7 @@ import { fetch_structure } from '$lib/server/fetchers/structure' import { is_structure_type } from '$shared/config' import { error } from '@sveltejs/kit' import { fetch_category } from '$lib/server/fetchers/category' -import { fetch_functor } from '$lib/server/fetchers/functor' -import { fetch_morphism } from '$lib/server/fetchers/morphism' -import { add_math, strip_math } from '$shared/utils' -import { fetch_symmetric_monoidal_category } from '$lib/server/fetchers/symmetric_monoidal_category' - -const special_fetchers = { - category: fetch_category, - functor: fetch_functor, - morphism: fetch_morphism, - symmetric_monoidal_category: fetch_symmetric_monoidal_category -} +import { adjust_functor_notation } from '$lib/server/transforms' export const load = (event) => { const type = event.params.type @@ -23,13 +13,9 @@ export const load = (event) => { const structure_data = fetch_structure(type, id) - const special_structure_data = special_fetchers[type](id) + if (type === 'functor') adjust_functor_notation(structure_data) - if (special_structure_data.type === 'functor') { - structure_data.structure.notation = add_math( - `${strip_math(structure_data.structure.notation)}: ${strip_math(special_structure_data.domain.notation)} \\to ${strip_math(special_structure_data.codomain.notation)}` - ) - } + const special_structure_data = type === 'category' ? fetch_category(id) : { type } return render_nested_formulas({ structure_data, diff --git a/src/routes/[type]/[id]/+page.svelte b/src/routes/[type]/[id]/+page.svelte index da567a1e3..51e3acc60 100644 --- a/src/routes/[type]/[id]/+page.svelte +++ b/src/routes/[type]/[id]/+page.svelte @@ -1,29 +1,12 @@ - - {#if data.special_structure_data.type === 'category'} -{/if} - -{#if data.special_structure_data.type === 'functor'} - -{/if} - -{#if data.special_structure_data.type === 'morphism'} - -{/if} - -{#if data.special_structure_data.type === 'symmetric_monoidal_category'} - +{:else} + {/if} From 393d87247ee0ae6897df8a68485e3908a694d968 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 15 Aug 2026 08:34:31 +0200 Subject: [PATCH 8/8] ensure that required associated structures are set in seed script --- database/schema/001_structures.sql | 2 -- database/scripts/seed.ts | 20 +++++++++++++++----- 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index c1f5fb737..37aa6bcd7 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -21,8 +21,6 @@ CREATE TABLE structure_maps ( FOREIGN KEY (mapped_type) REFERENCES structure_types (type) ON DELETE CASCADE ); --- TODO: check somewhere that the required fields are indeed filled for every structure. - INSERT INTO structure_maps (map, type, mapped_type, required) VALUES diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index 3adccbe4d..1ed21d37f 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -11,7 +11,7 @@ import type { } from './utils/seed.types' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' import { STRUCTURE_TYPES, type StructureType, PLURALS } from '$shared/config' -import { are_disjoint, devlog } from '$shared/utils' +import { are_disjoint, capitalize, devlog } from '$shared/utils' const db = get_client({ readonly: false }) @@ -208,8 +208,11 @@ function seed_structures({ extra?: (structure: T) => void }) { const structure_maps = db - .prepare<[StructureType], { map: keyof T; mapped_type: StructureType }>( - `SELECT map, mapped_type + .prepare< + [StructureType], + { map: keyof T; mapped_type: StructureType; required: 0 | 1 } + >( + `SELECT map, mapped_type, required FROM structure_maps WHERE type = ?` ) .all(type) @@ -282,7 +285,14 @@ function seed_structures({ structure.parent || null ) - for (const { map, mapped_type } of structure_maps) { + for (const { map, mapped_type, required } of structure_maps) { + if (required && !structure[map]) { + console.error( + `❌ ${capitalize(type)} "${structure.id}" has no ${map.toString()}` + ) + process.exit(1) + } + if (structure[map]) { structure_map_assignment_insert.run( map, @@ -295,7 +305,7 @@ function seed_structures({ } if (!structure.tags.length) { - console.error(`❌ Structure "${structure.id}" has no tags`) + console.error(`❌ ${capitalize(type)} "${structure.id}" has no tags`) process.exit(1) }