From eb5d7bfb8d8ca6dbb840989bc990f4299d80388f Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 13 Apr 2026 09:42:05 +0200 Subject: [PATCH 1/6] add dual column to special objects table --- .../006_special-objects/001_special_object_types.sql | 10 +++++----- database/migrations/017_special_objects_duals.sql | 1 + 2 files changed, 6 insertions(+), 5 deletions(-) create mode 100644 database/migrations/017_special_objects_duals.sql diff --git a/database/data/006_special-objects/001_special_object_types.sql b/database/data/006_special-objects/001_special_object_types.sql index 5907dedf..6f192144 100644 --- a/database/data/006_special-objects/001_special_object_types.sql +++ b/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); diff --git a/database/migrations/017_special_objects_duals.sql b/database/migrations/017_special_objects_duals.sql new file mode 100644 index 00000000..137027ed --- /dev/null +++ b/database/migrations/017_special_objects_duals.sql @@ -0,0 +1 @@ +ALTER TABLE special_object_types ADD COLUMN dual TEXT REFERENCES special_object_types (type); \ No newline at end of file From 28fdbe7f447910f9c984de767ae1cba8258f0e3c Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 13 Apr 2026 10:00:22 +0200 Subject: [PATCH 2/6] deduce special objects for dual categories --- scripts/deduce-special-objects.ts | 17 +++++++++++++++++ scripts/deduce.ts | 3 +++ 2 files changed, 20 insertions(+) create mode 100644 scripts/deduce-special-objects.ts diff --git a/scripts/deduce-special-objects.ts b/scripts/deduce-special-objects.ts new file mode 100644 index 00000000..42680d93 --- /dev/null +++ b/scripts/deduce-special-objects.ts @@ -0,0 +1,17 @@ +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) { + 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 + `) +} diff --git a/scripts/deduce.ts b/scripts/deduce.ts index df2618ac..bf336dce 100644 --- a/scripts/deduce.ts +++ b/scripts/deduce.ts @@ -4,6 +4,7 @@ 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' dotenv.config({ quiet: true }) @@ -22,5 +23,7 @@ await db.execute('PRAGMA foreign_keys = ON') await deduce_category_implications(db) await deduce_category_properties(db) +await deduce_special_objects(db) + await deduce_functor_implications(db) await deduce_functor_properties(db) From 9131f1029fd96c40f4bc19c83da04f49b9a086bd Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 13 Apr 2026 10:02:48 +0200 Subject: [PATCH 3/6] add dual column to special morphisms table --- .../001_special_morphism_types.sql | 12 ++++++------ database/migrations/018_special_morphism_duals.sql | 1 + 2 files changed, 7 insertions(+), 6 deletions(-) create mode 100644 database/migrations/018_special_morphism_duals.sql diff --git a/database/data/007_special-morphisms/001_special_morphism_types.sql b/database/data/007_special-morphisms/001_special_morphism_types.sql index 5f44c43a..2402de08 100644 --- a/database/data/007_special-morphisms/001_special_morphism_types.sql +++ b/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); \ No newline at end of file +('isomorphisms', 'isomorphisms', 0), +('monomorphisms', 'epimorphisms', 1), +('epimorphisms', 'monomorphisms', 2), +('regular monomorphisms', 'regular epimorphisms', 3), +('regular epimorphisms', 'regular monomorphisms', 4); \ No newline at end of file diff --git a/database/migrations/018_special_morphism_duals.sql b/database/migrations/018_special_morphism_duals.sql new file mode 100644 index 00000000..fde4774d --- /dev/null +++ b/database/migrations/018_special_morphism_duals.sql @@ -0,0 +1 @@ +ALTER TABLE special_morphism_types ADD COLUMN dual TEXT REFERENCES special_morphism_types (type); \ No newline at end of file From d8989f5ee1ade7c759f9e4e30ff33c9fa70985d0 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 13 Apr 2026 10:14:13 +0200 Subject: [PATCH 4/6] deduce special morphisms for dual categories --- scripts/deduce-special-morphisms.ts | 21 +++++++++++++++++++++ scripts/deduce.ts | 2 ++ 2 files changed, 23 insertions(+) create mode 100644 scripts/deduce-special-morphisms.ts diff --git a/scripts/deduce-special-morphisms.ts b/scripts/deduce-special-morphisms.ts new file mode 100644 index 00000000..8910ee97 --- /dev/null +++ b/scripts/deduce-special-morphisms.ts @@ -0,0 +1,21 @@ +import { Client } from '@libsql/client' + +export async function deduce_special_morphisms(db: Client) { + await deduce_special_morphisms_of_dual_categories(db) +} + +async function deduce_special_morphisms_of_dual_categories(db: Client) { + 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 + `) +} diff --git a/scripts/deduce.ts b/scripts/deduce.ts index bf336dce..ce7c7838 100644 --- a/scripts/deduce.ts +++ b/scripts/deduce.ts @@ -5,6 +5,7 @@ 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 }) @@ -24,6 +25,7 @@ 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) From 2c5483842712427498d1e1d8dab7b743adacddb7 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 13 Apr 2026 10:15:27 +0200 Subject: [PATCH 5/6] add logs for dualization --- scripts/deduce-special-morphisms.ts | 4 +++- scripts/deduce-special-objects.ts | 9 +++++++-- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/scripts/deduce-special-morphisms.ts b/scripts/deduce-special-morphisms.ts index 8910ee97..32ca8ee2 100644 --- a/scripts/deduce-special-morphisms.ts +++ b/scripts/deduce-special-morphisms.ts @@ -5,7 +5,7 @@ export async function deduce_special_morphisms(db: Client) { } async function deduce_special_morphisms_of_dual_categories(db: Client) { - await db.execute(` + const res = await db.execute(` INSERT INTO special_morphisms (category_id, type, description, reason) SELECT c.dual_category_id, @@ -18,4 +18,6 @@ async function deduce_special_morphisms_of_dual_categories(db: Client) { WHERE c.dual_category_id IS NOT NULL ON CONFLICT DO NOTHING `) + + console.info(`Dualized ${res.rowsAffected} special morphisms`) } diff --git a/scripts/deduce-special-objects.ts b/scripts/deduce-special-objects.ts index 42680d93..b5341238 100644 --- a/scripts/deduce-special-objects.ts +++ b/scripts/deduce-special-objects.ts @@ -5,13 +5,18 @@ export async function deduce_special_objects(db: Client) { } async function deduce_special_objects_of_dual_categories(db: Client) { - await db.execute(` + const res = await db.execute(` INSERT INTO special_objects (category_id, type, description) - SELECT c.dual_category_id, t.dual, o.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`) } From 1ff9070e80d599c7ed08bc089f49838d8cfb5460 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 13 Apr 2026 10:20:11 +0200 Subject: [PATCH 6/6] document TODOs --- scripts/deduce-special-morphisms.ts | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/deduce-special-morphisms.ts b/scripts/deduce-special-morphisms.ts index 32ca8ee2..41197f1f 100644 --- a/scripts/deduce-special-morphisms.ts +++ b/scripts/deduce-special-morphisms.ts @@ -2,6 +2,9 @@ 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) {