Add "locally strongly finitely presentable" as a property

database/data/003_properties/006_additional-structure.sql

@@ -10,7 +10,7 @@ VALUES
 (
 	'finitary algebraic',
 	'is',
-	'A category is <i>finitary algebraic</i> if it is equivalent to the category of models of a finitary algebraic theory. This is also known as a variety of finitary algebras.',
+	'A category is <i>finitary algebraic</i> if it is equivalent to the category of models of a one-sorted finitary algebraic theory. This is also known as a variety of one-sorted finitary algebras.',
 	'https://ncatlab.org/nlab/show/algebraic+category',
 	NULL,
 	TRUE

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

@@ -10,15 +10,15 @@ VALUES
 (
 	'locally finitely presentable',
 	'is',
-	'A category is <i>locally finitely presentable</i> if it is locally essentially small*, 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.<br>*Many authors assume the category to be locally small, but this is inconvenient since then locally finitely presentable categories would not be invariant under equivalences of categories.',
+	'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.',
 	'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 locally essentially small*, 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$.<br>*Many authors assume the category to be locally small, but this is inconvenient since then locally presentable categories would not be invariant under equivalences of categories.',
+	'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$.',
 	'https://ncatlab.org/nlab/show/locally+presentable+category',
 	NULL,
 	TRUE
@@ -30,4 +30,20 @@ VALUES
 	'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$.
+	There are several equivalent conditions:
+	<ul style="list-style-type: circle;">
+		<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 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>
+	</ul>
+	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
 );

database/data/003_properties/100_related_properties.sql

@@ -30,7 +30,9 @@ VALUES
 ('pointed', 'terminal object'),
 ('locally finitely presentable', 'cocomplete'),
 ('locally finitely presentable', 'locally presentable'),
+('locally finitely presentable', 'locally strongly finitely presentable'),
 ('locally finitely presentable', 'locally ℵ₁-presentable'),
+('locally strongly finitely presentable', 'locally finitely presentable'),
 ('locally presentable', 'cocomplete'),
 ('locally presentable', 'locally finitely presentable'),
 ('locally presentable', 'locally ℵ₁-presentable'),

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

@@ -31,9 +31,9 @@ VALUES
 ),
 (
 	'N_oo',
-	'locally finitely presentable',
+	'locally strongly finitely presentable',
 	TRUE,
-	'Every natural number is finitely presentable, and $\infty$ is the colimit of all $n < \infty$.'
+	'Every natural number is strongly finitely presentable, and $\infty$ is the colimit of all $n < \infty$.'
 ),
 (
 	'N_oo',

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

@@ -7,7 +7,7 @@ INSERT INTO category_property_assignments (
 VALUES
 (
 	'Set_op',
-	'finitary algebraic',
+	'locally presentable',
 	FALSE,
-	NULL
+	'This follows from the fact that the opposite category of a complete accessible large category is never accessible. See <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>, Thm. 3.4.3.'
 );

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

@@ -19,9 +19,9 @@ VALUES
 ),
 (
 	'sSet',
-	'locally finitely presentable',
+	'locally strongly finitely presentable',
 	TRUE,
-	'This follows from the fact that the free cocompletion of a small category is locally finitely presentable.'
+	'This follows from the fact that every category of presheaves over a small category is locally strongly finitely presentable.'
 ),
 (
 	'sSet',

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

@@ -23,12 +23,6 @@ VALUES
 	TRUE,
 	'trivial'
 ),
-(
-	'walking_composable_pair',
-	'locally finitely presentable',
-	TRUE,
-	'We get coproducts by taking the supremum inside $\{0 < 1 < 2\}$. The objects $0,1,2$ are finitely presentable for trivial reasons.'
-),
 (
 	'walking_composable_pair',
 	'self-dual',
@@ -40,4 +34,12 @@ VALUES
 	'finitary algebraic',
 	FALSE,
 	'More generally, let $\mathcal{C}$ be a thin finitary algebraic category. Let $F : \mathbf{Set} \to \mathcal{C}$ denote the free algebra functor. Every object $A \in \mathcal{C}$ admits a regular epimorphism $F(X) \to A$ for some set $X$. But since $\mathcal{C}$ is left cancellative, every regular epimorphism must be an isomorphism. Also, $F(X)$ is a coproduct of copies of $F(1)$, which means it is either the initial object $0$ or $F(1)$ itself (since $\mathcal{C}$ is thin). This shows that $\mathcal{C}$ must have at most $2$ objects up to isomorphism. In fact, either $\mathcal{C}$ is trivial or equivalent to the <a href="/category/walking_morphism">interval category</a> $\{0 \to 1\}$ (which <i>is</i> finitary algebraic).'
-);
+),
+(
+	'walking_composable_pair',
+	'locally strongly finitely presentable',
+	TRUE,
+	'Take the two-sorted (finitary) algebraic theory with exactly one unary operation between them and the equation $x=y$ for each sort. There are exactly three algebras for this theory up to isomorphism: the identities on the empty set and the singleton, the morphism from the empty set to the singleton.
+	Hence we get the equivalence to $\{0 \to  1 \to 2\}$.'
+)
+;

