Skip to content

Commit 17ecbcc

Browse files
varkorvarkor
committed
Add "walking_composable_pair", "locally cartesian closed" and "strongly connected"
1 parent 11794e6 commit 17ecbcc

11 files changed

Lines changed: 171 additions & 11 deletions

‎database/data/001_categories.sql‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -274,6 +274,14 @@ VALUES
274274
'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.',
275275
'https://ncatlab.org/nlab/show/walking+isomorphism'
276276
),
277+
(
278+
'walking_composable_pair',
279+
'walking composable pair',
280+
'$\{ 0 \to 1 \to 2 \}$',
281+
'a single morphism from each natural number to one greater than or equal to it',
282+
'The name of this category comes from the fact that a functor out of it is the same as a composable pair of morphisms.',
283+
'https://ncatlab.org/nlab/show/composable+pair'
284+
),
277285

278286
-- examples of thin categories
279287
(

‎database/data/002_tags.sql‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -158,6 +158,9 @@ VALUES
158158
('walking_isomorphism', 'artificial'),
159159
('walking_isomorphism', 'category theory'),
160160
('walking_isomorphism', 'badly-behaved'),
161+
('walking_composable_pair', 'artificial'),
162+
('walking_composable_pair', 'category theory'),
163+
('walking_composable_pair', 'badly-behaved'),
161164
('Setne', 'artificial'),
162165
('Setne', 'set theory'),
163166
('Setne', 'well-behaved'),

‎database/data/003_related-categories.sql‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,7 @@ VALUES
7676
('walking_pair', 'walking_morphism'),
7777
('walking_isomorphism', 'walking_morphism'),
7878
('walking_isomorphism', '1'),
79+
('walking_composable_pair', 'walking_morphism'),
7980
('Setne', 'Set'),
8081
('B', 'FI'),
8182
('B', 'FS'),

‎database/data/005_properties.sql‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,14 @@ VALUES
3232
NULL,
3333
TRUE
3434
),
35+
(
36+
'locally cartesian closed',
37+
'is',
38+
'A category is <i>locally cartesian closed</i> if each of its slice categories is cartesian closed.',
39+
'https://ncatlab.org/nlab/show/locally+cartesian+closed+category',
40+
NULL,
41+
TRUE
42+
),
3543
(
3644
'pullbacks',
3745
'has',
@@ -541,6 +549,14 @@ VALUES
541549
'connected',
542550
TRUE
543551
),
552+
(
553+
'strongly connected',
554+
'is',
555+
'A category is <i>strongly connected</i> if it is inhabited and every two objects can be joined via a morphism.',
556+
NULL,
557+
'strongly connected',
558+
TRUE
559+
),
544560
(
545561
'balanced',
546562
'is',

‎database/data/006_related_properties.sql‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ VALUES
44
('locally small', 'locally essentially small'),
55
('locally essentially small', 'locally small'),
66
('cartesian closed', 'finite products'),
7+
('locally cartesian closed', 'cartesian closed'),
78
('zero morphisms', 'preadditive'),
89
('zero morphisms', 'pointed'),
910
('preadditive', 'additive'),

‎database/data/007_category-properties.sql‎

Lines changed: 77 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,11 @@ VALUES
1515
'Grothendieck topos',
1616
'It is equivalent to the category of sheaves on a one-point space.'
1717
),
18+
(
19+
'Set',
20+
'strongly connected',
21+
'Every nonempty set is weakly terminal.'
22+
),
1823
(
1924
'Set',
2025
'finitary algebraic',
@@ -335,6 +340,11 @@ VALUES
335340
'disjoint coproducts',
336341
'This follows easily from the corresponding fact for sets, since the coproduct of posets is built using the disjoint union.'
337342
),
343+
(
344+
'Pos',
345+
'strongly connected',
346+
'Every nonempty preorder is weakly terminal.'
347+
),
338348
(
339349
'M-Set',
340350
'locally small',
@@ -423,6 +433,11 @@ VALUES
423433
'generator',
424434
'The one-point set is a generator since it represents the forgetful functor $\mathbf{FinSet} \to \mathbf{Set}$.'
425435
),
436+
(
437+
'FinSet',
438+
'strongly connected',
439+
'Every nonempty finite set is weakly terminal.'
440+
),
426441
(
427442
'FinSet',
428443
'cogenerator',
@@ -591,6 +606,11 @@ VALUES
591606
'finite',
592607
'trivial'
593608
),
609+
(
610+
'0',
611+
'locally cartesian closed',
612+
'This is vacuously true.'
613+
),
594614
(
595615
'1',
596616
'trivial',
@@ -646,6 +666,11 @@ VALUES
646666
'skeletal',
647667
'The two objects are not isomorphic'
648668
),
669+
(
670+
'walking_morphism',
671+
'strongly connected',
672+
'trivial'
673+
),
649674

