From 46f67c02f64970b91d5b58b71e7cf057e10535cd Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Thu, 26 Mar 2026 16:36:26 +0000 Subject: [PATCH 01/13] Add property lsfp --- .../003_properties/008_locally-presentable.sql | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index c998892c..e4ebb367 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -30,4 +30,20 @@ VALUES 'https://ncatlab.org/nlab/show/locally+presentable+category', NULL, TRUE +), +( + 'locally strongly finitely presentable', + 'is a', + 'A category is a locally strongly finitely presentable 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: + + A category satisfying this property is simply called a variety (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 ); \ No newline at end of file From af3d453da19256ce41ae1f0ae6cbb6e9de92f911 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Thu, 26 Mar 2026 17:19:54 +0000 Subject: [PATCH 02/13] Enable target-blank --- database/data/003_properties/008_locally-presentable.sql | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index e4ebb367..2e902256 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -40,7 +40,7 @@ VALUES
  • It is equivalent to the category of models of a many-sorted finitary equational theory.
  • It is equivalent to the category of finite-product-preserving functors to $\mathbf{Set}$ from a small category with finite products (=Lawvere theory).
  • It is equivalent to the Eilenberg–Moore category of a finitary (=filtered-colimit-preserving) monad on $\mathbf{Set}^S$ for some set $S$.
    • -
  • It is equivalent to the Eilenberg–Moore category of a sifted-colimit-preserving monad on $\mathbf{Set}^S$ for some set $S$. (cf. [KR12, Proposition 3.3])
    • +
  • It is equivalent to the Eilenberg–Moore category of a sifted-colimit-preserving monad on $\mathbf{Set}^S$ for some set $S$. (cf. [KR12, Proposition 3.3])
    • A category satisfying this property is simply called a variety (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', From be5fada80919a3658f1708f2601dc13689acbf0c Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Thu, 26 Mar 2026 17:20:33 +0000 Subject: [PATCH 03/13] lsfp implies lfp --- .../007_locally-presentable-implications.sql | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index 2797caa3..02601f4d 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/database/data/005_implications/007_locally-presentable-implications.sql @@ -54,4 +54,11 @@ VALUES '["locally presentable"]', 'See Deriving Auslander''s formula, Cor. 5.2, or Sheafifiable homotopy model categories, Prop. 3.10.', FALSE +), +( + 'locally_strongly_finitely_presentable_raise', + '["locally strongly finitely presentable"]', + '["locally finitely presentable"]', + 'See Adamek-Rosicky, Cor. 3.7.', + FALSE ); \ No newline at end of file From 7b3a946d69925706a767b09fc8984711d87a331e Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Thu, 26 Mar 2026 17:21:51 +0000 Subject: [PATCH 04/13] Emphasize one-sort condition in finitary algebraic --- database/data/003_properties/006_additional-structure.sql | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/data/003_properties/006_additional-structure.sql b/database/data/003_properties/006_additional-structure.sql index d3be2cfb..d8d2d785 100644 --- a/database/data/003_properties/006_additional-structure.sql +++ b/database/data/003_properties/006_additional-structure.sql @@ -10,7 +10,7 @@ VALUES ( 'finitary algebraic', 'is', - 'A category is finitary algebraic 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 finitary algebraic if it is equivalent to the category of models of a one-sorted finitary equational theory. This is also known as a variety of one-sorted finitary algebras.', 'https://ncatlab.org/nlab/show/algebraic+category', NULL, TRUE From a71bad330aa2dbd9e463b5d065f04c6a213709fe Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Thu, 26 Mar 2026 17:23:42 +0000 Subject: [PATCH 05/13] finalg to lsfp to regular --- .../005_additional-structure-implications.sql | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/database/data/005_implications/005_additional-structure-implications.sql b/database/data/005_implications/005_additional-structure-implications.sql index 2c8673b1..a6df1476 100644 --- a/database/data/005_implications/005_additional-structure-implications.sql +++ b/database/data/005_implications/005_additional-structure-implications.sql @@ -9,8 +9,8 @@ VALUES ( 'finitary_algebraic_consequence', '["finitary algebraic"]', - '["locally finitely presentable"]', - 'See Adamek-Rosicky, 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 ), ( From ae74ebb7f67252b9ee3943460a8cdaa37d089c93 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Thu, 26 Mar 2026 17:32:13 +0000 Subject: [PATCH 06/13] Change equational into algebraic --- database/data/003_properties/006_additional-structure.sql | 2 +- database/data/003_properties/008_locally-presentable.sql | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/003_properties/006_additional-structure.sql b/database/data/003_properties/006_additional-structure.sql index d8d2d785..70c57761 100644 --- a/database/data/003_properties/006_additional-structure.sql +++ b/database/data/003_properties/006_additional-structure.sql @@ -10,7 +10,7 @@ VALUES ( 'finitary algebraic', 'is', - 'A category is finitary algebraic if it is equivalent to the category of models of a one-sorted finitary equational theory. This is also known as a variety of one-sorted finitary algebras.', + 'A category is finitary algebraic 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 diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index 2e902256..51019f9e 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -37,7 +37,7 @@ VALUES 'A category is a locally strongly finitely presentable 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:
      -
    • It is equivalent to the category of models of a many-sorted finitary equational theory.
      • +
    • It is equivalent to the category of models of a many-sorted finitary algebraic theory.
    • It is equivalent to the category of finite-product-preserving functors to $\mathbf{Set}$ from a small category with finite products (=Lawvere theory).
    • It is equivalent to the Eilenberg–Moore category of a finitary (=filtered-colimit-preserving) monad on $\mathbf{Set}^S$ for some set $S$.
    • It is equivalent to the Eilenberg–Moore category of a sifted-colimit-preserving monad on $\mathbf{Set}^S$ for some set $S$. (cf. [KR12, Proposition 3.3])
      • From 8f814ee37fd1beec609c9904be108dced5599c33 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Thu, 26 Mar 2026 17:56:42 +0000 Subject: [PATCH 07/13] sSet lsfp --- database/data/004_property-assignments/sSet.sql | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/004_property-assignments/sSet.sql b/database/data/004_property-assignments/sSet.sql index 13231fbd..1866aec0 100644 --- a/database/data/004_property-assignments/sSet.sql +++ b/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', From ae00d9cda6b6aa2d1e69b5a900d2ca929607775c Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Thu, 26 Mar 2026 17:57:05 +0000 Subject: [PATCH 08/13] Fix grammar --- database/data/003_properties/008_locally-presentable.sql | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index 51019f9e..a34e47c7 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -33,7 +33,7 @@ VALUES ), ( 'locally strongly finitely presentable', - 'is a', + 'is', 'A category is a locally strongly finitely presentable 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:
        From bd9f19ac16a3e6410c53e9275d5d0289b4fd3705 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Thu, 26 Mar 2026 18:13:34 +0000 Subject: [PATCH 09/13] locally presentable implies locally (ess) small --- database/data/003_properties/008_locally-presentable.sql | 4 ++-- .../005_implications/007_locally-presentable-implications.sql | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index a34e47c7..49696723 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -10,7 +10,7 @@ VALUES ( 'locally finitely presentable', 'is', - 'A category is locally finitely presentable 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.
        *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 locally finitely presentable 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 @@ -18,7 +18,7 @@ VALUES ( 'locally presentable', 'is', - 'Let $\kappa$ be a regular cardinal. A category is locally $\kappa$-presentable 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 locally presentable if it is locally $\kappa$-presentable for some regular cardinal $\kappa$.
        *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 locally $\kappa$-presentable 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 locally presentable if it is locally $\kappa$-presentable for some regular cardinal $\kappa$.', 'https://ncatlab.org/nlab/show/locally+presentable+category', NULL, TRUE diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index 02601f4d..ec583800 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/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 Adamek-Rosicky, Thm. 1.20, Cor. 1.28, Rem. 1.56, Thm. 1.58.', + 'For the local smallness, see the proof of Prop. 2.1.5 in Makkai-Pare. For the other non-trivial conclusions see Adamek-Rosicky, Thm. 1.20, Cor. 1.28, Rem. 1.56, Thm. 1.58.', FALSE ), ( From f542c727f8a435c5c3f1456eaa9f942e26c9a453 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 26 Mar 2026 21:24:05 +0100 Subject: [PATCH 10/13] fix tests --- scripts/expected-data/Ab.json | 1 + scripts/expected-data/Set.json | 1 + scripts/expected-data/Top.json | 3 ++- 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index 4baeef54..090753e1 100644 --- a/scripts/expected-data/Ab.json +++ b/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, diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index 8ec7b3de..13129f63 100644 --- a/scripts/expected-data/Set.json +++ b/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, diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index e0668065..5c406157 100644 --- a/scripts/expected-data/Top.json +++ b/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 } From 92e8146d4babe1d1ed42af59ec4bb6672d6e8282 Mon Sep 17 00:00:00 2001 From: ykawase5048 <114643337+ykawase5048@users.noreply.github.com> Date: Fri, 27 Mar 2026 10:16:59 +0900 Subject: [PATCH 11/13] Apply suggestion from @ScriptRaccoon Co-authored-by: Script Raccoon --- .../005_implications/007_locally-presentable-implications.sql | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index ec583800..99f44e53 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/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 local smallness, see the proof of Prop. 2.1.5 in Makkai-Pare. For the other non-trivial conclusions see Adamek-Rosicky, 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 Makkai-Pare. For the other non-trivial conclusions see Adamek-Rosicky, Thm. 1.20, Cor. 1.28, Rem. 1.56, Thm. 1.58.', FALSE ), ( From 9dea17a01ab61ba55c8efb37265d103bb88b1314 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 27 Mar 2026 09:55:06 +0100 Subject: [PATCH 12/13] Fill some missing information --- database/data/004_property-assignments/N_oo.sql | 4 ++-- .../data/004_property-assignments/Set_op.sql | 4 ++-- .../walking_composable_pair.sql | 16 +++++++++------- 3 files changed, 13 insertions(+), 11 deletions(-) diff --git a/database/data/004_property-assignments/N_oo.sql b/database/data/004_property-assignments/N_oo.sql index 22dc1487..fef35213 100644 --- a/database/data/004_property-assignments/N_oo.sql +++ b/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', diff --git a/database/data/004_property-assignments/Set_op.sql b/database/data/004_property-assignments/Set_op.sql index 791817ad..0e6c6982 100644 --- a/database/data/004_property-assignments/Set_op.sql +++ b/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 Makkai-Pare, Thm. 3.4.3.' ); diff --git a/database/data/004_property-assignments/walking_composable_pair.sql b/database/data/004_property-assignments/walking_composable_pair.sql index fb3e1238..94c34fdd 100644 --- a/database/data/004_property-assignments/walking_composable_pair.sql +++ b/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 interval category $\{0 \to 1\}$ (which is 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\}$.' +) +; From 83184d7577d7861b8b95f60822fc91560c6cf230 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 27 Mar 2026 09:59:26 +0100 Subject: [PATCH 13/13] add related properties to lsfp --- database/data/003_properties/100_related_properties.sql | 2 ++ 1 file changed, 2 insertions(+) diff --git a/database/data/003_properties/100_related_properties.sql b/database/data/003_properties/100_related_properties.sql index ed5534b4..586996c1 100644 --- a/database/data/003_properties/100_related_properties.sql +++ b/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'),