From cfd64d5510c47a37a1552411248e593cdd869c7f Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 01:29:55 +0200 Subject: [PATCH 01/10] Met_c does not have sequential colimits --- database/data/004_property-assignments/Met_c.sql | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/004_property-assignments/Met_c.sql b/database/data/004_property-assignments/Met_c.sql index 42ac3cee..2dd5084b 100644 --- a/database/data/004_property-assignments/Met_c.sql +++ b/database/data/004_property-assignments/Met_c.sql @@ -97,7 +97,7 @@ VALUES ), ( 'Met_c', - 'coequalizers', + 'sequential colimits', FALSE, - 'See MO/509548.' + 'See MO/510316.' ); From c93545b717a94268fab37f87282647063d728d71 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 02:44:31 +0200 Subject: [PATCH 02/10] remove "lextensive" (for now) --- .vscode/settings.json | 1 - .../data/003_properties/003_limits-colimits-behavior.sql | 8 -------- database/data/003_properties/100_related-properties.sql | 3 --- .../002_limits-colimits-behavior-implications.sql | 7 ------- scripts/expected-data/Ab.json | 1 - scripts/expected-data/Set.json | 1 - scripts/expected-data/Top.json | 1 - 7 files changed, 22 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index 8bf28de5..f94b26bd 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -130,7 +130,6 @@ "Kashiwara", "katex", "Kolmogorov", - "lextensive", "libsql", "Lindelöf", "Malcev", diff --git a/database/data/003_properties/003_limits-colimits-behavior.sql b/database/data/003_properties/003_limits-colimits-behavior.sql index 48aee05f..59d6b5b5 100644 --- a/database/data/003_properties/003_limits-colimits-behavior.sql +++ b/database/data/003_properties/003_limits-colimits-behavior.sql @@ -164,14 +164,6 @@ VALUES 'extensive', TRUE ), -( - 'lextensive', - 'is', - 'A category $\mathcal{C}$ is lextensive when it is extensive and has finite limits.', - 'https://ncatlab.org/nlab/show/extensive+category', - NULL, - TRUE -), ( 'infinitary extensive', 'is', diff --git a/database/data/003_properties/100_related-properties.sql b/database/data/003_properties/100_related-properties.sql index 5dfc8c8a..cb9923e1 100644 --- a/database/data/003_properties/100_related-properties.sql +++ b/database/data/003_properties/100_related-properties.sql @@ -217,9 +217,6 @@ VALUES ('extensive', 'infinitary extensive'), ('extensive', 'finite coproducts'), ('extensive', 'disjoint finite coproducts'), -('extensive', 'lextensive'), -('lextensive', 'extensive'), -('lextensive', 'finitely complete'), ('infinitary extensive', 'extensive'), ('infinitary extensive', 'coproducts'), ('infinitary extensive', 'disjoint coproducts'), diff --git a/database/data/005_implications/002_limits-colimits-behavior-implications.sql b/database/data/005_implications/002_limits-colimits-behavior-implications.sql index b7f00e0f..95b2972a 100644 --- a/database/data/005_implications/002_limits-colimits-behavior-implications.sql +++ b/database/data/005_implications/002_limits-colimits-behavior-implications.sql @@ -230,13 +230,6 @@ VALUES 'This holds by definition of a regular category.', FALSE ), -( - 'lextensive_def', - '["lextensive"]', - '["extensive", "finitely complete"]', - 'This holds by definition.', - TRUE -), ( 'power_construction', '["copowers", "cartesian closed"]', diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index 3b0ab31d..65d6a56a 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -130,7 +130,6 @@ "infinitary extensive": false, "coextensive": false, "infinitary coextensive": false, - "lextensive": false, "regular subobject classifier": false, "direct": false, "inverse": false, diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index 899b6a95..5d5e6f4c 100644 --- a/scripts/expected-data/Set.json +++ b/scripts/expected-data/Set.json @@ -62,7 +62,6 @@ "extensive": true, "infinitary extensive": true, "co-Malcev": true, - "lextensive": true, "locally strongly finitely presentable": true, "regular subobject classifier": true, "coreflexive equalizers": true, diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index 821cfbf5..6229543a 100644 --- a/scripts/expected-data/Top.json +++ b/scripts/expected-data/Top.json @@ -47,7 +47,6 @@ "coregular": true, "extensive": true, "infinitary extensive": true, - "lextensive": true, "regular subobject classifier": true, "coreflexive equalizers": true, "reflexive coequalizers": true, From 916ab786eb09d90f7f3e3308ec72f7cbda01950a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 01:37:03 +0200 Subject: [PATCH 03/10] refine freyd's lemma --- ...limits-colimits-existence-implications.sql | 2 +- .../006_trivial-categories-implications.sql | 30 ++++++++++++++----- 2 files changed, 23 insertions(+), 9 deletions(-) diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index 8ef2e6c2..0690aa81 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -206,7 +206,7 @@ VALUES 'wide_pullbacks_finite', '["pullbacks", "essentially finite"]', '["wide pullbacks"]', - 'Each slice category has finite products and is essentially finite, hence has all products.', + 'Each slice category has finite products and is essentially finite, hence has all products by this result followed by this result.', FALSE ), ( diff --git a/database/data/005_implications/006_trivial-categories-implications.sql b/database/data/005_implications/006_trivial-categories-implications.sql index 8d23cdcf..4f8bb5a6 100644 --- a/database/data/005_implications/006_trivial-categories-implications.sql +++ b/database/data/005_implications/006_trivial-categories-implications.sql @@ -64,23 +64,37 @@ VALUES ), ( 'freyd_small', - '["essentially small", "products"]', + '["essentially small", "powers"]', '["thin"]', - 'See Mac Lane, V.2, Prop. 3. The proof works for any category with products.', + 'See Mac Lane, V.2, Prop. 3. The proof works for any category with powers.', FALSE ), ( 'freyd_countable', - '["essentially countable", "countable products"]', - '["thin", "products"]', - 'To see that the category is thin, use Mac Lane, V.2, Prop. 3. The proof can easily be adapted to this case. So the category is equivalent to a countable preordered set. But then products are just infima, so that repetitions of objects do not matter, and every product can be reduced to a countable one.', + '["essentially countable", "countable powers"]', + '["thin"]', + 'Adjust the proof of Mac Lane, V.2, Prop. 3.', FALSE ), ( 'freyd_finite', - '["essentially finite", "finite products"]', - '["thin", "products"]', - 'To see that the category is thin, use Mac Lane, V.2, Prop. 3. The proof can easily be adapted to this case. So the category is equivalent to a finite preordered set. But then products are just infima, so that repetitions of objects do not matter, and every product can be reduced to a finite one.', + '["essentially finite", "finite powers"]', + '["thin"]', + 'Adjust the proof of Mac Lane, V.2, Prop. 3.', + FALSE +), +( + 'thin_finite_product_reduction', + '["thin", "essentially finite", "finite products"]', + '["products"]', + 'The category is equivalent to a finite preordered set. But then products are just infima, so that repetitions of objects do not matter, and every product can be reduced to a finite one.', + FALSE +), +( + 'thin_countable_product_reduction', + '["thin", "essentially countable", "countable products"]', + '["products"]', + 'The category is equivalent to a countable preordered set. But then products are just infima, so that repetitions of objects do not matter, and every product can be reduced to a countable one.', FALSE ), ( From 2c200a389a36f588596dd9142d91d03b1e442870 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 01:46:05 +0200 Subject: [PATCH 04/10] prefer dual form --- .../005_implications/004_morphism-behavior-implications.sql | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/005_implications/004_morphism-behavior-implications.sql b/database/data/005_implications/004_morphism-behavior-implications.sql index ce4edcfd..130cdd1b 100644 --- a/database/data/005_implications/004_morphism-behavior-implications.sql +++ b/database/data/005_implications/004_morphism-behavior-implications.sql @@ -8,9 +8,9 @@ INSERT INTO implication_input ( VALUES ( 'cancellative_consequence', - '["left cancellative", "coequalizers"]', + '["right cancellative", "equalizers"]', '["thin"]', - 'If $f,g$ are two parallel morphisms, then their coequalizer is a regular epimorphism, but also a monomorphism by assumption, so it must be an isomorphism. But this means that $f = g$.', + 'If $f,g$ are two parallel morphisms, then their equalizer is a regular monomorphism, but also an epimorphism by assumption, so it must be an isomorphism. But this means that $f = g$.', FALSE ), ( From e64119319d247d2a1312347859b11b18d4e9f38e Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 01:55:32 +0200 Subject: [PATCH 05/10] remove redundant implications --- ...limits-colimits-existence-implications.sql | 14 ---------- .../004_morphism-behavior-implications.sql | 28 ------------------- .../008_topos-theory-implications.sql | 14 ---------- 3 files changed, 56 deletions(-) diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index 0690aa81..eacd59aa 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -76,20 +76,6 @@ VALUES 'If $1$ is a terminal object, then $X \times_1 Y = X \times Y$.', FALSE ), -( - 'terminal_consequence', - '["terminal object"]', - '["connected"]', - 'If $1$ denotes the terminal object, then for any two objects $A,B$ we have the zig-zag $A \rightarrow 1 \leftarrow B$.', - FALSE -), -( - 'binary_products_consequence', - '["binary products", "inhabited"]', - '["connected"]', - 'For any two objects $A,B$ we have the zig-zag $A \leftarrow A \times B \rightarrow B$.', - FALSE -), ( 'countable_products_consequence', '["countable products"]', diff --git a/database/data/005_implications/004_morphism-behavior-implications.sql b/database/data/005_implications/004_morphism-behavior-implications.sql index 130cdd1b..6581fb16 100644 --- a/database/data/005_implications/004_morphism-behavior-implications.sql +++ b/database/data/005_implications/004_morphism-behavior-implications.sql @@ -55,34 +55,6 @@ VALUES 'This is trivial.', FALSE ), -( - 'groupoid_thin', - '["groupoid", "equalizers"]', - '["thin"]', - 'The equalizer of any parallel pair $f,g$ must be an isomorphism, so $f=g$.', - FALSE -), -( - 'groupoid_products', - '["groupoid", "binary products", "inhabited"]', - '["trivial"]', - 'Let $\mathcal{C}$ be an inhabited groupoid with binary products. Then it is connected, so we may assume $\mathcal{C}=BG$ for a group $G$ with unique object $*$. But then $* \times * = *$, so there are $p,q \in G$ such that $G \to G \times G$, $x \mapsto (px,qx)$ is bijective. From here it is an easy exercise to deduce $G=1$.', - FALSE -), -( - 'groupoid_initial', - '["groupoid", "initial object"]', - '["trivial"]', - 'This is easy.', - FALSE -), -( - 'groupoid_zero', - '["groupoid", "zero morphisms", "inhabited"]', - '["trivial"]', - 'This is easy.', - FALSE -), ( 'groupoid_connected', '["groupoid", "connected"]', diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql index 7ef2880c..e25358a3 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -41,13 +41,6 @@ VALUES 'If a morphism $X \to Y$ exists, we get a morphism $1 \to [X,Y]$, which forces $[X,Y]$ to be a terminal object by assumption. But then any two morphisms $1 \rightrightarrows [X,Y]$ are equal, so that any two morphisms $X \rightrightarrows Y$ are equal.', FALSE ), -( - 'pointed_ccc_trivial', - '["pointed", "cartesian closed"]', - '["trivial"]', - 'We have $X \cong X \times 1 \cong X \times 0 \cong 0$ for every object $X$.', - FALSE -), ( 'topos_definition', '["elementary topos"]', @@ -69,13 +62,6 @@ VALUES 'The universal property of $\top : 0 \to \Omega$ precisely says that every monomorphism $A \to B$ is the kernel of a unique morphism $B \to \Omega$, so it is normal.', FALSE ), -( - 'subobject_classifier_collapse', - '["subobject classifier", "strict terminal object"]', - '["trivial"]', - 'Since $1 \to \Omega$ is an isomorphism, every monomorphism must be an isomorphism. Applying this to the equalizer of a pair of morphisms, we see that the category is thin. But in a thin category, every morphism is a monomorphism. So every object $X$ has a unique isomorphism $X \to 1$.', - FALSE -), ( 'additive_trivial_condition', '["regular subobject classifier", "additive"]', From 5f3016e1e18fccf02fcaafc638941d62a23de4c5 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 03:05:23 +0200 Subject: [PATCH 06/10] remark about deduced implications --- src/routes/category-implications/+page.svelte | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/routes/category-implications/+page.svelte b/src/routes/category-implications/+page.svelte index d793449e..be9279e9 100644 --- a/src/routes/category-implications/+page.svelte +++ b/src/routes/category-implications/+page.svelte @@ -59,6 +59,12 @@ property of having a terminal object is automatically inferred and added.

+

+ Implications can be combined to yield longer, non-obvious deductions that are not + explicitly listed above. For example, the listed implications imply that every + inhabited groupoid with binary products is trivial. +

+

Moreover, implications are automatically dualized when the corresponding dual properties exist. For example, the statement that finitely complete categories with From fb8d21567860141d168db416a963df2036eb69e9 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 02:21:40 +0200 Subject: [PATCH 07/10] group various implications --- ...limits-colimits-existence-implications.sql | 31 +++---------------- ..._limits-colimits-behavior-implications.sql | 13 ++------ .../003_size-constraints-implications.sql | 11 ++----- .../004_morphism-behavior-implications.sql | 7 ----- .../006_trivial-categories-implications.sql | 4 +-- .../008_topos-theory-implications.sql | 11 ++----- 6 files changed, 14 insertions(+), 63 deletions(-) diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index eacd59aa..efda49c6 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -49,9 +49,9 @@ VALUES FALSE ), ( - 'products_consequence', + 'products_consequences', '["products"]', - '["finite products", "countable products"]', + '["finite products", "countable products", "powers"]', 'This is trivial.', FALSE ), @@ -79,7 +79,7 @@ VALUES ( 'countable_products_consequence', '["countable products"]', - '["finite products"]', + '["finite products", "countable powers"]', 'This is trivial.', FALSE ), @@ -209,20 +209,6 @@ VALUES 'If $X_1,X_2,\dotsc$ is an infinite sequence of objects, then their product is the limit of the sequence $\cdots \to X_2 \times X_1 \to X_1$.', FALSE ), -( - 'products_include_powers', - '["products"]', - '["powers"]', - 'This is trivial.', - FALSE -), -( - 'countable_products_include_countable_powers', - '["countable products"]', - '["countable powers"]', - 'This is trivial.', - FALSE -), ( 'finite_products_include_finite_powers', '["finite products"]', @@ -237,13 +223,6 @@ VALUES 'This is trivial.', FALSE ), -( - 'empty_power', - '["finite powers"]', - '["terminal object"]', - 'The empty power is a terminal object.', - FALSE -), ( 'powers_include_countable_powers', '["powers"]', @@ -259,9 +238,9 @@ VALUES FALSE ), ( - 'finite_powers_include_binary_powers', + 'finite_powers_consequences', '["finite powers"]', - '["binary powers"]', + '["binary powers", "terminal object"]', 'This is trivial.', FALSE ), diff --git a/database/data/005_implications/002_limits-colimits-behavior-implications.sql b/database/data/005_implications/002_limits-colimits-behavior-implications.sql index 95b2972a..ac23032e 100644 --- a/database/data/005_implications/002_limits-colimits-behavior-implications.sql +++ b/database/data/005_implications/002_limits-colimits-behavior-implications.sql @@ -196,17 +196,10 @@ VALUES FALSE ), ( - 'extensive_strict', + 'extensive_consequences', '["extensive"]', - '["strict initial object"]', - 'This is Prop. 2.8 in Introduction to extensive and distributive categories.', - FALSE -), -( - 'extensive_consequence', - '["extensive"]', - '["disjoint finite coproducts"]', - 'This is Prop. 2.6 in Introduction to extensive and distributive categories.', + '["disjoint finite coproducts", "strict initial object"]', + 'These are Prop. 2.6 and 2.8 in Introduction to extensive and distributive categories.', FALSE ), ( diff --git a/database/data/005_implications/003_size-constraints-implications.sql b/database/data/005_implications/003_size-constraints-implications.sql index 2e209325..42d90d9a 100644 --- a/database/data/005_implications/003_size-constraints-implications.sql +++ b/database/data/005_implications/003_size-constraints-implications.sql @@ -14,9 +14,9 @@ VALUES FALSE ), ( - 'essentially_small_consequence', + 'essentially_small_consequences', '["essentially small"]', - '["well-powered", "well-copowered", "locally essentially small"]', + '["well-powered", "well-copowered", "locally essentially small", "generating set"]', 'This is trivial.', FALSE ), @@ -69,13 +69,6 @@ VALUES 'If $S$ is a generating set, we claim that $U := \coprod_{G \in S} G$ is a generator. Let $f,g : A \rightrightarrows B$ be two morphisms with $f h = g h$ for all $h : U \to A$. If $G \in S$, any morphism $G \to A$ extends to $U$ by using zero morphisms outside of $G$. Thus, $fh = gh$ holds for all $h : G \to A$ and $G \in S$. Since $S$ is a generating set, this implies $f = g$.', FALSE ), -( - 'generating_set_small_categories', - '["essentially small"]', - '["generating set"]', - 'In a small category, the set of all objects is clearly a generating set.', - FALSE -), ( 'free-algebra-generates', '["finitary algebraic"]', diff --git a/database/data/005_implications/004_morphism-behavior-implications.sql b/database/data/005_implications/004_morphism-behavior-implications.sql index 6581fb16..951bc3e4 100644 --- a/database/data/005_implications/004_morphism-behavior-implications.sql +++ b/database/data/005_implications/004_morphism-behavior-implications.sql @@ -139,13 +139,6 @@ VALUES 'If $f,g : A \rightrightarrows B$ are two morphisms, then $f^{-1} \circ g : A \to A$ must be the identity, so that $f = g$.', FALSE ), -( - 'discrete_implies_direct', - '["discrete"]', - '["direct"]', - 'This is trivial.', - FALSE -), ( 'direct_implies_sequential_limits', '["direct"]', diff --git a/database/data/005_implications/006_trivial-categories-implications.sql b/database/data/005_implications/006_trivial-categories-implications.sql index 4f8bb5a6..6ad51eb0 100644 --- a/database/data/005_implications/006_trivial-categories-implications.sql +++ b/database/data/005_implications/006_trivial-categories-implications.sql @@ -7,9 +7,9 @@ INSERT INTO implication_input ( ) VALUES ( - 'discrete_consequence', + 'discrete_consequences', '["discrete"]', - '["essentially discrete", "locally small", "skeletal"]', + '["essentially discrete", "locally small", "skeletal", "direct"]', 'This is trivial.', FALSE ), diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql index e25358a3..778e6960 100644 --- a/database/data/005_implications/008_topos-theory-implications.sql +++ b/database/data/005_implications/008_topos-theory-implications.sql @@ -142,8 +142,8 @@ VALUES ( 'grothendieck_topos_consequence', '["Grothendieck topos"]', - '["locally presentable", "cogenerator"]', - 'For "locally presentable" see Prop. 3.4.16 in Handbook of Categorical Algebra Vol. 3. For "cogenerator" see the nLab.', + '["locally presentable", "cogenerator", "infinitary extensive"]', + 'A Grothendieck topos is locally presentable by Prop. 3.4.16 in Handbook of Categorical Algebra Vol. 3, has a cogenerator (see nLab) and is infinitary extensive by Giraud''s Theorem.', FALSE ), ( @@ -181,13 +181,6 @@ VALUES 'The pullback functor preserves coproducts because it has a right adjoint. See also Remark 2.6 at the nLab.', FALSE ), -( - 'Grothendieck_extensive', - '["Grothendieck topos"]', - '["infinitary extensive"]', - 'This is a part of Giraud''s Theorem.', - FALSE -), ( 'topos_is_malcev', '["elementary topos"]', From b7349a1bb411f98a76d69cfdc4ad810ef2c33fdc Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 11:13:30 +0200 Subject: [PATCH 08/10] create separate implication --- .../007_locally-presentable-implications.sql | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index 30a87204..8bce5ab3 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/database/data/005_implications/007_locally-presentable-implications.sql @@ -23,8 +23,15 @@ VALUES ( 'accessible_trivial_consequence', '["accessible"]', - '["well-powered", "generating set"]', - 'For well-poweredness, see nLab. For a $\kappa$-accessible category, the set $G$ appearing in the definition gives a small dense full subcategory, which is in particular a generating set.', + '["generating set"]', + 'For a $\kappa$-accessible category, the set $G$ appearing in the definition gives a small dense full subcategory, which is in particular a generating set.', + FALSE +), +( + 'accessible_well-powered', + '["accessible"]', + '["well-powered"]', + 'See nLab.', FALSE ), ( From 16c74c9a46963eee0412cd8baf1722e6abe91164 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 11:18:06 +0200 Subject: [PATCH 09/10] expand dictionary --- .vscode/settings.json | 11 ++++++++++- .../007_locally-presentable-implications.sql | 2 +- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index f94b26bd..627e8a24 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -17,7 +17,8 @@ "Prost", "SetxSet", "hilberts", - "maxage" + "maxage", + "ndash" ], "cSpell.words": [ "abelian", @@ -39,6 +40,7 @@ "catdat", "clopen", "Clowder", + "coaccessible", "cocartesian", "coclosed", "cocomplete", @@ -70,6 +72,7 @@ "conormal", "copower", "copowers", + "copresentable", "coprime", "coproduct", "coproducts", @@ -88,10 +91,12 @@ "delooping", "deloopings", "Demazure", + "Diers", "diffeomorphism", "diffeomorphisms", "dualizable", "Dualization", + "Eilenberg", "endofunctors", "Engelking", "epimorphic", @@ -130,8 +135,10 @@ "Kashiwara", "katex", "Kolmogorov", + "Lawvere", "libsql", "Lindelöf", + "Makkai", "Malcev", "Mathoverflow", "metrizable", @@ -147,6 +154,7 @@ "Niefield", "nilradical", "nlab", + "Noetherian", "objectwise", "pointwise", "Pontryagin", @@ -154,6 +162,7 @@ "posets", "preadditive", "precomposed", + "precomposition", "preimage", "preimages", "preordered", diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index 8bce5ab3..d57c5142 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/database/data/005_implications/007_locally-presentable-implications.sql @@ -42,7 +42,7 @@ VALUES FALSE ), ( - 'accessible_wellcopowered', + 'accessible_well-copowered', '["accessible", "pushouts"]', '["well-copowered"]', 'See Thm. 2.49 in Adamek-Rosicky or Prop. 6.1.3 in Makkai-Pare.', From 8ea3ba52c49b9eb75ee2dd5c2c754f55db29900f Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Apr 2026 11:35:09 +0200 Subject: [PATCH 10/10] minor additions to 0,1,2 --- database/data/001_categories/007_tiny.sql | 10 +++++----- .../data/001_categories/100_related-categories.sql | 2 ++ 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/database/data/001_categories/007_tiny.sql b/database/data/001_categories/007_tiny.sql index 8f00beb9..0d6fb6f2 100644 --- a/database/data/001_categories/007_tiny.sql +++ b/database/data/001_categories/007_tiny.sql @@ -12,10 +12,10 @@ VALUES ( '0', 'empty category', - '$0$', + '$\mathbf{0}$', 'no objects', 'no morphisms', - 'This is the category with no objects and no morphisms. It is the initial object in the category of (small) categories.', + 'This is the category with no objects and no morphisms. It is the initial object in the category of small categories.', 'https://ncatlab.org/nlab/show/empty+category', NULL ), @@ -25,7 +25,7 @@ VALUES '$\mathbf{1}$', 'a single object $0$', 'only the identity morphism', - 'This is the simplest category, consisting of a single object $0$ and its identity morphism $0 \to 0$. It is the terminal object in the category of small categories.', + 'This is the simplest category, consisting of a single object $0$ and its identity morphism $0 \to 0$. A concrete representation is the full subcategory of $\mathbf{Set}$ consisting of the empty set. It is the terminal object in the category of small categories.', 'https://ncatlab.org/nlab/show/terminal+category', NULL ), @@ -33,9 +33,9 @@ VALUES '2', 'discrete category on two objects', '$\mathbf{2}$', - 'two objects', + 'two objects $0$ and $1$', 'only the two identity morphisms', - 'For a more concrete representation, this is the subcategory of $\mathbf{CRing}$ of the two fields $\mathbb{F}_2$ and $\mathbb{F}_3$.', + 'A concrete representation is the full subcategory of $\mathbf{CRing}$ consisting of the two fields $\mathbb{F}_2$ and $\mathbb{F}_3$.', NULL, NULL ), diff --git a/database/data/001_categories/100_related-categories.sql b/database/data/001_categories/100_related-categories.sql index 571d5705..09a3d7c8 100644 --- a/database/data/001_categories/100_related-categories.sql +++ b/database/data/001_categories/100_related-categories.sql @@ -1,5 +1,7 @@ INSERT INTO related_categories (category_id, related_category_id) VALUES +('0', '1'), +('1', '0'), ('1', '2'), ('2', '1'), ('Ab', 'CMon'),