diff --git a/.vscode/settings.json b/.vscode/settings.json
index 8bf28de5..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,9 +135,10 @@
"Kashiwara",
"katex",
"Kolmogorov",
- "lextensive",
+ "Lawvere",
"libsql",
"Lindelöf",
+ "Makkai",
"Malcev",
"Mathoverflow",
"metrizable",
@@ -148,6 +154,7 @@
"Niefield",
"nilradical",
"nlab",
+ "Noetherian",
"objectwise",
"pointwise",
"Pontryagin",
@@ -155,6 +162,7 @@
"posets",
"preadditive",
"precomposed",
+ "precomposition",
"preimage",
"preimages",
"preordered",
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'),
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/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.'
);
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..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
),
@@ -76,24 +76,10 @@ 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"]',
- '["finite products"]',
+ '["finite products", "countable powers"]',
'This is trivial.',
FALSE
),
@@ -206,7 +192,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
),
(
@@ -223,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"]',
@@ -251,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"]',
@@ -273,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 b7f00e0f..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
),
(
@@ -230,13 +223,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/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 ce4edcfd..951bc3e4 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
),
(
@@ -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"]',
@@ -167,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 8d23cdcf..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
),
@@ -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
),
(
diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql
index 30a87204..d57c5142 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
),
(
@@ -35,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.',
diff --git a/database/data/005_implications/008_topos-theory-implications.sql b/database/data/005_implications/008_topos-theory-implications.sql
index 7ef2880c..778e6960 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"]',
@@ -156,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
),
(
@@ -195,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"]',
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,
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