Dualize special objects and morphisms for dual categories

database/data/006_special-objects/001_special_object_types.sql

@@ -1,6 +1,6 @@
-INSERT INTO special_object_types (type, position)
+INSERT INTO special_object_types (type, dual, position)
 VALUES
-('terminal object', 0),
-('initial object', 1),
-('products', 2),
-('coproducts', 3);
+('terminal object', 'initial object', 0),
+('initial object', 'terminal object', 1),
+('products', 'coproducts', 2),
+('coproducts', 'products', 3);

database/data/007_special-morphisms/001_special_morphism_types.sql

@@ -1,7 +1,7 @@
-INSERT INTO special_morphism_types (type, position)
+INSERT INTO special_morphism_types (type, dual, position)
 VALUES
-('isomorphisms', 0),
-('monomorphisms', 1),
-('epimorphisms', 2),
-('regular monomorphisms', 3),
-('regular epimorphisms', 4);
+('isomorphisms', 'isomorphisms', 0),
+('monomorphisms', 'epimorphisms', 1),
+('epimorphisms', 'monomorphisms', 2),
+('regular monomorphisms', 'regular epimorphisms', 3),
+('regular epimorphisms', 'regular monomorphisms', 4);

database/migrations/017_special_objects_duals.sql

@@ -0,0 +1 @@
+ALTER TABLE special_object_types ADD COLUMN dual TEXT REFERENCES special_object_types (type);

database/migrations/018_special_morphism_duals.sql

@@ -0,0 +1 @@
+ALTER TABLE special_morphism_types ADD COLUMN dual TEXT REFERENCES special_morphism_types (type);

scripts/deduce-special-morphisms.ts

@@ -0,0 +1,26 @@
+import { Client } from '@libsql/client'
+
+export async function deduce_special_morphisms(db: Client) {
+	await deduce_special_morphisms_of_dual_categories(db)
+	// TODO: deduce further morphisms,
+	// e.g. isomorphisms = bijective morphisms in algebraic categories,
+	// e.g. regular monomorphisms = same as monomorphisms in mono-regular categories,
+}
+
+async function deduce_special_morphisms_of_dual_categories(db: Client) {
+	const res = await db.execute(`
+        INSERT INTO special_morphisms (category_id, type, description, reason)
+        SELECT
+            c.dual_category_id,
+            t.dual,
+            m.description,
+            'This is deduced from its dual category.'
+        FROM categories c
+        INNER JOIN special_morphisms m ON m.category_id = c.id
+        INNER JOIN special_morphism_types t ON t.type = m.type
+        WHERE c.dual_category_id IS NOT NULL
+        ON CONFLICT DO NOTHING
+    `)
+
+	console.info(`Dualized ${res.rowsAffected} special morphisms`)
+}

scripts/deduce-special-objects.ts

@@ -0,0 +1,22 @@
+import { Client } from '@libsql/client'
+
+export async function deduce_special_objects(db: Client) {
+	await deduce_special_objects_of_dual_categories(db)
+}
+
+async function deduce_special_objects_of_dual_categories(db: Client) {
+	const res = await db.execute(`
+        INSERT INTO special_objects (category_id, type, description)
+        SELECT
+            c.dual_category_id,
+            t.dual,
+            o.description
+        FROM categories c
+        INNER JOIN special_objects o ON o.category_id = c.id
+        INNER JOIN special_object_types t ON t.type = o.type
+        WHERE c.dual_category_id IS NOT NULL
+        ON CONFLICT DO NOTHING
+    `)
+
+	console.info(`Dualized ${res.rowsAffected} special objects`)
+}

scripts/deduce.ts

@@ -4,6 +4,8 @@ import { deduce_category_implications } from './deduce-category-implications'
 import { deduce_category_properties } from './deduce-category-properties'
 import { deduce_functor_implications } from './deduce-functor-implications'
 import { deduce_functor_properties } from './deduce-functor-properties'
+import { deduce_special_objects } from './deduce-special-objects'
+import { deduce_special_morphisms } from './deduce-special-morphisms'
 
 dotenv.config({ quiet: true })
 
@@ -22,5 +24,8 @@ await db.execute('PRAGMA foreign_keys = ON')
 await deduce_category_implications(db)
 await deduce_category_properties(db)
 
+await deduce_special_objects(db)
+await deduce_special_morphisms(db)
+
 await deduce_functor_implications(db)
 await deduce_functor_properties(db)