Add Functors to CatDat

.vscode/settings.json

@@ -28,11 +28,14 @@
 		"coequalizer",
 		"coequalizers",
 		"cofiltered",
+		"cofinitary",
 		"cogenerates",
 		"cogenerator",
 		"cokernel",
 		"colimit",
 		"colimits",
+		"comonad",
+		"comonadic",
 		"conormal",
 		"coproduct",
 		"coproducts",
@@ -105,6 +108,7 @@
 		"rng",
 		"rngs",
 		"Rosicky",
+		"saft",
 		"Schapira",
 		"semisimple",
 		"setoid",

database/data/000_clear.sql

@@ -20,6 +20,18 @@ DELETE FROM tags;
 
 DELETE FROM related_properties;
 DELETE FROM properties;
+
+DELETE FROM functor_property_assignments;
+DELETE FROM functor_non_property_assignments;
+DELETE FROM functor_properties;
+DELETE FROM functors;
+
 DELETE FROM prefixes;
 
+DELETE FROM functor_implication_assumptions;
+DELETE FROM functor_implication_conclusions;
+DELETE FROM functor_implication_source_assumptions;
+DELETE FROM functor_implication_target_assumptions;
+DELETE FROM functor_implications;
+
 PRAGMA foreign_keys = ON;

database/data/004_prefixes.sql

@@ -4,4 +4,5 @@ INSERT INTO prefixes (prefix, negation) VALUES
 	('is an', 'is not an'),
 	('has', 'does not have'),
 	('has a', 'does not have a'),
-	('has an', 'does not have an');
+	('has an', 'does not have an'),
+	('', 'does not');

database/data/014_functor-properties.sql