650675
(
651676
'walking_pair',
@@ -659,7 +684,7 @@ VALUES
659684
),
660685
(
661686
'walking_pair',
662-
'connected',
687+
'strongly connected',
663688
'trivial'
664689
),
665690
(
@@ -692,6 +717,31 @@ VALUES
692717
'finite',
693718
'trivial'
694719
),
720+
(
721+
'walking_composable_pair',
722+
'finite',
723+
'trivial'
724+
),
725+
(
726+
'walking_composable_pair',
727+
'strongly connected',
728+
'trivial'
729+
),
730+
(
731+
'walking_composable_pair',
732+
'skeletal',
733+
'trivial'
734+
),
735+
(
736+
'walking_composable_pair',
737+
'products',
738+
'trivial'
739+
),
740+
(
741+
'walking_composable_pair',
742+
'coproducts',
743+
'trivial'
744+
),
695745

696746
-- geometric categories
697747
(
@@ -1013,6 +1063,11 @@ VALUES
10131063
'skeletal',
10141064
'The relation $\leq$ is antisymmetric.'
10151065
),
1066+
(
1067+
'N',
1068+
'strongly connected',
1069+
'trivial'
1070+
),
10161071
(
10171072
'On',
10181073
'thin',
@@ -1048,6 +1103,11 @@ VALUES
10481103
'skeletal',
10491104
'The relation $\leq$ is antisymmetric'
10501105
),
1106+
(
1107+
'On',
1108+
'strongly connected',
1109+
'trivial'
1110+
),
10511111
(
10521112
'real_interval',
10531113
'small',
@@ -1060,8 +1120,8 @@ VALUES
10601120
),
10611121
(
10621122
'real_interval',
1063-
'cartesian closed',
1064-
'The exponential $a \Rightarrow b$ (Heyting implication) is $1$ when $a \leq b$ and otherwise $b$.'
1123+
'strongly connected',
1124+
'trivial'
10651125
),
10661126
(
10671127
'real_interval',
@@ -1118,6 +1178,11 @@ VALUES
11181178
'locally finitely presentable',
11191179
'Every natural number is finitely presentable, and $\infty$ is the colimit of all $n < \infty$.'
11201180
),
1181+
(
1182+
'Noo',
1183+
'strongly connected',
1184+
'trivial'
1185+
),
11211186

