From 95c7ca1d07e99a09dd325bc2b83df3249d15f654 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 14 Aug 2026 17:37:39 +0200 Subject: [PATCH 01/13] 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 02/13] 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 03/13] 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 04/13] 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 05/13] 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 e660cd171494e43aa8e002f07fb1ac5f698051b8 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 14 Aug 2026 23:21:57 +0200 Subject: [PATCH 06/13] add tests for adjoint functor relationships --- database/schema/001_structures.sql | 2 - database/scripts/test.ts | 118 +++++++++++++++++++++++++++++ 2 files changed, 118 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..b0d084fb9 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,120 @@ 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 checks: Array<{ + query: string + format: (row: Record) => string + }> = [ + { + query: ` + 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) + `, + format: ({ right_1, left, right_2 }) => + `❌ Adjoint asymmetry: ${left} is declared as left adjoint to ${right_1}, but ${right_2 ?? 'no functor'} is recorded as its right adjoint.` + }, + { + query: ` + 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) + `, + format: ({ left_1, right, left_2 }) => + `❌ Adjoint asymmetry: ${right} is declared as right adjoint to ${left_1}, but ${left_2 ?? 'no functor'} is recorded as its left adjoint.` + }, + { + query: ` + 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 + `, + format: ({ functor, left_adjoint, functor_domain, left_adjoint_codomain }) => + `❌ Domain/codomain mismatch: ${functor} has domain ${functor_domain}, but its left adjoint ${left_adjoint} has codomain ${left_adjoint_codomain}.` + }, + { + query: ` + 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`, + format: ({ functor, left_adjoint, functor_codomain, left_adjoint_domain }) => + `❌ Domain/codomain mismatch: ${functor} has codomain ${functor_codomain}, but its left adjoint ${left_adjoint} has domain ${left_adjoint_domain}.` + } + ] + + const violations = checks.flatMap(({ query, format }) => + db + .prepare>(query) + .all() + .map((row) => format(row)) + ) + + if (violations.length > 0) { + throw new Error(violations.join('\n')) + } + + console.info('✅ Adjoint functor relationships are valid') +} From e9fda4831bba382485bfe261e9adeb94f9a643b7 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 15 Aug 2026 08:25:07 +0200 Subject: [PATCH 07/13] 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 1af32fbb7677b3a5fbc432265ba45f36f77e192f Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 15 Aug 2026 08:34:31 +0200 Subject: [PATCH 08/13] 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) } From b5d9206fe107918d019dec46992fd4e9eb995544 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 15 Aug 2026 11:12:21 +0200 Subject: [PATCH 09/13] rename `structure_maps` to `associated_structure_types` and `structure_map_assignments` to `associated_structures` --- database/schema/001_structures.sql | 34 +++++----- database/schema/003_implications.sql | 2 +- database/scripts/deduce-implications.ts | 14 ++-- .../scripts/restrict-functor-properties.ts | 6 +- .../scripts/restrict-morphism-properties.ts | 6 +- database/scripts/seed.ts | 47 ++++++------- database/scripts/test.ts | 68 +++++++++---------- database/scripts/utils/structures.ts | 14 ++-- src/lib/commons/types.ts | 6 +- src/lib/server/fetchers/implication.ts | 18 ++--- src/lib/server/fetchers/structure.ts | 18 ++--- src/lib/server/transforms.ts | 4 +- src/pages/ImplicationPage.svelte | 18 +++-- src/pages/StructureDetailPage.svelte | 4 +- 14 files changed, 132 insertions(+), 127 deletions(-) diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index 37aa6bcd7..4df33d6ad 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -9,20 +9,20 @@ INSERT INTO structure_types (type) VALUES ('symmetric_monoidal_category'); -CREATE TABLE structure_maps ( - map TEXT NOT NULL, +CREATE TABLE associated_structure_types ( + label TEXT NOT NULL, type TEXT NOT NULL, - mapped_type TEXT NOT NULL, + associated_type TEXT NOT NULL, required INTEGER NOT NULL CHECK (required in (TRUE, FALSE)), - PRIMARY KEY (map, type, mapped_type), - UNIQUE (map, type), + PRIMARY KEY (label, type, associated_type), + UNIQUE (label, type), FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE CASCADE, - FOREIGN KEY (mapped_type) REFERENCES structure_types (type) ON DELETE CASCADE + FOREIGN KEY (associated_type) REFERENCES structure_types (type) ON DELETE CASCADE ); -INSERT INTO structure_maps - (map, type, mapped_type, required) +INSERT INTO associated_structure_types + (label, type, associated_type, required) VALUES ('domain', 'functor', 'category', TRUE), ('codomain', 'functor', 'category', TRUE), @@ -31,9 +31,6 @@ VALUES ('left_adjoint', 'functor', 'functor', FALSE), ('right_adjoint', 'functor', 'functor', FALSE); --- TODO: perhaps make dual a structure_map (with required = FALSE) --- TODO: perhaps also "parent" - CREATE TABLE structures ( id TEXT PRIMARY KEY, type TEXT NOT NULL, @@ -89,16 +86,17 @@ CREATE TABLE structure_tag_assignments ( FOREIGN KEY (tag, type) REFERENCES structure_tags (tag, type) ON DELETE CASCADE ); -CREATE TABLE structure_map_assignments ( - map TEXT NOT NULL, +CREATE TABLE associated_structures ( + label TEXT NOT NULL, type TEXT NOT NULL, - mapped_type TEXT NOT NULL, + associated_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, + associated_structure_id TEXT NOT NULL, + FOREIGN KEY (label, type, associated_type) + REFERENCES associated_structure_types (label, type, associated_type) + ON DELETE CASCADE, FOREIGN KEY (structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE, - FOREIGN KEY (mapped_structure_id, mapped_type) + FOREIGN KEY (associated_structure_id, associated_type) REFERENCES structures (id, type) ON DELETE CASCADE ); \ No newline at end of file diff --git a/database/schema/003_implications.sql b/database/schema/003_implications.sql index 0d3738df7..5e50e13b8 100644 --- a/database/schema/003_implications.sql +++ b/database/schema/003_implications.sql @@ -50,7 +50,7 @@ CREATE TABLE mapped_assumptions ( FOREIGN KEY (property_id, property_type) REFERENCES properties (id, type) ON DELETE CASCADE, FOREIGN KEY (map, type, property_type) - REFERENCES structure_maps (map, type, mapped_type) + REFERENCES associated_structure_types (label, type, associated_type) ON DELETE RESTRICT ); diff --git a/database/scripts/deduce-implications.ts b/database/scripts/deduce-implications.ts index 6eafa4966..fcc3089ae 100644 --- a/database/scripts/deduce-implications.ts +++ b/database/scripts/deduce-implications.ts @@ -24,10 +24,10 @@ export function clear_deduced_implications(type: StructureType) { * then P^op ===> Q^op holds as well. */ export function create_dualized_implications(type: StructureType) { - const structure_maps = db - .prepare<[StructureType], { map: string; mapped_type: StructureType }>( - `SELECT map, mapped_type - FROM structure_maps WHERE type = ?` + const associated_structure_types = db + .prepare<[StructureType], { label: string; associated_type: StructureType }>( + `SELECT label, associated_type + FROM associated_structure_types WHERE type = ?` ) .all(type) @@ -148,10 +148,10 @@ export function create_dualized_implications(type: StructureType) { conclusion_insert.run(dual_id, c, type) } - for (const { map, mapped_type } of structure_maps) { - const duals = dual_mapped_assumptions[map] + for (const { label, associated_type } of associated_structure_types) { + const duals = dual_mapped_assumptions[label] for (const d of duals ?? []) { - mapped_assumption_insert.run(dual_id, map, d, type, mapped_type) + mapped_assumption_insert.run(dual_id, label, d, type, associated_type) } } } diff --git a/database/scripts/restrict-functor-properties.ts b/database/scripts/restrict-functor-properties.ts index 5a8fbed22..7230b0092 100644 --- a/database/scripts/restrict-functor-properties.ts +++ b/database/scripts/restrict-functor-properties.ts @@ -36,11 +36,11 @@ function restrict_representable_functors() { 'The codomain is not $\\Set$.', TRUE, FALSE - FROM structure_map_assignments a + FROM associated_structures a WHERE a.type = 'functor' - AND a.map = 'codomain' - AND a.mapped_structure_id <> 'Set' + AND a.label = 'codomain' + AND a.associated_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 13eb177b7..e9e087f96 100644 --- a/database/scripts/restrict-morphism-properties.ts +++ b/database/scripts/restrict-morphism-properties.ts @@ -39,14 +39,14 @@ function restrict_normal_morphisms(variant: 'mono' | 'epi') { 'The ' || c.name || ' has no zero morphisms.', TRUE, FALSE - FROM structure_map_assignments sa + FROM associated_structures sa INNER JOIN structures c - ON c.id = sa.mapped_structure_id + ON c.id = sa.associated_structure_id INNER JOIN property_assignments a ON a.structure_id = c.id WHERE sa.type = 'morphism' - AND sa.map = 'category' + AND sa.label = 'category' AND a.property_id = 'zero morphisms' AND a.is_satisfied = FALSE ON CONFLICT (structure_id, property_id) diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index 1ed21d37f..515614956 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -104,7 +104,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() + db.prepare(`DELETE FROM associated_structures`).run() }) try { @@ -207,13 +207,13 @@ function seed_structures({ folder: string extra?: (structure: T) => void }) { - const structure_maps = db + const associated_structure_types = db .prepare< [StructureType], - { map: keyof T; mapped_type: StructureType; required: 0 | 1 } + { label: keyof T; associated_type: StructureType; required: 0 | 1 } >( - `SELECT map, mapped_type, required - FROM structure_maps WHERE type = ?` + `SELECT label, associated_type, required + FROM associated_structure_types WHERE type = ?` ) .all(type) @@ -253,9 +253,10 @@ function seed_structures({ ) VALUES (?, ?, ?, ?)` ) - const structure_map_assignment_insert = db.prepare( - `INSERT INTO structure_map_assignments ( - map, type, mapped_type, structure_id, mapped_structure_id + const associated_structure_insert = db.prepare( + `INSERT INTO associated_structures ( + label, type, associated_type, + structure_id, associated_structure_id ) VALUES (?, ?, ?, ?, ?)` ) @@ -285,21 +286,21 @@ function seed_structures({ structure.parent || null ) - for (const { map, mapped_type, required } of structure_maps) { - if (required && !structure[map]) { + for (const { label, associated_type, required } of associated_structure_types) { + if (required && !structure[label]) { console.error( - `❌ ${capitalize(type)} "${structure.id}" has no ${map.toString()}` + `❌ ${capitalize(type)} "${structure.id}" has no ${label.toString()}` ) process.exit(1) } - if (structure[map]) { - structure_map_assignment_insert.run( - map, + if (structure[label]) { + associated_structure_insert.run( + label, type, - mapped_type, + associated_type, structure.id, - structure[map] + structure[label] ) } } @@ -438,10 +439,10 @@ function seed_properties({ type, folder }: { type: StructureType; folder: string * Seeds all implications of a given type from YAML files. */ function seed_implications({ type, folder }: { type: StructureType; folder: string }) { - const structure_maps = db - .prepare<[StructureType], { map: string; mapped_type: StructureType }>( - `SELECT map, mapped_type - FROM structure_maps WHERE type = ?` + const associated_structure_types = db + .prepare<[StructureType], { label: string; associated_type: StructureType }>( + `SELECT label, associated_type + FROM associated_structure_types WHERE type = ?` ) .all(type) @@ -493,10 +494,10 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri if (!impl.mapped_assumptions) continue - for (const { map, mapped_type } of structure_maps) { - const assumptions = impl.mapped_assumptions[map] ?? [] + for (const { label, associated_type } of associated_structure_types) { + const assumptions = impl.mapped_assumptions[label] ?? [] for (const p of assumptions) { - mapped_assumption_insert.run(impl.id, map, p, type, mapped_type) + mapped_assumption_insert.run(impl.id, label, p, type, associated_type) } } } diff --git a/database/scripts/test.ts b/database/scripts/test.ts index b0d084fb9..79ef2c916 100644 --- a/database/scripts/test.ts +++ b/database/scripts/test.ts @@ -316,17 +316,17 @@ function test_adjoint_functor_relationships() { query: ` 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 + sm1.associated_structure_id AS left, + sm2.associated_structure_id AS right_2 + FROM associated_structures sm1 + LEFT JOIN associated_structures sm2 ON sm2.type = 'functor' - AND sm2.structure_id = sm1.mapped_structure_id - AND sm2.map = 'right_adjoint' + AND sm2.structure_id = sm1.associated_structure_id + AND sm2.label = 'right_adjoint' WHERE sm1.type = 'functor' - AND sm1.map = 'left_adjoint' + AND sm1.label = 'left_adjoint' AND (right_2 IS NULL OR right_2 <> right_1) `, format: ({ right_1, left, right_2 }) => @@ -336,17 +336,17 @@ function test_adjoint_functor_relationships() { query: ` 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 + sm1.associated_structure_id AS right, + sm2.associated_structure_id AS left_2 + FROM associated_structures sm1 + LEFT JOIN associated_structures sm2 ON sm2.type = 'functor' - AND sm2.structure_id = sm1.mapped_structure_id - AND sm2.map = 'left_adjoint' + AND sm2.structure_id = sm1.associated_structure_id + AND sm2.label = 'left_adjoint' WHERE sm1.type = 'functor' - AND sm1.map = 'right_adjoint' + AND sm1.label = 'right_adjoint' AND (left_2 IS NULL OR left_2 <> left_1) `, format: ({ left_1, right, left_2 }) => @@ -356,23 +356,23 @@ function test_adjoint_functor_relationships() { query: ` 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 + sm.associated_structure_id AS left_adjoint, + dom.associated_structure_id AS functor_domain, + adj_cod.associated_structure_id AS left_adjoint_codomain FROM - structure_map_assignments sm - INNER JOIN structure_map_assignments dom + associated_structures sm + INNER JOIN associated_structures dom ON - dom.map = 'domain' + dom.label = 'domain' AND dom.type = 'functor' AND dom.structure_id = sm.structure_id - INNER JOIN structure_map_assignments adj_cod + INNER JOIN associated_structures adj_cod ON - adj_cod.map = 'codomain' + adj_cod.label = 'codomain' AND adj_cod.type = 'functor' - AND adj_cod.structure_id = sm.mapped_structure_id + AND adj_cod.structure_id = sm.associated_structure_id WHERE - sm.map = 'left_adjoint' + sm.label = 'left_adjoint' AND functor_domain <> left_adjoint_codomain `, format: ({ functor, left_adjoint, functor_domain, left_adjoint_codomain }) => @@ -382,23 +382,23 @@ function test_adjoint_functor_relationships() { query: ` 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 + sm.associated_structure_id AS left_adjoint, + cod.associated_structure_id AS functor_codomain, + adj_dom.associated_structure_id AS left_adjoint_domain FROM - structure_map_assignments sm - INNER JOIN structure_map_assignments cod + associated_structures sm + INNER JOIN associated_structures cod ON - cod.map = 'codomain' + cod.label = 'codomain' AND cod.type = 'functor' AND cod.structure_id = sm.structure_id - INNER JOIN structure_map_assignments adj_dom + INNER JOIN associated_structures adj_dom ON - adj_dom.map = 'domain' + adj_dom.label = 'domain' AND adj_dom.type = 'functor' - AND adj_dom.structure_id = sm.mapped_structure_id + AND adj_dom.structure_id = sm.associated_structure_id WHERE - sm.map = 'left_adjoint' + sm.label = 'left_adjoint' AND functor_codomain <> left_adjoint_domain`, format: ({ functor, left_adjoint, functor_codomain, left_adjoint_domain }) => `❌ Domain/codomain mismatch: ${functor} has codomain ${functor_codomain}, but its left adjoint ${left_adjoint} has domain ${left_adjoint_domain}.` diff --git a/database/scripts/utils/structures.ts b/database/scripts/utils/structures.ts index 8d3e5d9a5..c23735c18 100644 --- a/database/scripts/utils/structures.ts +++ b/database/scripts/utils/structures.ts @@ -27,26 +27,26 @@ export function get_structures(db: Database, type: StructureType): StructureMeta properties: string } >( - `WITH mapped_properties AS ( + `WITH associated_properties AS ( SELECT s.id, s.name, s.dual_structure_id AS dual, - m.map, + m.label, json_group_array(a.property_id) AS props FROM structures s - LEFT JOIN structure_map_assignments m + LEFT JOIN associated_structures m ON m.structure_id = s.id LEFT JOIN property_assignments a - ON a.structure_id = m.mapped_structure_id + ON a.structure_id = m.associated_structure_id AND a.is_satisfied = TRUE WHERE s.type = ? - GROUP BY s.id, m.map + GROUP BY s.id, m.label ) SELECT id, name, dual, - json_group_object(map, props) AS properties - FROM mapped_properties + json_group_object(label, props) AS properties + FROM associated_properties GROUP BY id ORDER BY id` ) diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 5b9826228..dc138ac6b 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -14,8 +14,8 @@ export type StructureShortDictionary = Partial +export type AssociatedTypes = Record export type CommentObject = { id: number; comment: string } diff --git a/src/lib/server/fetchers/implication.ts b/src/lib/server/fetchers/implication.ts index e0ef45a42..09289fb0c 100644 --- a/src/lib/server/fetchers/implication.ts +++ b/src/lib/server/fetchers/implication.ts @@ -2,7 +2,7 @@ import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' import type { ImplicationDB, - MappedTypes, + AssociatedTypes, StructureShort, StructureType } from '$lib/commons/types' @@ -43,19 +43,19 @@ export function fetch_implication(type: StructureType, id: string) { ) .all(type, id) - const structure_maps = db - .prepare<[StructureType], { map: string; mapped_type: StructureType }>( - `SELECT map, mapped_type - FROM structure_maps + const associated_structure_types = db + .prepare<[StructureType], { label: string; associated_type: StructureType }>( + `SELECT label, associated_type + FROM associated_structure_types WHERE type = ?` ) .all(type) - const mapped_types: MappedTypes = {} + const associated_types: AssociatedTypes = {} - for (const { map, mapped_type } of structure_maps) { - mapped_types[map] = mapped_type + for (const { label, associated_type } of associated_structure_types) { + associated_types[label] = associated_type } - return { type, implication, property_relation_dict, structures, mapped_types } + return { type, implication, property_relation_dict, structures, associated_types } } diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts index 8e1edf07b..5b279865e 100644 --- a/src/lib/server/fetchers/structure.ts +++ b/src/lib/server/fetchers/structure.ts @@ -46,11 +46,11 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai s.id, s.name, s.notation, - a.map, - a.mapped_type - FROM structure_map_assignments a + a.label, + a.associated_type + FROM associated_structures a INNER JOIN structures s - ON s.id = a.mapped_structure_id + ON s.id = a.associated_structure_id WHERE a.structure_id = ?` ) .all(id) @@ -71,15 +71,15 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai const list_structures_based_on = db .prepare<[string], StructureShort & { type: StructureType }>( `SELECT DISTINCT s.id, s.name, a.type - FROM structure_map_assignments a + FROM associated_structures a INNER JOIN structures s ON s.id = a.structure_id - INNER JOIN structure_maps m + INNER JOIN associated_structure_types m ON - m.map = a.map + m.label = a.label AND m.type = a.type - AND m.mapped_type = a.mapped_type - WHERE a.mapped_structure_id = ? AND m.required = TRUE + AND m.associated_type = a.associated_type + WHERE a.associated_structure_id = ? AND m.required = TRUE ORDER BY a.type, lower(s.name)` ) .all(id) diff --git a/src/lib/server/transforms.ts b/src/lib/server/transforms.ts index 4bd9b07a3..1c0fcc309 100644 --- a/src/lib/server/transforms.ts +++ b/src/lib/server/transforms.ts @@ -44,8 +44,8 @@ export function display_implication(implication: ImplicationDB): ImplicationDisp } 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') + const domain = functor.associated_structures.find((s) => s.label == 'domain') + const codomain = functor.associated_structures.find((s) => s.label == 'codomain') if (!domain || !codomain) return functor.structure.notation = add_math( diff --git a/src/pages/ImplicationPage.svelte b/src/pages/ImplicationPage.svelte index 06f29490b..63e06f56e 100644 --- a/src/pages/ImplicationPage.svelte +++ b/src/pages/ImplicationPage.svelte @@ -6,8 +6,8 @@ import { get_property_url } from '$shared/property.utils' import type { ImplicationDisplay, - MappedTypes, StructureShort, + AssociatedTypes, StructureType } from '$lib/commons/types' import { PLURALS } from '$shared/config' @@ -16,12 +16,17 @@ type: StructureType implication: ImplicationDisplay structures: StructureShort[] - mapped_types: MappedTypes + associated_types: AssociatedTypes property_relation_dict: Record> } - let { type, implication, structures, mapped_types, property_relation_dict }: Props = - $props() + let { + type, + implication, + structures, + associated_types, + property_relation_dict + }: Props = $props() let has_additional_assumptions = $derived( Object.values(implication.mapped_assumptions).some((list) => list?.size) @@ -41,8 +46,9 @@ whose {remove_underscores(map)} {#each set as property, index} - {property_relation_dict[mapped_types[map]][property]} - {property}{property}{#if index < set.size - 1}  and  {/if} diff --git a/src/pages/StructureDetailPage.svelte b/src/pages/StructureDetailPage.svelte index 716bf3ae9..7cc8a2a8e 100644 --- a/src/pages/StructureDetailPage.svelte +++ b/src/pages/StructureDetailPage.svelte @@ -75,8 +75,8 @@ {#each associated_structures as a}
  • - {capitalize(remove_underscores(a.map))}: - {a.name} + {capitalize(remove_underscores(a.label))}: + {a.name}
    • {/each} From 8fc3c3a6c3cc76deb8a2d0818db8e821278d6cb0 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 15 Aug 2026 11:13:10 +0200 Subject: [PATCH 10/13] rename `mapped_assumptions` for implications to `associated_assumptions` --- DATABASE.md | 2 +- .../data/functor-implications/adjoints.yaml | 6 ++-- .../limits preservation.yaml | 30 ++++++++-------- database/data/functor-implications/misc.yaml | 20 +++++------ .../data/functor-implications/monadic.yaml | 2 +- database/data/morphism-implications/misc.yaml | 4 +-- .../morphism-implications/mono-epi-iso.yaml | 20 +++++------ .../closed.yaml | 10 +++--- .../limits-colimits.yaml | 6 ++-- .../misc.yaml | 2 +- database/schema/003_implications.sql | 20 +++++------ database/scripts/deduce-implications.ts | 36 +++++++++++-------- database/scripts/seed.ts | 22 +++++++----- database/scripts/utils/implications.ts | 8 ++--- database/scripts/utils/seed.types.ts | 2 +- shared/deduction.utils.ts | 6 ++-- shared/implications.ts | 20 ++++++----- src/components/ImplicationItem.svelte | 8 ++--- src/lib/commons/types.ts | 4 +-- src/lib/server/consistency.ts | 2 +- src/lib/server/fetchers/content.ts | 2 +- src/lib/server/fetchers/implication.ts | 2 +- src/lib/server/fetchers/implications.ts | 2 +- src/lib/server/fetchers/missing_data.ts | 2 +- src/lib/server/fetchers/property.ts | 2 +- src/lib/server/transforms.ts | 2 +- src/pages/ImplicationPage.svelte | 16 ++++----- 27 files changed, 137 insertions(+), 121 deletions(-) diff --git a/DATABASE.md b/DATABASE.md index fe58e40ea..8286d0d8b 100644 --- a/DATABASE.md +++ b/DATABASE.md @@ -34,7 +34,7 @@ These tables are abstracted through the `implications_view` view. Functor implications may also depend on properties of the domain or codomain category. Likewise, morphism implications may depend on properties of the ambient category. Such dependencies are stored in the following table: -- `mapped_assumptions` +- `associated_assumptions` Additional tables are available. For a complete overview, see the diagram below. diff --git a/database/data/functor-implications/adjoints.yaml b/database/data/functor-implications/adjoints.yaml index 5fbc20eee..2df2c48dc 100644 --- a/database/data/functor-implications/adjoints.yaml +++ b/database/data/functor-implications/adjoints.yaml @@ -9,7 +9,7 @@ - id: saft assumptions: - continuous - mapped_assumptions: + associated_assumptions: domain: - cogenerating set - complete @@ -34,7 +34,7 @@ - id: representable_right_adjoint assumptions: - representable - mapped_assumptions: + associated_assumptions: domain: - locally essentially small - coproducts @@ -45,7 +45,7 @@ - id: initial_object_as_left_adjoint assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - initial object codomain: diff --git a/database/data/functor-implications/limits preservation.yaml b/database/data/functor-implications/limits preservation.yaml index ba2e0549e..86cbef071 100644 --- a/database/data/functor-implications/limits preservation.yaml +++ b/database/data/functor-implications/limits preservation.yaml @@ -29,7 +29,7 @@ assumptions: - preserves terminal objects - preserves binary products - mapped_assumptions: + associated_assumptions: domain: - finite products conclusions: @@ -41,7 +41,7 @@ assumptions: - preserves equalizers - preserves products - mapped_assumptions: + associated_assumptions: domain: - products conclusions: @@ -53,7 +53,7 @@ assumptions: - cofinitary - left exact - mapped_assumptions: + associated_assumptions: domain: - finitely complete conclusions: @@ -65,7 +65,7 @@ assumptions: - cofinitary - preserves finite products - mapped_assumptions: + associated_assumptions: domain: - finite products conclusions: @@ -99,7 +99,7 @@ assumptions: - preserves equalizers - preserves finite products - mapped_assumptions: + associated_assumptions: domain: - finite products conclusions: @@ -128,7 +128,7 @@ assumptions: - preserves coreflexive equalizers - preserves binary products - mapped_assumptions: + associated_assumptions: domain: - binary products conclusions: @@ -139,7 +139,7 @@ - id: mono-preserving_criterion assumptions: - preserves regular monomorphisms - mapped_assumptions: + associated_assumptions: domain: - mono-regular conclusions: @@ -150,7 +150,7 @@ - id: regular-mono-preserving_criterion assumptions: - preserves monomorphisms - mapped_assumptions: + associated_assumptions: codomain: - mono-regular conclusions: @@ -161,7 +161,7 @@ - id: another_regular-mono-preserving_criterion assumptions: - preserves coreflexive equalizers - mapped_assumptions: + associated_assumptions: domain: - pushouts conclusions: @@ -172,7 +172,7 @@ - id: zero_preserving_condition assumptions: - preserves terminal objects - mapped_assumptions: + associated_assumptions: domain: - pointed codomain: @@ -185,7 +185,7 @@ - id: biproduct_preserving_condition assumptions: - preserves finite coproducts - mapped_assumptions: + associated_assumptions: domain: - biproducts codomain: @@ -233,7 +233,7 @@ - id: trivial_functors_continuous assumptions: [] - mapped_assumptions: + associated_assumptions: codomain: - trivial conclusions: @@ -243,7 +243,7 @@ - id: automatically_preserve_equalizers assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - regular-subobject-trivial conclusions: @@ -254,7 +254,7 @@ - id: trivial_coreflexive_equalizer_preservation # TODO: rework this once we add "split-epi-trivial" assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - regular-quotient-trivial conclusions: @@ -264,7 +264,7 @@ - id: thin_binary_product_preservation assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - thin - semi-strongly connected diff --git a/database/data/functor-implications/misc.yaml b/database/data/functor-implications/misc.yaml index 5bb0c681c..6ff468de1 100644 --- a/database/data/functor-implications/misc.yaml +++ b/database/data/functor-implications/misc.yaml @@ -11,7 +11,7 @@ assumptions: - conservative - preserves equalizers - mapped_assumptions: + associated_assumptions: domain: - equalizers conclusions: @@ -30,7 +30,7 @@ - id: faithful_with_balanced_domain assumptions: - faithful - mapped_assumptions: + associated_assumptions: domain: - balanced conclusions: @@ -101,7 +101,7 @@ - id: surjective_functor_to_core_connected_category assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - inhabited codomain: @@ -113,7 +113,7 @@ - id: right_invertible_functor_to_trivial_category assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - inhabited codomain: @@ -126,7 +126,7 @@ - id: full_functor_to_trivial_category # TODO: add the converse once we have category_conclusions assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - strongly connected codomain: @@ -138,7 +138,7 @@ - id: functor_conservative_on_groupoids assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - groupoid conclusions: @@ -148,7 +148,7 @@ - id: automatic_ess_injective_functors assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - core-connected conclusions: @@ -158,7 +158,7 @@ - id: automatic_full_on_isos_functors assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - core-connected codomain: @@ -172,7 +172,7 @@ # TODO: rework this once we add "split-mono trivial" assumptions: - dominant - mapped_assumptions: + associated_assumptions: codomain: - regular-subobject-trivial conclusions: @@ -182,7 +182,7 @@ - id: automatic_preserves_mono assumptions: [] - mapped_assumptions: + associated_assumptions: codomain: - left cancellative conclusions: diff --git a/database/data/functor-implications/monadic.yaml b/database/data/functor-implications/monadic.yaml index 9742136f3..591fb5c80 100644 --- a/database/data/functor-implications/monadic.yaml +++ b/database/data/functor-implications/monadic.yaml @@ -13,7 +13,7 @@ - right adjoint - conservative - preserves reflexive coequalizers - mapped_assumptions: + associated_assumptions: domain: - reflexive coequalizers conclusions: diff --git a/database/data/morphism-implications/misc.yaml b/database/data/morphism-implications/misc.yaml index b5e4e52e7..6dd219795 100644 --- a/database/data/morphism-implications/misc.yaml +++ b/database/data/morphism-implications/misc.yaml @@ -1,6 +1,6 @@ - id: thin_implies_constant assumptions: [] - mapped_assumptions: + associated_assumptions: category: - thin conclusions: @@ -20,7 +20,7 @@ - id: zero_morphism_criterion assumptions: - constant - mapped_assumptions: + associated_assumptions: category: - zero morphisms conclusions: diff --git a/database/data/morphism-implications/mono-epi-iso.yaml b/database/data/morphism-implications/mono-epi-iso.yaml index fdd418f3f..040be5a18 100644 --- a/database/data/morphism-implications/mono-epi-iso.yaml +++ b/database/data/morphism-implications/mono-epi-iso.yaml @@ -29,7 +29,7 @@ - id: mono_is_iso assumptions: - monomorphism - mapped_assumptions: + associated_assumptions: category: - subobject-trivial conclusions: @@ -41,7 +41,7 @@ assumptions: - monomorphism - epimorphism - mapped_assumptions: + associated_assumptions: category: - balanced conclusions: @@ -52,7 +52,7 @@ - id: mono-regular_def assumptions: - monomorphism - mapped_assumptions: + associated_assumptions: category: - mono-regular conclusions: @@ -79,7 +79,7 @@ - id: strict_monos_are_often_effective assumptions: - strict monomorphism - mapped_assumptions: + associated_assumptions: category: - pushouts conclusions: @@ -95,7 +95,7 @@ - id: iso_is_normal_mono assumptions: - isomorphism - mapped_assumptions: + associated_assumptions: category: - zero morphisms conclusions: @@ -114,7 +114,7 @@ - id: regular_implies_normal_mono_preadditive_case assumptions: - regular monomorphism - mapped_assumptions: + associated_assumptions: category: - preadditive conclusions: @@ -164,7 +164,7 @@ - id: extremal_monos_are_regular_in_coregular_category assumptions: - extremal monomorphism - mapped_assumptions: + associated_assumptions: category: - coregular conclusions: @@ -178,7 +178,7 @@ - id: extremal_mono_strong_criterion assumptions: - extremal monomorphism - mapped_assumptions: + associated_assumptions: category: - pushouts conclusions: @@ -195,7 +195,7 @@ - id: extremal_mono_balanced assumptions: - monomorphism - mapped_assumptions: + associated_assumptions: category: - balanced conclusions: @@ -206,7 +206,7 @@ - id: every_mono_strong_criterion assumptions: - monomorphism - mapped_assumptions: + associated_assumptions: category: - epi-regular conclusions: diff --git a/database/data/symmetric_monoidal_category_implications/closed.yaml b/database/data/symmetric_monoidal_category_implications/closed.yaml index 1b83ed28d..5da42f186 100644 --- a/database/data/symmetric_monoidal_category_implications/closed.yaml +++ b/database/data/symmetric_monoidal_category_implications/closed.yaml @@ -3,7 +3,7 @@ - id: closed_cartesian_symmetric_monoidal assumptions: - cartesian - mapped_assumptions: + associated_assumptions: underlying_category: - cartesian closed conclusions: @@ -14,7 +14,7 @@ - id: when_closed_implies_cocomplete assumptions: - closed - mapped_assumptions: + associated_assumptions: underlying_category: - cocomplete conclusions: @@ -25,7 +25,7 @@ - id: when_closed_implies_finitely_cocomplete assumptions: - closed - mapped_assumptions: + associated_assumptions: underlying_category: - finitely cocomplete conclusions: @@ -36,7 +36,7 @@ - id: when_closed_implies_distributive assumptions: - closed - mapped_assumptions: + associated_assumptions: underlying_category: - finite coproducts conclusions: @@ -47,7 +47,7 @@ - id: when_closed_implies_infinitary_distributive assumptions: - closed - mapped_assumptions: + associated_assumptions: underlying_category: - coproducts conclusions: diff --git a/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml b/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml index 02a7f4167..de4941f54 100644 --- a/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml +++ b/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml @@ -28,7 +28,7 @@ - id: distributive_cartesian assumptions: - cartesian - mapped_assumptions: + associated_assumptions: underlying_category: - distributive conclusions: @@ -40,7 +40,7 @@ - id: infinitary_distributive_cartesian assumptions: - cartesian - mapped_assumptions: + associated_assumptions: underlying_category: - infinitary distributive conclusions: @@ -61,7 +61,7 @@ - id: preadditive_codistributive_criterion assumptions: - distributive - mapped_assumptions: + associated_assumptions: underlying_category: - biproducts conclusions: diff --git a/database/data/symmetric_monoidal_category_implications/misc.yaml b/database/data/symmetric_monoidal_category_implications/misc.yaml index 26f25512a..e1fdfc0ff 100644 --- a/database/data/symmetric_monoidal_category_implications/misc.yaml +++ b/database/data/symmetric_monoidal_category_implications/misc.yaml @@ -22,7 +22,7 @@ - id: thin_is_well_pointed assumptions: [] - mapped_assumptions: + associated_assumptions: underlying_category: - thin conclusions: diff --git a/database/schema/003_implications.sql b/database/schema/003_implications.sql index 5e50e13b8..a9c94bd22 100644 --- a/database/schema/003_implications.sql +++ b/database/schema/003_implications.sql @@ -38,23 +38,23 @@ CREATE TABLE conclusions ( CREATE INDEX idx_conclusions_property ON conclusions (property_id); -CREATE TABLE mapped_assumptions ( +CREATE TABLE associated_assumptions ( implication_id TEXT NOT NULL, - map TEXT NOT NULL, + label TEXT NOT NULL, property_id TEXT NOT NULL, type TEXT NOT NULL, property_type TEXT NOT NULL, - PRIMARY KEY (implication_id, map, property_id), + PRIMARY KEY (implication_id, label, property_id), FOREIGN KEY (implication_id, type) REFERENCES implications (id, type) ON DELETE CASCADE, FOREIGN KEY (property_id, property_type) REFERENCES properties (id, type) ON DELETE CASCADE, - FOREIGN KEY (map, type, property_type) + FOREIGN KEY (label, type, property_type) REFERENCES associated_structure_types (label, type, associated_type) ON DELETE RESTRICT ); -CREATE INDEX idx_assumptions_mapped_property ON mapped_assumptions (property_id); +CREATE INDEX idx_assumptions_associated_property ON associated_assumptions (property_id); CREATE VIEW implications_view AS SELECT @@ -74,15 +74,15 @@ CREATE VIEW implications_view AS ORDER BY lower(c.property_id) ) AS conclusions, ( - SELECT json_group_object(map, properties) + SELECT json_group_object(label, properties) FROM ( SELECT - a.map, + a.label, json_group_array(a.property_id) AS properties - FROM mapped_assumptions a + FROM associated_assumptions a WHERE a.implication_id = i.id - GROUP BY a.map + GROUP BY a.label ) - ) AS mapped_assumptions + ) AS associated_assumptions FROM implications i ; \ No newline at end of file diff --git a/database/scripts/deduce-implications.ts b/database/scripts/deduce-implications.ts index fcc3089ae..b72bb540f 100644 --- a/database/scripts/deduce-implications.ts +++ b/database/scripts/deduce-implications.ts @@ -40,7 +40,7 @@ export function create_dualized_implications(type: StructureType) { conclusions: string dual_assumptions: string dual_conclusions: string - dual_mapped_assumptions: string + dual_associated_assumptions: string } >( `SELECT @@ -63,18 +63,18 @@ export function create_dualized_implications(type: StructureType) { WHERE a.implication_id = i.id ) AS dual_conclusions, ( - SELECT json_group_object(map, properties) + SELECT json_group_object(label, properties) FROM ( SELECT - a.map, + a.label, json_group_array(p.dual_property_id) AS properties - FROM mapped_assumptions a + FROM associated_assumptions a INNER JOIN properties p ON p.id = a.property_id AND p.type = a.property_type WHERE a.implication_id = i.id - GROUP BY a.map + GROUP BY a.label ) - ) AS dual_mapped_assumptions + ) AS dual_associated_assumptions FROM implications_view i WHERE i.type = ? AND i.is_deduced = FALSE` ) @@ -97,9 +97,9 @@ export function create_dualized_implications(type: StructureType) { VALUES (?, ?, ?) `) - const mapped_assumption_insert = db.prepare(` - INSERT INTO mapped_assumptions - (implication_id, map, property_id, type, property_type) + const associated_assumption_insert = db.prepare(` + INSERT INTO associated_assumptions + (implication_id, label, property_id, type, property_type) VALUES (?, ?, ?, ?, ?) `) @@ -113,14 +113,16 @@ export function create_dualized_implications(type: StructureType) { const dual_assumptions = parse_json_set(impl.dual_assumptions) const conclusions = parse_json_set(impl.conclusions) const dual_conclusions = parse_json_set(impl.dual_conclusions) - const dual_mapped_assumptions = parse_nested_json_set( - impl.dual_mapped_assumptions + const dual_associated_assumptions = parse_nested_json_set( + impl.dual_associated_assumptions ) if (dual_assumptions.has(null)) continue if (dual_conclusions.has(null)) continue - if (Object.values(dual_mapped_assumptions).some((set) => set?.has(null))) { + if ( + Object.values(dual_associated_assumptions).some((set) => set?.has(null)) + ) { continue } @@ -149,9 +151,15 @@ export function create_dualized_implications(type: StructureType) { } for (const { label, associated_type } of associated_structure_types) { - const duals = dual_mapped_assumptions[label] + const duals = dual_associated_assumptions[label] for (const d of duals ?? []) { - mapped_assumption_insert.run(dual_id, label, d, type, associated_type) + associated_assumption_insert.run( + dual_id, + label, + d, + type, + associated_type + ) } } } diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index 515614956..9d08286fb 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -86,7 +86,7 @@ function clear_all_tables() { db.prepare(`DELETE FROM special_object_assignments`).run() db.prepare(`DELETE FROM special_object_types`).run() - db.prepare(`DELETE FROM mapped_assumptions`).run() + db.prepare(`DELETE FROM associated_assumptions`).run() db.prepare(`DELETE FROM assumptions`).run() db.prepare(`DELETE FROM conclusions`).run() db.prepare(`DELETE FROM implications`).run() @@ -464,15 +464,15 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri ) VALUES (?, ?, ?)` ) - const mapped_assumption_insert = db.prepare( - `INSERT INTO mapped_assumptions ( - implication_id, map, property_id, type, property_type + const associated_assumption_insert = db.prepare( + `INSERT INTO associated_assumptions ( + implication_id, label, property_id, type, property_type ) VALUES (?, ?, ?, ?, ?)` ) function insert_implications(implications: ImplicationYaml[]) { for (const impl of implications) { - if (!impl.assumptions.length && !impl.mapped_assumptions) { + if (!impl.assumptions.length && !impl.associated_assumptions) { console.error(`❌ Implication ${impl.id} has no assumptions.`) process.exit(1) } @@ -492,12 +492,18 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri conclusion_insert.run(impl.id, conclusion, type) } - if (!impl.mapped_assumptions) continue + if (!impl.associated_assumptions) continue for (const { label, associated_type } of associated_structure_types) { - const assumptions = impl.mapped_assumptions[label] ?? [] + const assumptions = impl.associated_assumptions[label] ?? [] for (const p of assumptions) { - mapped_assumption_insert.run(impl.id, label, p, type, associated_type) + associated_assumption_insert.run( + impl.id, + label, + p, + type, + associated_type + ) } } } diff --git a/database/scripts/utils/implications.ts b/database/scripts/utils/implications.ts index 90778783a..fd96cf1cd 100644 --- a/database/scripts/utils/implications.ts +++ b/database/scripts/utils/implications.ts @@ -21,16 +21,16 @@ function get_assumption_string( .join(' and ') : `is a ${remove_underscores(type)}` - if (!implication.mapped_assumptions) return own + if (!implication.associated_assumptions) return own - const mapped = Object.entries(implication.mapped_assumptions) + const associated = Object.entries(implication.associated_assumptions) .map( ([map, props]) => `and the ${remove_underscores(map)} has the required properties (${Array.from(props!).join(', ')})` ) .join(', ') - return `${own}, ${mapped}` + return `${own}, ${associated}` } function get_conclusion_string( @@ -71,7 +71,7 @@ export function get_contradiction_string( const conclusion_string = get_conclusion_string(implication, properties_dict, true) const has_multiple_assumptions = - implication.assumptions.size > 1 || !!implication.mapped_assumptions + implication.assumptions.size > 1 || !!implication.associated_assumptions const ref = `by this result` diff --git a/database/scripts/utils/seed.types.ts b/database/scripts/utils/seed.types.ts index 1846f6305..7009feb84 100644 --- a/database/scripts/utils/seed.types.ts +++ b/database/scripts/utils/seed.types.ts @@ -85,7 +85,7 @@ export type ImplicationYaml = { id: string assumptions: string[] conclusions: string[] - mapped_assumptions?: Partial> + associated_assumptions?: Partial> proof: string is_equivalence: boolean } diff --git a/shared/deduction.utils.ts b/shared/deduction.utils.ts index 4fe21763f..541c3c5cb 100644 --- a/shared/deduction.utils.ts +++ b/shared/deduction.utils.ts @@ -123,10 +123,10 @@ function is_applicable( associated_satisfied_properties?: Partial>> ) { return ( - !implication.mapped_assumptions || - Object.keys(implication.mapped_assumptions).every((key) => { + !implication.associated_assumptions || + Object.keys(implication.associated_assumptions).every((key) => { return is_subset( - implication.mapped_assumptions?.[key] ?? new Set(), + implication.associated_assumptions?.[key] ?? new Set(), associated_satisfied_properties?.[key] ?? new Set() ) }) diff --git a/shared/implications.ts b/shared/implications.ts index 9fbfb749f..3f7574954 100644 --- a/shared/implications.ts +++ b/shared/implications.ts @@ -6,7 +6,7 @@ export type NormalizedImplication = { id: string assumptions: Set conclusion: string - mapped_assumptions?: Partial>> + associated_assumptions?: Partial>> } /** @@ -30,7 +30,7 @@ export function get_normalized_implications( is_equivalence: 0 | 1 assumptions: string conclusions: string - mapped_assumptions: string + associated_assumptions: string } >( `SELECT @@ -38,7 +38,7 @@ export function get_normalized_implications( is_equivalence, assumptions, conclusions, - mapped_assumptions + associated_assumptions FROM implications_view WHERE type = ?` ) @@ -49,9 +49,11 @@ export function get_normalized_implications( for (const impl of implications_db) { const assumptions = parse_json_set(impl.assumptions) const conclusions = parse_json_set(impl.conclusions) - const mapped_assumptions = parse_nested_json_set(impl.mapped_assumptions) + const associated_assumptions = parse_nested_json_set( + impl.associated_assumptions + ) - const has_mapped_assumptions = Object.keys(mapped_assumptions).length > 0 + const has_associated_assumptions = Object.keys(associated_assumptions).length > 0 for (const conclusion of conclusions) { const implication: NormalizedImplication = { @@ -60,8 +62,8 @@ export function get_normalized_implications( conclusion } - if (has_mapped_assumptions) { - implication.mapped_assumptions = mapped_assumptions + if (has_associated_assumptions) { + implication.associated_assumptions = associated_assumptions } implications.push(implication) @@ -75,8 +77,8 @@ export function get_normalized_implications( conclusion: assumption } - if (has_mapped_assumptions) { - implication.mapped_assumptions = mapped_assumptions + if (has_associated_assumptions) { + implication.associated_assumptions = associated_assumptions } implications.push(implication) diff --git a/src/components/ImplicationItem.svelte b/src/components/ImplicationItem.svelte index 4e4932536..066be4e0e 100644 --- a/src/components/ImplicationItem.svelte +++ b/src/components/ImplicationItem.svelte @@ -17,8 +17,8 @@ let { type, implication, highlighted_property }: Props = $props() - let has_additional_assumptions = $derived( - Object.values(implication.mapped_assumptions).some((list) => list?.size) + let has_associated_assumptions = $derived( + Object.values(implication.associated_assumptions).some((list) => list?.size) ) @@ -46,11 +46,11 @@ {/each} diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index dc138ac6b..d4c5f4599 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -96,7 +96,7 @@ export type ImplicationDB = { proof: string assumptions: string conclusions: string - mapped_assumptions: string + associated_assumptions: string } export type ImplicationDisplay = Replace< @@ -106,7 +106,7 @@ export type ImplicationDisplay = Replace< is_deduced: boolean assumptions: string[] conclusions: string[] - mapped_assumptions: Partial>> + associated_assumptions: Partial>> } > diff --git a/src/lib/server/consistency.ts b/src/lib/server/consistency.ts index 1e9cab31a..978298ddc 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -18,7 +18,7 @@ export function get_contradiction( } const implications = get_normalized_implications(db, type).filter( - (impl) => !impl.mapped_assumptions + (impl) => !impl.associated_assumptions ) const contradiction = contradiction_worker( diff --git a/src/lib/server/fetchers/content.ts b/src/lib/server/fetchers/content.ts index aa719517d..6b665f037 100644 --- a/src/lib/server/fetchers/content.ts +++ b/src/lib/server/fetchers/content.ts @@ -52,7 +52,7 @@ export function fetch_content_references(content_id: string) { proof, assumptions, conclusions, - mapped_assumptions + associated_assumptions FROM implications_view WHERE proof LIKE '%/content/' || ? || '%' ORDER BY lower(assumptions) || ' ' || lower(conclusions)` diff --git a/src/lib/server/fetchers/implication.ts b/src/lib/server/fetchers/implication.ts index 09289fb0c..e537723ad 100644 --- a/src/lib/server/fetchers/implication.ts +++ b/src/lib/server/fetchers/implication.ts @@ -21,7 +21,7 @@ export function fetch_implication(type: StructureType, id: string) { proof, assumptions, conclusions, - mapped_assumptions + associated_assumptions FROM implications_view WHERE id = ?` ) diff --git a/src/lib/server/fetchers/implications.ts b/src/lib/server/fetchers/implications.ts index 37a1e301e..a4077f90b 100644 --- a/src/lib/server/fetchers/implications.ts +++ b/src/lib/server/fetchers/implications.ts @@ -12,7 +12,7 @@ export function fetch_implications(type: StructureType) { proof, assumptions, conclusions, - mapped_assumptions + associated_assumptions FROM implications_view WHERE type = ? ORDER BY lower(assumptions) || ' ' || lower(conclusions)` diff --git a/src/lib/server/fetchers/missing_data.ts b/src/lib/server/fetchers/missing_data.ts index 47d58cbaf..93bc435e5 100644 --- a/src/lib/server/fetchers/missing_data.ts +++ b/src/lib/server/fetchers/missing_data.ts @@ -78,7 +78,7 @@ export function fetch_missing_data(type: StructureType) { ) const implications = get_normalized_implications(db, type).filter( - (impl) => !impl.mapped_assumptions + (impl) => !impl.associated_assumptions ) const witnessed_pairs_set = new Set(witnessed_pairs.map(({ p, q }) => `${p}|${q}`)) diff --git a/src/lib/server/fetchers/property.ts b/src/lib/server/fetchers/property.ts index a903c975d..3486723f3 100644 --- a/src/lib/server/fetchers/property.ts +++ b/src/lib/server/fetchers/property.ts @@ -60,7 +60,7 @@ export function fetch_property(type: StructureType, id: string) { proof, assumptions, conclusions, - mapped_assumptions + associated_assumptions FROM implications_view WHERE type = ? AND ( diff --git a/src/lib/server/transforms.ts b/src/lib/server/transforms.ts index 1c0fcc309..aff337e0f 100644 --- a/src/lib/server/transforms.ts +++ b/src/lib/server/transforms.ts @@ -39,7 +39,7 @@ export function display_implication(implication: ImplicationDB): ImplicationDisp proof: implication.proof, assumptions: JSON.parse(implication.assumptions), conclusions: JSON.parse(implication.conclusions), - mapped_assumptions: parse_nested_json_set(implication.mapped_assumptions) + associated_assumptions: parse_nested_json_set(implication.associated_assumptions) } } diff --git a/src/pages/ImplicationPage.svelte b/src/pages/ImplicationPage.svelte index 63e06f56e..4f1cd8536 100644 --- a/src/pages/ImplicationPage.svelte +++ b/src/pages/ImplicationPage.svelte @@ -28,8 +28,8 @@ property_relation_dict }: Props = $props() - let has_additional_assumptions = $derived( - Object.values(implication.mapped_assumptions).some((list) => list?.size) + let has_associated_assumptions = $derived( + Object.values(implication.associated_assumptions).some((list) => list?.size) ) @@ -39,20 +39,20 @@

    Claim: - {#if has_additional_assumptions} + {#if has_associated_assumptions} Given a {remove_underscores(type)} - {#each Object.entries(implication.mapped_assumptions) as [map, set], ind} + {#each Object.entries(implication.associated_assumptions) as [label, set], ind} {#if set} whose - {remove_underscores(map)} + {remove_underscores(label)} {#each set as property, index} - {property_relation_dict[associated_types[map]][property]} - {property}{#if index < set.size - 1}  and  {/if} - {/each}{#if ind < Object.entries(implication.mapped_assumptions).length - 1} + {/each}{#if ind < Object.entries(implication.associated_assumptions).length - 1} , and  {/if} {/if} From 6007a58c211ff555fbcd23908d8261e1bfea8592 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 15 Aug 2026 11:31:25 +0200 Subject: [PATCH 11/13] update database diagram --- DATABASE.md | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/DATABASE.md b/DATABASE.md index 8286d0d8b..f994351f5 100644 --- a/DATABASE.md +++ b/DATABASE.md @@ -14,13 +14,6 @@ The `structures` table stores data that is common to all types of categorical st - `structure_types` -Structure-specific data is stored in additional tables, such as: - -- `categories` -- `functors` -- `morphisms` -- `symmetric_monoidal_categories` - Properties (whether satisfied or not) are associated with categorical structures via the following table: - `property_assignments` @@ -110,6 +103,6 @@ to check for redundant assignments of properties to categorical structures. ## Diagram -This is the database schema as of 13.08.2026; changes may occur. +This is the database schema as of 15.08.2026; changes may occur. -database diagram +database diagram From 83b10a247572b4fa5790b473c40b81bdbe5b378c Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 15 Aug 2026 19:34:57 +0200 Subject: [PATCH 12/13] replace CTE by simple subquery --- database/scripts/utils/structures.ts | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/database/scripts/utils/structures.ts b/database/scripts/utils/structures.ts index c23735c18..60bff16de 100644 --- a/database/scripts/utils/structures.ts +++ b/database/scripts/utils/structures.ts @@ -27,7 +27,11 @@ export function get_structures(db: Database, type: StructureType): StructureMeta properties: string } >( - `WITH associated_properties AS ( + ` + SELECT + id, name, dual, + json_group_object(label, props) AS properties + FROM ( SELECT s.id, s.name, @@ -43,10 +47,6 @@ export function get_structures(db: Database, type: StructureType): StructureMeta WHERE s.type = ? GROUP BY s.id, m.label ) - SELECT - id, name, dual, - json_group_object(label, props) AS properties - FROM associated_properties GROUP BY id ORDER BY id` ) From b9bab7a0fe54821e247efa65a2885502780a3343 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 15 Aug 2026 20:04:33 +0200 Subject: [PATCH 13/13] improve table aliases --- database/scripts/deduce-implications.ts | 16 ++++++++-------- database/scripts/utils/structures.ts | 16 ++++++++-------- src/lib/server/fetchers/category.ts | 13 ++++++------- src/lib/server/fetchers/missing_data.ts | 16 +++++++++------- src/lib/server/fetchers/properties.ts | 18 +++++++++--------- src/lib/server/fetchers/property.ts | 12 ++++++------ src/lib/server/fetchers/structure.ts | 10 +++++----- 7 files changed, 51 insertions(+), 50 deletions(-) diff --git a/database/scripts/deduce-implications.ts b/database/scripts/deduce-implications.ts index b72bb540f..75d955f18 100644 --- a/database/scripts/deduce-implications.ts +++ b/database/scripts/deduce-implications.ts @@ -57,22 +57,22 @@ export function create_dualized_implications(type: StructureType) { ) AS dual_assumptions, ( SELECT json_group_array(p.dual_property_id) - FROM conclusions a + FROM conclusions c LEFT JOIN properties p - ON p.id = a.property_id AND p.type = i.type - WHERE a.implication_id = i.id + ON p.id = c.property_id AND p.type = i.type + WHERE c.implication_id = i.id ) AS dual_conclusions, ( SELECT json_group_object(label, properties) FROM ( SELECT - a.label, + aa.label, json_group_array(p.dual_property_id) AS properties - FROM associated_assumptions a + FROM associated_assumptions aa INNER JOIN properties p - ON p.id = a.property_id AND p.type = a.property_type - WHERE a.implication_id = i.id - GROUP BY a.label + ON p.id = aa.property_id AND p.type = aa.property_type + WHERE aa.implication_id = i.id + GROUP BY aa.label ) ) AS dual_associated_assumptions FROM implications_view i diff --git a/database/scripts/utils/structures.ts b/database/scripts/utils/structures.ts index 60bff16de..ea8037204 100644 --- a/database/scripts/utils/structures.ts +++ b/database/scripts/utils/structures.ts @@ -36,16 +36,16 @@ export function get_structures(db: Database, type: StructureType): StructureMeta s.id, s.name, s.dual_structure_id AS dual, - m.label, - json_group_array(a.property_id) AS props + ass.label, + json_group_array(pa.property_id) AS props FROM structures s - LEFT JOIN associated_structures m - ON m.structure_id = s.id - LEFT JOIN property_assignments a - ON a.structure_id = m.associated_structure_id - AND a.is_satisfied = TRUE + LEFT JOIN associated_structures ass + ON ass.structure_id = s.id + LEFT JOIN property_assignments pa + ON pa.structure_id = ass.associated_structure_id + AND pa.is_satisfied = TRUE WHERE s.type = ? - GROUP BY s.id, m.label + GROUP BY s.id, ass.label ) GROUP BY id ORDER BY id` diff --git a/src/lib/server/fetchers/category.ts b/src/lib/server/fetchers/category.ts index 7ac4fe7cc..ddd3d5bda 100644 --- a/src/lib/server/fetchers/category.ts +++ b/src/lib/server/fetchers/category.ts @@ -10,9 +10,8 @@ import { error } from '@sveltejs/kit' export function fetch_category(id: string) { const category = db .prepare<[string], CategoryDefinition>( - `SELECT c.objects, c.morphisms - FROM categories c - WHERE c.id = ?` + `SELECT objects, morphisms FROM categories + WHERE id = ?` ) .get(id) @@ -20,11 +19,11 @@ export function fetch_category(id: string) { const special_objects = db .prepare<[string], SpecialObject>( - `SELECT s.type, s.description - FROM special_object_assignments s + `SELECT o.type, o.description + FROM special_object_assignments o INNER JOIN special_object_types t - ON t.type = s.type - WHERE s.category_id = ? + ON t.type = o.type + WHERE o.category_id = ? ORDER BY t.id` ) .all(id) diff --git a/src/lib/server/fetchers/missing_data.ts b/src/lib/server/fetchers/missing_data.ts index 93bc435e5..9f9a11c6b 100644 --- a/src/lib/server/fetchers/missing_data.ts +++ b/src/lib/server/fetchers/missing_data.ts @@ -26,21 +26,23 @@ export function fetch_missing_data(type: StructureType) { { id1: string; name1: string; id2: string; name2: string } >( `SELECT - s1.id AS id1, s1.name AS name1, - s2.id AS id2, s2.name AS name2 + s1.id AS id1, + s1.name AS name1, + s2.id AS id2, + s2.name AS name2 FROM structures s1 JOIN structures s2 ON s1.id < s2.id AND s2.type = s1.type JOIN properties p ON p.type = s1.type - LEFT JOIN property_assignments a1 - ON a1.structure_id = s1.id AND a1.property_id = p.id - LEFT JOIN property_assignments a2 - ON a2.structure_id = s2.id AND a2.property_id = p.id + LEFT JOIN property_assignments pa1 + ON pa1.structure_id = s1.id AND pa1.property_id = p.id + LEFT JOIN property_assignments pa2 + ON pa2.structure_id = s2.id AND pa2.property_id = p.id WHERE s1.type = ? GROUP BY s1.id, s1.name, s2.id, s2.name HAVING SUM( CASE - WHEN a1.is_satisfied IS a2.is_satisfied THEN 0 + WHEN pa1.is_satisfied IS pa2.is_satisfied THEN 0 ELSE 1 END ) = 0` diff --git a/src/lib/server/fetchers/properties.ts b/src/lib/server/fetchers/properties.ts index dbfefad14..ea52f8484 100644 --- a/src/lib/server/fetchers/properties.ts +++ b/src/lib/server/fetchers/properties.ts @@ -46,14 +46,14 @@ export function fetch_grouped_properties_and_tags(type: StructureType) { const tags = db .prepare<[StructureType], string>( - `SELECT t.tag - FROM property_tags t - WHERE t.type = ? + `SELECT pt.tag + FROM property_tags pt + WHERE pt.type = ? AND EXISTS ( - SELECT 1 FROM property_tag_assignments a - WHERE a.tag = t.tag AND a.type = t.type + SELECT 1 FROM property_tag_assignments pta + WHERE pta.tag = pt.tag AND pta.type = pt.type ) - ORDER BY t.id` + ORDER BY pt.id` ) .pluck() .all(type) @@ -92,10 +92,10 @@ export function fetch_tagged_properties(type: StructureType, tag: string) { const properties = db .prepare<[StructureType, string], PropertyShort>( `SELECT p.id, p.relation - FROM property_tag_assignments t + FROM property_tag_assignments pta INNER JOIN properties p - ON p.id = t.property_id AND p.type = ? - WHERE t.tag = ? AND t.type = p.type + ON p.id = pta.property_id AND p.type = ? + WHERE pta.tag = ? AND pta.type = p.type ORDER BY lower(id)` ) .all(type, tag) diff --git a/src/lib/server/fetchers/property.ts b/src/lib/server/fetchers/property.ts index 3486723f3..2ce1e5a0f 100644 --- a/src/lib/server/fetchers/property.ts +++ b/src/lib/server/fetchers/property.ts @@ -41,12 +41,12 @@ export function fetch_property(type: StructureType, id: string) { const tags = db .prepare<[StructureType, string], string>( - `SELECT pt.tag - FROM property_tag_assignments pt - INNER JOIN property_tags t - ON t.tag = pt.tag AND t.type = ? - WHERE pt.property_id = ? AND pt.type = t.type - ORDER BY t.id` + `SELECT pta.tag + FROM property_tag_assignments pta + INNER JOIN property_tags pt + ON pt.tag = pta.tag AND pt.type = ? + WHERE pta.property_id = ? AND pta.type = pt.type + ORDER BY pt.id` ) .pluck() .all(type, id) diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts index 5b279865e..515d2bb20 100644 --- a/src/lib/server/fetchers/structure.ts +++ b/src/lib/server/fetchers/structure.ts @@ -74,12 +74,12 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai FROM associated_structures a INNER JOIN structures s ON s.id = a.structure_id - INNER JOIN associated_structure_types m + INNER JOIN associated_structure_types ast ON - m.label = a.label - AND m.type = a.type - AND m.associated_type = a.associated_type - WHERE a.associated_structure_id = ? AND m.required = TRUE + ast.label = a.label + AND ast.type = a.type + AND ast.associated_type = a.associated_type + WHERE a.associated_structure_id = ? AND ast.required = TRUE ORDER BY a.type, lower(s.name)` ) .all(id)