Identify properties by ID and type

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

databases/catdat/data/functor-properties/coregular.yaml

@@ -0,0 +1,13 @@
+id: coregular
+relation: is
+description: 'A functor $F : \C \to \D$ is <i>coregular</i> 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

databases/catdat/data/functor-properties/regular.yaml

@@ -0,0 +1,13 @@
+id: regular
+relation: is
+description: 'A functor $F : \C \to \D$ is <i>regular</i> 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

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)

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
 				)

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
 }

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
 }

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)

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

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)
 	`)

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

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<StructureShort>({
 		sql: search_query,
 		values: [
-			type,
 			type,
 			...all_selected_properties,
 			...satisfied_properties,

src/lib/server/fetchers/structure.ts

@@ -68,15 +68,16 @@ 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
         `,
 		// unknown properties
 		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,16 +87,15 @@ 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
             LEFT JOIN property_assignments up
                 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(