database/data/005_implications/005_additional-structure-implications.sql

@@ -9,8 +9,8 @@ VALUES
 (
 	'finitary_algebraic_consequence',
 	'["finitary algebraic"]',
-	'["locally finitely presentable"]',
-	'See <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Cor. 3.7.',
+	'["locally strongly finitely presentable"]',
+	'This is trivial because a locally strongly finitely presentable category is a variety of many-sorted finitary algebras.',
 	FALSE
 ),
 (
@@ -91,10 +91,10 @@ VALUES
 	FALSE
 ),
 (
-	'algebraic_implies_regular',
-	'["finitary algebraic"]',
+	'many_sorted_algebraic_implies_regular',
+	'["locally strongly finitely presentable"]',
 	'["regular"]',
-	'The regular epimorphisms are precisely the surjective algebra homomorphisms, which are clearly stable under pullbacks.',
+	'The regular epimorphisms are precisely the sort-wise surjective homomorphisms, which are clearly stable under pullbacks.',
 	FALSE
 ),
 (

database/data/005_implications/007_locally-presentable-implications.sql

@@ -31,7 +31,7 @@ VALUES
 	'locally_presentable_consequence',
 	'["locally presentable"]',
 	'["locally essentially small", "well-powered", "well-copowered", "complete", "cocomplete", "generator"]',
-	'For the non-trivial conclusions see <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Thm. 1.20, Cor. 1.28, Rem. 1.56, Thm. 1.58.',
+	'For locally essential smallness, see the proof of Prop. 2.1.5 in <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>. For the other non-trivial conclusions see <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Thm. 1.20, Cor. 1.28, Rem. 1.56, Thm. 1.58.',
 	FALSE
 ),
 (
@@ -54,4 +54,11 @@ VALUES
 	'["locally presentable"]',
 	'See <a href="https://arxiv.org/abs/1409.7051" target="_blank">Deriving Auslander''s formula</a>, Cor. 5.2, or <a href="https://arxiv.org/abs/math/0102087" target="_blank">Sheafifiable homotopy model categories</a>, Prop. 3.10.',
 	FALSE
+),
+(
+	'locally_strongly_finitely_presentable_raise',
+	'["locally strongly finitely presentable"]',
+	'["locally finitely presentable"]',
+	'See <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Cor. 3.7.',
+	FALSE
 );

scripts/expected-data/Ab.json

@@ -59,6 +59,7 @@
 	"coregular": true,
 	"disjoint finite products": true,
 	"disjoint products": true,
+	"locally strongly finitely presentable": true,
 	"co-Malcev": true,
 	"unital": true,
 	"counital": true,

scripts/expected-data/Set.json

@@ -61,6 +61,7 @@
 	"infinitary extensive": true,
 	"co-Malcev": true,
 	"lextensive": true,
+	"locally strongly finitely presentable": true,
 
 	"Grothendieck abelian": false,
 	"Malcev": false,

scripts/expected-data/Top.json

@@ -92,5 +92,6 @@
 	"infinitary coextensive": false,
 	"co-Malcev": false,
 	"unital": false,
-	"counital": false
+	"counital": false,
+	"locally strongly finitely presentable": false
 }