Skip to content

Add "locally cartesian closed" property #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
varkor wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Add "locally cartesian closed" property #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
17ecbcc
Add "walking_composable_pair", "locally cartesian closed" and "strong…
varkor Mar 18, 2026
feeebc0
fix data
ScriptRaccoon Mar 19, 2026
f8df03d
remove redundant assumption
ScriptRaccoon Mar 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions database/data/001_categories.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
(
Expand Down
3 changes: 3 additions & 0 deletions database/data/002_tags.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'),
Expand Down
1 change: 1 addition & 0 deletions database/data/003_related-categories.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'),
Expand Down
16 changes: 16 additions & 0 deletions database/data/005_properties.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,14 @@ VALUES
NULL,
TRUE
),
(
'locally cartesian closed',
'is',
'A category is <i>locally cartesian closed</i> if each of its slice categories is cartesian closed.',
'https://ncatlab.org/nlab/show/locally+cartesian+closed+category',
NULL,
TRUE
),
(
'pullbacks',
'has',
Expand Down Expand Up @@ -541,6 +549,14 @@ VALUES
'connected',
TRUE
),
(
'strongly connected',
'is',
'A category is <i>strongly connected</i> if it is inhabited and every two objects can be joined via a morphism.',
NULL,
'strongly connected',
TRUE
),
(
'balanced',
'is',
Expand Down
1 change: 1 addition & 0 deletions database/data/006_related_properties.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'),
Expand Down
89 changes: 82 additions & 7 deletions database/data/007_category-properties.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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',
Expand Down Expand Up @@ -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',
Expand Down Expand Up @@ -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',
Expand Down Expand Up @@ -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',
Expand Down Expand Up @@ -591,6 +611,11 @@ VALUES
'finite',
'trivial'
),
(
'0',
'locally cartesian closed',
'This is vacuously true.'
),
(
'1',
'trivial',
Expand Down Expand Up @@ -646,6 +671,11 @@ VALUES
'skeletal',
'The two objects are not isomorphic'
),
(
'walking_morphism',
'strongly connected',
'trivial'
),

(
'walking_pair',
Expand All @@ -659,7 +689,7 @@ VALUES
),
(
'walking_pair',
'connected',
'strongly connected',
'trivial'
),
(
Expand Down Expand Up @@ -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
(
Expand Down Expand Up @@ -1013,6 +1068,11 @@ VALUES
'skeletal',
'The relation $\leq$ is antisymmetric.'
),
(
'N',
'strongly connected',
'trivial'
),
(
'On',
'thin',
Expand Down Expand Up @@ -1048,6 +1108,11 @@ VALUES
'skeletal',
'The relation $\leq$ is antisymmetric'
),
(
'On',
'strongly connected',
'trivial'
),
(
'real_interval',
'small',
Expand All @@ -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',
Expand Down Expand Up @@ -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
(
Expand All @@ -1132,7 +1202,7 @@ VALUES
),
(
'BG',
'connected',
'strongly connected',
'trivial'
),
(
Expand All @@ -1157,7 +1227,7 @@ VALUES
),
(
'BGf',
'connected',
'strongly connected',
'trivial'
),
(
Expand All @@ -1177,7 +1247,7 @@ VALUES
),
(
'BN',
'connected',
'strongly connected',
'trivial'
),
(
Expand Down Expand Up @@ -1208,7 +1278,7 @@ VALUES

(
'BOn',
'connected',
'strongly connected',
'trivial'
),
(
Expand Down Expand Up @@ -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',
Expand Down
10 changes: 10 additions & 0 deletions database/data/008_category-non-properties.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -275,6 +275,11 @@ VALUES
'Malcev',
NULL
),
(
'Pos',
'locally cartesian closed',
'See §2 of <a href="http://www.tac.mta.ca/tac/volumes/8/n2/8-02abs.html" target="_blank">Niefield 2001</a>.'
),
(
'M-Set',
'strict terminal object',
Expand Down Expand Up @@ -1090,6 +1095,11 @@ VALUES
'Malcev',
NULL
),
(
'Cat',
'locally cartesian closed',
'See Theorem 4.4 of <a href="https://www.numdam.org/item/MSMF_1964__2__R3_0/" target="_blank">Giraud 1964</a>.'
),
(
'Fld',
'connected',
Expand Down
55 changes: 52 additions & 3 deletions database/data/013_implications.sql
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
),
(
Expand Down Expand Up @@ -403,13 +403,27 @@ VALUES
'This is easy.',
FALSE
),
(
'groupoid_connected',
'["groupoid", "connected"]',
'["strongly connected"]',
'trivial',
FALSE
),
(
'connected_consequence',
'["connected"]',
'["inhabited"]',
'This holds by definition.',
FALSE
),
(
'strongly_connected_consequence',
'["strongly connected"]',
'["connected"]',
'This holds by definition.',
FALSE
),
(
'generator_consequence',
'["generator"]',
Expand Down Expand Up @@ -622,6 +636,34 @@ VALUES
'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>.',
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
(
Expand Down Expand Up @@ -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, <i>Abelian categories</i>, p. 116.',
FALSE
),
(
'topos_is_locally_cartesian_closed',
'["elementary topos"]',
'["locally cartesian closed"]',
'See <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Cor. A2.3.4.',
FALSE
);

Loading