Add new structure type: morphisms

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

databases/catdat/data/morphism-implications/mono-epi-iso.yaml

@@ -0,0 +1,66 @@
+- 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: '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
+  assumptions:
+    - monomorphism
+  mapped_assumptions:
+    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:
+    category:
+      - balanced
+  conclusions:
+    - 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:
+    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

databases/catdat/data/morphism-properties/epimorphism.yaml

@@ -0,0 +1,12 @@
+id: epimorphism
+relation: is an
+description: 'A morphism $f : A \to B$ is an <i>epimorphism</i> 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
+  - regular epimorphism
+
+tags:
+  - types of epimorphisms

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 <i>isomorphism</i> 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

databases/catdat/data/morphism-properties/monomorphism.yaml

@@ -0,0 +1,12 @@
+id: monomorphism
+relation: is a
+description: 'A morphism $f : A \to B$ is a <i>monomorphism</i> 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
+  - regular monomorphism
+
+tags:
+  - types of monomorphisms

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 <i>regular epimorphism</i> 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

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 <i>regular monomorphism</i> 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

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 <i>split epimorphism</i> 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

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 <i>split monomorphism</i> 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

databases/catdat/data/morphisms/empty-map.yaml

@@ -0,0 +1,22 @@
+id: empty-map
+name: map from the empty set
+notation: $!$
+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.
+
+  - property: split monomorphism
+    proof: There is no map $X \to \varnothing$.

databases/catdat/data/morphisms/id_X.yaml

@@ -0,0 +1,17 @@
+id: id_X
+name: identity map of a set
+notation: $\id_X$
+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: []

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}$
+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.

databases/catdat/data/morphisms/terminal-map.yaml

@@ -0,0 +1,19 @@
+id: terminal-map
+name: map into the singleton set
+notation: $!$
+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: 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
+    proof: Since $X$ has two different elements by assumption, which trivially have the same image, the map is not injective.

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');
+    ('target', 'functor', 'category'),
+    ('category', 'morphism', 'category');

databases/catdat/schema/008_morphisms.sql

@@ -0,0 +1,17 @@
+CREATE TABLE morphisms (
+    id TEXT PRIMARY KEY,
+    category TEXT NOT NULL,
+    FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE,
+    FOREIGN KEY (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;

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

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')
 }

databases/catdat/scripts/expected-data/decided-morphisms.json

@@ -0,0 +1 @@
+["id_X"]

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<T extends StructureYaml>({
 			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, category)
+		VALUES (?, ?)`,
+	)
+
+	morphism_insert.run(morphism.id, morphism.category)
+}
+
 /**
  * Seeds all properties of a given type from YAML files.
  */