Add accessible categories and related properties

database/data/001_categories/008_one-object.sql

@@ -10,12 +10,12 @@ INSERT INTO categories (
 )
 VALUES
 (
-	'BG',
-	'delooping of an infinite group',
+	'BG_c',
+	'delooping of an infinite countable group',
 	'$BG$',
 	'a single object',
-	'the elements of an infinite group $G$',
-	'Every group $G$ yields a groupoid $BG$ with a single object $*$, morphisms given by the elements of $G$, and composition given by the group operation. In this example, we consider the case of an infinite group $G$.',
+	'the elements of an infinite countable group $G$',
+	'Every group $G$ yields a groupoid $BG$ with a single object $*$, morphisms given by the elements of $G$, and composition given by the group operation. In this example, we consider the case of an infinite countable group $G$ (such as $G = \mathbb{Z}$).',
 	'https://ncatlab.org/nlab/show/delooping',
 	NULL
 ),

database/data/001_categories/100_related-categories.sql

@@ -14,11 +14,11 @@ VALUES
 ('Ban','Met'),
 ('B', 'FI'),
 ('B', 'FS'),
-('BG', 'BG_f'),
-('BG', 'BN'),
-('BG_f', 'BG'),
+('BG_c', 'BG_f'),
+('BG_c', 'BN'),
+('BG_f', 'BG_c'),
 ('BG_f', 'BN'),
-('BN', 'BG'),
+('BN', 'BG_c'),
 ('BN', 'BOn'),
 ('BOn', 'BN'),
 ('CAlg(R)', 'Alg(R)'),

database/data/002_tags/002_category-tags.sql

@@ -13,9 +13,9 @@ VALUES
 ('B', 'combinatorics'),
 ('B', 'set theory'),
 ('Ban', 'analysis'),
-('BG', 'single object'),
-('BG', 'algebra'),
-('BG', 'category theory'),
+('BG_c', 'single object'),
+('BG_c', 'algebra'),
+('BG_c', 'category theory'),
 ('BG_f', 'single object'),
 ('BG_f', 'algebra'),
 ('BG_f', 'finite'),

database/data/003_properties/002_limits-colimits-existence.sql

@@ -342,4 +342,36 @@ VALUES
 	'https://ncatlab.org/nlab/show/sifted+colimit',
 	'cosifted limits',
 	TRUE
+),
+(
+	'multi-complete',
+	'is',
+	'A <i>multi-limit</i> of a diagram $D\colon \mathcal{S} \to \mathcal{C}$ is a set $I$ of cones over $D$ such that every cone over $D$ uniquely factors through a unique cone belonging to $I$. This property refers to the existence of multi-limits of small diagrams. Note that any diagram with no cone admits a multi-limit, which is the empty set of cones.',
+	'https://ncatlab.org/nlab/show/multilimit',
+	'multi-cocomplete',
+	TRUE
+),
+(
+	'multi-cocomplete',
+	'is',
+	'A <i>multi-colimit</i> of a diagram $D\colon \mathcal{S} \to \mathcal{C}$ is a set $I$ of cocones under $D$ such that every cocone under $D$ uniquely factors through a unique cocone belonging to $I$. This property refers to the existence of multi-colimits of small diagrams. Note that any diagram with no cocone admits a multi-colimit, which is the empty set of cocones.',
+	'https://ncatlab.org/nlab/show/multilimit',
+	'multi-complete',
+	TRUE
+),
+(
+	'multi-terminal object',
+	'has a',
+	'This property refers to the existence of a multi-limit of the empty diagram. A category has a multi-terminal object if and only if each connected component has a terminal object.',
+	'https://ncatlab.org/nlab/show/multilimit',
+	'multi-initial object',
+	TRUE
+),
+(
+	'multi-initial object',
+	'has a',
+	'This property refers to the existence of a multi-colimit of the empty diagram. A category has a multi-initial object if and only if each connected component has a initial object.',
+	'https://ncatlab.org/nlab/show/multilimit',
+	'multi-terminal object',
+	TRUE
 );

database/data/003_properties/004_size-constraints.sql

@@ -63,6 +63,22 @@ VALUES
 	'essentially finite',
 	TRUE
 ),
