group various implications

Author: ScriptRaccoon

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
 ),

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 <a href="https://doi.org/10.1016/0022-4049(93)90035-R" target="_blank">Introduction to extensive and distributive categories</a>.',
-	FALSE
-),
-(
-	'extensive_consequence',
-	'["extensive"]',
-	'["disjoint finite coproducts"]',
-	'This is Prop. 2.6 in <a href="https://doi.org/10.1016/0022-4049(93)90035-R" target="_blank">Introduction to extensive and distributive categories</a>.',
+	'["disjoint finite coproducts", "strict initial object"]',
+	'These are Prop. 2.6 and 2.8 in <a href="https://doi.org/10.1016/0022-4049(93)90035-R" target="_blank">Introduction to extensive and distributive categories</a>.',
 	FALSE
 ),
 (

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
 ),
@@ -55,13 +55,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"]',

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"]',

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
 ),

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 <a href="https://www.cambridge.org/core/books/handbook-of-categorical-algebra/5033A02442342401E7BCC26A042DAB94" target="_blank">Handbook of Categorical Algebra Vol. 3</a>. For "cogenerator" see the <a href="https://ncatlab.org/nlab/show/cogenerator" target="_blank">nLab</a>.',
+	'["locally presentable", "cogenerator", "infinitary extensive"]',
+	'A Grothendieck topos is locally presentable by Prop. 3.4.16 in <a href="https://www.cambridge.org/core/books/handbook-of-categorical-algebra/5033A02442342401E7BCC26A042DAB94" target="_blank">Handbook of Categorical Algebra Vol. 3</a>, has a cogenerator (see <a href="https://ncatlab.org/nlab/show/cogenerator" target="_blank">nLab</a>) and is infinitary extensive by <a href="https://ncatlab.org/nlab/show/Giraud%27s+theorem" target="_blank">Giraud''s Theorem</a>.',
 	FALSE
 ),
 (
@@ -181,13 +181,6 @@ VALUES
 	'The pullback functor preserves coproducts because it has a right adjoint. See also Remark 2.6 at the <a href="https://ncatlab.org/nlab/show/extensive+category" target="_blank">nLab</a>.',
 	FALSE
 ),
-(
-	'Grothendieck_extensive',
-	'["Grothendieck topos"]',
-	'["infinitary extensive"]',
-	'This is a part of <a href="https://ncatlab.org/nlab/show/Giraud%27s+theorem" target="_blank">Giraud''s Theorem</a>.',
-	FALSE
-),
 (
 	'topos_is_malcev',
 	'["elementary topos"]',