diff --git a/database/data/003_properties/006_additional-structure.sql b/database/data/003_properties/006_additional-structure.sql index d3be2cfb..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 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 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 c998892c..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 @@ -30,4 +30,20 @@ VALUES 'https://ncatlab.org/nlab/show/locally+presentable+category', NULL, TRUE +), +( + 'locally strongly finitely presentable', + '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: + + 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 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'), 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/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', 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\}$.' +) +; 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 ), ( diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index 2797caa3..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 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 ), ( @@ -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 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 }