+(
+	'countable',
+	'is',
+	'A category is <i>countable</i> if it has countably many objects and morphisms.',
+	NULL,
+	'countable',
+	FALSE
+),
+(
+	'essentially countable',
+	'is',
+	'A category is <i>essentially countable</i> if it is equivalent to a countable category.',
+	NULL,
+	'essentially countable',
+	TRUE
+),
 (
 	'well-powered',
 	'is',

database/data/003_properties/008_locally-presentable.sql

@@ -10,40 +10,157 @@ VALUES
 (
 	'locally finitely presentable',
 	'is',
-	'A category is <i>locally finitely presentable</i> if it is cocomplete and there is a set $S$ of finitely presentable objects such that every object is a filtered colimit of objects in $S$. This is the same as being locally $\aleph_0$-presentable.',
+	'A category is <i>locally finitely presentable</i> if it satisfies one of the following equivalent conditions:
+	<ol>
+		<li>It is finitely accessible and cocomplete.</li>
+		<li>It is finitely accessible and complete.</li>
+		<li>It is equivalent to the category of finite-limit-preserving functors to $\mathbf{Set}$ from a small category with finite limits.</li>
+		<li>It is equivalent to the category of models of a small finite-limit sketch.</li>
+	</ol>
+	For equivalence of conditions above, see Cor. 2.47, Thm. 1.46, and Cor. 1.52 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>. This is the same as being locally $\aleph_0$-presentable.',
 	'https://ncatlab.org/nlab/show/locally+finitely+presentable+category',
 	NULL,
 	TRUE
 ),
 (
 	'locally presentable',
 	'is',
-	'Let $\kappa$ be a regular cardinal. A category is <i>locally $\kappa$-presentable</i> if it is cocomplete and there is a set of $\kappa$-presentable objects $S$ such that every object is a $\kappa$-filtered colimit of objects in $S$. A category is <i>locally presentable</i> if it is locally $\kappa$-presentable for some regular cardinal $\kappa$.',
+	'Let $\kappa$ be a regular cardinal. A category is <i>locally $\kappa$-presentable</i> if it satisfies one of the following equivalent conditions:
+	<ol>
+		<li>It is $\kappa$-accessible and cocomplete.</li>
+		<li>It is $\kappa$-accessible and complete.</li>
+		<li>It is equivalent to the category of $\kappa$-limit-preserving functors to $\mathbf{Set}$ from a small category with $\kappa$-limits.</li>
+		<li>It is equivalent to the category of models of a small $\kappa$-limit sketch.</li>
+	</ol>
+	For equivalence of conditions above, see Cor. 2.47, Thm. 1.46, and Cor. 1.52 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>.
+	A category is <i>locally presentable</i> if it is locally $\kappa$-presentable for some regular cardinal $\kappa$.',
 	'https://ncatlab.org/nlab/show/locally+presentable+category',
+	'locally copresentable',
+	TRUE
+),
+(
+	'locally copresentable',
+	'is',
+	'A category is <i>locally copresentable</i> if its opposite category is locally presentable.',
 	NULL,
+	'locally presentable',
 	TRUE
 ),
 (
 	'locally ℵ₁-presentable',
 	'is',
-	'This is the special case of the notion of a locally $\kappa$-presentable, where $\kappa = \aleph_1$ is the first uncountable cardinal.',
+	'This is the special case of the notion of locally $\kappa$-presentable categories, where $\kappa = \aleph_1$ is the first uncountable cardinal.',
 	'https://ncatlab.org/nlab/show/locally+presentable+category',
 	NULL,
 	TRUE
 ),
 (
 	'locally strongly finitely presentable',
 	'is',
-	'A category is a <i>locally strongly finitely presentable</i> if it is cocomplete and there is a set $G$ of strongly finitely presentable objects such that every object is a sifted colimit of objects from $G$.
+	'A category is <i>locally strongly finitely presentable</i> if it is cocomplete and there is a set $G$ of strongly finitely presentable objects such that every object is a sifted colimit of objects from $G$.
 	There are several equivalent conditions:
 	<ol>
 		<li>It is equivalent to the category of models of a many-sorted finitary algebraic theory.</li>
 		<li>It is equivalent to the category of finite-product-preserving functors to $\mathbf{Set}$ from a small category with finite products (=Lawvere theory).</li>
+		<li>It is equivalent to the category of models of a small finite-product sketch.</li>
 		<li>It is equivalent to the Eilenberg&ndash;Moore category of a finitary (=filtered-colimit-preserving) monad on $\mathbf{Set}^S$ for some set $S$.</li>
 		<li>It is equivalent to the Eilenberg&ndash;Moore category of a sifted-colimit-preserving monad on $\mathbf{Set}^S$ for some set $S$. (cf. [<a href="https://doi.org/10.2168/LMCS-8(3:14)2012" target="_blank">KR12</a>, Proposition 3.3])</li>
 	</ol>
 	A category satisfying this property is simply called a <i>variety</i> (of algebras) by some authors, although one should be aware that this term is sometimes used only for the one-sorted case.',
 	'https://ncatlab.org/nlab/show/locally+strongly+finitely+presentable+category',
 	NULL,
 	TRUE
+),
+(
+	'accessible',
+	'is',
+	'Let $\kappa$ be a regular cardinal. A category is <i>$\kappa$-accessible</i> if it has $\kappa$-filtered colimits and there is a (small) set $G$ of $\kappa$-presentable objects such that every object is a $\kappa$-filtered colimit of objects in $G$. A category is <i>accessible</i> if it is $\kappa$-accessible for some regular cardinal $\kappa$.',
+	'https://ncatlab.org/nlab/show/accessible+category',
+	'coaccessible',
+	TRUE
+),
+(
+	'coaccessible',
+	'is',
+	'A category is <i>coaccessible</i> if its opposite category is accessible.',
+	NULL,
+	'accessible',
+	TRUE
+),
+(
+	'finitely accessible',
+	'is',
+	'A category is <i>finitely accessible</i> if it has filtered colimits and there is a (small) set $G$ of finitely presentable objects such that every object is a filtered colimit of objects in $S$.',
+	'https://ncatlab.org/nlab/show/accessible+category',
+	NULL,
+	TRUE
+),
+(
+	'ℵ₁-accessible',
+	'is',
+	'This is the special case of the notion of $\kappa$-accessible categories, where $\kappa = \aleph_1$ is the first uncountable cardinal.',
+	'https://ncatlab.org/nlab/show/accessible+category',
+	NULL,
+	TRUE
+),
+(
+	'generalized variety',
+	'is a',
+	'A category is a <i>generalized variety</i> if it has sifted colimits and there is a (small) set $G$ of strongly finitely presentable objects such that every object is a sifted colimit of objects from $G$. Generalized varieties are like locally strongly finitely presentable categories but without colimits. The relation is similar as between finitely accessible and locally finitely presentable categories. This notion is defined in <a href="http://www.tac.mta.ca/tac/volumes/8/n3/8-03abs.html" target="_blank">[AR01, Def. 3.6]</a>.',
+	NULL,
+	NULL,
+	TRUE
+),
+(
+	'multi-algebraic',
+	'is',
+	'A category is <i>multi-algebraic</i> if it satisfies one of the following equivalent conditions:
+	<ol>
+		<li>It is a multi-cocomplete generalized variety, that is, it has multi-colimits and sifted colimits of all small diagrams, and there is a (small) set $G$ of strongly finitely presentable objects such that every object is a sifted colimit of objects from $G$.</li>
+		<li>It is equivalent to the category of models of a small (finite product, coproduct)-sketch, shortly small <i>FPC-sketch</i>.</li>
+		<li>It is equivalent to the category of multi-finite-product-preserving functors to $\mathbf{Set}$ from a small category with multi-finite-products (<i>multi-algebraic theory</i>). Here, multi-finite-products means multi-limits of finite discrete diagrams.</li>
+		<li>It is equivalent to the category of models of a small multi-finite-product sketch.</li>
+	</ol>
+	Multi-algebraic categories are like locally strongly finitely presentable categories but only with multi-colimits. The relation is similar as between locally finitely multi-presentable and locally finitely presentable categories.
+	For equivalence of conditions above, see [<a href="https://doi.org/10.1016/S0022-4049(01)00015-9" target="_blank">AR01a</a>, Lem. 1] and [<a href="http://www.tac.mta.ca/tac/volumes/8/n3/8-03abs.html" target="_blank">AR01b</a>, Thm. 4.4].
+	This notion was originally introduced by <a href="https://doi.org/10.1007/BF01224953" target="_blank">Diers</a>.',
+	NULL,
+	NULL,
+	TRUE
+),
+(
+	'locally multi-presentable',
+	'is',
+	'Let $\kappa$ be a regular cardinal. A category is <i>locally $\kappa$-multi-presentable</i> if it satisfies one of the following equivalent conditions:
+	<ol>
+		<li>It is $\kappa$-accessible and multi-cocomplete.</li>
+		<li>It is $\kappa$-accessible and has connected limits.</li>
+		<li>It is equivalent to the category of models of a small ($\kappa$-limit, coproduct)-sketch.</li>
+	</ol>
+	For equivalence of conditions above, see Thm. 4.30, Thm. 4.32, and the remark below in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>. A category is <i>locally multi-presentable</i> if it is locally $\kappa$-multi-presentable for some $\kappa$.',
+	'https://ncatlab.org/nlab/show/locally+multipresentable+category',
+	NULL,
+	TRUE
+),
+(
+	'locally finitely multi-presentable',
+	'is',
+	'A category is <i>locally finitely multi-presentable</i> if it satisfies one of the following equivalent conditions:
+	<ol>
+		<li>It is finitely accessible and multi-cocomplete.</li>
+		<li>It is finitely accessible and has connected limits.</li>
+		<li>It is equivalent to the category of models of a small (finite limit, coproduct)-sketch.</li>
+	</ol>
+	For equivalence of conditions above, see Thm. 4.30, Thm. 4.32, and the remark below in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>.',
+	'https://ncatlab.org/nlab/show/locally+multipresentable+category',
+	NULL,
+	TRUE
+),
+(
+	'locally poly-presentable',
+	'is',
+	'A category is <i>locally poly-presentable</i> if it is accessible and has wide pullbacks.',
+	'https://ncatlab.org/nlab/show/locally+polypresentable+category',
+	NULL,
+	TRUE
 );

database/data/003_properties/100_related-properties.sql

@@ -40,22 +40,33 @@ VALUES
 ('locally finitely presentable', 'locally presentable'),
 ('locally finitely presentable', 'locally strongly finitely presentable'),
 ('locally finitely presentable', 'locally ℵ₁-presentable'),
+('locally finitely presentable', 'finitely accessible'),
+('locally finitely presentable', 'locally finitely multi-presentable'),
 ('locally strongly finitely presentable', 'locally finitely presentable'),
+('locally strongly finitely presentable', 'multi-algebraic'),
+('locally strongly finitely presentable', 'generalized variety'),
 ('locally presentable', 'cocomplete'),
 ('locally presentable', 'locally finitely presentable'),
 ('locally presentable', 'locally ℵ₁-presentable'),
+('locally presentable', 'accessible'),
+('locally presentable', 'locally multi-presentable'),
+('locally presentable', 'locally poly-presentable'),
 ('locally ℵ₁-presentable', 'cocomplete'),
 ('locally ℵ₁-presentable', 'locally finitely presentable'),
 ('locally ℵ₁-presentable', 'locally presentable'),
+('locally ℵ₁-presentable', 'ℵ₁-accessible'),
 ('elementary topos', 'Grothendieck topos'),
 ('elementary topos', 'cartesian closed'),
 ('elementary topos', 'finitely complete'),
 ('elementary topos', 'subobject classifier'),
 ('Grothendieck topos', 'elementary topos'),
 ('initial object', 'finite coproducts'),
+('initial object', 'multi-initial object'),
 ('terminal object', 'finite products'),
+('terminal object', 'multi-terminal object'),
 ('complete', 'equalizers'),
 ('complete', 'products'),
+('complete', 'multi-complete'),
 ('equalizers', 'finitely complete'),
 ('equalizers', 'coreflexive equalizers'),
 ('equalizers', 'kernels'),
@@ -70,6 +81,7 @@ VALUES
 ('cokernels', 'conormal'),
 ('cocomplete', 'coequalizers'),
 ('cocomplete', 'coproducts'),
+('cocomplete', 'multi-cocomplete'),
 ('products', 'complete'),
 ('products', 'finite products'),
 ('products', 'powers'),
@@ -122,8 +134,14 @@ VALUES
 ('essentially discrete', 'discrete'),
 ('finite', 'essentially finite'),
 ('finite', 'small'),
+('finite', 'countable'),
 ('essentially finite', 'finite'),
 ('essentially finite', 'essentially small'),
+('essentially finite', 'essentially countable'),
+('countable', 'essentially countable'),
+('countable', 'finite'),
+('essentially countable', 'countable'),
+('essentially countable', 'essentially finite'),
 ('pullbacks', 'wide pullbacks'),
 ('pullbacks', 'binary products'),
 ('pushouts', 'wide pushouts'),
@@ -278,4 +296,49 @@ VALUES
 ('normal', 'kernels'),
 ('conormal', 'zero morphisms'),
 ('conormal', 'epi-regular'),
-('conormal', 'cokernels');
+('conormal', 'cokernels'),
+('multi-complete', 'complete'),
+('multi-complete', 'multi-terminal object'),
+('multi-terminal object', 'multi-complete'),
+('multi-terminal object', 'terminal object'),
+('multi-cocomplete', 'cocomplete'),
+('multi-cocomplete', 'multi-initial object'),
+('multi-initial object', 'multi-cocomplete'),
+('multi-initial object', 'initial object'),
+('accessible', 'finitely accessible'),
+('accessible', 'ℵ₁-accessible'),
+('accessible', 'locally presentable'),
+('accessible', 'locally multi-presentable'),
+('accessible', 'locally poly-presentable'),
+('ℵ₁-accessible', 'accessible'),
+('ℵ₁-accessible', 'finitely accessible'),
+('ℵ₁-accessible', 'locally ℵ₁-presentable'),
+('finitely accessible', 'accessible'),
+('finitely accessible', 'ℵ₁-accessible'),
+('finitely accessible', 'locally finitely presentable'),
+('finitely accessible', 'locally finitely multi-presentable'),
+('finitely accessible', 'filtered colimits'),
+('locally multi-presentable', 'locally finitely multi-presentable'),
+('locally multi-presentable', 'locally presentable'),
+('locally multi-presentable', 'locally poly-presentable'),
+('locally multi-presentable', 'accessible'),
+('locally multi-presentable', 'multi-cocomplete'),
+('locally multi-presentable', 'connected limits'),
+('locally finitely multi-presentable', 'locally multi-presentable'),
+('locally finitely multi-presentable', 'finitely accessible'),
+('locally finitely multi-presentable', 'filtered colimits'),
+('locally finitely multi-presentable', 'multi-cocomplete'),
+('locally finitely multi-presentable', 'connected limits'),
+('locally finitely multi-presentable', 'multi-algebraic'),
+('locally poly-presentable', 'locally presentable'),
+('locally poly-presentable', 'locally multi-presentable'),
+('locally poly-presentable', 'accessible'),
+('locally poly-presentable', 'wide pullbacks'),
+('multi-algebraic', 'locally finitely multi-presentable'),
+('multi-algebraic', 'locally strongly finitely presentable'),
+('multi-algebraic', 'generalized variety'),
+('multi-algebraic', 'sifted colimits'),
+('multi-algebraic', 'multi-cocomplete'),
+('generalized variety', 'multi-algebraic'),
+('generalized variety', 'locally strongly finitely presentable'),
+('generalized variety', 'sifted colimits');

database/data/004_property-assignments/0.sql

@@ -29,6 +29,18 @@ VALUES
 	TRUE,
 	'This is trivial.'
 ),
+(
+	'0',
+	'small',
+	TRUE,
+	'This is trivial.'
+),
+(
+	'0',
+	'multi-algebraic',
+	TRUE,
+	'The terminal category $\mathbf{1}$ becomes an FPC-sketch by selecting the unique empty cone and cocone. Then, a $\mathbf{Set}$-valued model of this sketch is a functor $\mathbf{1} \to \mathbf{Set}$ sending the unique object to a terminal and initial object, which never exists. Hence, $\mathbf{0}$ is the category of models of this FPC-sketch.'
+),
 (
 	'0',
 	'inhabited',