From 1d75e887bd9de87d725805feae3a09494bc39bd8 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 3 Jul 2026 08:28:55 +0200 Subject: [PATCH 1/2] make (id, type) the primary key for properties --- databases/catdat/schema/002_properties.sql | 8 ++++---- databases/catdat/scripts/deduce-implications.ts | 9 ++++++--- databases/catdat/scripts/utils/properties.ts | 2 +- src/lib/server/fetchers/missing_data.ts | 14 +++++--------- src/lib/server/fetchers/properties.ts | 2 +- src/lib/server/fetchers/property.ts | 4 ++-- src/lib/server/fetchers/search.ts | 3 +-- src/lib/server/fetchers/structure.ts | 10 +++++----- 8 files changed, 25 insertions(+), 27 deletions(-) diff --git a/databases/catdat/schema/002_properties.sql b/databases/catdat/schema/002_properties.sql index 64e83018..89710619 100644 --- a/databases/catdat/schema/002_properties.sql +++ b/databases/catdat/schema/002_properties.sql @@ -4,28 +4,28 @@ CREATE TABLE relations ( ); CREATE TABLE properties ( - id TEXT PRIMARY KEY, + id TEXT NOT NULL, type TEXT NOT NULL, relation TEXT NOT NULL, description TEXT NOT NULL CHECK (length(description) > 0), nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'), invariant_under_equivalences INTEGER NOT NULL DEFAULT TRUE, dual_property_id TEXT, - UNIQUE (id, type), -- TODO: make (id, type) the primary key + PRIMARY KEY (id, type), FOREIGN KEY (relation) REFERENCES relations (relation) ON DELETE RESTRICT, FOREIGN KEY (dual_property_id, type) REFERENCES properties (id, type) ON DELETE RESTRICT, FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT ); -CREATE UNIQUE INDEX properties_lower_id_unique ON properties (lower(id)); +CREATE UNIQUE INDEX properties_lower_id_unique ON properties (lower(id), type); CREATE TABLE related_properties ( property_id TEXT NOT NULL, related_property_id TEXT NOT NULL, type TEXT NOT NULL, CHECK (property_id != related_property_id), - PRIMARY KEY (property_id, related_property_id), + PRIMARY KEY (property_id, related_property_id, type), FOREIGN KEY (property_id, type) REFERENCES properties (id, type) ON DELETE CASCADE, FOREIGN KEY (related_property_id, type) diff --git a/databases/catdat/scripts/deduce-implications.ts b/databases/catdat/scripts/deduce-implications.ts index c8f8e06d..033d1205 100644 --- a/databases/catdat/scripts/deduce-implications.ts +++ b/databases/catdat/scripts/deduce-implications.ts @@ -45,13 +45,15 @@ export function create_dualized_implications(type: StructureType) { ( SELECT json_group_array(p.dual_property_id) FROM assumptions a - LEFT JOIN properties p ON p.id = a.property_id + LEFT JOIN properties p + ON p.id = a.property_id AND p.type = i.type WHERE a.implication_id = i.id ) AS dual_assumptions, ( SELECT json_group_array(p.dual_property_id) FROM conclusions a - LEFT JOIN properties p ON p.id = a.property_id + LEFT JOIN properties p + ON p.id = a.property_id AND p.type = i.type WHERE a.implication_id = i.id ) AS dual_conclusions, ( @@ -61,7 +63,8 @@ export function create_dualized_implications(type: StructureType) { a.map, json_group_array(p.dual_property_id) AS properties FROM mapped_assumptions a - INNER JOIN properties p ON p.id = a.property_id + 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 ) diff --git a/databases/catdat/scripts/utils/properties.ts b/databases/catdat/scripts/utils/properties.ts index b9a1d5b0..68bfc47b 100644 --- a/databases/catdat/scripts/utils/properties.ts +++ b/databases/catdat/scripts/utils/properties.ts @@ -24,7 +24,7 @@ export function get_properties_dict(db: Database, type: StructureType) { r.conditional AS conditional_relation FROM properties p INNER JOIN relations r ON r.relation = p.relation - WHERE type = ? + WHERE p.type = ? ORDER BY lower(p.id)`, ) .all(type) diff --git a/src/lib/server/fetchers/missing_data.ts b/src/lib/server/fetchers/missing_data.ts index 80996ed3..3eaaa43d 100644 --- a/src/lib/server/fetchers/missing_data.ts +++ b/src/lib/server/fetchers/missing_data.ts @@ -18,13 +18,12 @@ export function fetch_missing_data(type: StructureType) { sql` SELECT s.id, s.name, COUNT(*) AS count FROM structures s - INNER JOIN properties p + INNER JOIN properties p ON p.type = s.type LEFT JOIN property_assignments pa ON pa.structure_id = s.id AND pa.property_id = p.id WHERE - p.type = ${type} - AND s.type = ${type} + s.type = ${type} AND pa.property_id IS NULL GROUP BY s.id ORDER BY lower(s.name); @@ -36,16 +35,13 @@ export function fetch_missing_data(type: StructureType) { s2.id AS id2, s2.name AS name2 FROM structures s1 JOIN structures s2 - ON s1.id < s2.id - JOIN properties p + 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 - WHERE - p.type = ${type} - AND s1.type = ${type} - AND s2.type = ${type} + WHERE s1.type = ${type} GROUP BY s1.id, s1.name, s2.id, s2.name HAVING SUM( CASE diff --git a/src/lib/server/fetchers/properties.ts b/src/lib/server/fetchers/properties.ts index 8dbd4ca8..3c90e8da 100644 --- a/src/lib/server/fetchers/properties.ts +++ b/src/lib/server/fetchers/properties.ts @@ -83,7 +83,7 @@ export function fetch_tagged_properties(type: StructureType, tag: string) { SELECT p.id, p.relation FROM property_tag_assignments t INNER JOIN properties p - ON p.id = t.property_id + ON p.id = t.property_id AND p.type = ${type} WHERE t.tag = ${tag} AND t.type = ${type} ORDER BY lower(id) `) diff --git a/src/lib/server/fetchers/property.ts b/src/lib/server/fetchers/property.ts index 5677f693..105c9212 100644 --- a/src/lib/server/fetchers/property.ts +++ b/src/lib/server/fetchers/property.ts @@ -31,13 +31,13 @@ export function fetch_property(type: StructureType, id: string) { nlab_link, invariant_under_equivalences FROM properties - WHERE id = ${id} + WHERE id = ${id} AND type = ${type} `, // related properties sql` SELECT related_property_id AS id FROM related_properties - WHERE property_id = ${id} + WHERE property_id = ${id} AND type = ${type} ORDER BY lower(id) `, // tags diff --git a/src/lib/server/fetchers/search.ts b/src/lib/server/fetchers/search.ts index c363df58..42eb75ee 100644 --- a/src/lib/server/fetchers/search.ts +++ b/src/lib/server/fetchers/search.ts @@ -99,7 +99,7 @@ export function fetch_search_results( SELECT s.id, s.name FROM structures s INNER JOIN property_assignments a ON a.structure_id = s.id WHERE - a.type = ? AND s.type = ? + s.type = ? AND a.type = s.type AND property_id IN (${to_placeholders(all_selected_properties)}) GROUP BY structure_id HAVING @@ -128,7 +128,6 @@ export function fetch_search_results( const { rows: found_structures, err } = query({ sql: search_query, values: [ - type, type, ...all_selected_properties, ...satisfied_properties, diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts index fbfa1e9b..9929f93c 100644 --- a/src/lib/server/fetchers/structure.ts +++ b/src/lib/server/fetchers/structure.ts @@ -68,7 +68,8 @@ export function fetch_structure(type: StructureType, id: string) { pa.is_deduced, p.relation FROM property_assignments pa - INNER JOIN properties p ON p.id = pa.property_id + INNER JOIN properties p + ON p.id = pa.property_id AND p.type = pa.type WHERE pa.structure_id = ${id} ORDER BY pa.id `, @@ -76,7 +77,7 @@ export function fetch_structure(type: StructureType, id: string) { sql` SELECT p.id, p.relation FROM properties p - WHERE type = ${type} AND NOT EXISTS ( + WHERE p.type = ${type} AND NOT EXISTS ( SELECT 1 FROM property_assignments WHERE structure_id = ${id} AND property_id = p.id ) @@ -86,7 +87,7 @@ export function fetch_structure(type: StructureType, id: string) { sql` SELECT u.id, u.name FROM structures u - JOIN properties p + JOIN properties p ON p.type = u.type LEFT JOIN property_assignments pa ON pa.structure_id = ${id} AND pa.property_id = p.id @@ -94,8 +95,7 @@ export function fetch_structure(type: StructureType, id: string) { ON up.structure_id = u.id AND up.property_id = p.id WHERE - p.type = ${type} - AND u.type = ${type} + u.type = ${type} AND u.id != ${id} GROUP BY u.id, u.name HAVING SUM( From 00af974cfbeb489dbd3887f59531275ace963317 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 3 Jul 2026 20:03:50 +0200 Subject: [PATCH 2/2] add regular and coregular functors this proves that now different properties can have the same name across different structure types (regular functor != regular category), implemented in the previous commit --- .../functor-implications/limits preservation.yaml | 9 +++++++++ .../catdat/data/functor-properties/coregular.yaml | 13 +++++++++++++ .../catdat/data/functor-properties/regular.yaml | 13 +++++++++++++ .../catdat/scripts/expected-data/forget_vector.json | 4 +++- databases/catdat/scripts/expected-data/id_Set.json | 4 +++- 5 files changed, 41 insertions(+), 2 deletions(-) create mode 100644 databases/catdat/data/functor-properties/coregular.yaml create mode 100644 databases/catdat/data/functor-properties/regular.yaml diff --git a/databases/catdat/data/functor-implications/limits preservation.yaml b/databases/catdat/data/functor-implications/limits preservation.yaml index eb8aa8ea..aba24134 100644 --- a/databases/catdat/data/functor-implications/limits preservation.yaml +++ b/databases/catdat/data/functor-implications/limits preservation.yaml @@ -194,3 +194,12 @@ - preserves finite coproducts proof: This is trivial. is_equivalence: false + +- id: regular_functor_definition + assumptions: + - left exact + - preserves regular epimorphisms + conclusions: + - regular + proof: This holds by definition of a regular functor. + is_equivalence: true diff --git a/databases/catdat/data/functor-properties/coregular.yaml b/databases/catdat/data/functor-properties/coregular.yaml new file mode 100644 index 00000000..8d9a70f5 --- /dev/null +++ b/databases/catdat/data/functor-properties/coregular.yaml @@ -0,0 +1,13 @@ +id: coregular +relation: is +description: 'A functor $F : \C \to \D$ is coregular when it preserves finite colimits and regular monomorphisms. This notion is used in particular when $\C$ and $\D$ are coregular categories.' +nlab_link: null +invariant_under_equivalences: true +dual_property: regular +related_properties: + - right exact + - preserves regular monomorphisms + +tags: + - colimit preservation + - morphism behavior diff --git a/databases/catdat/data/functor-properties/regular.yaml b/databases/catdat/data/functor-properties/regular.yaml new file mode 100644 index 00000000..8e0801b1 --- /dev/null +++ b/databases/catdat/data/functor-properties/regular.yaml @@ -0,0 +1,13 @@ +id: regular +relation: is +description: 'A functor $F : \C \to \D$ is regular when it preserves finite limits and regular epimorphisms. This notion is used in particular when $\C$ and $\D$ are regular categories.' +nlab_link: https://ncatlab.org/nlab/show/regular+functor +invariant_under_equivalences: true +dual_property: coregular +related_properties: + - left exact + - preserves regular epimorphisms + +tags: + - limit preservation + - morphism behavior diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json index bf3952fe..aa0394b2 100644 --- a/databases/catdat/scripts/expected-data/forget_vector.json +++ b/databases/catdat/scripts/expected-data/forget_vector.json @@ -42,5 +42,7 @@ "preserves reflexive coequalizers": true, "preserves coreflexive equalizers": true, "preserves regular monomorphisms": true, - "preserves regular epimorphisms": true + "preserves regular epimorphisms": true, + "regular": true, + "coregular": false } diff --git a/databases/catdat/scripts/expected-data/id_Set.json b/databases/catdat/scripts/expected-data/id_Set.json index bda5a5f9..cbca186a 100644 --- a/databases/catdat/scripts/expected-data/id_Set.json +++ b/databases/catdat/scripts/expected-data/id_Set.json @@ -41,5 +41,7 @@ "dominant": true, "isomorphism": true, "preserves regular monomorphisms": true, - "preserves regular epimorphisms": true + "preserves regular epimorphisms": true, + "regular": true, + "coregular": true }