@@ -0,0 +1,169 @@
+INSERT INTO functor_properties (
+    id,
+    prefix,
+    description,
+    nlab_link,
+    invariant_under_equivalences,
+    dual_property_id
+)
+VALUES 
+    (
+        'faithful',
+        'is',
+        'A functor is faithful when it is injective on Hom-sets: If $F(f)=F(g)$, then $f=g$.',
+        'https://ncatlab.org/nlab/show/faithful+functor',
+        TRUE,
+        'faithful'
+    ),
+    (
+        'full',
+        'is',
+        'A functor is full when it is surjective on Hom-sets: Every morphism $F(A) \to F(B)$ is induced by a morphism $A \to B$.',
+        'https://ncatlab.org/nlab/show/full+functor',
+        TRUE,
+        'full'
+    ),
+    (
+        'essentially surjective',
+        'is',
+        'A functor $F : \mathcal{C} \to \mathcal{D}$ is essentially surjective when every object $Y \in \mathcal{D}$ is isomorphic to $F(X)$ for some $X \in \mathcal{C}$.',
+        'https://ncatlab.org/nlab/show/essentially+surjective+functor',
+        TRUE,
+        'essentially surjective'
+    ),
+    (
+        'equivalence',
+        'is an',
+        'A functor is an equivalence if it has a pseudo-inverse functor.',
+        'https://ncatlab.org/nlab/show/equivalence+of+categories',
+        TRUE,
+        'equivalence'
+    ),
+    (
+        'continuous',
+        'is',
+        'A functor is continuous when it preserves all small limits.',
+        'https://ncatlab.org/nlab/show/continuous+functor',
+        TRUE,
+        'cocontinuous'
+    ),
+    (
+        'cocontinuous',
+        'is',
+        'A functor is cocontinuous when it preserves all small colimits.',
+        'https://ncatlab.org/nlab/show/cocontinuous+functor',
+        TRUE,
+        'continuous'
+    ),
+    (
+        'preserves products',
+        '',
+        'A functor $F$ preserves products when for every family of objects $(A_i)$ in the source whose product $\prod_i A_i$ exists, also the product $\prod_i F(A_i)$ exists in the target and such that the canonical morphism $F(\prod_i A_i) \to \prod_i F(A_i)$ is an isomorphism.',
+        NULL,
+        TRUE,
+        'preserves coproducts'
+    ),
+    (
+        'preserves coproducts',
+        '',
+        'A functor $F$ preserves coproducts when for every family of objects $(A_i)$ in the source whose coproduct $\prod_i A_i$ exists, also the coproduct $\coprod_i F(A_i)$ exists in the target and such that the canonical morphism $\coprod_i F(A_i) \to F(\coprod_i A_i)$ is an isomorphism.',
+        NULL,
+        TRUE,
+        'preserves products'
+    ),
+    (
+        'preserves equalizers',
+        '',
+        'A functor $F$ preserves equalizers when for every parallel pair of morphisms $f,g : A \to B$ whose equalizer $i : E \to A$ exists, also $F(i) : F(E) \to F(A)$ is an equalizer of $F(f),F(g) : F(A) \to F(B)$.',
+        NULL,
+        TRUE,
+        'preserves coequalizers'
+    ),
+    (
+        'preserves coequalizers',
+        '',
+        'A functor $F$ preserves coequalizers when for every parallel pair of morphisms $f,g : A \to B$ whose coequalizer $p : B \to Q$ exists, also $F(p) : F(B) \to F(Q)$ is an coequalizer of $F(f),F(g) : F(A) \to F(B)$.',
+        NULL,
+        TRUE,
+        'preserves equalizers'
+    ),
+    (
+        'left adjoint',
+        'is a',
+        'A functor $F : \mathcal{C} \to \mathcal{D}$ is a left adjoint when there is a functor $G : \mathcal{D} \to \mathcal{C}$ such that there are natural bijections $\hom(F(A),B) \cong \hom(A,G(B))$.',
+        'https://ncatlab.org/nlab/show/left+adjoint',
+        TRUE,
+        'right adjoint'
+    ),
+    (
+        'right adjoint',
+        'is a',
+        'A functor $F : \mathcal{C} \to \mathcal{D}$ is a right adjoint when there is a functor $G : \mathcal{D} \to \mathcal{C}$ such that there are natural bijections $\hom(G(A),B) \cong \hom(A,F(B))$.',
+        'https://ncatlab.org/nlab/show/right+adjoint',
+        TRUE,
+        'left adjoint'
+    ),
+    (
+        'monadic',
+        'is',
+        'A functor $F : \mathcal{C} \to \mathcal{D}$ is monadic when there is a monad $T$ on $\mathcal{D}$ such that $F$ is equivalent to the forgetful functor $U^T : \mathbf{Alg}(T) \to \mathcal{D}$.',
+        'https://ncatlab.org/nlab/show/monadic+functor',
+        TRUE,
+        'comonadic'
+    ),
+    (
+        'comonadic',
+        'is',
+        'A functor $F : \mathcal{C} \to \mathcal{D}$ is comonadic when there is a comonad $T$ on $\mathcal{D}$ such that $F$ is equivalent to the forgetful functor $U^T : \mathbf{CoAlg}(T) \to \mathcal{D}$.',
+        'https://ncatlab.org/nlab/show/comonadic+functor',
+        TRUE,
+        'monadic'
+    ),
+    (
+        'conservative',
+        'is',
+        'A functor $F : \mathcal{C} \to \mathcal{D}$ is conservative when it is isomorphic-reflecting: If $f$ is a morphism in $\mathcal{C}$ such that $F(f)$ is an isomorphism, then $f$ is an isomorphism.',
+        'https://ncatlab.org/nlab/show/conservative+functor',
+        TRUE,
+        'conservative'
+    ),
+    (
+        'finitary',
+        'is',
+        'A functor is finitary when it preserves filtered colimits.',
+        'https://ncatlab.org/nlab/show/finitary+functor',
+        TRUE,
+        'cofinitary'
+    ),
+    (
+        'cofinitary',
+        'is',
+        'A functor is cofinitary when it preserves filtered limits.',
+        NULL,
+        TRUE,
+        'finitary'
+    ),
+    (
+        'left exact',
+        'is',
+        'A functor is left exact when it preserves finite limits.',
+        'https://ncatlab.org/nlab/show/exact+functor',
+        TRUE,
+        'right exact'
+    ),
+    (
+        'right exact',
+        'is',
+        'A functor is right exact when it preserves finite colimits.',
+        'https://ncatlab.org/nlab/show/exact+functor',
+        TRUE,
+        'left exact'
+    ),
+    (
+        'exact',
+        'is',
+        'A functor is exact when it is left exact and right exact.',
+        'https://ncatlab.org/nlab/show/exact+functor',
+        TRUE,
+        'exact'
+    );

database/data/015_functor-implications.sql

