From 0bb798062fef2732bcf55953a041312f7facff7b Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 4 Jul 2026 10:47:47 +0200 Subject: [PATCH 01/10] add new structure type: morphisms --- databases/catdat/data/config.yaml | 8 +++ databases/catdat/schema/001_structures.sql | 6 ++- databases/catdat/schema/008_morphisms.sql | 17 ++++++ databases/catdat/scripts/config.ts | 6 ++- databases/catdat/scripts/deduce.ts | 5 ++ databases/catdat/scripts/seed.ts | 18 +++++++ databases/catdat/scripts/utils/seed.types.ts | 8 ++- src/lib/commons/structures.ts | 3 +- src/lib/commons/types.ts | 8 ++- src/lib/server/fetchers/morphism.ts | 25 +++++++++ src/pages/StructureListPage.svelte | 9 ++++ src/routes/missing/+page.server.ts | 6 +++ src/routes/missing/+page.svelte | 52 ++++++++++--------- .../morphism-implication/[id]/+page.server.ts | 8 +++ .../morphism-implication/[id]/+page.svelte | 7 +++ .../morphism-implications/+page.server.ts | 8 +++ src/routes/morphism-implications/+page.svelte | 15 ++++++ .../morphism-properties/+page.server.ts | 5 ++ src/routes/morphism-properties/+page.svelte | 7 +++ .../morphism-properties/[tag]/+page.server.ts | 11 ++++ .../morphism-properties/[tag]/+page.svelte | 7 +++ .../morphism-property/[id]/+page.server.ts | 11 ++++ .../morphism-property/[id]/+page.svelte | 7 +++ src/routes/morphism/[id]/+page.server.ts | 34 ++++++++++++ src/routes/morphism/[id]/+page.svelte | 16 ++++++ src/routes/morphisms/+page.server.ts | 5 ++ src/routes/morphisms/+page.svelte | 7 +++ src/routes/morphisms/[tag]/+page.server.ts | 12 +++++ src/routes/morphisms/[tag]/+page.svelte | 7 +++ 29 files changed, 306 insertions(+), 32 deletions(-) create mode 100644 databases/catdat/schema/008_morphisms.sql create mode 100644 src/lib/server/fetchers/morphism.ts create mode 100644 src/routes/morphism-implication/[id]/+page.server.ts create mode 100644 src/routes/morphism-implication/[id]/+page.svelte create mode 100644 src/routes/morphism-implications/+page.server.ts create mode 100644 src/routes/morphism-implications/+page.svelte create mode 100644 src/routes/morphism-properties/+page.server.ts create mode 100644 src/routes/morphism-properties/+page.svelte create mode 100644 src/routes/morphism-properties/[tag]/+page.server.ts create mode 100644 src/routes/morphism-properties/[tag]/+page.svelte create mode 100644 src/routes/morphism-property/[id]/+page.server.ts create mode 100644 src/routes/morphism-property/[id]/+page.svelte create mode 100644 src/routes/morphism/[id]/+page.server.ts create mode 100644 src/routes/morphism/[id]/+page.svelte create mode 100644 src/routes/morphisms/+page.server.ts create mode 100644 src/routes/morphisms/+page.svelte create mode 100644 src/routes/morphisms/[tag]/+page.server.ts create mode 100644 src/routes/morphisms/[tag]/+page.svelte diff --git a/databases/catdat/data/config.yaml b/databases/catdat/data/config.yaml index 1c596e0c..f67ae6a4 100644 --- a/databases/catdat/data/config.yaml +++ b/databases/catdat/data/config.yaml @@ -18,6 +18,9 @@ functor_tags: - forgetful - free +morphism_tags: + - misc + category_property_tags: - limits - colimits @@ -41,6 +44,11 @@ functor_property_tags: - invertibility - misc +morphism_property_tags: + - types of monomorphisms + - types of epimorphisms + - invertibility + relations: - relation: is conditional: would be diff --git a/databases/catdat/schema/001_structures.sql b/databases/catdat/schema/001_structures.sql index 9662fa6e..f1c285b2 100644 --- a/databases/catdat/schema/001_structures.sql +++ b/databases/catdat/schema/001_structures.sql @@ -4,7 +4,8 @@ CREATE TABLE structure_types ( INSERT INTO structure_types (type) VALUES ('category'), - ('functor'); + ('functor'), + ('morphism'); CREATE TABLE structures ( id TEXT PRIMARY KEY, @@ -73,4 +74,5 @@ INSERT INTO structure_maps (map, type, mapped_type) VALUES ('source', 'functor', 'category'), - ('target', 'functor', 'category'); \ No newline at end of file + ('target', 'functor', 'category'), + ('ambient_category', 'morphism', 'category'); \ No newline at end of file diff --git a/databases/catdat/schema/008_morphisms.sql b/databases/catdat/schema/008_morphisms.sql new file mode 100644 index 00000000..dcd5f804 --- /dev/null +++ b/databases/catdat/schema/008_morphisms.sql @@ -0,0 +1,17 @@ +CREATE TABLE morphisms ( + id TEXT PRIMARY KEY, + ambient_category TEXT NOT NULL, + FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE, + FOREIGN KEY (ambient_category) REFERENCES categories (id) ON DELETE CASCADE +); + +CREATE TRIGGER trg_morphism_type_check +BEFORE INSERT ON morphisms +BEGIN + SELECT + CASE + WHEN + (SELECT type FROM structures WHERE id = NEW.id) != 'morphism' + THEN RAISE(ABORT, 'Morphisms must have type "morphism"') + END; +END; \ No newline at end of file diff --git a/databases/catdat/scripts/config.ts b/databases/catdat/scripts/config.ts index 2b08d9a1..b916e370 100644 --- a/databases/catdat/scripts/config.ts +++ b/databases/catdat/scripts/config.ts @@ -1,15 +1,17 @@ -export type StructureType = 'category' | 'functor' +export type StructureType = 'category' | 'functor' | 'morphism' export const PLURALS = { category: 'categories', functor: 'functors', + morphism: 'morphisms', } as const -export const STRUCTURES: StructureType[] = ['category', 'functor'] +export const STRUCTURES: StructureType[] = ['category', 'functor', 'morphism'] export const STRUCTURES_WITH_DUALS: StructureType[] = ['category'] export const TABLES = { category: 'categories', functor: 'functors', + morphism: 'morphisms', } as const diff --git a/databases/catdat/scripts/deduce.ts b/databases/catdat/scripts/deduce.ts index 80c8c69c..65f2b382 100644 --- a/databases/catdat/scripts/deduce.ts +++ b/databases/catdat/scripts/deduce.ts @@ -27,4 +27,9 @@ function deduce() { create_dualized_implications('functor') deduce_properties_for_structures('functor') restrict_representable_functors() + + // --- morphisms --- + clear_deduced_implications('morphism') + create_dualized_implications('morphism') + deduce_properties_for_structures('morphism') } diff --git a/databases/catdat/scripts/seed.ts b/databases/catdat/scripts/seed.ts index 91abc95c..e993eefe 100644 --- a/databases/catdat/scripts/seed.ts +++ b/databases/catdat/scripts/seed.ts @@ -9,6 +9,7 @@ import type { PropertyEntry, StructureYaml, PropertyYaml, + MorphismYaml, } from './utils/seed.types' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' import { PLURALS, STRUCTURES, type StructureType } from './config' @@ -36,6 +37,10 @@ function seed() { seed_properties({ type: 'functor', folder: 'functor-properties' }) seed_implications({ type: 'functor', folder: 'functor-implications' }) seed_structures({ type: 'functor', folder: 'functors', extra: insert_functor }) + + seed_properties({ type: 'morphism', folder: 'morphism-properties' }) + seed_implications({ type: 'morphism', folder: 'morphism-implications' }) + seed_structures({ type: 'morphism', folder: 'morphisms', extra: insert_morphism }) } /** @@ -218,6 +223,7 @@ function seed_structures({ structure.notation, structure.description, structure.nlab_link, + // @ts-ignore FIXME structure[`dual_${type}`] || null, ) @@ -301,6 +307,18 @@ function insert_functor(functor: FunctorYaml) { ) } +/** + * Inserts the data of a morphism that is specific to morphisms. + */ +function insert_morphism(morphism: MorphismYaml) { + const morphism_insert = db.prepare( + `INSERT INTO morphisms (id, ambient_category) + VALUES (?, ?)`, + ) + + morphism_insert.run(morphism.id, morphism.ambient_category) +} + /** * Seeds all properties of a given type from YAML files. */ diff --git a/databases/catdat/scripts/utils/seed.types.ts b/databases/catdat/scripts/utils/seed.types.ts index 2d0b24d0..2f201508 100644 --- a/databases/catdat/scripts/utils/seed.types.ts +++ b/databases/catdat/scripts/utils/seed.types.ts @@ -2,8 +2,10 @@ export type ConfigYaml = { structure_tags: string[] category_tags: string[] functor_tags: string[] + morphism_tags: string[] category_property_tags: string[] functor_property_tags: string[] + morphism_property_tags: string[] relations: { relation: string conditional: string @@ -43,8 +45,8 @@ export type StructureYaml = { tags: string[] related_categories?: string[] // TODO: improve this related_functors?: string[] + related_morphisms?: string[] dual_category?: string // TODO: improve this - dual_functor?: string satisfied_properties: PropertyEntry[] unsatisfied_properties: PropertyEntry[] undecidable_properties?: PropertyEntry[] @@ -65,6 +67,10 @@ export type FunctorYaml = StructureYaml & { left_adjoint?: string } +export type MorphismYaml = StructureYaml & { + ambient_category: string +} + export type PropertyYaml = { id: string relation: string diff --git a/src/lib/commons/structures.ts b/src/lib/commons/structures.ts index 72e79708..37f9699a 100644 --- a/src/lib/commons/structures.ts +++ b/src/lib/commons/structures.ts @@ -1,10 +1,11 @@ import type { StructureType } from './types' -export const STRUCTURES: StructureType[] = ['category', 'functor'] +export const STRUCTURES: StructureType[] = ['category', 'functor', 'morphism'] export const PLURALS = { category: 'categories', functor: 'functors', + morphism: 'morphisms', } export function get_selected_type(pathname: string): StructureType { diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index af2ebcb2..840de28b 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -4,7 +4,7 @@ export type Arrayed = { type Replace>> = Omit & R -export type StructureType = 'category' | 'functor' +export type StructureType = 'category' | 'functor' | 'morphism' export type StructureShort = { id: string @@ -44,6 +44,12 @@ export type FunctorSpecificDisplay = { right_adjoint_notation: string | null } +export type MorphismSpecificDisplay = { + ambient_category: string + ambient_category_name: string + ambient_category_notation: string +} + export type MappedTypes = Record export type TagObject = { tag: string } diff --git a/src/lib/server/fetchers/morphism.ts b/src/lib/server/fetchers/morphism.ts new file mode 100644 index 00000000..d259093d --- /dev/null +++ b/src/lib/server/fetchers/morphism.ts @@ -0,0 +1,25 @@ +import type { MorphismSpecificDisplay } from '$lib/commons/types' +import sql from 'sql-template-tag' +import { query } from '$lib/server/db.catdat' +import { error } from '@sveltejs/kit' + +export function fetch_morphism(id: string) { + const { rows: morphisms, err } = query( + // specific information for the morphism + sql` + SELECT + c.id AS ambient_category, + c.name AS ambient_category_name, + c.notation AS ambient_category_notation + FROM morphisms m + INNER JOIN structures AS c ON c.id = m.ambient_category + WHERE m.id = ${id} + `, + ) + + if (err) error(500, 'Could not load morphism') + + if (!morphisms.length) error(404, `Could not find morphism with ID '${id}'`) + + return morphisms[0] +} diff --git a/src/pages/StructureListPage.svelte b/src/pages/StructureListPage.svelte index 08ba5b0e..20648b8c 100644 --- a/src/pages/StructureListPage.svelte +++ b/src/pages/StructureListPage.svelte @@ -43,6 +43,15 @@

{/if} + {#if type === 'morphism'} + +

+ + The morphism application is still in its early stages. More morphisms will be added + soon. +

+ {/if} +

diff --git a/src/routes/missing/+page.server.ts b/src/routes/missing/+page.server.ts index 7017258e..309428e6 100644 --- a/src/routes/missing/+page.server.ts +++ b/src/routes/missing/+page.server.ts @@ -1,28 +1,34 @@ import { fetch_missing_data } from '$lib/server/fetchers/missing_data' import { fetch_categories_with_missing_morphisms } from '$lib/server/fetchers/category' +// TODO: remove code duplication export const load = () => { const categories_with_missing_morphisms = fetch_categories_with_missing_morphisms() const missing_category_data = fetch_missing_data('category') const missing_functor_data = fetch_missing_data('functor') + const missing_morphism_data = fetch_missing_data('morphism') return { structures_with_unknown_properties: { category: missing_category_data.structures_with_unknown_properties, functor: missing_functor_data.structures_with_unknown_properties, + morphism: missing_morphism_data.structures_with_unknown_properties, }, unknown_totals: { category: missing_category_data.total_unknown_property_pairs, functor: missing_functor_data.total_unknown_property_pairs, + morphism: missing_morphism_data.total_unknown_property_pairs, }, undistinguishable_pairs: { category: missing_category_data.undistinguishable_structure_pairs, functor: missing_functor_data.undistinguishable_structure_pairs, + morphism: missing_morphism_data.undistinguishable_structure_pairs, }, missing_combinations: { category: missing_category_data.missing_combinations, functor: missing_functor_data.missing_combinations, + morphism: missing_morphism_data.missing_combinations, }, categories_with_missing_morphisms, } diff --git a/src/routes/missing/+page.svelte b/src/routes/missing/+page.svelte index 117a5191..b566f809 100644 --- a/src/routes/missing/+page.svelte +++ b/src/routes/missing/+page.svelte @@ -87,33 +87,35 @@ {#each STRUCTURES as type} {@const combinations = data.missing_combinations[type]} -

-

Missing {type} combinations

+ {#if combinations.length > 0} +
+

Missing {type} combinations

-

- Among the consistent {type} combinations of the form p ∧ ¬q, the following - are not yet witnessed by a {type} in the database or its dual. If some of these - combinations are - inconsistent, this indicates that some - implication is missing. -

+

+ Among the consistent {type} combinations of the form p ∧ ¬q, the following + are not yet witnessed by a {type} in the database or its dual. If some of these + combinations are + inconsistent, this indicates that some + implication is missing. +

-
- - Show all {combinations.length} combinations - - -
    - {#each combinations as [p, q]} -
  • - {p} ∧ ¬{q} -
    • - {/each} -
-
-
+
+ + Show all {combinations.length} combinations + + +
    + {#each combinations as [p, q]} +
  • + {p} ∧ ¬{q} +
    • + {/each} +
+
+
+ {/if} {/each} diff --git a/src/routes/morphism-implication/[id]/+page.server.ts b/src/routes/morphism-implication/[id]/+page.server.ts new file mode 100644 index 00000000..bb302106 --- /dev/null +++ b/src/routes/morphism-implication/[id]/+page.server.ts @@ -0,0 +1,8 @@ +import { fetch_implication } from '$lib/server/fetchers/implication' +import { render_nested_formulas } from '$lib/server/formulas' + +export const load = (event) => { + const id = event.params.id + + return render_nested_formulas(fetch_implication('morphism', id)) +} diff --git a/src/routes/morphism-implication/[id]/+page.svelte b/src/routes/morphism-implication/[id]/+page.svelte new file mode 100644 index 00000000..a97e46ff --- /dev/null +++ b/src/routes/morphism-implication/[id]/+page.svelte @@ -0,0 +1,7 @@ + + + diff --git a/src/routes/morphism-implications/+page.server.ts b/src/routes/morphism-implications/+page.server.ts new file mode 100644 index 00000000..c3c4e42b --- /dev/null +++ b/src/routes/morphism-implications/+page.server.ts @@ -0,0 +1,8 @@ +import { render_nested_formulas } from '$lib/server/formulas' +import { fetch_implications } from '$lib/server/fetchers/implications' + +export const load = () => { + const { implications } = fetch_implications('morphism') + + return render_nested_formulas({ implications }) +} diff --git a/src/routes/morphism-implications/+page.svelte b/src/routes/morphism-implications/+page.svelte new file mode 100644 index 00000000..fd3605ac --- /dev/null +++ b/src/routes/morphism-implications/+page.svelte @@ -0,0 +1,15 @@ + + + + {#snippet hints()} +

+ *Deductions from these implications are automatically incorporated into each + morphism whenever applicable. Moreover, implications are automatically + dualized when the corresponding dual properties exist. +

+ {/snippet} + diff --git a/src/routes/morphism-properties/+page.server.ts b/src/routes/morphism-properties/+page.server.ts new file mode 100644 index 00000000..65095e1b --- /dev/null +++ b/src/routes/morphism-properties/+page.server.ts @@ -0,0 +1,5 @@ +import { fetch_grouped_properties_and_tags } from '$lib/server/fetchers/properties' + +export const load = () => { + return fetch_grouped_properties_and_tags('morphism') +} diff --git a/src/routes/morphism-properties/+page.svelte b/src/routes/morphism-properties/+page.svelte new file mode 100644 index 00000000..dadefb7f --- /dev/null +++ b/src/routes/morphism-properties/+page.svelte @@ -0,0 +1,7 @@ + + + diff --git a/src/routes/morphism-properties/[tag]/+page.server.ts b/src/routes/morphism-properties/[tag]/+page.server.ts new file mode 100644 index 00000000..ccbb6896 --- /dev/null +++ b/src/routes/morphism-properties/[tag]/+page.server.ts @@ -0,0 +1,11 @@ +import { fetch_tagged_properties } from '$lib/server/fetchers/properties' +import { fetch_property_tags } from '$lib/server/fetchers/tags' +import type { EntryGenerator } from './$types' + +export const entries: EntryGenerator = () => { + return fetch_property_tags('morphism') +} + +export const load = (event) => { + return fetch_tagged_properties('morphism', event.params.tag) +} diff --git a/src/routes/morphism-properties/[tag]/+page.svelte b/src/routes/morphism-properties/[tag]/+page.svelte new file mode 100644 index 00000000..62fb6cb9 --- /dev/null +++ b/src/routes/morphism-properties/[tag]/+page.svelte @@ -0,0 +1,7 @@ + + + diff --git a/src/routes/morphism-property/[id]/+page.server.ts b/src/routes/morphism-property/[id]/+page.server.ts new file mode 100644 index 00000000..3ce350d5 --- /dev/null +++ b/src/routes/morphism-property/[id]/+page.server.ts @@ -0,0 +1,11 @@ +import { render_nested_formulas } from '$lib/server/formulas' +import { decode_property_ID } from '$lib/commons/property.url' +import { fetch_property } from '$lib/server/fetchers/property' + +export const load = (event) => { + const id = decode_property_ID(event.params.id) + + const property_data = fetch_property('morphism', id) + + return render_nested_formulas(property_data) +} diff --git a/src/routes/morphism-property/[id]/+page.svelte b/src/routes/morphism-property/[id]/+page.svelte new file mode 100644 index 00000000..acb5718b --- /dev/null +++ b/src/routes/morphism-property/[id]/+page.svelte @@ -0,0 +1,7 @@ + + + diff --git a/src/routes/morphism/[id]/+page.server.ts b/src/routes/morphism/[id]/+page.server.ts new file mode 100644 index 00000000..6923eaf4 --- /dev/null +++ b/src/routes/morphism/[id]/+page.server.ts @@ -0,0 +1,34 @@ +import { fetch_morphism } from '$lib/server/fetchers/morphism' +import { fetch_structure } from '$lib/server/fetchers/structure' +import { render_nested_formulas } from '$lib/server/formulas' + +export const load = (event) => { + const id = event.params.id + + const { + structure, + related_structures, + tags, + satisfied_properties, + unsatisfied_properties, + unknown_properties, + undecidable_properties, + undistinguishable_structures, + comments, + } = fetch_structure('morphism', id) + + const morphism = fetch_morphism(id) + + return render_nested_formulas({ + structure, + morphism, + related_structures, + tags, + satisfied_properties, + unsatisfied_properties, + unknown_properties, + undecidable_properties, + undistinguishable_structures, + comments, + }) +} diff --git a/src/routes/morphism/[id]/+page.svelte b/src/routes/morphism/[id]/+page.svelte new file mode 100644 index 00000000..fb6a3186 --- /dev/null +++ b/src/routes/morphism/[id]/+page.svelte @@ -0,0 +1,16 @@ + + + + {#snippet definition()} +
  • + Ambient category: + + {data.morphism.ambient_category_name} + +
    • + {/snippet} +     diff --git a/src/routes/morphisms/+page.server.ts b/src/routes/morphisms/+page.server.ts new file mode 100644 index 00000000..0825b73e --- /dev/null +++ b/src/routes/morphisms/+page.server.ts @@ -0,0 +1,5 @@ +import { fetch_structures_and_tags } from '$lib/server/fetchers/structures' + +export const load = () => { + return fetch_structures_and_tags('morphism') +} diff --git a/src/routes/morphisms/+page.svelte b/src/routes/morphisms/+page.svelte new file mode 100644 index 00000000..f94edcfc --- /dev/null +++ b/src/routes/morphisms/+page.svelte @@ -0,0 +1,7 @@ + + + diff --git a/src/routes/morphisms/[tag]/+page.server.ts b/src/routes/morphisms/[tag]/+page.server.ts new file mode 100644 index 00000000..7624ca36 --- /dev/null +++ b/src/routes/morphisms/[tag]/+page.server.ts @@ -0,0 +1,12 @@ +import type { EntryGenerator } from './$types' +import { fetch_tagged_structures } from '$lib/server/fetchers/structures' +import { fetch_structure_tags } from '$lib/server/fetchers/tags' + +export const entries: EntryGenerator = () => { + return fetch_structure_tags('morphism') +} + +export const load = (event) => { + const tag = event.params.tag + return fetch_tagged_structures('morphism', tag) +} diff --git a/src/routes/morphisms/[tag]/+page.svelte b/src/routes/morphisms/[tag]/+page.svelte new file mode 100644 index 00000000..d3340462 --- /dev/null +++ b/src/routes/morphisms/[tag]/+page.svelte @@ -0,0 +1,7 @@ + + + From 8b6931179a3fb934834c3ef0253f7ea26a62944a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 4 Jul 2026 10:49:13 +0200 Subject: [PATCH 02/10] add first morphism properties: monomorphisms, epimorphisms, isomorphisms --- .../morphism-implications/mono-epi-iso.yaml | 30 +++++++++++++++++++ .../data/morphism-properties/epimorphism.yaml | 11 +++++++ .../data/morphism-properties/isomorphism.yaml | 12 ++++++++ .../morphism-properties/monomorphism.yaml | 11 +++++++ 4 files changed, 64 insertions(+) create mode 100644 databases/catdat/data/morphism-implications/mono-epi-iso.yaml create mode 100644 databases/catdat/data/morphism-properties/epimorphism.yaml create mode 100644 databases/catdat/data/morphism-properties/isomorphism.yaml create mode 100644 databases/catdat/data/morphism-properties/monomorphism.yaml diff --git a/databases/catdat/data/morphism-implications/mono-epi-iso.yaml b/databases/catdat/data/morphism-implications/mono-epi-iso.yaml new file mode 100644 index 00000000..fe7b01f8 --- /dev/null +++ b/databases/catdat/data/morphism-implications/mono-epi-iso.yaml @@ -0,0 +1,30 @@ +- id: iso_is_mono + assumptions: + - isomorphism + conclusions: + - monomorphism + proof: This is easy. + is_equivalence: false + +- id: mono_is_iso + assumptions: + - monomorphism + mapped_assumptions: + ambient_category: + - subobject-trivial + conclusions: + - isomorphism + proof: This holds by definition of a subobject-trivial category. + is_equivalence: false + +- id: balanced_def + assumptions: + - monomorphism + - epimorphism + mapped_assumptions: + ambient_category: + - balanced + conclusions: + - isomorphism + proof: This holds by definition of a balanced category. + is_equivalence: false diff --git a/databases/catdat/data/morphism-properties/epimorphism.yaml b/databases/catdat/data/morphism-properties/epimorphism.yaml new file mode 100644 index 00000000..c2b666a2 --- /dev/null +++ b/databases/catdat/data/morphism-properties/epimorphism.yaml @@ -0,0 +1,11 @@ +id: epimorphism +relation: is an +description: 'A morphism $f : A \to B$ is an epimorphism if it is right-cancellative, i.e. if $g \circ f = h \circ f$ for two morphisms $g,h : B \rightrightarrows T$, then $g = h$. In many concrete categories appearing in practice, these are are a bit harder to understand than monomorphisms; in particular, epimorphisms usually are not to be confused with surjective structure-preserving maps.' +nlab_link: https://ncatlab.org/nlab/show/epimorphism +invariant_under_equivalences: true +dual_property: monomorphism +related_properties: + - isomorphism + +tags: + - types of epimorphisms diff --git a/databases/catdat/data/morphism-properties/isomorphism.yaml b/databases/catdat/data/morphism-properties/isomorphism.yaml new file mode 100644 index 00000000..9d86db1d --- /dev/null +++ b/databases/catdat/data/morphism-properties/isomorphism.yaml @@ -0,0 +1,12 @@ +id: isomorphism +relation: is an +description: 'A morphism $f : A \to B$ is an isomorphism if it has an inverse, i.e. a morphism $f^{-1} : B \to A$ satisfying $f \circ f^{-1} = \id_B$ and $f^{-1} \circ f = \id_A$.' +nlab_link: https://ncatlab.org/nlab/show/isomorphism +invariant_under_equivalences: true +dual_property: isomorphism +related_properties: + - monomorphism + - epimorphism + +tags: + - invertibility diff --git a/databases/catdat/data/morphism-properties/monomorphism.yaml b/databases/catdat/data/morphism-properties/monomorphism.yaml new file mode 100644 index 00000000..f84eff07 --- /dev/null +++ b/databases/catdat/data/morphism-properties/monomorphism.yaml @@ -0,0 +1,11 @@ +id: monomorphism +relation: is a +description: 'A morphism $f : A \to B$ is a monomorphism if it is left-cancellative, i.e. if $f \circ g = f \circ h$ for two morphisms $g,h : T \rightrightarrows A$, then $g = h$. In many concrete categories appearing in practice, these are injective structure-preserving maps.' +nlab_link: https://ncatlab.org/nlab/show/monomorphism +invariant_under_equivalences: true +dual_property: epimorphism +related_properties: + - isomorphism + +tags: + - types of monomorphisms From b29a841d3c50ca70d6662ffa26135c05589412ce Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 4 Jul 2026 10:49:48 +0200 Subject: [PATCH 03/10] add first examples of morphisms --- .../catdat/data/morphisms/empty-map.yaml | 19 ++++++++++++++++ databases/catdat/data/morphisms/id_X.yaml | 17 ++++++++++++++ .../morphisms/integer-rational-embedding.yaml | 22 +++++++++++++++++++ .../catdat/data/morphisms/terminal-map.yaml | 19 ++++++++++++++++ 4 files changed, 77 insertions(+) create mode 100644 databases/catdat/data/morphisms/empty-map.yaml create mode 100644 databases/catdat/data/morphisms/id_X.yaml create mode 100644 databases/catdat/data/morphisms/integer-rational-embedding.yaml create mode 100644 databases/catdat/data/morphisms/terminal-map.yaml diff --git a/databases/catdat/data/morphisms/empty-map.yaml b/databases/catdat/data/morphisms/empty-map.yaml new file mode 100644 index 00000000..7ada0437 --- /dev/null +++ b/databases/catdat/data/morphisms/empty-map.yaml @@ -0,0 +1,19 @@ +id: empty-map +name: map from the empty set +notation: $!$ +ambient_category: Set +description: 'For every set $X$ there is a unique map $! : \varnothing \hookrightarrow X$, the empty map. In this entry, we require that $X$ is non-empty.' +nlab_link: https://ncatlab.org/nlab/show/empty+set + +tags: + - set theory + +related_morphisms: [] + +satisfied_properties: + - property: monomorphism + proof: It is vacuously injective. + +unsatisfied_properties: + - property: epimorphism + proof: Since $X$ is non-empty, the map is not surjective. diff --git a/databases/catdat/data/morphisms/id_X.yaml b/databases/catdat/data/morphisms/id_X.yaml new file mode 100644 index 00000000..75e27374 --- /dev/null +++ b/databases/catdat/data/morphisms/id_X.yaml @@ -0,0 +1,17 @@ +id: id_X +name: identity map of a set +notation: $\id_X$ +ambient_category: Set +description: 'Every object of a category has an identity morphism. In this case, we take a set $X$ and consider its identity morphism $\id_X : X \to X$ in $\Set$.' +nlab_link: https://ncatlab.org/nlab/show/identity+morphism + +tags: + - set theory + +related_morphisms: [] + +satisfied_properties: + - property: isomorphism + proof: This is obvious. + +unsatisfied_properties: [] diff --git a/databases/catdat/data/morphisms/integer-rational-embedding.yaml b/databases/catdat/data/morphisms/integer-rational-embedding.yaml new file mode 100644 index 00000000..5e5ef096 --- /dev/null +++ b/databases/catdat/data/morphisms/integer-rational-embedding.yaml @@ -0,0 +1,22 @@ +id: integer-rational-embedding +name: embedding of integer into rational numbers +notation: $\iota_{\IZ,\IQ}$ +ambient_category: CRing +description: 'The inclusion $\iota_{\IZ,\IQ} : \IZ \hookrightarrow \IQ$ is a typical example of a localization. It is a standard example of a mono- and epimorphism which is not an isomorphism in the category of (commutative) rings.' +nlab_link: https://ncatlab.org/nlab/show/localization+of+a+commutative+ringlization + +tags: + - algebra + +related_morphisms: [] + +satisfied_properties: + - property: monomorphism + proof: It is clearly injective. + + - property: epimorphism + proof: Every localization $R \to S^{-1} R$ has this property by the universal property of localizations. + +unsatisfied_properties: + - property: isomorphism + proof: Clearly, this map is not surjective. diff --git a/databases/catdat/data/morphisms/terminal-map.yaml b/databases/catdat/data/morphisms/terminal-map.yaml new file mode 100644 index 00000000..c2014410 --- /dev/null +++ b/databases/catdat/data/morphisms/terminal-map.yaml @@ -0,0 +1,19 @@ +id: terminal-map +name: map into the singleton set +notation: $!$ +ambient_category: Set +description: 'For every set $X$ there is a unique map $! : X \to 1$, where $1$ is the singleton set. In this entry, we require that $X$ has at least $2$ elements.' +nlab_link: null + +tags: + - set theory + +related_morphisms: [] + +satisfied_properties: + - property: epimorphism + proof: The map is surjective because $X$ is non-empty. + +unsatisfied_properties: + - property: monomorphism + proof: Since $X$ has two different elements by assumption, which trivially have the same image, the map is not injective. From d558bbe8adbcd7ab0d3621cddc7e58cd6d75c8e7 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 4 Jul 2026 10:49:57 +0200 Subject: [PATCH 04/10] add tests for morphisms --- .../catdat/scripts/expected-data/decided-morphisms.json | 1 + databases/catdat/scripts/test.ts | 8 ++++++++ 2 files changed, 9 insertions(+) create mode 100644 databases/catdat/scripts/expected-data/decided-morphisms.json diff --git a/databases/catdat/scripts/expected-data/decided-morphisms.json b/databases/catdat/scripts/expected-data/decided-morphisms.json new file mode 100644 index 00000000..10d11d5c --- /dev/null +++ b/databases/catdat/scripts/expected-data/decided-morphisms.json @@ -0,0 +1 @@ +["id_X"] diff --git a/databases/catdat/scripts/test.ts b/databases/catdat/scripts/test.ts index ae5a9484..a1bcfd7d 100644 --- a/databases/catdat/scripts/test.ts +++ b/databases/catdat/scripts/test.ts @@ -11,6 +11,7 @@ import forget_vector_expected from './expected-data/forget_vector.json' import id_Set_expected from './expected-data/id_Set.json' import decided_categories from './expected-data/decided-categories.json' import decided_functors from './expected-data/decided-functors.json' +import decided_morphisms from './expected-data/decided-morphisms.json' import { capitalize } from './utils/helpers' import { get_client } from './utils/db' import { PLURALS, STRUCTURES, type StructureType } from './config' @@ -31,6 +32,7 @@ function execute_tests() { check_link_targets_exist() console.info('\n--- Test categories ---') + test_mutual_structure_duals('category') test_positivity('1', 'category') test_mutual_property_duals('category') @@ -41,6 +43,7 @@ function execute_tests() { ) console.info('\n--- Test functors ---') + test_positivity('id_Set', 'functor') test_mutual_property_duals('functor') test_decided_structures(decided_functors, 'functor') @@ -48,6 +51,11 @@ function execute_tests() { { forget_vector: forget_vector_expected, id_Set: id_Set_expected }, 'functor', ) + + console.info('\n--- Test morphisms ---') + + test_positivity('id_X', 'morphism') + test_decided_structures(decided_morphisms, 'morphism') } catch (err) { if (err instanceof Error) { console.error(err.message) From 44f6b71e3004e53ecb989e9221050f2dc6851bb8 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 4 Jul 2026 11:21:11 +0200 Subject: [PATCH 05/10] add regular epis and monos --- .../morphism-implications/mono-epi-iso.yaml | 32 +++++++++++++++++-- .../data/morphism-properties/epimorphism.yaml | 1 + .../morphism-properties/monomorphism.yaml | 1 + .../regular epimorphism.yaml | 11 +++++++ .../regular monomorphism.yaml | 11 +++++++ 5 files changed, 54 insertions(+), 2 deletions(-) create mode 100644 databases/catdat/data/morphism-properties/regular epimorphism.yaml create mode 100644 databases/catdat/data/morphism-properties/regular monomorphism.yaml diff --git a/databases/catdat/data/morphism-implications/mono-epi-iso.yaml b/databases/catdat/data/morphism-implications/mono-epi-iso.yaml index fe7b01f8..b92f51d7 100644 --- a/databases/catdat/data/morphism-implications/mono-epi-iso.yaml +++ b/databases/catdat/data/morphism-implications/mono-epi-iso.yaml @@ -2,8 +2,8 @@ assumptions: - isomorphism conclusions: - - monomorphism - proof: This is easy. + - regular monomorphism + proof: 'If $f : A \to B$ is an isomorphism, it is an equalizer of $\id_B, \id_B : B \rightrightarrows B$.' is_equivalence: false - id: mono_is_iso @@ -28,3 +28,31 @@ - isomorphism proof: This holds by definition of a balanced category. is_equivalence: false + +- id: regular_mono_is_mono + assumptions: + - regular monomorphism + conclusions: + - monomorphism + proof: This is an immediate consequence of the definition of an equalizer. + is_equivalence: false + +- id: mono-regular_def + assumptions: + - monomorphism + mapped_assumptions: + ambient_category: + - mono-regular + conclusions: + - regular monomorphism + proof: This is the definition of a mono-regular category. + is_equivalence: false + +- id: regular_epi_and_mono_is_iso + assumptions: + - regular epimorphism + - monomorphism + conclusions: + - isomorphism + proof: 'If $p : A \to B$ is the coequalizer of $f,g : C \rightrightarrows A$, then $p \circ f = p \circ g$. If $p$ is also a monomorphism, this implies $f = g$. But then $\id_B$ is a coequalizer of $f,g$, so that $p$ is an isomorphism.' + is_equivalence: false diff --git a/databases/catdat/data/morphism-properties/epimorphism.yaml b/databases/catdat/data/morphism-properties/epimorphism.yaml index c2b666a2..322a1ff3 100644 --- a/databases/catdat/data/morphism-properties/epimorphism.yaml +++ b/databases/catdat/data/morphism-properties/epimorphism.yaml @@ -6,6 +6,7 @@ invariant_under_equivalences: true dual_property: monomorphism related_properties: - isomorphism + - regular epimorphism tags: - types of epimorphisms diff --git a/databases/catdat/data/morphism-properties/monomorphism.yaml b/databases/catdat/data/morphism-properties/monomorphism.yaml index f84eff07..664c832d 100644 --- a/databases/catdat/data/morphism-properties/monomorphism.yaml +++ b/databases/catdat/data/morphism-properties/monomorphism.yaml @@ -6,6 +6,7 @@ invariant_under_equivalences: true dual_property: epimorphism related_properties: - isomorphism + - regular monomorphism tags: - types of monomorphisms diff --git a/databases/catdat/data/morphism-properties/regular epimorphism.yaml b/databases/catdat/data/morphism-properties/regular epimorphism.yaml new file mode 100644 index 00000000..ff0a8532 --- /dev/null +++ b/databases/catdat/data/morphism-properties/regular epimorphism.yaml @@ -0,0 +1,11 @@ +id: regular epimorphism +relation: is a +description: 'A morphism $f : A \to B$ is a regular epimorphism if it is the coequalizer of a pair of morphisms $g,h : C \rightrightarrows A$. In many categories appearing in practice, this is the same as a quotient.' +nlab_link: https://ncatlab.org/nlab/show/regular+epimorphism +invariant_under_equivalences: true +dual_property: regular monomorphism +related_properties: + - epimorphism + +tags: + - types of epimorphisms diff --git a/databases/catdat/data/morphism-properties/regular monomorphism.yaml b/databases/catdat/data/morphism-properties/regular monomorphism.yaml new file mode 100644 index 00000000..1788bdcd --- /dev/null +++ b/databases/catdat/data/morphism-properties/regular monomorphism.yaml @@ -0,0 +1,11 @@ +id: regular monomorphism +relation: is a +description: 'A morphism $f : A \to B$ is a regular monomorphism if it is the equalizer of a pair of morphisms $g,h : B \rightrightarrows C$. In many categories appearing in practice, this is the same as an embedding.' +nlab_link: https://ncatlab.org/nlab/show/regular+monomorphism +invariant_under_equivalences: true +dual_property: regular epimorphism +related_properties: + - monomorphism + +tags: + - types of monomorphisms From 04b06a75223976abe3daddb7d8c4d272c5cf1607 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 4 Jul 2026 11:33:25 +0200 Subject: [PATCH 06/10] remove code duplication in transforming missing data --- src/routes/missing/+page.server.ts | 42 +++++++++++++----------------- 1 file changed, 18 insertions(+), 24 deletions(-) diff --git a/src/routes/missing/+page.server.ts b/src/routes/missing/+page.server.ts index 309428e6..b25f2c69 100644 --- a/src/routes/missing/+page.server.ts +++ b/src/routes/missing/+page.server.ts @@ -1,35 +1,29 @@ import { fetch_missing_data } from '$lib/server/fetchers/missing_data' import { fetch_categories_with_missing_morphisms } from '$lib/server/fetchers/category' +import { STRUCTURES } from '$lib/commons/structures' -// TODO: remove code duplication export const load = () => { const categories_with_missing_morphisms = fetch_categories_with_missing_morphisms() - const missing_category_data = fetch_missing_data('category') - const missing_functor_data = fetch_missing_data('functor') - const missing_morphism_data = fetch_missing_data('morphism') + const missing_data = Object.fromEntries( + STRUCTURES.map((type) => [type, fetch_missing_data(type)]), + ) + + function select( + selector: (data: (typeof missing_data)[keyof typeof missing_data]) => T, + ) { + return Object.fromEntries( + STRUCTURES.map((type) => [type, selector(missing_data[type])]), + ) + } return { - structures_with_unknown_properties: { - category: missing_category_data.structures_with_unknown_properties, - functor: missing_functor_data.structures_with_unknown_properties, - morphism: missing_morphism_data.structures_with_unknown_properties, - }, - unknown_totals: { - category: missing_category_data.total_unknown_property_pairs, - functor: missing_functor_data.total_unknown_property_pairs, - morphism: missing_morphism_data.total_unknown_property_pairs, - }, - undistinguishable_pairs: { - category: missing_category_data.undistinguishable_structure_pairs, - functor: missing_functor_data.undistinguishable_structure_pairs, - morphism: missing_morphism_data.undistinguishable_structure_pairs, - }, - missing_combinations: { - category: missing_category_data.missing_combinations, - functor: missing_functor_data.missing_combinations, - morphism: missing_morphism_data.missing_combinations, - }, + structures_with_unknown_properties: select( + (data) => data.structures_with_unknown_properties, + ), + unknown_totals: select((data) => data.total_unknown_property_pairs), + undistinguishable_pairs: select((data) => data.undistinguishable_structure_pairs), + missing_combinations: select((data) => data.missing_combinations), categories_with_missing_morphisms, } } From 2020b0f42b29669fe913b0cbe8790eb8e104a72c Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 4 Jul 2026 11:37:58 +0200 Subject: [PATCH 07/10] add comparison and search feature for morphisms --- src/routes/morphism-comparison/+page.server.ts | 5 +++++ src/routes/morphism-comparison/+page.svelte | 7 +++++++ .../morphism-comparison/[...ids]/+page.server.ts | 12 ++++++++++++ .../morphism-comparison/[...ids]/+page.svelte | 7 +++++++ src/routes/morphism-search/+page.server.ts | 5 +++++ src/routes/morphism-search/+page.svelte | 13 +++++++++++++ src/routes/morphism-search/results/+page.server.ts | 13 +++++++++++++ src/routes/morphism-search/results/+page.svelte | 7 +++++++ 8 files changed, 69 insertions(+) create mode 100644 src/routes/morphism-comparison/+page.server.ts create mode 100644 src/routes/morphism-comparison/+page.svelte create mode 100644 src/routes/morphism-comparison/[...ids]/+page.server.ts create mode 100644 src/routes/morphism-comparison/[...ids]/+page.svelte create mode 100644 src/routes/morphism-search/+page.server.ts create mode 100644 src/routes/morphism-search/+page.svelte create mode 100644 src/routes/morphism-search/results/+page.server.ts create mode 100644 src/routes/morphism-search/results/+page.svelte diff --git a/src/routes/morphism-comparison/+page.server.ts b/src/routes/morphism-comparison/+page.server.ts new file mode 100644 index 00000000..27b026bc --- /dev/null +++ b/src/routes/morphism-comparison/+page.server.ts @@ -0,0 +1,5 @@ +import { fetch_structures } from '$lib/server/fetchers/structures' + +export const load = () => { + return fetch_structures('morphism') +} diff --git a/src/routes/morphism-comparison/+page.svelte b/src/routes/morphism-comparison/+page.svelte new file mode 100644 index 00000000..626b192e --- /dev/null +++ b/src/routes/morphism-comparison/+page.svelte @@ -0,0 +1,7 @@ + + + diff --git a/src/routes/morphism-comparison/[...ids]/+page.server.ts b/src/routes/morphism-comparison/[...ids]/+page.server.ts new file mode 100644 index 00000000..12443fd9 --- /dev/null +++ b/src/routes/morphism-comparison/[...ids]/+page.server.ts @@ -0,0 +1,12 @@ +import { fetch_comparison_result } from '$lib/server/fetchers/comparison' +import { cache_page } from '$lib/server/utils' + +export const prerender = false + +export const load = (event) => { + const compared_ids = event.params.ids.split('/') + + return fetch_comparison_result(compared_ids, 'morphism', () => { + cache_page(event) + }) +} diff --git a/src/routes/morphism-comparison/[...ids]/+page.svelte b/src/routes/morphism-comparison/[...ids]/+page.svelte new file mode 100644 index 00000000..11f4d1e6 --- /dev/null +++ b/src/routes/morphism-comparison/[...ids]/+page.svelte @@ -0,0 +1,7 @@ + + + diff --git a/src/routes/morphism-search/+page.server.ts b/src/routes/morphism-search/+page.server.ts new file mode 100644 index 00000000..6ba761c3 --- /dev/null +++ b/src/routes/morphism-search/+page.server.ts @@ -0,0 +1,5 @@ +import { get_property_ids } from '$lib/server/fetchers/properties' + +export const load = () => { + return { all_properties: get_property_ids('morphism') } +} diff --git a/src/routes/morphism-search/+page.svelte b/src/routes/morphism-search/+page.svelte new file mode 100644 index 00000000..d62dc5d3 --- /dev/null +++ b/src/routes/morphism-search/+page.svelte @@ -0,0 +1,13 @@ + + + + Search for morphism with certain properties while excluding others. For example, you + can look for morphisms which are monomorphisms and epimorphisms, + but no isomorphisms. + diff --git a/src/routes/morphism-search/results/+page.server.ts b/src/routes/morphism-search/results/+page.server.ts new file mode 100644 index 00000000..390cfa6b --- /dev/null +++ b/src/routes/morphism-search/results/+page.server.ts @@ -0,0 +1,13 @@ +import { fetch_search_results } from '$lib/server/fetchers/search' +import { cache_page } from '$lib/server/utils' + +export const prerender = false + +export const load = (event) => { + const satisfied_query = event.url.searchParams.get('satisfied') + const unsatisfied_query = event.url.searchParams.get('unsatisfied') + + return fetch_search_results(satisfied_query, unsatisfied_query, 'morphism', () => + cache_page(event), + ) +} diff --git a/src/routes/morphism-search/results/+page.svelte b/src/routes/morphism-search/results/+page.svelte new file mode 100644 index 00000000..2a2557f4 --- /dev/null +++ b/src/routes/morphism-search/results/+page.svelte @@ -0,0 +1,7 @@ + + + From 6713d7ee9bade1e3ad6172dac57f3d1567cc0bb6 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 4 Jul 2026 11:52:45 +0200 Subject: [PATCH 08/10] add split epis and monos --- .../data/morphism-implications/mono-epi-iso.yaml | 10 +++++++++- .../data/morphism-properties/split epimorphism.yaml | 11 +++++++++++ .../data/morphism-properties/split monomorphism.yaml | 11 +++++++++++ databases/catdat/data/morphisms/empty-map.yaml | 3 +++ databases/catdat/data/morphisms/terminal-map.yaml | 4 ++-- 5 files changed, 36 insertions(+), 3 deletions(-) create mode 100644 databases/catdat/data/morphism-properties/split epimorphism.yaml create mode 100644 databases/catdat/data/morphism-properties/split monomorphism.yaml diff --git a/databases/catdat/data/morphism-implications/mono-epi-iso.yaml b/databases/catdat/data/morphism-implications/mono-epi-iso.yaml index b92f51d7..3d51a141 100644 --- a/databases/catdat/data/morphism-implications/mono-epi-iso.yaml +++ b/databases/catdat/data/morphism-implications/mono-epi-iso.yaml @@ -1,9 +1,17 @@ - id: iso_is_mono assumptions: - isomorphism + conclusions: + - split monomorphism + proof: This is trivial. + is_equivalence: false + +- id: split_mono_is_regular_mono + assumptions: + - split monomorphism conclusions: - regular monomorphism - proof: 'If $f : A \to B$ is an isomorphism, it is an equalizer of $\id_B, \id_B : B \rightrightarrows B$.' + proof: 'Let $f : A \to B$ be a split monomorphism, and choose a morphism $g : B \to A$ with $g \circ f = \id_A$. Then it is easy to check that $f$ is an equalizer of $\id_B, f \circ g : B \rightrightarrows B$.' is_equivalence: false - id: mono_is_iso diff --git a/databases/catdat/data/morphism-properties/split epimorphism.yaml b/databases/catdat/data/morphism-properties/split epimorphism.yaml new file mode 100644 index 00000000..d2076752 --- /dev/null +++ b/databases/catdat/data/morphism-properties/split epimorphism.yaml @@ -0,0 +1,11 @@ +id: split epimorphism +relation: is a +description: 'A morphism $f : A \to B$ is a split epimorphism if there is a morphism $g : B \to A$ with $f \circ g = \id_B$.' +nlab_link: https://ncatlab.org/nlab/show/split+epimorphism +invariant_under_equivalences: true +dual_property: split monomorphism +related_properties: + - epimorphism + +tags: + - types of epimorphisms diff --git a/databases/catdat/data/morphism-properties/split monomorphism.yaml b/databases/catdat/data/morphism-properties/split monomorphism.yaml new file mode 100644 index 00000000..3c6caee5 --- /dev/null +++ b/databases/catdat/data/morphism-properties/split monomorphism.yaml @@ -0,0 +1,11 @@ +id: split monomorphism +relation: is a +description: 'A morphism $f : A \to B$ is a split monomorphism if there is a morphism $g : B \to A$ with $g \circ f = \id_A$.' +nlab_link: https://ncatlab.org/nlab/show/split+monomorphism +invariant_under_equivalences: true +dual_property: split epimorphism +related_properties: + - monomorphism + +tags: + - types of monomorphisms diff --git a/databases/catdat/data/morphisms/empty-map.yaml b/databases/catdat/data/morphisms/empty-map.yaml index 7ada0437..659aa892 100644 --- a/databases/catdat/data/morphisms/empty-map.yaml +++ b/databases/catdat/data/morphisms/empty-map.yaml @@ -17,3 +17,6 @@ satisfied_properties: unsatisfied_properties: - property: epimorphism proof: Since $X$ is non-empty, the map is not surjective. + + - property: split monomorphism + proof: There is no map $X \to \varnothing$. diff --git a/databases/catdat/data/morphisms/terminal-map.yaml b/databases/catdat/data/morphisms/terminal-map.yaml index c2014410..986a4fd9 100644 --- a/databases/catdat/data/morphisms/terminal-map.yaml +++ b/databases/catdat/data/morphisms/terminal-map.yaml @@ -11,8 +11,8 @@ tags: related_morphisms: [] satisfied_properties: - - property: epimorphism - proof: The map is surjective because $X$ is non-empty. + - property: split epimorphism + proof: 'Take any element $x \in X$. The corresponding map $x : 1 \to X$ is a section of $! : X \to 1$.' unsatisfied_properties: - property: monomorphism From 6c24e6f126afeaab48311201274da3ff918dbe69 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 5 Jul 2026 08:29:49 +0200 Subject: [PATCH 09/10] reword requirements text on implication page --- src/pages/ImplicationPage.svelte | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pages/ImplicationPage.svelte b/src/pages/ImplicationPage.svelte index 39db6aa7..3dc99f43 100644 --- a/src/pages/ImplicationPage.svelte +++ b/src/pages/ImplicationPage.svelte @@ -42,7 +42,7 @@ {#each Object.entries(implication.mapped_assumptions) as [map, list]} {#if list?.length}

    - Assumptions on {map} {mapped_types[map]}: + Requirements of the {map}: {#each list as property, index} {property} Date: Sun, 5 Jul 2026 08:30:04 +0200 Subject: [PATCH 10/10] rename: ambient_category ---> category (for morphism type) --- .../catdat/data/morphism-implications/mono-epi-iso.yaml | 6 +++--- databases/catdat/data/morphisms/empty-map.yaml | 2 +- databases/catdat/data/morphisms/id_X.yaml | 2 +- .../catdat/data/morphisms/integer-rational-embedding.yaml | 2 +- databases/catdat/data/morphisms/terminal-map.yaml | 2 +- databases/catdat/schema/001_structures.sql | 2 +- databases/catdat/schema/008_morphisms.sql | 4 ++-- databases/catdat/scripts/seed.ts | 4 ++-- databases/catdat/scripts/utils/seed.types.ts | 2 +- src/lib/commons/types.ts | 6 +++--- src/lib/server/fetchers/morphism.ts | 8 ++++---- src/routes/morphism/[id]/+page.svelte | 6 +++--- 12 files changed, 23 insertions(+), 23 deletions(-) diff --git a/databases/catdat/data/morphism-implications/mono-epi-iso.yaml b/databases/catdat/data/morphism-implications/mono-epi-iso.yaml index 3d51a141..7cedee2c 100644 --- a/databases/catdat/data/morphism-implications/mono-epi-iso.yaml +++ b/databases/catdat/data/morphism-implications/mono-epi-iso.yaml @@ -18,7 +18,7 @@ assumptions: - monomorphism mapped_assumptions: - ambient_category: + category: - subobject-trivial conclusions: - isomorphism @@ -30,7 +30,7 @@ - monomorphism - epimorphism mapped_assumptions: - ambient_category: + category: - balanced conclusions: - isomorphism @@ -49,7 +49,7 @@ assumptions: - monomorphism mapped_assumptions: - ambient_category: + category: - mono-regular conclusions: - regular monomorphism diff --git a/databases/catdat/data/morphisms/empty-map.yaml b/databases/catdat/data/morphisms/empty-map.yaml index 659aa892..cc53d00c 100644 --- a/databases/catdat/data/morphisms/empty-map.yaml +++ b/databases/catdat/data/morphisms/empty-map.yaml @@ -1,7 +1,7 @@ id: empty-map name: map from the empty set notation: $!$ -ambient_category: Set +category: Set description: 'For every set $X$ there is a unique map $! : \varnothing \hookrightarrow X$, the empty map. In this entry, we require that $X$ is non-empty.' nlab_link: https://ncatlab.org/nlab/show/empty+set diff --git a/databases/catdat/data/morphisms/id_X.yaml b/databases/catdat/data/morphisms/id_X.yaml index 75e27374..6595e969 100644 --- a/databases/catdat/data/morphisms/id_X.yaml +++ b/databases/catdat/data/morphisms/id_X.yaml @@ -1,7 +1,7 @@ id: id_X name: identity map of a set notation: $\id_X$ -ambient_category: Set +category: Set description: 'Every object of a category has an identity morphism. In this case, we take a set $X$ and consider its identity morphism $\id_X : X \to X$ in $\Set$.' nlab_link: https://ncatlab.org/nlab/show/identity+morphism diff --git a/databases/catdat/data/morphisms/integer-rational-embedding.yaml b/databases/catdat/data/morphisms/integer-rational-embedding.yaml index 5e5ef096..5641ed10 100644 --- a/databases/catdat/data/morphisms/integer-rational-embedding.yaml +++ b/databases/catdat/data/morphisms/integer-rational-embedding.yaml @@ -1,7 +1,7 @@ id: integer-rational-embedding name: embedding of integer into rational numbers notation: $\iota_{\IZ,\IQ}$ -ambient_category: CRing +category: CRing description: 'The inclusion $\iota_{\IZ,\IQ} : \IZ \hookrightarrow \IQ$ is a typical example of a localization. It is a standard example of a mono- and epimorphism which is not an isomorphism in the category of (commutative) rings.' nlab_link: https://ncatlab.org/nlab/show/localization+of+a+commutative+ringlization diff --git a/databases/catdat/data/morphisms/terminal-map.yaml b/databases/catdat/data/morphisms/terminal-map.yaml index 986a4fd9..3e3c891e 100644 --- a/databases/catdat/data/morphisms/terminal-map.yaml +++ b/databases/catdat/data/morphisms/terminal-map.yaml @@ -1,7 +1,7 @@ id: terminal-map name: map into the singleton set notation: $!$ -ambient_category: Set +category: Set description: 'For every set $X$ there is a unique map $! : X \to 1$, where $1$ is the singleton set. In this entry, we require that $X$ has at least $2$ elements.' nlab_link: null diff --git a/databases/catdat/schema/001_structures.sql b/databases/catdat/schema/001_structures.sql index f1c285b2..18313c1f 100644 --- a/databases/catdat/schema/001_structures.sql +++ b/databases/catdat/schema/001_structures.sql @@ -75,4 +75,4 @@ INSERT INTO structure_maps VALUES ('source', 'functor', 'category'), ('target', 'functor', 'category'), - ('ambient_category', 'morphism', 'category'); \ No newline at end of file + ('category', 'morphism', 'category'); \ No newline at end of file diff --git a/databases/catdat/schema/008_morphisms.sql b/databases/catdat/schema/008_morphisms.sql index dcd5f804..dfc9ea41 100644 --- a/databases/catdat/schema/008_morphisms.sql +++ b/databases/catdat/schema/008_morphisms.sql @@ -1,8 +1,8 @@ CREATE TABLE morphisms ( id TEXT PRIMARY KEY, - ambient_category TEXT NOT NULL, + category TEXT NOT NULL, FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE, - FOREIGN KEY (ambient_category) REFERENCES categories (id) ON DELETE CASCADE + FOREIGN KEY (category) REFERENCES categories (id) ON DELETE CASCADE ); CREATE TRIGGER trg_morphism_type_check diff --git a/databases/catdat/scripts/seed.ts b/databases/catdat/scripts/seed.ts index e993eefe..0d5c6e5d 100644 --- a/databases/catdat/scripts/seed.ts +++ b/databases/catdat/scripts/seed.ts @@ -312,11 +312,11 @@ function insert_functor(functor: FunctorYaml) { */ function insert_morphism(morphism: MorphismYaml) { const morphism_insert = db.prepare( - `INSERT INTO morphisms (id, ambient_category) + `INSERT INTO morphisms (id, category) VALUES (?, ?)`, ) - morphism_insert.run(morphism.id, morphism.ambient_category) + morphism_insert.run(morphism.id, morphism.category) } /** diff --git a/databases/catdat/scripts/utils/seed.types.ts b/databases/catdat/scripts/utils/seed.types.ts index 2f201508..f266a68c 100644 --- a/databases/catdat/scripts/utils/seed.types.ts +++ b/databases/catdat/scripts/utils/seed.types.ts @@ -68,7 +68,7 @@ export type FunctorYaml = StructureYaml & { } export type MorphismYaml = StructureYaml & { - ambient_category: string + category: string } export type PropertyYaml = { diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 840de28b..cc128c81 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -45,9 +45,9 @@ export type FunctorSpecificDisplay = { } export type MorphismSpecificDisplay = { - ambient_category: string - ambient_category_name: string - ambient_category_notation: string + category: string + category_name: string + category_notation: string } export type MappedTypes = Record diff --git a/src/lib/server/fetchers/morphism.ts b/src/lib/server/fetchers/morphism.ts index d259093d..c1b7d33b 100644 --- a/src/lib/server/fetchers/morphism.ts +++ b/src/lib/server/fetchers/morphism.ts @@ -8,11 +8,11 @@ export function fetch_morphism(id: string) { // specific information for the morphism sql` SELECT - c.id AS ambient_category, - c.name AS ambient_category_name, - c.notation AS ambient_category_notation + c.id AS category, + c.name AS category_name, + c.notation AS category_notation FROM morphisms m - INNER JOIN structures AS c ON c.id = m.ambient_category + INNER JOIN structures AS c ON c.id = m.category WHERE m.id = ${id} `, ) diff --git a/src/routes/morphism/[id]/+page.svelte b/src/routes/morphism/[id]/+page.svelte index fb6a3186..0e2550a6 100644 --- a/src/routes/morphism/[id]/+page.svelte +++ b/src/routes/morphism/[id]/+page.svelte @@ -7,9 +7,9 @@ {#snippet definition()}

  • - Ambient category: - - {data.morphism.ambient_category_name} + Category: + + {data.morphism.category_name}
    • {/snippet}