diff --git a/database/data/001_categories.sql b/database/data/001_categories.sql index c8c0a203..639da125 100644 --- a/database/data/001_categories.sql +++ b/database/data/001_categories.sql @@ -274,6 +274,15 @@ VALUES 'The name of this category comes from the fact that it consists of two objects and an isomorphism between them, and a functor out of this category is the same as an isomorphism in the target category. The walking isomorphism is actually equivalent to the trivial category.', 'https://ncatlab.org/nlab/show/walking+isomorphism' ), + ( + 'walking_composable_pair', + 'walking composable pair', + '$\{ 0 \to 1 \to 2 \}$', + 'three objects $0,1,2$', + 'a single morphism from each natural number to one greater than or equal to it', + 'The name of this category comes from the fact that a functor out of it is the same as a composable pair of morphisms.', + 'https://ncatlab.org/nlab/show/composable+pair' + ), -- examples of thin categories ( diff --git a/database/data/002_tags.sql b/database/data/002_tags.sql index d7ae97d8..e0b0dde2 100644 --- a/database/data/002_tags.sql +++ b/database/data/002_tags.sql @@ -158,6 +158,9 @@ VALUES ('walking_isomorphism', 'artificial'), ('walking_isomorphism', 'category theory'), ('walking_isomorphism', 'badly-behaved'), + ('walking_composable_pair', 'artificial'), + ('walking_composable_pair', 'category theory'), + ('walking_composable_pair', 'badly-behaved'), ('Setne', 'artificial'), ('Setne', 'set theory'), ('Setne', 'well-behaved'), diff --git a/database/data/003_related-categories.sql b/database/data/003_related-categories.sql index 52db4a5f..6094802d 100644 --- a/database/data/003_related-categories.sql +++ b/database/data/003_related-categories.sql @@ -76,6 +76,7 @@ VALUES ('walking_pair', 'walking_morphism'), ('walking_isomorphism', 'walking_morphism'), ('walking_isomorphism', '1'), + ('walking_composable_pair', 'walking_morphism'), ('Setne', 'Set'), ('B', 'FI'), ('B', 'FS'), diff --git a/database/data/005_properties.sql b/database/data/005_properties.sql index ddba0753..7d695ec0 100644 --- a/database/data/005_properties.sql +++ b/database/data/005_properties.sql @@ -32,6 +32,14 @@ VALUES NULL, TRUE ), + ( + 'locally cartesian closed', + 'is', + 'A category is locally cartesian closed if each of its slice categories is cartesian closed.', + 'https://ncatlab.org/nlab/show/locally+cartesian+closed+category', + NULL, + TRUE + ), ( 'pullbacks', 'has', @@ -541,6 +549,14 @@ VALUES 'connected', TRUE ), + ( + 'strongly connected', + 'is', + 'A category is strongly connected if it is inhabited and every two objects can be joined via a morphism.', + NULL, + 'strongly connected', + TRUE + ), ( 'balanced', 'is', diff --git a/database/data/006_related_properties.sql b/database/data/006_related_properties.sql index 3b6d98ea..43415fcf 100644 --- a/database/data/006_related_properties.sql +++ b/database/data/006_related_properties.sql @@ -4,6 +4,7 @@ VALUES ('locally small', 'locally essentially small'), ('locally essentially small', 'locally small'), ('cartesian closed', 'finite products'), + ('locally cartesian closed', 'cartesian closed'), ('zero morphisms', 'preadditive'), ('zero morphisms', 'pointed'), ('preadditive', 'additive'), diff --git a/database/data/007_category-properties.sql b/database/data/007_category-properties.sql index 58defb18..349a9f7c 100644 --- a/database/data/007_category-properties.sql +++ b/database/data/007_category-properties.sql @@ -15,6 +15,11 @@ VALUES 'Grothendieck topos', 'It is equivalent to the category of sheaves on a one-point space.' ), + ( + 'Set', + 'strongly connected', + 'Every nonempty set is weakly terminal.' + ), ( 'Set', 'finitary algebraic', @@ -80,6 +85,11 @@ VALUES 'disjoint coproducts', 'This follows easily from the corresponding fact for sets.' ), + ( + 'Top', + 'strongly connected', + 'Every nonempty space is weakly terminal.' + ), ( 'Grp', 'locally small', @@ -335,6 +345,11 @@ VALUES 'disjoint coproducts', 'This follows easily from the corresponding fact for sets, since the coproduct of posets is built using the disjoint union.' ), + ( + 'Pos', + 'strongly connected', + 'Every nonempty preorder is weakly terminal.' + ), ( 'M-Set', 'locally small', @@ -423,6 +438,11 @@ VALUES 'generator', 'The one-point set is a generator since it represents the forgetful functor $\mathbf{FinSet} \to \mathbf{Set}$.' ), + ( + 'FinSet', + 'strongly connected', + 'Every nonempty finite set is weakly terminal.' + ), ( 'FinSet', 'cogenerator', @@ -591,6 +611,11 @@ VALUES 'finite', 'trivial' ), + ( + '0', + 'locally cartesian closed', + 'This is vacuously true.' + ), ( '1', 'trivial', @@ -646,6 +671,11 @@ VALUES 'skeletal', 'The two objects are not isomorphic' ), + ( + 'walking_morphism', + 'strongly connected', + 'trivial' + ), ( 'walking_pair', @@ -659,7 +689,7 @@ VALUES ), ( 'walking_pair', - 'connected', + 'strongly connected', 'trivial' ), ( @@ -692,6 +722,31 @@ VALUES 'finite', 'trivial' ), + ( + 'walking_composable_pair', + 'finite', + 'trivial' + ), + ( + 'walking_composable_pair', + 'strongly connected', + 'trivial' + ), + ( + 'walking_composable_pair', + 'skeletal', + 'trivial' + ), + ( + 'walking_composable_pair', + 'products', + 'trivial' + ), + ( + 'walking_composable_pair', + 'coproducts', + 'trivial' + ), -- geometric categories ( @@ -1013,6 +1068,11 @@ VALUES 'skeletal', 'The relation $\leq$ is antisymmetric.' ), + ( + 'N', + 'strongly connected', + 'trivial' + ), ( 'On', 'thin', @@ -1048,6 +1108,11 @@ VALUES 'skeletal', 'The relation $\leq$ is antisymmetric' ), + ( + 'On', + 'strongly connected', + 'trivial' + ), ( 'real_interval', 'small', @@ -1060,8 +1125,8 @@ VALUES ), ( 'real_interval', - 'cartesian closed', - 'The exponential $a \Rightarrow b$ (Heyting implication) is $1$ when $a \leq b$ and otherwise $b$.' + 'strongly connected', + 'trivial' ), ( 'real_interval', @@ -1118,6 +1183,11 @@ VALUES 'locally finitely presentable', 'Every natural number is finitely presentable, and $\infty$ is the colimit of all $n < \infty$.' ), + ( + 'Noo', + 'strongly connected', + 'trivial' + ), -- deloopings ( @@ -1132,7 +1202,7 @@ VALUES ), ( 'BG', - 'connected', + 'strongly connected', 'trivial' ), ( @@ -1157,7 +1227,7 @@ VALUES ), ( 'BGf', - 'connected', + 'strongly connected', 'trivial' ), ( @@ -1177,7 +1247,7 @@ VALUES ), ( 'BN', - 'connected', + 'strongly connected', 'trivial' ), ( @@ -1208,7 +1278,7 @@ VALUES ( 'BOn', - 'connected', + 'strongly connected', 'trivial' ), ( @@ -1338,6 +1408,11 @@ VALUES 'disjoint coproducts', 'This follows easily from the description of a coproduct of categories (based on disjoint unions).' ), + ( + 'Cat', + 'strongly connected', + 'Every nonempty category is weakly terminal.' + ), ( 'Fld', 'locally small', diff --git a/database/data/008_category-non-properties.sql b/database/data/008_category-non-properties.sql index 25b22fbd..e8a5e0e7 100644 --- a/database/data/008_category-non-properties.sql +++ b/database/data/008_category-non-properties.sql @@ -275,6 +275,11 @@ VALUES 'Malcev', NULL ), + ( + 'Pos', + 'locally cartesian closed', + 'See ยง2 of Niefield 2001.' + ), ( 'M-Set', 'strict terminal object', @@ -1090,6 +1095,11 @@ VALUES 'Malcev', NULL ), + ( + 'Cat', + 'locally cartesian closed', + 'See Theorem 4.4 of Giraud 1964.' + ), ( 'Fld', 'connected', diff --git a/database/data/013_implications.sql b/database/data/013_implications.sql index d376cac3..4f3e501f 100644 --- a/database/data/013_implications.sql +++ b/database/data/013_implications.sql @@ -278,10 +278,10 @@ VALUES FALSE ), ( - 'connected_criterion', + 'zero_morphisms_mean_strongly_connected', '["zero morphisms", "inhabited"]', - '["connected"]', - 'This is trivial.', + '["strongly connected"]', + 'This holds by definition.', FALSE ), ( @@ -403,6 +403,13 @@ VALUES 'This is easy.', FALSE ), + ( + 'groupoid_connected', + '["groupoid", "connected"]', + '["strongly connected"]', + 'trivial', + FALSE + ), ( 'connected_consequence', '["connected"]', @@ -410,6 +417,13 @@ VALUES 'This holds by definition.', FALSE ), + ( + 'strongly_connected_consequence', + '["strongly connected"]', + '["connected"]', + 'This holds by definition.', + FALSE + ), ( 'generator_consequence', '["generator"]', @@ -622,6 +636,34 @@ VALUES 'See Prop. 2.2.13. in Malcev, protomodular, homological and semi-abelian categories.', FALSE ), + ( + 'pullbacks_are_local_products', + '["locally cartesian closed"]', + '["pullbacks"]', + 'Pullbacks are binary products in slice categories.', + FALSE + ), + ( + 'locally_cartesian_closed_with_terminal_is_closed', + '["locally cartesian closed", "terminal object"]', + '["cartesian closed"]', + 'The slice over the terminal object is the category itself.', + FALSE + ), + ( + 'discrete_is_locally_cartesian_closed', + '["discrete"]', + '["locally cartesian closed"]', + 'Each slice of a discrete category is terminal.', + FALSE + ), + ( + 'sequential_implies_lcc', + '["thin", "strongly connected"]', + '["locally cartesian closed"]', + 'Each slice is thin, strongly connected, and has a terminal object. Every such category is cartesian closed, where the exponential $a \Rightarrow b$ (Heyting implication) is $1$ when $a \leq b$ and otherwise $b$.', + FALSE + ), -- non-trivial implications ( @@ -693,5 +735,12 @@ VALUES '["trivial"]', 'This follows since the dual of a non-trivial Grothendieck abelian category cannot be Grothendieck abelian. See Peter Freyd, Abelian categories, p. 116.', FALSE + ), + ( + 'topos_is_locally_cartesian_closed', + '["elementary topos"]', + '["locally cartesian closed"]', + 'See Johnstone, Cor. A2.3.4.', + FALSE ); diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index 11037ce8..ab1b5063 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -46,6 +46,7 @@ "pushouts", "sequential colimits", "sequential limits", + "strongly connected", "terminal object", "well-copowered", "well-powered", @@ -66,6 +67,7 @@ "groupoid", "infinitary distributive", "left cancellative", + "locally cartesian closed", "right cancellative", "self-dual", "skeletal", diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index 1630077e..74c71fd8 100644 --- a/scripts/expected-data/Set.json +++ b/scripts/expected-data/Set.json @@ -34,6 +34,7 @@ "infinitary distributive", "inhabited", "initial object", + "locally cartesian closed", "locally essentially small", "locally finitely presentable", "locally presentable", @@ -46,6 +47,7 @@ "sequential colimits", "sequential limits", "strict initial object", + "strongly connected", "subobject classifier", "terminal object", "well-copowered", diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index e7b16f88..467d7b64 100644 --- a/scripts/expected-data/Top.json +++ b/scripts/expected-data/Top.json @@ -35,6 +35,7 @@ "sequential colimits", "sequential limits", "strict initial object", + "strongly connected", "terminal object", "well-copowered", "well-powered", @@ -46,6 +47,7 @@ "additive", "balanced", "cartesian closed", + "locally cartesian closed", "discrete", "elementary topos", "epi-regular",