11221187
-- deloopings
11231188
(
@@ -1132,7 +1197,7 @@ VALUES
11321197
),
11331198
(
11341199
'BG',
1135-
'connected',
1200+
'strongly connected',
11361201
'trivial'
11371202
),
11381203
(
@@ -1157,7 +1222,7 @@ VALUES
11571222
),
11581223
(
11591224
'BGf',
1160-
'connected',
1225+
'strongly connected',
11611226
'trivial'
11621227
),
11631228
(
@@ -1177,7 +1242,7 @@ VALUES
11771242
),
11781243
(
11791244
'BN',
1180-
'connected',
1245+
'strongly connected',
11811246
'trivial'
11821247
),
11831248
(
@@ -1208,7 +1273,7 @@ VALUES
12081273

12091274
(
12101275
'BOn',
1211-
'connected',
1276+
'strongly connected',
12121277
'trivial'
12131278
),
12141279
(
@@ -1338,6 +1403,11 @@ VALUES
13381403
'disjoint coproducts',
13391404
'This follows easily from the description of a coproduct of categories (based on disjoint unions).'
13401405
),
1406+
(
1407+
'Cat',
1408+
'strongly connected',
1409+
'Every nonempty category is weakly terminal.'
1410+
),
13411411
(
13421412
'Fld',
13431413
'locally small',

‎database/data/008_category-non-properties.sql‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -275,6 +275,11 @@ VALUES
275275
'Malcev',
276276
NULL
277277
),
278+
(
279+
'Pos',
280+
'locally cartesian closed',
281+
'See §2 of <a href="http://www.tac.mta.ca/tac/volumes/8/n2/8-02abs.html" target="_blank">Niefield 2001</a>.'
282+
),
278283
(
279284
'M-Set',
280285
'strict terminal object',
@@ -1090,6 +1095,11 @@ VALUES
10901095
'Malcev',
10911096
NULL
10921097
),
1098+
(
1099+
'Cat',
1100+
'locally cartesian closed',
1101+
'See Theorem 4.4 of <a href="https://www.numdam.org/item/MSMF_1964__2__R3_0/" target="_blank">Giraud 1964</a>.'
1102+
),
10931103
(
10941104
'Fld',
10951105
'connected',

‎database/data/013_implications.sql‎

Lines changed: 52 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -278,10 +278,10 @@ VALUES
278278
FALSE
279279
),
280280
(
281-
'connected_criterion',
282-
'["zero morphisms", "inhabited"]',
283-
'["connected"]',
284-
'This is trivial.',
281+
'zero_morphisms_mean_strongly_connected',
282+
'["zero morphisms"]',
283+
'["strongly connected"]',
284+
'This holds by definition.',
285285
FALSE
286286
),
287287
(
@@ -403,13 +403,27 @@ VALUES
403403
'This is easy.',
404404
FALSE
405405
),
406+
(
407+
'groupoid_connected',
408+
'["groupoid", "connected"]',
409+
'["strongly connected"]',
410+
'trivial',
411+
FALSE
412+
),
406413
(
407414
'connected_consequence',
408415
'["connected"]',
409416
'["inhabited"]',
410417
'This holds by definition.',
411418
FALSE
412419
),
420+
(
421+
'strongly_connected_consequence',
422+
'["strongly connected"]',
423+
'["connected"]',
424+
'This holds by definition.',
425+
FALSE
426+
),
413427
(
414428
'generator_consequence',
415429
'["generator"]',
@@ -622,6 +636,33 @@ VALUES
622636
'See Prop. 2.2.13. in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>.',
623637
FALSE
624638
),
639+
(
640+
'pullbacks_are_local_products',
641+
'["locally cartesian closed"]',
642+
'["pullbacks"]',
643+
'Pullbacks are binary products in slice categories.',
644+
FALSE
645+
),
646+
(
647+
'locally_cartesian_closed_with_terminal_is_closed',
648+
'["locally cartesian closed", "terminal object"]',
649+
'["cartesian closed"]',
650+
'The slice over the terminal object is the category itself.',
651+
FALSE
652+
),
653+
(
654+
'discrete_is_locally_cartesian_closed',
655+
'["discrete"]',
656+
'["locally cartesian closed"]',
657+
'Each slice of a discrete category is terminal.',
658+
FALSE
659+
),
660+
(
661+
'sequential_implies_lcc',
662+
'["thin", "strongly connected", "terminal object"]',
663+
'["locally cartesian closed"]',
664+
'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$.'
665+
)
625666

626667
-- non-trivial implications
627668
(
@@ -693,5 +734,12 @@ VALUES
693734
'["trivial"]',
694735
'This follows since the dual of a non-trivial Grothendieck abelian category cannot be Grothendieck abelian. See Peter Freyd, <i>Abelian categories</i>, p. 116.',
695736
FALSE
737+
),
738+
(
739+
'topos_is_locally_cartesian_closed',
740+
'["elementary topos"]',
741+
'["locally cartesian closed"]',
742+
'See <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Cor. A2.3.4.',
743+
FALSE
696744
);
697745

‎scripts/expected-data/Ab.json‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,7 @@
6666
"groupoid",
6767
"infinitary distributive",
6868
"left cancellative",
69+
"locally cartesian closed",
6970
"right cancellative",
7071
"self-dual",
7172
"skeletal",

‎scripts/expected-data/Set.json‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@
3434
"infinitary distributive",
3535
"inhabited",
3636
"initial object",
37+
"locally cartesian closed",
3738
"locally essentially small",
3839
"locally finitely presentable",
3940
"locally presentable",

0 commit comments

Comments
 (0)