diff --git a/DATABASE.md b/DATABASE.md index fc1cea5fd..da1d32158 100644 --- a/DATABASE.md +++ b/DATABASE.md @@ -105,4 +105,4 @@ to check for redundant assignments of properties to categorical structures. This is the database schema as of 18.09.2026; changes may occur. -database diagram +database diagram diff --git a/database/data/config.yaml b/database/data/config.yaml index a3f2d28ed..0546f4f55 100644 --- a/database/data/config.yaml +++ b/database/data/config.yaml @@ -82,24 +82,24 @@ relations: negation: does not preserve conditional: would preserve -special_object_types: - - type: terminal object +special_objects: + - kind: terminal object dual: initial object - - type: initial object + - kind: initial object dual: terminal object - - type: products + - kind: products dual: coproducts - - type: coproducts + - kind: coproducts dual: products -special_morphism_types: - - type: isomorphisms +special_morphisms: + - kind: isomorphisms dual: isomorphisms - - type: monomorphisms + - kind: monomorphisms dual: epimorphisms - - type: epimorphisms + - kind: epimorphisms dual: monomorphisms - - type: regular monomorphisms + - kind: regular monomorphisms dual: regular epimorphisms - - type: regular epimorphisms + - kind: regular epimorphisms dual: regular monomorphisms diff --git a/database/data/special-morphism-rules.yaml b/database/data/special-morphism-rules.yaml index 6b0634a5b..8fb40c080 100644 --- a/database/data/special-morphism-rules.yaml +++ b/database/data/special-morphism-rules.yaml @@ -1,84 +1,84 @@ - property: groupoid - type: isomorphisms + kind: isomorphisms description: every morphism proof: The category is a groupoid. - property: gaunt - type: isomorphisms + kind: isomorphisms description: only the identities proof: The category is gaunt. - property: thin - type: monomorphisms + kind: monomorphisms description: every morphism proof: It is a thin category. - property: thin - type: epimorphisms + kind: epimorphisms description: every morphism proof: It is a thin category. - property: left cancellative - type: monomorphisms + kind: monomorphisms description: every morphism proof: The category is left cancellative. - property: right cancellative - type: epimorphisms + kind: epimorphisms description: every morphism proof: The category is right cancellative. - property: left cancellative - type: regular epimorphisms + kind: regular epimorphisms description: same as isomorphisms proof: The category is left cancellative, and a regular epimorphism which is a monomorphism must be an isomorphism. - property: right cancellative - type: regular monomorphisms + kind: regular monomorphisms description: same as isomorphisms proof: The category is right cancellative, and a regular monomorphism which is an epimorphism must be an isomorphism. - property: one-sorted finitary algebraic - type: isomorphisms + kind: isomorphisms description: bijective morphisms proof: 'This holds in every one-sorted finitary algebraic category: the inverse of a bijective morphism is again a morphism.' - property: one-sorted finitary algebraic - type: monomorphisms + kind: monomorphisms description: injective morphisms proof: 'This holds in every one-sorted finitary algebraic category: the forgetful functor to sets is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.' - property: one-sorted finitary algebraic - type: regular epimorphisms + kind: regular epimorphisms description: surjective morphisms proof: 'This holds in every one-sorted finitary algebraic category: the construction of coequalizers shows that every regular epimorphism is surjective. Conversely, the fundamental theorem on homomorphisms states that every surjective homomorphism $A \to B$ is the coequalizer of the two projections $A \times_B A \rightrightarrows A$.' - property: mono-regular - type: regular monomorphisms + kind: regular monomorphisms description: same as monomorphisms proof: The category is mono-regular. - property: epi-regular - type: regular epimorphisms + kind: regular epimorphisms description: same as epimorphisms proof: The category is epi-regular. - property: subobject-trivial - type: monomorphisms + kind: monomorphisms description: same as isomorphisms proof: The category is subobject-trivial. - property: quotient-trivial - type: epimorphisms + kind: epimorphisms description: same as isomorphisms proof: The category is quotient-trivial. - property: regular-subobject-trivial - type: regular monomorphisms + kind: regular monomorphisms description: same as isomorphisms proof: The category is regular-subobject-trivial. - property: regular-quotient-trivial - type: regular epimorphisms + kind: regular epimorphisms description: same as isomorphisms proof: The category is regular-quotient-trivial. diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index 36dfab28a..c0ff2432a 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -8,29 +8,6 @@ INSERT INTO structure_types (type) VALUES ('morphism'), ('symmetric_monoidal_category'); - -CREATE TABLE associated_structure_types ( - label TEXT NOT NULL, - type TEXT NOT NULL, - associated_type TEXT NOT NULL, - required INTEGER NOT NULL - CHECK (required in (TRUE, FALSE)), - PRIMARY KEY (label, type, associated_type), - UNIQUE (label, type), - FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE CASCADE, - FOREIGN KEY (associated_type) REFERENCES structure_types (type) ON DELETE CASCADE -); - -INSERT INTO associated_structure_types - (label, type, associated_type, required) -VALUES - ('domain', 'functor', 'category', TRUE), - ('codomain', 'functor', 'category', TRUE), - ('category', 'morphism', 'category', TRUE), - ('underlying_category', 'symmetric_monoidal_category', 'category', TRUE), - ('left_adjoint', 'functor', 'functor', FALSE), - ('right_adjoint', 'functor', 'functor', FALSE); - CREATE TABLE structures ( id TEXT PRIMARY KEY, type TEXT NOT NULL, @@ -39,16 +16,18 @@ CREATE TABLE structures ( description TEXT NOT NULL, nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), dual_structure_id TEXT, - parent TEXT, + parent_structure_id TEXT, UNIQUE (id, type), FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT, - FOREIGN KEY (dual_structure_id, type) REFERENCES structures (id, type) ON DELETE RESTRICT - FOREIGN KEY (parent, type) REFERENCES structures (id, type) ON DELETE RESTRICT + FOREIGN KEY (dual_structure_id, type) REFERENCES structures (id, type) ON DELETE RESTRICT, + FOREIGN KEY (parent_structure_id, type) REFERENCES structures (id, type) ON DELETE RESTRICT ); CREATE UNIQUE INDEX structures_lower_id_unique ON structures (lower(id)); -CREATE INDEX structure_by_type ON structures (type); +CREATE INDEX idx_structures_by_type ON structures (type); + +CREATE INDEX idx_structures_by_parent ON structures (parent_structure_id, type); CREATE TABLE related_structures ( id INTEGER PRIMARY KEY, @@ -68,7 +47,7 @@ CREATE TABLE structure_comments ( FOREIGN KEY (structure_id) REFERENCES structures (id) ON DELETE CASCADE ); -CREATE INDEX idx_structure_comments ON structure_comments (structure_id); +CREATE INDEX idx_comments_by_structure ON structure_comments (structure_id); CREATE TABLE structure_tags ( id INTEGER PRIMARY KEY, @@ -87,17 +66,45 @@ CREATE TABLE structure_tag_assignments ( FOREIGN KEY (tag, type) REFERENCES structure_tags (tag, type) ON DELETE CASCADE ); +CREATE INDEX idx_structures_by_tag ON structure_tag_assignments (type, tag, structure_id); + +CREATE TABLE structure_associations ( + label TEXT NOT NULL, + source_type TEXT NOT NULL, + target_type TEXT NOT NULL, + required INTEGER NOT NULL CHECK (required in (TRUE, FALSE)), + PRIMARY KEY (label, source_type), + UNIQUE (label, source_type, target_type), + FOREIGN KEY (source_type) REFERENCES structure_types (type) ON DELETE CASCADE, + FOREIGN KEY (target_type) REFERENCES structure_types (type) ON DELETE CASCADE +); + +INSERT INTO structure_associations + (label, source_type, target_type, required) +VALUES + ('domain', 'functor', 'category', TRUE), + ('codomain', 'functor', 'category', TRUE), + ('category', 'morphism', 'category', TRUE), + ('underlying_category', 'symmetric_monoidal_category', 'category', TRUE), + ('left_adjoint', 'functor', 'functor', FALSE), + ('right_adjoint', 'functor', 'functor', FALSE); + CREATE TABLE associated_structures ( label TEXT NOT NULL, - type TEXT NOT NULL, - associated_type TEXT NOT NULL, - structure_id TEXT NOT NULL, - associated_structure_id TEXT NOT NULL, - FOREIGN KEY (label, type, associated_type) - REFERENCES associated_structure_types (label, type, associated_type) + source_type TEXT NOT NULL, + target_type TEXT NOT NULL, + source_structure_id TEXT NOT NULL, + target_structure_id TEXT NOT NULL, + PRIMARY KEY (label, source_type, source_structure_id), + FOREIGN KEY (label, source_type, target_type) + REFERENCES structure_associations (label, source_type, target_type) ON DELETE CASCADE, - FOREIGN KEY (structure_id, type) + FOREIGN KEY (source_structure_id, source_type) REFERENCES structures (id, type) ON DELETE CASCADE, - FOREIGN KEY (associated_structure_id, associated_type) + FOREIGN KEY (target_structure_id, target_type) REFERENCES structures (id, type) ON DELETE CASCADE -); \ No newline at end of file +); + +CREATE INDEX idx_associated_structures_by_source ON associated_structures (source_structure_id); + +CREATE INDEX idx_associated_structures_by_target ON associated_structures (target_structure_id); \ No newline at end of file diff --git a/database/schema/002_properties.sql b/database/schema/002_properties.sql index 439aaae8d..3f6369d09 100644 --- a/database/schema/002_properties.sql +++ b/database/schema/002_properties.sql @@ -54,7 +54,7 @@ CREATE TABLE property_assignments ( REFERENCES properties (id, type) ON DELETE CASCADE ); -CREATE INDEX idx_property_assigned ON property_assignments (property_id); +CREATE INDEX idx_property_assignments_by_property ON property_assignments (property_id); CREATE TABLE property_tags ( id INTEGER PRIMARY KEY, diff --git a/database/schema/003_implications.sql b/database/schema/003_implications.sql index 35b27e616..7765e4b57 100644 --- a/database/schema/003_implications.sql +++ b/database/schema/003_implications.sql @@ -8,7 +8,7 @@ CREATE TABLE implications ( dual_implication_id TEXT, UNIQUE (id, type), FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT, - FOREIGN KEY (dual_implication_id) REFERENCES implications (id) + FOREIGN KEY (dual_implication_id, type) REFERENCES implications (id, type) ); CREATE UNIQUE INDEX idx_implications_lower_id_unique ON implications (lower(id)); @@ -26,7 +26,7 @@ CREATE TABLE assumptions ( REFERENCES properties (id, type) ON DELETE CASCADE ); -CREATE INDEX idx_assumptions_property ON assumptions (property_id); +CREATE INDEX idx_assumptions_by_property ON assumptions (property_id); CREATE TABLE conclusions ( implication_id TEXT NOT NULL, @@ -39,7 +39,7 @@ CREATE TABLE conclusions ( REFERENCES properties (id, type) ON DELETE CASCADE ); -CREATE INDEX idx_conclusions_property ON conclusions (property_id); +CREATE INDEX idx_conclusions_by_property ON conclusions (property_id); CREATE TABLE associated_assumptions ( implication_id TEXT NOT NULL, @@ -53,11 +53,11 @@ CREATE TABLE associated_assumptions ( FOREIGN KEY (property_id, property_type) REFERENCES properties (id, type) ON DELETE CASCADE, FOREIGN KEY (label, type, property_type) - REFERENCES associated_structure_types (label, type, associated_type) + REFERENCES structure_associations (label, source_type, target_type) ON DELETE RESTRICT ); -CREATE INDEX idx_assumptions_associated_property ON associated_assumptions (property_id); +CREATE INDEX idx_associated_assumptions_by_property ON associated_assumptions (property_id); CREATE VIEW implications_view AS SELECT diff --git a/database/schema/005_special_objects.sql b/database/schema/005_special_objects.sql index 14c3857cb..9a9b774fe 100644 --- a/database/schema/005_special_objects.sql +++ b/database/schema/005_special_objects.sql @@ -1,18 +1,18 @@ -CREATE TABLE special_object_types ( +CREATE TABLE special_objects ( id INTEGER PRIMARY KEY, - type TEXT NOT NULL UNIQUE, + kind TEXT NOT NULL UNIQUE, dual TEXT, - FOREIGN KEY (dual) REFERENCES special_object_types (type) ON DELETE SET NULL + FOREIGN KEY (dual) REFERENCES special_objects (kind) ON DELETE SET NULL ); CREATE TABLE special_object_assignments ( category_id TEXT NOT NULL, - type TEXT NOT NULL, + kind TEXT NOT NULL, description TEXT NOT NULL, is_deduced INTEGER NOT NULL DEFAULT FALSE CHECK (is_deduced in (TRUE, FALSE)), - PRIMARY KEY (category_id, type), - FOREIGN KEY (type) REFERENCES special_object_types (type) ON DELETE RESTRICT, + PRIMARY KEY (category_id, kind), + FOREIGN KEY (kind) REFERENCES special_objects (kind) ON DELETE RESTRICT, FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE ); diff --git a/database/schema/006_special-morphisms.sql b/database/schema/006_special-morphisms.sql index 22c463e54..797652f5f 100644 --- a/database/schema/006_special-morphisms.sql +++ b/database/schema/006_special-morphisms.sql @@ -1,19 +1,19 @@ -CREATE TABLE special_morphism_types ( +CREATE TABLE special_morphisms ( id INTEGER PRIMARY KEY, - type TEXT NOT NULL UNIQUE, + kind TEXT NOT NULL UNIQUE, dual TEXT, - FOREIGN KEY (dual) REFERENCES special_morphism_types (type) ON DELETE SET NULL + FOREIGN KEY (dual) REFERENCES special_morphisms (kind) ON DELETE SET NULL ); CREATE TABLE special_morphism_assignments ( category_id TEXT NOT NULL, - type TEXT NOT NULL, + kind TEXT NOT NULL, description TEXT NOT NULL, proof TEXT NOT NULL, is_deduced INTEGER NOT NULL DEFAULT FALSE CHECK (is_deduced in (TRUE, FALSE)), - PRIMARY KEY (category_id, type), - FOREIGN KEY (type) REFERENCES special_morphism_types (type) ON DELETE RESTRICT, + PRIMARY KEY (category_id, kind), + FOREIGN KEY (kind) REFERENCES special_morphisms (kind) ON DELETE RESTRICT, FOREIGN KEY (category_id) REFERENCES categories (id) ON DELETE CASCADE ); @@ -23,10 +23,10 @@ CREATE TABLE special_morphism_rules ( id INTEGER PRIMARY KEY, property_id TEXT NOT NULL, property_type TEXT NOT NULL DEFAULT 'category', - type TEXT NOT NULL, + kind TEXT NOT NULL, description TEXT NOT NULL, proof TEXT NOT NULL, FOREIGN KEY (property_id, property_type) REFERENCES properties (id, type) ON DELETE CASCADE, - FOREIGN KEY (type) REFERENCES special_morphism_types (type) ON DELETE RESTRICT + FOREIGN KEY (kind) REFERENCES special_morphisms (kind) ON DELETE RESTRICT ); \ No newline at end of file diff --git a/database/scripts/deduce-implications.ts b/database/scripts/deduce-implications.ts index 896d7ed57..2a86aecdc 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 associated_structure_types = db - .prepare<[StructureType], { label: string; associated_type: StructureType }>( - `SELECT label, associated_type - FROM associated_structure_types WHERE type = ?` + const structure_associations = db + .prepare<[StructureType], { label: string; target_type: StructureType }>( + `SELECT label, target_type + FROM structure_associations WHERE source_type = ?` ) .all(type) @@ -149,23 +149,22 @@ export function create_dualized_implications(type: StructureType) { dual_update.run(dual_id, impl.id) - for (const a of dual_assumptions) { - assumption_insert.run(dual_id, a, type) + for (const assumption of dual_assumptions) { + assumption_insert.run(dual_id, assumption, type) } - for (const c of dual_conclusions) { - conclusion_insert.run(dual_id, c, type) + for (const conclusion of dual_conclusions) { + conclusion_insert.run(dual_id, conclusion, type) } - for (const { label, associated_type } of associated_structure_types) { - const duals = dual_associated_assumptions[label] - for (const d of duals ?? []) { + for (const { label, target_type } of structure_associations) { + for (const assumption of dual_associated_assumptions[label] ?? []) { associated_assumption_insert.run( dual_id, label, - d, + assumption, type, - associated_type + target_type ) } } diff --git a/database/scripts/deduce-special-morphisms.ts b/database/scripts/deduce-special-morphisms.ts index 465305478..7ef60ae2d 100644 --- a/database/scripts/deduce-special-morphisms.ts +++ b/database/scripts/deduce-special-morphisms.ts @@ -26,21 +26,21 @@ function clear_deduced_special_morphisms() { * Inherit special morphism assignments from parent categories */ function inherit_special_morphisms_from_parents() { - type SpecialMorphism = { type: string; description: string; proof: string } + type SpecialMorphism = { kind: string; description: string; proof: string } const parent_map = get_structure_parent_map(db, 'category') const get_parent_special_morphisms = db.prepare<[string], SpecialMorphism>( - `SELECT type, description, proof + `SELECT kind, description, proof FROM special_morphism_assignments WHERE category_id = ? AND is_deduced = FALSE` ) const insert_special_morphism = db.prepare( `INSERT INTO special_morphism_assignments ( - category_id, type, description, proof, is_deduced + category_id, kind, description, proof, is_deduced ) VALUES (?, ?, ?, ?, TRUE) - ON CONFLICT (category_id, type) DO NOTHING` + ON CONFLICT (category_id, kind) DO NOTHING` ) let inherited_count = 0 @@ -53,19 +53,19 @@ function inherit_special_morphisms_from_parents() { const parent_entries = get_parent_special_morphisms.all(current_id) for (const entry of parent_entries) { - if (!inherited_morphisms.has(entry.type)) { - inherited_morphisms.set(entry.type, entry) + if (!inherited_morphisms.has(entry.kind)) { + inherited_morphisms.set(entry.kind, entry) } } current_id = parent_map.get(current_id) ?? null } - for (const [type, entry] of inherited_morphisms) { + for (const [kind, entry] of inherited_morphisms) { const proof = `This follows from the parent.` const res = insert_special_morphism.run( category_id, - type, + kind, entry.description, proof ) @@ -84,25 +84,25 @@ function inherit_special_morphisms_from_parents() { function deduce_special_morphisms_by_rules() { type Rule = { property_id: string - type: string + kind: string description: string proof: string } const rules = db .prepare<[], Rule>( - `SELECT property_id, type, description, proof + `SELECT property_id, kind, description, proof FROM special_morphism_rules ORDER BY id` ) .all() - for (const { property_id, type, description, proof } of rules) { + for (const { property_id, kind, description, proof } of rules) { const res = db .prepare( `INSERT INTO special_morphism_assignments ( category_id, - type, + kind, description, proof, is_deduced @@ -117,12 +117,12 @@ function deduce_special_morphisms_by_rules() { WHERE pa.type = 'category' AND pa.property_id = ? AND pa.is_satisfied = TRUE - ON CONFLICT (category_id, type) DO NOTHING` + ON CONFLICT (category_id, kind) DO NOTHING` ) - .run(type, description, proof, property_id) + .run(kind, description, proof, property_id) devlog( - `Deduced ${res.changes} descriptions of ${type} in ${property_id} categories` + `Deduced ${res.changes} descriptions of ${kind} in ${property_id} categories` ) } } @@ -138,22 +138,22 @@ function deduce_special_morphisms_of_dual_categories() { .prepare( `INSERT INTO special_morphism_assignments ( category_id, - type, + kind, description, proof, is_deduced ) SELECT - c.dual_structure_id, - t.dual, - m.description, + s.dual_structure_id, + sm.dual, + sma.description, 'This is deduced from its dual category.', TRUE - FROM structures c - INNER JOIN special_morphism_assignments m ON m.category_id = c.id - INNER JOIN special_morphism_types t ON t.type = m.type - WHERE c.type = 'category' AND c.dual_structure_id IS NOT NULL - ON CONFLICT (category_id, type) DO NOTHING` + FROM structures s + INNER JOIN special_morphism_assignments sma ON sma.category_id = s.id + INNER JOIN special_morphisms sm ON sm.kind = sma.kind + WHERE s.type = 'category' AND s.dual_structure_id IS NOT NULL + ON CONFLICT (category_id, kind) DO NOTHING` ) .run() diff --git a/database/scripts/deduce-special-objects.ts b/database/scripts/deduce-special-objects.ts index 273867a3d..f59083b44 100644 --- a/database/scripts/deduce-special-objects.ts +++ b/database/scripts/deduce-special-objects.ts @@ -22,20 +22,20 @@ function clear_deduced_special_objects() { * Inherit special object assignments from parent categories */ function inherit_special_objects_from_parents() { - type SpecialObject = { type: string; description: string } + type SpecialObject = { kind: string; description: string } const parent_map = get_structure_parent_map(db, 'category') const get_parent_special_objects = db.prepare<[string], SpecialObject>( - `SELECT type, description FROM special_object_assignments + `SELECT kind, description FROM special_object_assignments WHERE category_id = ? AND is_deduced = FALSE` ) const insert_special_object = db.prepare( `INSERT INTO special_object_assignments ( - category_id, type, description, is_deduced + category_id, kind, description, is_deduced ) VALUES (?, ?, ?, TRUE) - ON CONFLICT (category_id, type) DO NOTHING` + ON CONFLICT (category_id, kind) DO NOTHING` ) let inherited_count = 0 @@ -48,16 +48,16 @@ function inherit_special_objects_from_parents() { const parent_entries = get_parent_special_objects.all(current_id) for (const entry of parent_entries) { - if (!inherited_objects.has(entry.type)) { - inherited_objects.set(entry.type, entry) + if (!inherited_objects.has(entry.kind)) { + inherited_objects.set(entry.kind, entry) } } current_id = parent_map.get(current_id) ?? null } - for (const [type, entry] of inherited_objects) { - const res = insert_special_object.run(category_id, type, entry.description) + for (const [kind, entry] of inherited_objects) { + const res = insert_special_object.run(category_id, kind, entry.description) inherited_count += res.changes } } @@ -74,19 +74,19 @@ function deduce_special_objects_of_dual_categories() { .prepare( `INSERT INTO special_object_assignments ( category_id, - type, + kind, description, is_deduced ) SELECT - c.dual_structure_id, - t.dual, - o.description, + s.dual_structure_id, + so.dual, + soa.description, TRUE - FROM structures c - INNER JOIN special_object_assignments o ON o.category_id = c.id - INNER JOIN special_object_types t ON t.type = o.type - WHERE c.type = 'category' AND c.dual_structure_id IS NOT NULL` + FROM structures s + INNER JOIN special_object_assignments soa ON soa.category_id = s.id + INNER JOIN special_objects so ON so.kind = soa.kind + WHERE s.type = 'category' AND s.dual_structure_id IS NOT NULL` ) .run() diff --git a/database/scripts/restrict-functor-properties.ts b/database/scripts/restrict-functor-properties.ts index 7230b0092..eb03a3cac 100644 --- a/database/scripts/restrict-functor-properties.ts +++ b/database/scripts/restrict-functor-properties.ts @@ -29,18 +29,18 @@ function restrict_representable_functors() { check_redundancy ) SELECT - a.structure_id, + ass.source_structure_id, 'representable', 'functor', FALSE, 'The codomain is not $\\Set$.', TRUE, FALSE - FROM associated_structures a + FROM associated_structures ass WHERE - a.type = 'functor' - AND a.label = 'codomain' - AND a.associated_structure_id <> 'Set' + ass.source_type = 'functor' + AND ass.label = 'codomain' + AND ass.target_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 e9e087f96..185829444 100644 --- a/database/scripts/restrict-morphism-properties.ts +++ b/database/scripts/restrict-morphism-properties.ts @@ -32,21 +32,21 @@ function restrict_normal_morphisms(variant: 'mono' | 'epi') { check_redundancy ) SELECT - sa.structure_id, + ass.source_structure_id, ?, 'morphism', FALSE, 'The ' || c.name || ' has no zero morphisms.', TRUE, FALSE - FROM associated_structures sa + FROM associated_structures ass INNER JOIN structures c - ON c.id = sa.associated_structure_id + ON c.id = ass.target_structure_id INNER JOIN property_assignments a ON a.structure_id = c.id WHERE - sa.type = 'morphism' - AND sa.label = 'category' + ass.source_type = 'morphism' + AND ass.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 5eb7c6059..0113fbc85 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -97,9 +97,9 @@ function clear_all_tables() { db.prepare(`DELETE FROM special_morphism_rules`).run() db.prepare(`DELETE FROM special_morphism_assignments`).run() - db.prepare(`DELETE FROM special_morphism_types`).run() + db.prepare(`DELETE FROM special_morphisms`).run() db.prepare(`DELETE FROM special_object_assignments`).run() - db.prepare(`DELETE FROM special_object_types`).run() + db.prepare(`DELETE FROM special_objects`).run() db.prepare(`DELETE FROM associated_assumptions`).run() db.prepare(`DELETE FROM assumptions`).run() @@ -146,12 +146,12 @@ function seed_config() { `INSERT INTO relations (relation, negation, conditional) VALUES (?, ?, ?)` ) - const object_insert = db.prepare( - `INSERT INTO special_object_types (type, dual) VALUES (?, ?)` + const special_object_insert = db.prepare( + `INSERT INTO special_objects (kind, dual) VALUES (?, ?)` ) - const morphism_insert = db.prepare( - `INSERT INTO special_morphism_types (type, dual) VALUES (?, ?)` + const special_morphism_insert = db.prepare( + `INSERT INTO special_morphisms (kind, dual) VALUES (?, ?)` ) function insert_config(config: ConfigYaml) { @@ -173,12 +173,12 @@ function seed_config() { relation_insert.run(relation, negation, conditional) } - for (const { type, dual } of config.special_object_types) { - object_insert.run(type, dual) + for (const { kind, dual } of config.special_objects) { + special_object_insert.run(kind, dual) } - for (const { type, dual } of config.special_morphism_types) { - morphism_insert.run(type, dual) + for (const { kind, dual } of config.special_morphisms) { + special_morphism_insert.run(kind, dual) } } @@ -191,13 +191,13 @@ function seed_config() { function seed_special_morphism_rules() { const rule_insert = db.prepare( `INSERT INTO special_morphism_rules - (property_id, type, description, proof) + (property_id, kind, description, proof) VALUES (?, ?, ?, ?)` ) function insert_rules(rules: SpecialMorphismRuleYaml[]) { - for (const { property, type, description, proof } of rules) { - rule_insert.run(property, type, description, proof) + for (const { property, kind, description, proof } of rules) { + rule_insert.run(property, kind, description, proof) } } @@ -222,20 +222,20 @@ function seed_structures({ folder: string extra?: (structure: T) => void }) { - const associated_structure_types = db + const structure_associations = db .prepare< [StructureType], - { label: keyof T; associated_type: StructureType; required: 0 | 1 } + { label: keyof T; target_type: StructureType; required: 0 | 1 } >( - `SELECT label, associated_type, required - FROM associated_structure_types WHERE type = ?` + `SELECT label, target_type, required + FROM structure_associations WHERE source_type = ?` ) .all(type) const structure_insert = db.prepare( `INSERT INTO structures ( id, type, name, notation, description, nlab_link, - dual_structure_id, parent + dual_structure_id, parent_structure_id ) VALUES (?, ?, ?, ?, ?, ?, ?, ?)` ) @@ -270,8 +270,8 @@ function seed_structures({ const associated_structure_insert = db.prepare( `INSERT INTO associated_structures ( - label, type, associated_type, - structure_id, associated_structure_id + label, source_type, target_type, + source_structure_id, target_structure_id ) VALUES (?, ?, ?, ?, ?)` ) @@ -303,7 +303,7 @@ function seed_structures({ record_structure_addition(structure.id) - for (const { label, associated_type, required } of associated_structure_types) { + for (const { label, target_type, required } of structure_associations) { if (required && !structure[label]) { console.error( `❌ ${capitalize(type)} "${structure.id}" has no ${label.toString()}` @@ -315,7 +315,7 @@ function seed_structures({ associated_structure_insert.run( label, type, - associated_type, + target_type, structure.id, structure[label] ) @@ -386,24 +386,24 @@ function insert_category(category: CategoryYaml) { const special_object_insert = db.prepare( `INSERT INTO special_object_assignments ( - category_id, type, description + category_id, kind, description ) VALUES (?, ?, ?)` ) const special_morphism_insert = db.prepare( `INSERT INTO special_morphism_assignments ( - category_id, type, description, proof + category_id, kind, description, proof ) VALUES (?, ?, ?, ?)` ) category_insert.run(category.id, category.objects, category.morphisms) - for (const [type, entry] of Object.entries(category.special_objects)) { - special_object_insert.run(category.id, type, entry.description) + for (const [kind, entry] of Object.entries(category.special_objects)) { + special_object_insert.run(category.id, kind, entry.description) } - for (const [type, entry] of Object.entries(category.special_morphisms)) { - special_morphism_insert.run(category.id, type, entry.description, entry.proof) + for (const [kind, entry] of Object.entries(category.special_morphisms)) { + special_morphism_insert.run(category.id, kind, entry.description, entry.proof) } } @@ -467,10 +467,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 associated_structure_types = db - .prepare<[StructureType], { label: string; associated_type: StructureType }>( - `SELECT label, associated_type - FROM associated_structure_types WHERE type = ?` + const structure_associations = db + .prepare<[StructureType], { label: string; target_type: StructureType }>( + `SELECT label, target_type + FROM structure_associations WHERE source_type = ?` ) .all(type) @@ -522,15 +522,14 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri if (!impl.associated_assumptions) continue - for (const { label, associated_type } of associated_structure_types) { - const assumptions = impl.associated_assumptions[label] ?? [] - for (const p of assumptions) { + for (const { label, target_type } of structure_associations) { + for (const assumption of impl.associated_assumptions[label] ?? []) { associated_assumption_insert.run( impl.id, label, - p, + assumption, type, - associated_type + target_type ) } } diff --git a/database/scripts/test.ts b/database/scripts/test.ts index 79ef2c916..24af5a1c9 100644 --- a/database/scripts/test.ts +++ b/database/scripts/test.ts @@ -315,18 +315,18 @@ function test_adjoint_functor_relationships() { { query: ` SELECT - sm1.structure_id AS right_1, - sm1.associated_structure_id AS left, - sm2.associated_structure_id AS right_2 - FROM associated_structures sm1 - LEFT JOIN associated_structures sm2 + ass1.source_structure_id AS right_1, + ass1.target_structure_id AS left, + ass2.target_structure_id AS right_2 + FROM associated_structures ass1 + LEFT JOIN associated_structures ass2 ON - sm2.type = 'functor' - AND sm2.structure_id = sm1.associated_structure_id - AND sm2.label = 'right_adjoint' + ass2.source_type = 'functor' + AND ass2.label = 'right_adjoint' + AND ass2.source_structure_id = ass1.target_structure_id WHERE - sm1.type = 'functor' - AND sm1.label = 'left_adjoint' + ass1.source_type = 'functor' + AND ass1.label = 'left_adjoint' AND (right_2 IS NULL OR right_2 <> right_1) `, format: ({ right_1, left, right_2 }) => @@ -335,18 +335,18 @@ function test_adjoint_functor_relationships() { { query: ` SELECT - sm1.structure_id AS left_1, - sm1.associated_structure_id AS right, - sm2.associated_structure_id AS left_2 - FROM associated_structures sm1 - LEFT JOIN associated_structures sm2 + ass1.source_structure_id AS left_1, + ass1.target_structure_id AS right, + ass2.target_structure_id AS left_2 + FROM associated_structures ass1 + LEFT JOIN associated_structures ass2 ON - sm2.type = 'functor' - AND sm2.structure_id = sm1.associated_structure_id - AND sm2.label = 'left_adjoint' + ass2.source_type = 'functor' + AND ass2.label = 'left_adjoint' + AND ass2.source_structure_id = ass1.target_structure_id WHERE - sm1.type = 'functor' - AND sm1.label = 'right_adjoint' + ass1.source_type = 'functor' + AND ass1.label = 'right_adjoint' AND (left_2 IS NULL OR left_2 <> left_1) `, format: ({ left_1, right, left_2 }) => @@ -355,24 +355,24 @@ function test_adjoint_functor_relationships() { { query: ` SELECT - sm.structure_id AS functor, - sm.associated_structure_id AS left_adjoint, - dom.associated_structure_id AS functor_domain, - adj_cod.associated_structure_id AS left_adjoint_codomain + ass.source_structure_id AS functor, + ass.target_structure_id AS left_adjoint, + dom.target_structure_id AS functor_domain, + adj_cod.target_structure_id AS left_adjoint_codomain FROM - associated_structures sm + associated_structures ass INNER JOIN associated_structures dom ON dom.label = 'domain' - AND dom.type = 'functor' - AND dom.structure_id = sm.structure_id + AND dom.source_type = 'functor' + AND dom.source_structure_id = ass.source_structure_id INNER JOIN associated_structures adj_cod ON adj_cod.label = 'codomain' - AND adj_cod.type = 'functor' - AND adj_cod.structure_id = sm.associated_structure_id + AND adj_cod.source_type = 'functor' + AND adj_cod.source_structure_id = ass.target_structure_id WHERE - sm.label = 'left_adjoint' + ass.label = 'left_adjoint' AND functor_domain <> left_adjoint_codomain `, format: ({ functor, left_adjoint, functor_domain, left_adjoint_codomain }) => @@ -381,24 +381,24 @@ function test_adjoint_functor_relationships() { { query: ` SELECT - sm.structure_id AS functor, - sm.associated_structure_id AS left_adjoint, - cod.associated_structure_id AS functor_codomain, - adj_dom.associated_structure_id AS left_adjoint_domain + ass.source_structure_id AS functor, + ass.target_structure_id AS left_adjoint, + cod.target_structure_id AS functor_codomain, + adj_dom.target_structure_id AS left_adjoint_domain FROM - associated_structures sm + associated_structures ass INNER JOIN associated_structures cod ON cod.label = 'codomain' - AND cod.type = 'functor' - AND cod.structure_id = sm.structure_id + AND cod.source_type = 'functor' + AND cod.source_structure_id = ass.source_structure_id INNER JOIN associated_structures adj_dom ON adj_dom.label = 'domain' - AND adj_dom.type = 'functor' - AND adj_dom.structure_id = sm.associated_structure_id + AND adj_dom.source_type = 'functor' + AND adj_dom.source_structure_id = ass.target_structure_id WHERE - sm.label = 'left_adjoint' + ass.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/seed.types.ts b/database/scripts/utils/seed.types.ts index 3220b3752..b2b8e2871 100644 --- a/database/scripts/utils/seed.types.ts +++ b/database/scripts/utils/seed.types.ts @@ -13,19 +13,19 @@ export type ConfigYaml = { negation: string conditional: string }[] - special_object_types: { - type: string + special_objects: { + kind: string dual: string }[] - special_morphism_types: { - type: string + special_morphisms: { + kind: string dual: string }[] } export type SpecialMorphismRuleYaml = { property: string - type: string + kind: string description: string proof: string } diff --git a/database/scripts/utils/structures.ts b/database/scripts/utils/structures.ts index ea8037204..f4b92dd20 100644 --- a/database/scripts/utils/structures.ts +++ b/database/scripts/utils/structures.ts @@ -40,9 +40,9 @@ export function get_structures(db: Database, type: StructureType): StructureMeta json_group_array(pa.property_id) AS props FROM structures s LEFT JOIN associated_structures ass - ON ass.structure_id = s.id + ON ass.source_structure_id = s.id LEFT JOIN property_assignments pa - ON pa.structure_id = ass.associated_structure_id + ON pa.structure_id = ass.target_structure_id AND pa.is_satisfied = TRUE WHERE s.type = ? GROUP BY s.id, ass.label @@ -83,11 +83,13 @@ export function is_dual_structure( */ export function get_structure_parent_map(db: Database, type: StructureType) { const structures = db - .prepare< - [StructureType], - { id: string; parent: string | null } - >(`SELECT id, parent FROM structures WHERE type = ?`) + .prepare<[StructureType], { id: string; parent_structure_id: string | null }>( + `SELECT id, parent_structure_id + FROM structures WHERE type = ?` + ) .all(type) - return new Map(structures.map((structure) => [structure.id, structure.parent])) + return new Map( + structures.map((structure) => [structure.id, structure.parent_structure_id]) + ) } diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 4969fb48a..00f56c077 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -15,7 +15,7 @@ export type RelatedStructure = StructureShort & { notation: string } export type AssociatedStructure = RelatedStructure & { label: string - associated_type: StructureType + type: StructureType } export type StructureDisplay = { @@ -27,12 +27,12 @@ export type StructureDisplay = { dual_structure_id: string | null dual_structure_name: string | null dual_structure_notation: string | null - parent: string | null + parent_structure_id: string | null parent_name: string | null parent_notation: string | null } -export type AssociatedTypes = Record +export type TargetTypes = Record export type CommentObject = { id: number; comment: string } @@ -78,12 +78,12 @@ export type CategoryDefinition = { } export type SpecialObject = { - type: string + kind: string description: string } export type SpecialMorphism = { - type: string + kind: string // null when the morphisms of this type have not been determined description: string | null proof: string diff --git a/src/lib/server/fetchers/category.ts b/src/lib/server/fetchers/category.ts index ddd3d5bda..d7e3b9b7d 100644 --- a/src/lib/server/fetchers/category.ts +++ b/src/lib/server/fetchers/category.ts @@ -19,22 +19,22 @@ export function fetch_category(id: string) { const special_objects = db .prepare<[string], SpecialObject>( - `SELECT o.type, o.description - FROM special_object_assignments o - INNER JOIN special_object_types t - ON t.type = o.type - WHERE o.category_id = ? - ORDER BY t.id` + `SELECT soa.kind, soa.description + FROM special_object_assignments soa + INNER JOIN special_objects so + ON so.kind = soa.kind + WHERE soa.category_id = ? + ORDER BY so.id` ) .all(id) const special_morphisms = db .prepare<[string], SpecialMorphism>( - `SELECT t.type, s.description, s.proof - FROM special_morphism_types t - LEFT JOIN special_morphism_assignments s - ON s.type = t.type AND s.category_id = ? - ORDER BY t.id` + `SELECT sm.kind, sma.description, sma.proof + FROM special_morphisms sm + LEFT JOIN special_morphism_assignments sma + ON sma.kind = sm.kind AND sma.category_id = ? + ORDER BY sm.id` ) .all(id) @@ -54,10 +54,10 @@ export function fetch_categories_with_missing_morphisms() { s.name, COUNT(*) AS count FROM structures s - JOIN special_morphism_types t - LEFT JOIN special_morphism_assignments m - ON m.category_id = s.id AND m.type = t.type - WHERE s.type = 'category' AND m.type IS NULL + JOIN special_morphisms sm + LEFT JOIN special_morphism_assignments sma + ON sma.category_id = s.id AND sma.kind = sm.kind + WHERE s.type = 'category' AND sma.kind IS NULL GROUP BY s.id ORDER BY lower(s.name)` ) diff --git a/src/lib/server/fetchers/implication.ts b/src/lib/server/fetchers/implication.ts index d357d72c6..3509c4223 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, - AssociatedTypes, + TargetTypes, StructureShort, StructureType } from '$lib/commons/types' @@ -44,19 +44,19 @@ export function fetch_implication(type: StructureType, id: string) { ) .all(type, id) - const associated_structure_types = db - .prepare<[StructureType], { label: string; associated_type: StructureType }>( - `SELECT label, associated_type - FROM associated_structure_types - WHERE type = ?` + const structure_associations = db + .prepare<[StructureType], { label: string; target_type: StructureType }>( + `SELECT label, target_type + FROM structure_associations + WHERE source_type = ?` ) .all(type) - const associated_types: AssociatedTypes = {} + const target_types: TargetTypes = {} - for (const { label, associated_type } of associated_structure_types) { - associated_types[label] = associated_type + for (const { label, target_type } of structure_associations) { + target_types[label] = target_type } - return { type, implication, property_relation_dict, structures, associated_types } + return { type, implication, property_relation_dict, structures, target_types } } diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts index 460b8822d..884111b29 100644 --- a/src/lib/server/fetchers/structure.ts +++ b/src/lib/server/fetchers/structure.ts @@ -26,12 +26,12 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai s.dual_structure_id, ds.name AS dual_structure_name, ds.notation AS dual_structure_notation, - s.parent, + s.parent_structure_id, ps.name AS parent_name, ps.notation AS parent_notation FROM structures s LEFT JOIN structures ds ON ds.id = s.dual_structure_id - LEFT JOIN structures ps ON ps.id = s.parent + LEFT JOIN structures ps ON ps.id = s.parent_structure_id WHERE s.id = ?` ) .get(id) @@ -46,12 +46,12 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai s.id, s.name, s.notation, - a.label, - a.associated_type - FROM associated_structures a + s.type, + ass.label + FROM associated_structures ass INNER JOIN structures s - ON s.id = a.associated_structure_id - WHERE a.structure_id = ?` + ON s.id = ass.target_structure_id + WHERE ass.source_structure_id = ?` ) .all(id) @@ -70,17 +70,17 @@ 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 + `SELECT DISTINCT s.id, s.name, s.type FROM associated_structures a INNER JOIN structures s - ON s.id = a.structure_id - INNER JOIN associated_structure_types ast + ON s.id = a.source_structure_id + INNER JOIN structure_associations sa ON - 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)` + sa.label = a.label + AND sa.source_type = a.source_type + AND sa.target_type = a.target_type + WHERE a.target_structure_id = ? AND sa.required = TRUE + ORDER BY s.type, lower(s.name)` ) .all(id) @@ -94,7 +94,7 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai const children = db .prepare<[string], RelatedStructure>( `SELECT s.id, s.name, s.notation - FROM structures s WHERE s.parent = ?` + FROM structures s WHERE s.parent_structure_id = ?` ) .all(id) diff --git a/src/pages/CategoryPage.svelte b/src/pages/CategoryPage.svelte index 47aa6102e..fa8bca1a3 100644 --- a/src/pages/CategoryPage.svelte +++ b/src/pages/CategoryPage.svelte @@ -26,7 +26,7 @@ {#if data.special_objects.length}
    {#each data.special_objects as obj} -
  • {obj.type}: {@html obj.description}
    • +
  • {obj.kind}: {@html obj.description}
    • {/each}
{:else} @@ -42,9 +42,9 @@
  • {#if morph.description} - {morph.type}: {@html morph.description} + {morph.kind}: {@html morph.description} {:else} - {morph.type}: + {morph.kind}: {/if}
    • diff --git a/src/pages/ImplicationPage.svelte b/src/pages/ImplicationPage.svelte index 9eee9c025..31c790a6b 100644 --- a/src/pages/ImplicationPage.svelte +++ b/src/pages/ImplicationPage.svelte @@ -7,7 +7,7 @@ import type { ImplicationDisplay, StructureShort, - AssociatedTypes, + TargetTypes, StructureType } from '$lib/commons/types' import { PLURALS } from '$shared/config' @@ -18,17 +18,12 @@ type: StructureType implication: ImplicationDisplay structures: StructureShort[] - associated_types: AssociatedTypes + target_types: TargetTypes property_relation_dict: Record> } - let { - type, - implication, - structures, - associated_types, - property_relation_dict - }: Props = $props() + let { type, implication, structures, target_types, property_relation_dict }: Props = + $props() let has_associated_assumptions = $derived( Object.values(implication.associated_assumptions).some((list) => list?.size) @@ -54,8 +49,8 @@ whose {remove_underscores(label)} {#each set as property, index} - {property_relation_dict[associated_types[label]][property]} - {get_property_label(property)}{#if index < set.size - 1}  and  diff --git a/src/pages/StructurePage.svelte b/src/pages/StructurePage.svelte index 63084f6d0..9ae2ba54e 100644 --- a/src/pages/StructurePage.svelte +++ b/src/pages/StructurePage.svelte @@ -6,34 +6,11 @@ import TagList from '$components/TagList.svelte' import IndistinguishableStructures from '$components/IndistinguishableStructures.svelte' import StructuresBasedOn from '$components/StructuresBasedOn.svelte' - import type { - AssociatedStructure, - CommentObject, - PropertyAssignmentDisplay, - PropertyShort, - RelatedStructure, - StructureDisplay, - StructureShort, - StructureShortDictionary, - StructureType - } from '$lib/commons/types' + import type { StructureDetails } from '$lib/commons/types' import type { Snippet } from 'svelte' 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[] - tags: string[] - satisfied_properties: PropertyAssignmentDisplay[] - unsatisfied_properties: PropertyAssignmentDisplay[] - unknown_properties: PropertyShort[] - undecidable_properties: PropertyAssignmentDisplay[] - indistinguishable_structures: StructureShort[] - comments: CommentObject[] + type Props = StructureDetails & { definition?: Snippet specials?: Snippet } @@ -73,13 +50,16 @@ {#each associated_structures as a} {capitalize(remove_underscores(a.label))} - {a.name} + {a.name} {/each} - {#if structure.parent} + {#if structure.parent_structure_id} Parent - + {@html structure.parent_notation} diff --git a/src/pages/TaggedStructuresPage.svelte b/src/pages/TaggedStructuresPage.svelte index 39965f897..9b6ec66bc 100644 --- a/src/pages/TaggedStructuresPage.svelte +++ b/src/pages/TaggedStructuresPage.svelte @@ -1,7 +1,7 @@