diff --git a/DATABASE.md b/DATABASE.md index f994351f5..fc1cea5fd 100644 --- a/DATABASE.md +++ b/DATABASE.md @@ -103,6 +103,6 @@ to check for redundant assignments of properties to categorical structures. ## Diagram -This is the database schema as of 15.08.2026; changes may occur. +This is the database schema as of 18.09.2026; changes may occur. -database diagram +database diagram diff --git a/database/schema/003_implications.sql b/database/schema/003_implications.sql index 139793596..35b27e616 100644 --- a/database/schema/003_implications.sql +++ b/database/schema/003_implications.sql @@ -5,8 +5,10 @@ CREATE TABLE implications ( is_equivalence INTEGER NOT NULL DEFAULT FALSE CHECK (is_equivalence IN (TRUE, FALSE)), is_deduced INTEGER NOT NULL DEFAULT FALSE, + dual_implication_id TEXT, UNIQUE (id, type), - FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT + FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE RESTRICT, + FOREIGN KEY (dual_implication_id) REFERENCES implications (id) ); CREATE UNIQUE INDEX idx_implications_lower_id_unique ON implications (lower(id)); @@ -64,6 +66,7 @@ CREATE VIEW implications_view AS i.is_equivalence, i.is_deduced, i.proof, + i.dual_implication_id, ( SELECT json_group_array(a.property_id) FROM assumptions a WHERE a.implication_id = i.id diff --git a/database/scripts/deduce-implications.ts b/database/scripts/deduce-implications.ts index 75d955f18..896d7ed57 100644 --- a/database/scripts/deduce-implications.ts +++ b/database/scripts/deduce-implications.ts @@ -83,8 +83,12 @@ export function create_dualized_implications(type: StructureType) { const implication_insert = db.prepare(` INSERT INTO implications - (id, type, is_equivalence, proof, is_deduced) - VALUES (?, ?, ?, ?, TRUE) + (id, type, is_equivalence, proof, is_deduced, dual_implication_id) + VALUES (?, ?, ?, ?, TRUE, ?) + `) + + const dual_update = db.prepare(` + UPDATE implications SET dual_implication_id = ? WHERE id = ? `) const assumption_insert = db.prepare(` @@ -139,9 +143,12 @@ export function create_dualized_implications(type: StructureType) { dual_id, type, impl.is_equivalence, - `This follows from the dual implication.` + `This follows from the dual implication.`, + impl.id ) + dual_update.run(dual_id, impl.id) + for (const a of dual_assumptions) { assumption_insert.run(dual_id, a, type) } diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index d4c5f4599..4969fb48a 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -94,6 +94,7 @@ export type ImplicationDB = { is_equivalence: 0 | 1 is_deduced: 0 | 1 proof: string + dual_implication_id?: string | null assumptions: string conclusions: string associated_assumptions: string diff --git a/src/lib/server/fetchers/implication.ts b/src/lib/server/fetchers/implication.ts index e537723ad..d357d72c6 100644 --- a/src/lib/server/fetchers/implication.ts +++ b/src/lib/server/fetchers/implication.ts @@ -19,6 +19,7 @@ export function fetch_implication(type: StructureType, id: string) { is_equivalence, is_deduced, proof, + dual_implication_id, assumptions, conclusions, associated_assumptions diff --git a/src/lib/server/transforms.ts b/src/lib/server/transforms.ts index aff337e0f..6c77293cf 100644 --- a/src/lib/server/transforms.ts +++ b/src/lib/server/transforms.ts @@ -37,6 +37,7 @@ export function display_implication(implication: ImplicationDB): ImplicationDisp is_equivalence: Boolean(implication.is_equivalence), is_deduced: Boolean(implication.is_deduced), proof: implication.proof, + dual_implication_id: implication.dual_implication_id, assumptions: JSON.parse(implication.assumptions), conclusions: JSON.parse(implication.conclusions), associated_assumptions: parse_nested_json_set(implication.associated_assumptions) diff --git a/src/pages/ImplicationPage.svelte b/src/pages/ImplicationPage.svelte index 585f25fa8..9eee9c025 100644 --- a/src/pages/ImplicationPage.svelte +++ b/src/pages/ImplicationPage.svelte @@ -12,7 +12,7 @@ } from '$lib/commons/types' import { PLURALS } from '$shared/config' import Fa from 'svelte-fa' - import { faCircleArrowLeft } from '@fortawesome/free-solid-svg-icons' + import { faCircleArrowLeft, faInfoCircle } from '@fortawesome/free-solid-svg-icons' type Props = { type: StructureType @@ -101,6 +101,14 @@ {@html implication.proof}

