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/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/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 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 diff --git a/scripts/deduce-special-morphisms.ts b/scripts/deduce-special-morphisms.ts new file mode 100644 index 00000000..41197f1f --- /dev/null +++ b/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`) +} diff --git a/scripts/deduce-special-objects.ts b/scripts/deduce-special-objects.ts new file mode 100644 index 00000000..b5341238 --- /dev/null +++ b/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`) +} diff --git a/scripts/deduce.ts b/scripts/deduce.ts index df2618ac..ce7c7838 100644 --- a/scripts/deduce.ts +++ b/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)