@@ -0,0 +1,105 @@
+INSERT INTO functor_implication_input (
+    id,
+    assumptions,
+    source_assumptions,
+    target_assumptions,
+    conclusions,
+    reason,
+    is_equivalence
+)
+VALUES
+    (
+        'equivalence_criterion',
+        '["full", "faithful", "essentially surjective"]',
+        '[]',
+        '[]',
+        '["equivalence"]',
+        'TBA.', -- FIXME
+        TRUE
+    ),
+    (
+        'continuous_consequences', -- TODO: dualize automatically
+        '["continuous"]',
+        '[]',
+        '[]',
+        '["preserves products", "preserves equalizers", "cofinitary"]',
+        'This is trivial.',
+        FALSE
+    ),
+    (
+        'dual_continuous_consequences', -- TODO: remove this later
+        '["cocontinuous"]',
+        '[]',
+        '[]',
+        '["preserves coproducts", "preserves coequalizers", "finitary"]',
+        'This is trivial.',
+        FALSE
+    ),
+    (
+        'continuous_criterion',
+        '["preserves products", "preserves equalizers"]',
+        '["products"]',
+        '[]',
+        '["continuous"]',
+        'TBA.', -- FIXME
+        FALSE
+    ),
+    (
+        'continuous_criterion_filtered',
+        '["left exact", "cofinitary"]',
+        '["finitely complete"]',
+        '[]',
+        '["continuous"]',
+        'This is because every limit can be written as a filtered limit of finite limits.',
+        FALSE
+    ),
+    (
+        'exact_definition',
+        '["exact"]',
+        '[]',
+        '[]',
+        '["left exact", "right exact"]',
+        'This holds by definition.',
+        TRUE
+    ),
+    (
+        'equivalence_consequences', -- TODO: dualize automatically
+        '["equivalence"]',
+        '[]',
+        '[]',
+        '["continuous", "right adjoint"]',
+        'Easy.',
+        FALSE
+    ),
+    (
+        'right_adjoint_consequences', -- TODO: dualize automatically
+        '["right adjoint"]',
+        '[]',
+        '[]',
+        '["continuous"]',
+        'TBA.', -- FIXME
+        FALSE
+    ),
+    (
+        'saft', -- TODO: dualize automatically,
+        '["continuous"]',
+        '["complete", "locally small", "well-powered", "cogenerator"]',
+        '["locally small"]',
+        '["right adjoint"]',
+        'This is the Special Adjoint Functor Theorem. The proof can be found, for example, at the <a href="https://ncatlab.org/nlab/show/adjoint+functor+theorem" target="_blank">nLab</a>.',
+        FALSE
+    ),
+    (
+        'monadic_consequences', -- TODO: dualize automatically
+        '["monadic"]',
+        '[]',
+        '[]',
+        '["faithful", "right adjoint", "conservative"]',
+        'This is clear since the forgetful functor from the category of $T$-algebras has these properties, where $T$ is any monad.',
+        FALSE
+    );
+
+    -- TODO: remove this later:
+    UPDATE functor_implications
+    SET dualized_from = 'continuous_consequences'
+    WHERE id = 'dual_continuous_consequences';

database/migrations/014_functors-table.sql

@@ -0,0 +1,13 @@
+CREATE TABLE functors (
+    id TEXT PRIMARY KEY,
+    name TEXT NOT NULL UNIQUE,
+    notation TEXT,
+    objects TEXT NOT NULL,
+    source TEXT NOT NULL,
+    target TEXT NOT NULL,
+    description TEXT NOT NULL CHECK (length(description) > 0),
+    url TEXT CHECK (url IS NULL OR url like 'https://%'),
+    created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    FOREIGN KEY (source) REFERENCES categories (id) ON DELETE CASCADE,
+    FOREIGN KEY (target) REFERENCES categories (id) ON DELETE CASCADE
+);

database/migrations/015_functor-properties-tables.sql

@@ -0,0 +1,31 @@
+CREATE TABLE functor_properties (
+    id TEXT PRIMARY KEY,
+    prefix TEXT NOT NULL,
+    description TEXT NOT NULL CHECK (length(description) > 0),
+    nlab_link TEXT CHECK (nlab_link IS NULL OR nlab_link like 'https://%'),
+    invariant_under_equivalences INTEGER NOT NULL DEFAULT TRUE,
+    dual_property_id TEXT,
+    created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    FOREIGN KEY (prefix) REFERENCES prefixes (prefix) ON DELETE RESTRICT,
+    FOREIGN KEY (dual_property_id) REFERENCES functor_properties (id) ON DELETE SET NULL
+);
+
+CREATE TABLE functor_property_assignments (
+    functor_id TEXT NOT NULL,
+    property_id TEXT NOT NULL,
+    reason TEXT NOT NULL CHECK (length(reason) > 0),
+    created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    PRIMARY KEY (functor_id, property_id),
+    FOREIGN KEY (functor_id) REFERENCES functors (id) ON DELETE CASCADE,
+    FOREIGN KEY (property_id) REFERENCES functor_properties (id) ON DELETE CASCADE
+);
+
+CREATE TABLE functor_non_property_assignments (
+    functor_id TEXT NOT NULL,
+    non_property_id TEXT NOT NULL,
+    reason TEXT NOT NULL CHECK (length(reason) > 0),
+    created_at TEXT NOT NULL DEFAULT CURRENT_TIMESTAMP,
+    PRIMARY KEY (functor_id, non_property_id),
+    FOREIGN KEY (functor_id) REFERENCES functors (id) ON DELETE CASCADE,
+    FOREIGN KEY (non_property_id) REFERENCES functor_properties (id) ON DELETE CASCADE
+);