+{#if implication.dual_implication_id} +

+ + This implication has a + dual. +

+{/if} + {#if structures.length > 0}
diff --git a/tests/category-implications.spec.ts b/tests/category-implications.spec.ts index 533460995..6335a0c57 100644 --- a/tests/category-implications.spec.ts +++ b/tests/category-implications.spec.ts @@ -48,6 +48,10 @@ test('user can see the details of an implication', async ({ page }) => { }) ).toBeVisible() + await expect(page.locator('body')).toContainText( + 'If a category is cartesian closed, then it has finite products.' + ) + await expect( page.getByRole('link', { name: 'cartesian closed', @@ -65,6 +69,22 @@ test('user can see the details of an implication', async ({ page }) => { await expect(page.locator('body')).toContainText('Proof: This holds by definition') }) +test('user can navigate to the dual implication', async ({ page }) => { + await page.goto('/category-implication/abelian_implies_regular') + + await expect(page.locator('body')).toContainText( + 'If a category is abelian, then it is regular.' + ) + + await page.getByRole('link', { name: 'dual' }).click() + + await expect(page).toHaveURL('/category-implication/dual_abelian_implies_regular') + + await expect(page.locator('body')).toContainText( + 'If a category is abelian, then it is coregular.' + ) +}) + test('user can open the list of deduced implications', async ({ page }) => { await page.goto('/category-implications', { waitUntil: 'networkidle' }) diff --git a/tests/functor-implications.spec.ts b/tests/functor-implications.spec.ts index 4c006c3f8..937cdfb79 100644 --- a/tests/functor-implications.spec.ts +++ b/tests/functor-implications.spec.ts @@ -48,6 +48,10 @@ test('user can see the details of an implication', async ({ page }) => { }) ).toBeVisible() + await expect(page.locator('body')).toContainText( + 'If a functor is fully faithful, then it is conservative.' + ) + await expect( page.getByRole('link', { name: 'fully faithful', @@ -65,6 +69,22 @@ test('user can see the details of an implication', async ({ page }) => { await expect(page.locator('body')).toContainText(/Proof:.+follows that/) }) +test('user can navigate to the dual implication', async ({ page }) => { + await page.goto('/functor-implication/equivalence_consequences') + + await expect(page.locator('body')).toContainText( + 'If a functor is an equivalence, then it is monadic and is a reflector.' + ) + + await page.getByRole('link', { name: 'dual' }).click() + + await expect(page).toHaveURL('/functor-implication/dual_equivalence_consequences') + + await expect(page.locator('body')).toContainText( + 'If a functor is an equivalence, then it is comonadic and is a coreflector.' + ) +}) + test('user can open the list of deduced implications', async ({ page }) => { await page.goto('/functor-implications', { waitUntil: 'networkidle' }) diff --git a/tests/morphism-implications.spec.ts b/tests/morphism-implications.spec.ts index fe4bd8eb6..74756cf74 100644 --- a/tests/morphism-implications.spec.ts +++ b/tests/morphism-implications.spec.ts @@ -50,6 +50,10 @@ test('user can see the details of an implication', async ({ page }) => { }) ).toBeVisible() + await expect(page.locator('body')).toContainText( + 'If a morphism is a split monomorphism, then it is a regular monomorphism.' + ) + await expect( page.getByRole('link', { name: 'split monomorphism', @@ -67,6 +71,22 @@ test('user can see the details of an implication', async ({ page }) => { await expect(page.locator('body')).toContainText('Proof: Let') }) +test('user can navigate to the dual implication', async ({ page }) => { + await page.goto('/morphism-implication/split_mono_epi_is_iso') + + await expect(page.locator('body')).toContainText( + 'If a morphism is an epimorphism and is a split monomorphism, then it is an isomorphism.' + ) + + await page.getByRole('link', { name: 'dual' }).click() + + await expect(page).toHaveURL('/morphism-implication/dual_split_mono_epi_is_iso') + + await expect(page.locator('body')).toContainText( + 'If a morphism is a monomorphism and is a split epimorphism, then it is an isomorphism.' + ) +}) + test('user can open the list of deduced implications', async ({ page }) => { await page.goto('/morphism-implications', { waitUntil: 'networkidle' })