From 2f3c37d9a3aa4756c5b58e1ac93f5a136090dada Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Sat, 11 Apr 2026 18:35:38 +0900 Subject: [PATCH 01/29] Fix typos --- database/data/003_properties/008_locally-presentable.sql | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index 17e6ee20..1376f5d9 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -26,7 +26,7 @@ VALUES ( '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 @@ -34,7 +34,7 @@ VALUES ( '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$. + 'A category is 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:
  1. It is equivalent to the category of models of a many-sorted finitary algebraic theory.
    2. From 647f6b4457392a04d71a347257601c8f8da02e41 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Sat, 11 Apr 2026 20:23:02 +0900 Subject: [PATCH 02/29] Clarify the smallness of colimits --- database/data/003_properties/008_locally-presentable.sql | 6 +++--- 1 file 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 1376f5d9..62bacb1d 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 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 locally finitely presentable if it is cocomplete and there is a set $S$ of finitely presentable objects such that every object is a small 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 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$.', + '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 small $\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 @@ -34,7 +34,7 @@ VALUES ( 'locally strongly finitely presentable', 'is', - 'A category is 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$. + 'A category is 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 small sifted colimit of objects from $G$. There are several equivalent conditions:
    1. It is equivalent to the category of models of a many-sorted finitary algebraic theory.
      2. From 568ee6c74246e89b0c3c841c04c964bd80146ba7 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Sat, 11 Apr 2026 20:25:35 +0900 Subject: [PATCH 03/29] Refine the implication "finite_filtered_colimits" --- .../001_limits-colimits-existence-implications.sql | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index 15eaa5a3..5372c862 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -170,8 +170,8 @@ VALUES ( 'finite_filtered_colimits', '["finite", "Cauchy complete"]', - '["filtered colimits"]', - 'See MO/509853.', + '["finitely accessible"]', + 'See MO/509853, where it is in fact shown that the ind-completion of any finite Cauchy-complete category becomes itself.', FALSE ), ( From 31394035537ab7e8cfb7c025833f608065a6d42f Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Sat, 11 Apr 2026 20:25:03 +0900 Subject: [PATCH 04/29] Add several accessibilities --- .../008_locally-presentable.sql | 32 +++++++ .../007_locally-presentable-implications.sql | 93 +++++++++++++++++-- scripts/expected-data/Ab.json | 4 + scripts/expected-data/Set.json | 4 + scripts/expected-data/Top.json | 6 +- 5 files changed, 130 insertions(+), 9 deletions(-) diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index 62bacb1d..04509a0b 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -46,4 +46,36 @@ VALUES 'https://ncatlab.org/nlab/show/locally+strongly+finitely+presentable+category', NULL, TRUE +), +( + 'accessible', + 'is', + 'Let $\kappa$ be a regular cardinal. A category is $\kappa$-accessible if it has small $\kappa$-filtered colimits and there is a (small) set $G$ of $\kappa$-presentable objects such that every object is a small $\kappa$-filtered colimit of objects in $S$. A category is accessible if it is $\kappa$-accessible for some regular cardinal $\kappa$.', + 'https://ncatlab.org/nlab/show/accessible+category', + NULL, + TRUE +), +( + 'finitely accessible', + 'is', + 'A category is finitely accessible if it has small filtered colimits and there is a (small) set $G$ of finitely presentable objects such that every object is a small 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 generalized variety if it has small sifted colimits and there is a (small) set $G$ of strongly finitely presentable objects such that every object is a small sifted colimit of objects from $G$. This notion is defined in [AR01, Def. 3.6].', + NULL, + NULL, + TRUE ); \ No newline at end of file diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index 059756e1..ee0bc296 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/database/data/005_implications/007_locally-presentable-implications.sql @@ -6,13 +6,6 @@ INSERT INTO implication_input ( is_equivalence ) VALUES -( - 'locally_finitely_presentable_condition', - '["locally finitely presentable"]', - '["locally presentable"]', - 'Locally finitely presentable categories are by definition the locally $\aleph_0$-presentable categories.', - FALSE -), ( 'locally_finitely_presentable_raise', '["locally finitely presentable"]', @@ -30,7 +23,7 @@ VALUES ( 'locally_presentable_consequence', '["locally presentable"]', - '["locally essentially small", "well-powered", "well-copowered", "complete", "cocomplete", "generating set"]', + '["locally essentially small", "well-powered", "well-copowered", "complete", "generating set"]', '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 ), @@ -61,4 +54,88 @@ VALUES '["locally finitely presentable"]', 'See Adamek-Rosicky, Cor. 3.7.', FALSE +), +( + 'locally_presentable_definition_finite', + '["locally finitely presentable"]', + '["finitely accessible", "cocomplete"]', + 'This is trivial.', + TRUE +), +( + 'locally_presentable_definition_countable', + '["locally ℵ₁-presentable"]', + '["ℵ₁-accessible", "cocomplete"]', + 'This is trivial.', + TRUE +), +( + 'locally_presentable_definition', + '["locally presentable"]', + '["accessible", "cocomplete"]', + 'This is trivial.', + TRUE +), +( + 'finitely_accessible_raise', + '["finitely accessible"]', + '["ℵ₁-accessible"]', + 'This is because any regular cardinal is strictly smaller than its successor cardinal. See nLab.', + FALSE +), +( + 'countably_accessible_special_case', + '["ℵ₁-accessible"]', + '["accessible"]', + 'This is trivial.', + FALSE +), +( + 'accessible_require_filtered_colimit', + '["finitely accessible"]', + '["filtered colimits"]', + 'This is trivial.', + FALSE +), +( + 'accessible_require_Cauchy_complete', + '["accessible"]', + '["Cauchy complete"]', + 'This is because the walking idempotent is $\kappa$-filtered for any regular cardinal $\kappa$.', + FALSE +), +( + 'small_accessible_characterization', + '["small", "accessible"]', + '["small", "Cauchy complete"]', + 'See Makkai-Pare, Thm. 2.2.2.', + TRUE +), +( + 'locally_presentable_another_definition', + '["locally presentable"]', + '["accessible", "complete"]', + 'See Makkai-Pare, Thm. 6.1.4.', + TRUE +), +( + 'locally_strongly_finitely_presentable_definition', + '["locally strongly finitely presentable"]', + '["generalized variety", "cocomplete"]', + 'This is trivial.', + TRUE +), +( + 'generalized_variety_require_sifted_colimit', + '["generalized variety"]', + '["sifted colimits"]', + 'This is trivial.', + FALSE +), +( + 'generalized_variety_implies_accessible', + '["generalized variety"]', + '["ℵ₁-accessible"]', + 'See [AR01, Remark 4.8(2)].', + FALSE ); \ No newline at end of file diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index b387f2e5..930a1305 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -86,6 +86,10 @@ "cokernels": true, "normal": true, "conormal": true, + "accessible": true, + "finitely accessible": true, + "ℵ₁-accessible": true, + "generalized variety": true, "cartesian closed": false, "locally cartesian closed": false, diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index e714c158..81665405 100644 --- a/scripts/expected-data/Set.json +++ b/scripts/expected-data/Set.json @@ -81,6 +81,10 @@ "cofiltered": true, "sifted": true, "cosifted": true, + "accessible": true, + "finitely accessible": true, + "ℵ₁-accessible": true, + "generalized variety": true, "Grothendieck abelian": false, "Malcev": false, diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index 0458704a..c9a1cd45 100644 --- a/scripts/expected-data/Top.json +++ b/scripts/expected-data/Top.json @@ -124,5 +124,9 @@ "kernels": false, "cokernels": false, "normal": false, - "conormal": false + "conormal": false, + "accessible": false, + "finitely accessible": false, + "ℵ₁-accessible": false, + "generalized variety": false } From 3de1e5fc43c8d4fa4f89f90a6e1e50091fc9607d Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Sun, 12 Apr 2026 08:22:48 +0900 Subject: [PATCH 05/29] Add "locally multipresentable" and related notions --- .../002_limits-colimits-existence.sql | 32 +++++++++++ .../008_locally-presentable.sql | 32 +++++++++++ ...limits-colimits-existence-implications.sql | 21 +++++++ .../007_locally-presentable-implications.sql | 56 +++++++++++++++++++ 4 files changed, 141 insertions(+) diff --git a/database/data/003_properties/002_limits-colimits-existence.sql b/database/data/003_properties/002_limits-colimits-existence.sql index a13baac0..d929d248 100644 --- a/database/data/003_properties/002_limits-colimits-existence.sql +++ b/database/data/003_properties/002_limits-colimits-existence.sql @@ -342,4 +342,36 @@ VALUES 'https://ncatlab.org/nlab/show/sifted+colimit', 'cosifted limits', TRUE +), +( + 'multilimits', + 'has', + 'This property refers to the existence of multilimits of small diagrams. Note that any diagram with no cone admits a multilimit, which is the empty set of cones.', + 'https://ncatlab.org/nlab/show/multilimit', + 'multicolimits', + TRUE +), +( + 'multicolimits', + 'has', + 'This property refers to the existence of multicolimits of small diagrams. Note that any diagram with no cocone admits a multicolimit, which is the empty set of cocones.', + 'https://ncatlab.org/nlab/show/multilimit', + 'multilimits', + TRUE +), +( + 'multiterminal object', + 'has a', + 'This property refers to the existence of a multilimit of the empty diagram. A category has a multiterminal object if and only if each connected component has a terminal object.', + 'https://ncatlab.org/nlab/show/multilimit', + 'multiinitial object', + TRUE +), +( + 'multiinitial object', + 'has a', + 'This property refers to the existence of a multicolimit of the empty diagram. A category has a multiinitial object if and only if each connected component has a initial object.', + 'https://ncatlab.org/nlab/show/multilimit', + 'multiterminal object', + TRUE ); \ No newline at end of file diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index 04509a0b..90337e27 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -78,4 +78,36 @@ VALUES NULL, NULL, TRUE +), +( + 'multialgebraic', + 'is', + 'A category is multialgebraic if it is equivalent to the category of models of an FPC-sketch, where FPC represents finite products and small coproducts. This notion was introduced by Diers.', + NULL, + NULL, + TRUE +), +( + 'locally multipresentable', + 'is', + 'Let $\kappa$ be a regular cardinal. A category is locally $\kappa$-multipresentable if it is $\kappa$-accessible and has connected limits. It is known that a category is locally $\kappa$-multipresentable if and only if it is equivalent to the category of models of a limit-coproduct sketch; see Thm. 4.32 in Adamek-Rosicky and the remark below. A category is called locally multipresentable if it is locally $\kappa$-multipresentable for some $\kappa$, equivalently, it is accessible and has connected limits.', + 'https://ncatlab.org/nlab/show/locally+multipresentable+category', + NULL, + TRUE +), +( + 'locally finitely multipresentable', + 'is', + 'A category is locally finitely multipresentable if it is finitely accessible and has connected limits.', + 'https://ncatlab.org/nlab/show/locally+multipresentable+category', + NULL, + TRUE +), +( + 'locally polypresentable', + 'is', + 'A category is locally polypresentable if it is accessible and has wide pullbacks.', + 'https://ncatlab.org/nlab/show/locally+polypresentable+category', + NULL, + TRUE ); \ No newline at end of file diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index 5372c862..83ffb195 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -292,4 +292,25 @@ VALUES '["powers"]', 'The product $X^I$ is the cofiltered limit of the finite powers $X^E$, where $E$ ranges over the finite subsets of $I$.', FALSE +), +( + 'multilimits_generalize_limits', + '["complete"]', + '["multilimits"]', + 'Limits are precisely multilimits such that the set of cones is singleton.', + FALSE +), +( + 'multiterminal_special_case', + '["multilimits"]', + '["multiterminal object"]', + 'This is trivial.', + FALSE +), +( + 'multiterminal_with_connected', + '["connected","multiterminal object"]', + '["terminal object"]', + 'Let $(T_i)_{i\in I}$ be a multiterminal object in a connected category $\mathcal{C}$. By definition of multiterminal objects, for each object $C$, there are a unique index $i_C\in I$ and a unique morphism $C \to T_{i_C}$. Since the index $i_C$ is invariant under connected components, $I$ must be a singleton. The converse is trivial.', + TRUE ); \ No newline at end of file diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index ee0bc296..f2cc68a5 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/database/data/005_implications/007_locally-presentable-implications.sql @@ -138,4 +138,60 @@ VALUES '["ℵ₁-accessible"]', 'See [AR01, Remark 4.8(2)].', FALSE +), +( + 'locally_multipresentable_definition', + '["locally multipresentable"]', + '["accessible", "connected limits"]', + 'This is trivial.', + TRUE +), +( + 'locally_multipresentable_another_definition', + '["locally multipresentable"]', + '["accessible", "multicolimits"]', + 'See Adamek-Rosicky, 4.30.', + TRUE +), +( + 'locally_finitely_multipresentable_definition', + '["locally finitely multipresentable"]', + '["finitely accessible", "connected limits"]', + 'This is trivial.', + TRUE +), +( + 'locally_finitely_multipresentable_another_definition', + '["locally finitely multipresentable"]', + '["finitely accessible", "multicolimits"]', + 'See Adamek-Rosicky, 4.30.', + TRUE +), +( + 'locally_polypresentable_definition', + '["locally polypresentable"]', + '["accessible", "wide pullbacks"]', + 'This is trivial.', + TRUE +), +( + 'multialgebraic_implies_locally_finitely_multipresentable', + '["multialgebraic"]', + '["locally finitely multipresentable"]', + 'This follows from the fact that a category is locally finitely multipresentable if and only if it is equivalent to the category of models of an FLC-sketch, where FLC represents finite limits and small coproducts.', + FALSE +), +( + 'varieties_are_multialgebraic', + '["locally strongly finitely presentable"]', + '["multialgebraic"]', + 'This is because that every FP-sketch is an FPC-sketch.', + FALSE +), +( + 'multialgebraic_implies_generalized_variety', + '["multialgebraic"]', + '["generalized variety"]', + 'See [AR01, Thm. 4.4].', + FALSE ); \ No newline at end of file From 913e9014d34fa1c6dcd0166c220cbde093b75629 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Sun, 12 Apr 2026 08:27:59 +0900 Subject: [PATCH 06/29] Add several implications related with accessible categories --- .../008_locally-presentable.sql | 20 +++++++++++-- ...limits-colimits-existence-implications.sql | 2 +- .../007_locally-presentable-implications.sql | 28 ++++++++++++++----- 3 files changed, 40 insertions(+), 10 deletions(-) diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index 90337e27..51167c93 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -20,7 +20,15 @@ VALUES 'is', '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 small $\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, + 'locally copresentable', + TRUE +), +( + 'locally copresentable', + 'is', + 'A category is locally copresentable if its opposite category is locally presentable.', + 'https://ncatlab.org/nlab/show/locally+presentable+category', + 'locally presentable', TRUE ), ( @@ -52,7 +60,15 @@ VALUES 'is', 'Let $\kappa$ be a regular cardinal. A category is $\kappa$-accessible if it has small $\kappa$-filtered colimits and there is a (small) set $G$ of $\kappa$-presentable objects such that every object is a small $\kappa$-filtered colimit of objects in $S$. A category is accessible if it is $\kappa$-accessible for some regular cardinal $\kappa$.', 'https://ncatlab.org/nlab/show/accessible+category', - NULL, + 'coaccessible', + TRUE +), +( + 'coaccessible', + 'is', + 'A category is coaccessible if its opposite category is accessible.', + 'https://ncatlab.org/nlab/show/locally+presentable+category', + 'accessible', TRUE ), ( diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index 83ffb195..7b4637d1 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -169,7 +169,7 @@ VALUES ), ( 'finite_filtered_colimits', - '["finite", "Cauchy complete"]', + '["essentially finite", "Cauchy complete"]', '["finitely accessible"]', 'See MO/509853, where it is in fact shown that the ind-completion of any finite Cauchy-complete category becomes itself.', FALSE diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index f2cc68a5..a67e46d6 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/database/data/005_implications/007_locally-presentable-implications.sql @@ -21,10 +21,24 @@ VALUES FALSE ), ( - 'locally_presentable_consequence', - '["locally presentable"]', - '["locally essentially small", "well-powered", "well-copowered", "complete", "generating set"]', - '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.', + 'accessible_trivial_consequence', + '["accessible"]', + '["well-powered", "generating set"]', + 'For well-poweredness, see nLab. For a $\kappa$-accessible category, a skeleton of the full subcategory spanned by $\kappa$-presentable objects is small and dense, hence is a generating set.', + FALSE +), +( + 'accessible_locally_small', + '["accessible"]', + '["locally essentially small"]', + 'See the proof of Prop. 2.1.5 in Makkai-Pare.', + FALSE +), +( + 'accessible_wellcopowered', + '["accessible", "pushouts"]', + '["well-copowered"]', + 'See Thm. 2.49 in Adamek-Rosicky or Prop. 6.1.3 in Makkai-Pare.', FALSE ), ( @@ -36,7 +50,7 @@ VALUES ), ( 'locally_presentable_thin', - '["locally presentable", "self-dual"]', + '["locally presentable", "locally copresentable"]', '["thin"]', 'This follows from Adamek-Rosicky, Thm. 1.64.', FALSE @@ -106,8 +120,8 @@ VALUES ), ( 'small_accessible_characterization', - '["small", "accessible"]', - '["small", "Cauchy complete"]', + '["essentially small", "accessible"]', + '["essentially small", "Cauchy complete"]', 'See Makkai-Pare, Thm. 2.2.2.', TRUE ), From 8297aea418276be59cd5533890d8a666beaaf108 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Sun, 12 Apr 2026 08:29:20 +0900 Subject: [PATCH 07/29] Add "countable" and "essentially countable" --- .../003_properties/004_size-constraints.sql | 16 ++++++++++++++++ .../003_size-constraints-implications.sql | 18 ++++++++++++++++-- .../007_locally-presentable-implications.sql | 7 +++++++ 3 files changed, 39 insertions(+), 2 deletions(-) diff --git a/database/data/003_properties/004_size-constraints.sql b/database/data/003_properties/004_size-constraints.sql index 3861f7db..7f64adff 100644 --- a/database/data/003_properties/004_size-constraints.sql +++ b/database/data/003_properties/004_size-constraints.sql @@ -63,6 +63,22 @@ VALUES 'essentially finite', TRUE ), +( + 'countable', + 'is', + 'A category is countable if it has countably many objects and morphisms.', + NULL, + 'countable', + FALSE +), +( + 'essentially countable', + 'is', + 'A category is essentially countable if it is equivalent to a countable category.', + NULL, + 'essentially countable', + TRUE +), ( 'well-powered', 'is', diff --git a/database/data/005_implications/003_size-constraints-implications.sql b/database/data/005_implications/003_size-constraints-implications.sql index 5b4ee2cf..2e209325 100644 --- a/database/data/005_implications/003_size-constraints-implications.sql +++ b/database/data/005_implications/003_size-constraints-implications.sql @@ -23,13 +23,27 @@ VALUES ( 'finite_consequence', '["finite"]', - '["small", "essentially finite"]', + '["countable", "essentially finite"]', 'This is trivial.', FALSE ), ( - 'essentially_finite_consequence', + 'essentially_finite_raise', '["essentially finite"]', + '["essentially countable"]', + 'This is trivial.', + FALSE +), +( + 'countable_consequence', + '["countable"]', + '["essentially countable"]', + 'This is trivial.', + FALSE +), +( + 'essentially_countable_consequence', + '["essentially countable"]', '["essentially small"]', 'This is trivial.', FALSE diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index a67e46d6..172372d6 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/database/data/005_implications/007_locally-presentable-implications.sql @@ -125,6 +125,13 @@ VALUES 'See Makkai-Pare, Thm. 2.2.2.', TRUE ), +( + 'countably_accessible_thin', + '["essentially countable", "thin"]', + '["ℵ₁-accessible"]', + 'In general, every $\kappa$-filtered diagram in a poset whose elements are less than $\kappa$ admits the greatest element. Therefore, all the elements are $\kappa$-presentable, and the poset is $\kappa$-accessible.', + FALSE +), ( 'locally_presentable_another_definition', '["locally presentable"]', From 28c716f56a6c2e6417cf454732fd383e49650c87 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Sun, 12 Apr 2026 08:30:14 +0900 Subject: [PATCH 08/29] Assign properties --- database/data/004_property-assignments/0.sql | 6 ++++ database/data/004_property-assignments/2.sql | 6 ++++ .../data/004_property-assignments/Ab_fg.sql | 6 ++++ database/data/004_property-assignments/B.sql | 14 +++++++- database/data/004_property-assignments/BN.sql | 6 ++++ database/data/004_property-assignments/FI.sql | 8 ++++- database/data/004_property-assignments/FS.sql | 20 ++++++++++- .../data/004_property-assignments/FinAb.sql | 8 ++++- .../data/004_property-assignments/FinGrp.sql | 8 ++++- .../data/004_property-assignments/FinOrd.sql | 8 ++++- .../data/004_property-assignments/FinSet.sql | 8 ++++- .../data/004_property-assignments/Fld.sql | 34 +++++-------------- .../data/004_property-assignments/Man.sql | 6 ++++ database/data/004_property-assignments/N.sql | 6 ++++ .../data/004_property-assignments/N_oo.sql | 6 ++++ .../data/004_property-assignments/Set_op.sql | 2 +- .../data/004_property-assignments/Setne.sql | 18 ++++++++++ database/data/004_property-assignments/Sp.sql | 6 ++++ .../data/004_property-assignments/Top.sql | 6 ++++ .../data/004_property-assignments/Z_div.sql | 6 ++++ .../real_interval.sql | 2 +- scripts/expected-data/Ab.json | 14 +++++++- scripts/expected-data/Set.json | 14 +++++++- scripts/expected-data/Top.json | 14 +++++++- 24 files changed, 194 insertions(+), 38 deletions(-) diff --git a/database/data/004_property-assignments/0.sql b/database/data/004_property-assignments/0.sql index a1bf48f3..dd57b6a6 100644 --- a/database/data/004_property-assignments/0.sql +++ b/database/data/004_property-assignments/0.sql @@ -29,6 +29,12 @@ VALUES TRUE, 'This is trivial.' ), +( + '0', + 'multialgebraic', + 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', diff --git a/database/data/004_property-assignments/2.sql b/database/data/004_property-assignments/2.sql index d9886e05..a4a6f955 100644 --- a/database/data/004_property-assignments/2.sql +++ b/database/data/004_property-assignments/2.sql @@ -23,6 +23,12 @@ VALUES TRUE, 'This is trivial.' ), +( + '2', + 'multialgebraic', + TRUE, + 'There is an FPC-sketch whose $\mathbf{Set}$-model is precisely a pair $(X,Y)$ of sets such that the coproduct $X+Y$ is a singleton. Any $\mathbf{Set}$-model of such a sketch is isomorphic to either $(\varnothing, 1)$ or $(1, \varnothing)$, hence the category of models is equivalent to $\mathbf{2}$.' +), ( '2', 'connected', diff --git a/database/data/004_property-assignments/Ab_fg.sql b/database/data/004_property-assignments/Ab_fg.sql index dbbb9040..4533089d 100644 --- a/database/data/004_property-assignments/Ab_fg.sql +++ b/database/data/004_property-assignments/Ab_fg.sql @@ -64,4 +64,10 @@ VALUES 'skeletal', FALSE, 'This is trivial.' +), +( + 'Ab_fg', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/B.sql b/database/data/004_property-assignments/B.sql index 5783de5a..b6cc355b 100644 --- a/database/data/004_property-assignments/B.sql +++ b/database/data/004_property-assignments/B.sql @@ -13,7 +13,7 @@ VALUES ), ( 'B', - 'essentially small', + 'essentially countable', TRUE, 'Every finite set is isomorphic to some $[n] = \{1,\dotsc,n\}$ for some $n \in \mathbb{N}$.' ), @@ -58,4 +58,16 @@ VALUES 'skeletal', FALSE, 'This is trivial.' +), +( + 'B', + 'multiterminal object', + FALSE, + 'This is trivial.' +), +( + 'B', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/BN.sql b/database/data/004_property-assignments/BN.sql index 15027efe..1177063a 100644 --- a/database/data/004_property-assignments/BN.sql +++ b/database/data/004_property-assignments/BN.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'BN', + 'countable', + TRUE, + 'This is trivial.' +), ( 'BN', 'strongly connected', diff --git a/database/data/004_property-assignments/FI.sql b/database/data/004_property-assignments/FI.sql index 3133cd06..1c1adc8a 100644 --- a/database/data/004_property-assignments/FI.sql +++ b/database/data/004_property-assignments/FI.sql @@ -25,7 +25,7 @@ VALUES ), ( 'FI', - 'essentially small', + 'essentially countable', TRUE, 'Every finite set is isomorphic to some $[n] = \{1,\dotsc,n\}$ for some $n \in \mathbb{N}$.' ), @@ -118,4 +118,10 @@ VALUES 'strongly connected', FALSE, 'There is no map from a non-empty set to the empty set.' +), +( + 'FI', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/FS.sql b/database/data/004_property-assignments/FS.sql index b9df207b..0d46d39e 100644 --- a/database/data/004_property-assignments/FS.sql +++ b/database/data/004_property-assignments/FS.sql @@ -13,7 +13,7 @@ VALUES ), ( 'FS', - 'essentially small', + 'essentially countable', TRUE, 'Every finite set is isomorphic to some $[n] = \{1,\dotsc,n\}$ for some $n \in \mathbb{N}$.' ), @@ -53,6 +53,12 @@ VALUES TRUE, 'If $f : X \to Y$ is a surjective map of finite sets, it is the coequalizer of the two projections $p_1, p_2 : X \times_Y X \rightrightarrows X$ in $\mathbf{FinSet}$, but also in $\mathbf{FS}$. Notice that $p_1,p_2$ are surjective. Even though $X \times_Y X$ is not a pullback in $\mathbf{FS}$, we can use this finite set here.' ), +( + 'FS', + 'multiterminal object', + TRUE, + 'The empty set and a singleton give a multiterminal object.' +), ( 'FS', 'small', @@ -116,4 +122,16 @@ VALUES but $(E_1 \vee E_2) \wedge (E_1 \vee E_3) = \top \wedge \top = \top$.

      *For thin categories, the properties codistributive and distributive are equivalent.' +), +( + 'FS', + 'multiinitial object', + FALSE, + 'This is trivial.' +), +( + 'FS', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/FinAb.sql b/database/data/004_property-assignments/FinAb.sql index ff7575ef..7f8d58c1 100644 --- a/database/data/004_property-assignments/FinAb.sql +++ b/database/data/004_property-assignments/FinAb.sql @@ -13,7 +13,7 @@ VALUES ), ( 'FinAb', - 'essentially small', + 'essentially countable', TRUE, 'The underlying set of a finite structure can be chosen to be a subset of $\mathbb{N}$.' ), @@ -58,4 +58,10 @@ VALUES 'skeletal', FALSE, 'There are many trivial and hence isomorphic groups which are not equal.' +), +( + 'FinAb', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/FinGrp.sql b/database/data/004_property-assignments/FinGrp.sql index 096cc4aa..babb0a4f 100644 --- a/database/data/004_property-assignments/FinGrp.sql +++ b/database/data/004_property-assignments/FinGrp.sql @@ -19,7 +19,7 @@ VALUES ), ( 'FinGrp', - 'essentially small', + 'essentially countable', TRUE, 'The underlying set of a finite structure can be chosen to be a subset of $\mathbb{N}$.' ), @@ -106,4 +106,10 @@ VALUES 'sequential colimits', FALSE, 'This follows from this lemma.' +), +( + 'FinGrp', + 'countable', + FALSE, + 'This is trivial.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/FinOrd.sql b/database/data/004_property-assignments/FinOrd.sql index 6c952719..94fe6031 100644 --- a/database/data/004_property-assignments/FinOrd.sql +++ b/database/data/004_property-assignments/FinOrd.sql @@ -61,7 +61,7 @@ VALUES ), ( 'FinOrd', - 'essentially small', + 'essentially countable', TRUE, 'Every finite ordered set is isomorphic to $\{0 < \cdots < n-1 \}$ for some $n \in \mathbb{N}$.' ), @@ -124,4 +124,10 @@ VALUES 'one-way', FALSE, 'There are three different order-preserving maps $\{0 < 1\} \to \{0 < 1\}$.' +), +( + 'FinOrd', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/FinSet.sql b/database/data/004_property-assignments/FinSet.sql index d85eedd2..642480c4 100644 --- a/database/data/004_property-assignments/FinSet.sql +++ b/database/data/004_property-assignments/FinSet.sql @@ -13,7 +13,7 @@ VALUES ), ( 'FinSet', - 'essentially small', + 'essentially countable', TRUE, 'Every finite set is isomorphic to some $[n] = \{1,\dotsc,n\}$ for some $n \in \mathbb{N}$.' ), @@ -70,4 +70,10 @@ VALUES 'Malcev', FALSE, 'There are lots of non-symmetric reflexive relations.' +), +( + 'FinSet', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/Fld.sql b/database/data/004_property-assignments/Fld.sql index 51a01ab8..82e85f44 100644 --- a/database/data/004_property-assignments/Fld.sql +++ b/database/data/004_property-assignments/Fld.sql @@ -11,18 +11,6 @@ VALUES TRUE, 'There is a forgetful functor $\mathbf{Fld} \to \mathbf{Set}$ and $\mathbf{Set}$ is locally small.' ), -( - 'Fld', - 'directed colimits', - TRUE, - 'Consider a directed diagram $(F_i)$ of fields and take the colimit $F$ in the category of commutative rings. Now one checks that $F$ is a field as well, and the universal property remains true for fields.' -), -( - 'Fld', - 'connected limits', - TRUE, - 'Consider a connected diagram $(F_i)$ of fields and take the limit $F$ in the category of commutative rings. Now one checks that $F$ is a field as well, and the universal property remains true for fields. Namely, $1 = 0$ in $F$ would imply that $1 = 0$ in each $F_i$ and hence, since the diagram is connected, in some $F_i$, which is a contradiction. And if $x \in F$ is non-zero, then all components $x_i$ are non-zero and hence invertible: Choose some $j$ such that $x_j$ is non-zero. Since there is a zig zag path of morphisms between $i$ and $j$ in the index category, which get mapped to field homomorphisms which are injective, it follows that $x_i$ is non-zero.' -), ( 'Fld', 'inhabited', @@ -35,12 +23,6 @@ VALUES TRUE, 'It is well-known that every field homomorphism is injective and hence a monomorphism.' ), -( - 'Fld', - 'well-powered', - TRUE, - 'The subfields of a given field form a set.' -), ( 'Fld', 'well-copowered', @@ -49,9 +31,9 @@ VALUES ), ( 'Fld', - 'generating set', + 'multialgebraic', TRUE, - 'The fields $Q(\mathbb{Z}[X]/\mathfrak{p})$, where $\mathfrak{p}$ runs through all prime ideals of the polynomial ring, provide a generating set. This is because for every element $a \in K$ of a field $K$ there is a prime ideal $\mathfrak{p}$ with a homomorphism $Q(\mathbb{Z}[X]/\mathfrak{p}) \to K$ mapping $[X]$ to $a$: There is a homomorphism $\mathbb{Z}[X] \to K$ mapping $X \mapsto a$. Let $\mathfrak{p}$ be its kernel. Then it extends to a field homomorphism as desired.' + 'See Eg. 4.3(1) in [AR01].' ), ( 'Fld', @@ -83,12 +65,6 @@ VALUES FALSE, 'We apply this lemma to the collection of fields: Any homomorphism of fields is injective. For every infinite cardinal $\kappa$ the field of rational functions in $\kappa$ variables has cardinality $\geq \kappa$ and a non-trivial automorphism (swap two variables).' ), -( - 'Fld', - 'essentially small', - FALSE, - 'Consider function fields in any number of variables.' -), ( 'Fld', 'skeletal', @@ -112,4 +88,10 @@ VALUES 'binary powers', FALSE, 'Assume that the product $P := \mathbb{Q}(\sqrt{2}) \times \mathbb{Q}(\sqrt{2})$ exists. This field is isomorphic to a subfield of $\mathbb{Q}(\sqrt{2})$, hence $P \cong \mathbb{Q}$ or $P \cong \mathbb{Q}(\sqrt{2})$. In the first case, the two projections $P \rightrightarrows \mathbb{Q}(\sqrt{2})$ must be equal, which means that every two homomorphisms $K \rightrightarrows \mathbb{Q}(\sqrt{2})$ are equal, which is absurd (take $K = \mathbb{Q}(\sqrt{2})$ and its two automorphisms). In the second case, the projections induce for every field $K$ a bijection $\mathrm{Hom}(K,\mathbb{Q}(\sqrt{2})) \cong \mathrm{Hom}(K,\mathbb{Q}(\sqrt{2}))^2$, which however fails for $K = \mathbb{Q}(\sqrt{2})$: the left hand side has $2$ elements, the right hand side has $4$ elements. A more general result about products in $\mathbf{Fld}$ can be found at MSE/359352.' +), +( + 'Fld', + 'multiterminal object', + FALSE, + 'Every field has a non-trivial extension, for instance, the rational function field over itself in one variable. Hence, a multiterminal object never exists.' ); diff --git a/database/data/004_property-assignments/Man.sql b/database/data/004_property-assignments/Man.sql index b3fc32c9..304c9f6c 100644 --- a/database/data/004_property-assignments/Man.sql +++ b/database/data/004_property-assignments/Man.sql @@ -119,4 +119,10 @@ VALUES 'sequential colimits', FALSE, 'If $\mathbf{Man}$ had sequential colimits, then by this lemma there would be a manifold $M$ that admits a split epimorphism $M \to \mathbb{R}^n$ for every $n$. But then $M$ will have an infinite-dimensional tangent space, which is a contradiction.' +), +( + 'Man', + 'countable', + FALSE, + 'This is trivial.' ); diff --git a/database/data/004_property-assignments/N.sql b/database/data/004_property-assignments/N.sql index 79a47446..7d367ccb 100644 --- a/database/data/004_property-assignments/N.sql +++ b/database/data/004_property-assignments/N.sql @@ -53,6 +53,12 @@ VALUES TRUE, 'This is because the natural numbers with respect to $<$ are well-founded.' ), +( + 'N', + 'countable', + TRUE, + 'This is trivial.' +), ( 'N', 'countable coproducts', diff --git a/database/data/004_property-assignments/N_oo.sql b/database/data/004_property-assignments/N_oo.sql index c301d62a..beba103d 100644 --- a/database/data/004_property-assignments/N_oo.sql +++ b/database/data/004_property-assignments/N_oo.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'N_oo', + 'countable', + TRUE, + 'This is trivial.' +), ( 'N_oo', 'coproducts', diff --git a/database/data/004_property-assignments/Set_op.sql b/database/data/004_property-assignments/Set_op.sql index 0e6c6982..d834262b 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', - 'locally presentable', + 'accessible', FALSE, '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/Setne.sql b/database/data/004_property-assignments/Setne.sql index 90f13269..85116a3f 100644 --- a/database/data/004_property-assignments/Setne.sql +++ b/database/data/004_property-assignments/Setne.sql @@ -83,6 +83,24 @@ VALUES TRUE, 'Use constant maps.' ), +( + 'Setne', + 'generalized variety', + TRUE, + 'Since the inclusion $\mathbf{Set}_{\neq \varnothing} \hookrightarrow \mathbf{Set}$ is closed under non-empty colimits, it is also closed under sifted colimits. Therefore, non-empty finite sets are still strongly finitely presentable in $\mathbf{Set}_{\neq \varnothing}$, and every non-empty set is written as a small sifted colimit of them.' +), +( + 'Setne', + 'finitely accessible', + TRUE, + 'Since the inclusion $\mathbf{Set}_{\neq \varnothing} \hookrightarrow \mathbf{Set}$ is closed under non-empty colimits, it is also closed under filtered colimits. Therefore, non-empty finite sets are still finitely presentable in $\mathbf{Set}_{\neq \varnothing}$, and every non-empty set is written as a small filtered colimit of them.' +), +( + 'Setne', + 'multilimits', + TRUE, + 'Let $D$ be a diagram in $\mathbf{Set}_{\neq \varnothing}$, and let $L$ be a limit of $D$ in $\mathbf{Set}$. If $L$ is non-empty, it gives a limit in $\mathbf{Set}_{\neq \varnothing}$ as well. If $L$ is the empty set, there is no cone over $D$ in $\mathbf{Set}_{\neq \varnothing}$; hence the empty set of cone gives a multilimit of $D$ in $\mathbf{Set}_{\neq \varnothing}$.' +), ( 'Setne', 'sequential limits', diff --git a/database/data/004_property-assignments/Sp.sql b/database/data/004_property-assignments/Sp.sql index 58181ab1..b75420d1 100644 --- a/database/data/004_property-assignments/Sp.sql +++ b/database/data/004_property-assignments/Sp.sql @@ -64,4 +64,10 @@ VALUES 'generator', FALSE, 'Assume that a generator $G$ exists. For $n \geq 0$ let $F_n$ be the combinatorial species of sets of cardinality $\neq n$: $F_n(A) = \varnothing$ when $A$ has cardinality $n$, otherwise $F_n(A) = \{A\}$. There are two different morphisms $F_n \rightrightarrows F_n \sqcup F_n$. Hence, there must be at least one morphism $G \to F_n$. If $A$ has cardinality $n$, this implies $G(A) = \varnothing$. Since this holds for all $n$, $G$ is the initial object. But this is clearly no generator (it would mean that the category is thin).' +), +( + 'Sp', + 'essentially countable', + FALSE, + 'Any function $f\colon\mathbb{N} \to \mathbb{N}$ can be regarded as a combinatorial species with trivial actions, and distinct functions yield non-isomorphic species.' ); \ No newline at end of file diff --git a/database/data/004_property-assignments/Top.sql b/database/data/004_property-assignments/Top.sql index 7814a7c4..351e447f 100644 --- a/database/data/004_property-assignments/Top.sql +++ b/database/data/004_property-assignments/Top.sql @@ -118,4 +118,10 @@ VALUES 'co-Malcev', FALSE, 'See MO/509548. We can also phrase the proof as follows: Consider the forgetful functor $U : \mathbf{Top} \to \mathbf{Set}$ and the relation $R \subseteq U^2$ defined by $R(X) := \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the singleton and $R$ by the Sierpinski space. It is clear that $R$ is reflexive, but not symmetric.' +), +( + 'Top', + 'coaccessible', + FALSE, + 'Assume $\mathbf{Top}$ is coaccessible. Let $p\colon S \to I$ be the identity map from the Sierpinski space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\mathbf{Set}$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\mathbf{Set}$ is not coaccessible, this is a contradiction.' ); diff --git a/database/data/004_property-assignments/Z_div.sql b/database/data/004_property-assignments/Z_div.sql index d18ec05b..4f38b97f 100644 --- a/database/data/004_property-assignments/Z_div.sql +++ b/database/data/004_property-assignments/Z_div.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'Z_div', + 'countable', + TRUE, + 'This is trivial.' +), ( 'Z_div', 'products', diff --git a/database/data/004_property-assignments/real_interval.sql b/database/data/004_property-assignments/real_interval.sql index 9f66736c..85cd3ccb 100644 --- a/database/data/004_property-assignments/real_interval.sql +++ b/database/data/004_property-assignments/real_interval.sql @@ -37,7 +37,7 @@ VALUES ), ( 'real_interval', - 'essentially finite', + 'essentially countable', FALSE, 'This is trivial.' ), diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index 930a1305..fc7001e8 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -90,6 +90,14 @@ "finitely accessible": true, "ℵ₁-accessible": true, "generalized variety": true, + "locally finitely multipresentable": true, + "locally multipresentable": true, + "locally polypresentable": true, + "multialgebraic": true, + "multilimits": true, + "multicolimits": true, + "multiterminal object": true, + "multiinitial object": true, "cartesian closed": false, "locally cartesian closed": false, @@ -128,5 +136,9 @@ "cocartesian coclosed": false, "locally cocartesian coclosed": false, "quotient object classifier": false, - "regular quotient object classifier": false + "regular quotient object classifier": false, + "locally copresentable": false, + "coaccessible": false, + "countable": false, + "essentially countable": false } diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index 81665405..b9c34d9a 100644 --- a/scripts/expected-data/Set.json +++ b/scripts/expected-data/Set.json @@ -85,6 +85,14 @@ "finitely accessible": true, "ℵ₁-accessible": true, "generalized variety": true, + "locally finitely multipresentable": true, + "locally multipresentable": true, + "locally polypresentable": true, + "multialgebraic": true, + "multilimits": true, + "multicolimits": true, + "multiterminal object": true, + "multiinitial object": true, "Grothendieck abelian": false, "Malcev": false, @@ -128,5 +136,9 @@ "kernels": false, "cokernels": false, "normal": false, - "conormal": false + "conormal": false, + "locally copresentable": false, + "coaccessible": false, + "countable": false, + "essentially countable": false } diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index c9a1cd45..c8879886 100644 --- a/scripts/expected-data/Top.json +++ b/scripts/expected-data/Top.json @@ -65,6 +65,10 @@ "cofiltered": true, "sifted": true, "cosifted": true, + "multilimits": true, + "multicolimits": true, + "multiterminal object": true, + "multiinitial object": true, "abelian": false, "additive": false, @@ -128,5 +132,13 @@ "accessible": false, "finitely accessible": false, "ℵ₁-accessible": false, - "generalized variety": false + "generalized variety": false, + "locally finitely multipresentable": false, + "locally multipresentable": false, + "locally polypresentable": false, + "multialgebraic": false, + "locally copresentable": false, + "coaccessible": false, + "countable": false, + "essentially countable": false } From 1329af093c7fe4f8f1927be4ac29a5a2b6fecb93 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Sun, 12 Apr 2026 19:37:49 +0900 Subject: [PATCH 09/29] Add "generalized variety" + "multicolimits" = "multialgebraic"" --- .../007_locally-presentable-implications.sql | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index 172372d6..fcb1b8cb 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/database/data/005_implications/007_locally-presentable-implications.sql @@ -210,9 +210,9 @@ VALUES FALSE ), ( - 'multialgebraic_implies_generalized_variety', + 'multialgebraic_another_definition', '["multialgebraic"]', - '["generalized variety"]', + '["generalized variety", "multicolimits"]', 'See [AR01, Thm. 4.4].', - FALSE + TRUE ); \ No newline at end of file From 52dec606d162917e2b4a221a7aa4f01bdc53565f Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Mon, 13 Apr 2026 10:11:46 +0900 Subject: [PATCH 10/29] Adjust hyphenation and add definition of multi-limits --- .../002_limits-colimits-existence.sql | 24 +++++------ .../008_locally-presentable.sql | 16 +++---- database/data/004_property-assignments/0.sql | 2 +- database/data/004_property-assignments/2.sql | 2 +- database/data/004_property-assignments/B.sql | 2 +- database/data/004_property-assignments/FS.sql | 6 +-- .../data/004_property-assignments/Fld.sql | 6 +-- .../data/004_property-assignments/Setne.sql | 4 +- ...limits-colimits-existence-implications.sql | 18 ++++---- .../007_locally-presentable-implications.sql | 42 +++++++++---------- scripts/expected-data/Ab.json | 16 +++---- scripts/expected-data/Set.json | 16 +++---- scripts/expected-data/Top.json | 16 +++---- 13 files changed, 85 insertions(+), 85 deletions(-) diff --git a/database/data/003_properties/002_limits-colimits-existence.sql b/database/data/003_properties/002_limits-colimits-existence.sql index d929d248..ca5b8d9b 100644 --- a/database/data/003_properties/002_limits-colimits-existence.sql +++ b/database/data/003_properties/002_limits-colimits-existence.sql @@ -344,34 +344,34 @@ VALUES TRUE ), ( - 'multilimits', + 'multi-complete', 'has', - 'This property refers to the existence of multilimits of small diagrams. Note that any diagram with no cone admits a multilimit, which is the empty set of cones.', + 'A multi-limit 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', - 'multicolimits', + 'multi-cocomplete', TRUE ), ( - 'multicolimits', + 'multi-cocomplete', 'has', - 'This property refers to the existence of multicolimits of small diagrams. Note that any diagram with no cocone admits a multicolimit, which is the empty set of cocones.', + 'A multi-colimit of a diagram $D\colon \mathcal{S} \to \mathcal{C}$ is a set $I$ of cocones over $D$ such that every cocone over $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', - 'multilimits', + 'multi-complete', TRUE ), ( - 'multiterminal object', + 'multi-terminal object', 'has a', - 'This property refers to the existence of a multilimit of the empty diagram. A category has a multiterminal object if and only if each connected component has a terminal object.', + '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', - 'multiinitial object', + 'multi-initial object', TRUE ), ( - 'multiinitial object', + 'multi-initial object', 'has a', - 'This property refers to the existence of a multicolimit of the empty diagram. A category has a multiinitial object if and only if each connected component has a initial object.', + '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', - 'multiterminal object', + 'multi-terminal object', TRUE ); \ No newline at end of file diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index 51167c93..2145e503 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -96,33 +96,33 @@ VALUES TRUE ), ( - 'multialgebraic', + 'multi-algebraic', 'is', - 'A category is multialgebraic if it is equivalent to the category of models of an FPC-sketch, where FPC represents finite products and small coproducts. This notion was introduced by Diers.', + 'A category is multi-algebraic if it is equivalent to the category of models of an FPC-sketch, where FPC represents finite products and small coproducts. This notion was introduced by Diers.', NULL, NULL, TRUE ), ( - 'locally multipresentable', + 'locally multi-presentable', 'is', - 'Let $\kappa$ be a regular cardinal. A category is locally $\kappa$-multipresentable if it is $\kappa$-accessible and has connected limits. It is known that a category is locally $\kappa$-multipresentable if and only if it is equivalent to the category of models of a limit-coproduct sketch; see Thm. 4.32 in Adamek-Rosicky and the remark below. A category is called locally multipresentable if it is locally $\kappa$-multipresentable for some $\kappa$, equivalently, it is accessible and has connected limits.', + 'Let $\kappa$ be a regular cardinal. A category is locally $\kappa$-multi-presentable if it is $\kappa$-accessible and has connected limits. It is known that a category is locally $\kappa$-multi-presentable if and only if it is equivalent to the category of models of a limit-coproduct sketch; see Thm. 4.32 in Adamek-Rosicky and the remark below. A category is called locally multi-presentable if it is locally $\kappa$-multi-presentable for some $\kappa$, equivalently, it is accessible and has connected limits.', 'https://ncatlab.org/nlab/show/locally+multipresentable+category', NULL, TRUE ), ( - 'locally finitely multipresentable', + 'locally finitely multi-presentable', 'is', - 'A category is locally finitely multipresentable if it is finitely accessible and has connected limits.', + 'A category is locally finitely multi-presentable if it is finitely accessible and has connected limits.', 'https://ncatlab.org/nlab/show/locally+multipresentable+category', NULL, TRUE ), ( - 'locally polypresentable', + 'locally poly-presentable', 'is', - 'A category is locally polypresentable if it is accessible and has wide pullbacks.', + 'A category is locally poly-presentable if it is accessible and has wide pullbacks.', 'https://ncatlab.org/nlab/show/locally+polypresentable+category', NULL, TRUE diff --git a/database/data/004_property-assignments/0.sql b/database/data/004_property-assignments/0.sql index dd57b6a6..cbbe1462 100644 --- a/database/data/004_property-assignments/0.sql +++ b/database/data/004_property-assignments/0.sql @@ -31,7 +31,7 @@ VALUES ), ( '0', - 'multialgebraic', + '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.' ), diff --git a/database/data/004_property-assignments/2.sql b/database/data/004_property-assignments/2.sql index a4a6f955..266543cb 100644 --- a/database/data/004_property-assignments/2.sql +++ b/database/data/004_property-assignments/2.sql @@ -25,7 +25,7 @@ VALUES ), ( '2', - 'multialgebraic', + 'multi-algebraic', TRUE, 'There is an FPC-sketch whose $\mathbf{Set}$-model is precisely a pair $(X,Y)$ of sets such that the coproduct $X+Y$ is a singleton. Any $\mathbf{Set}$-model of such a sketch is isomorphic to either $(\varnothing, 1)$ or $(1, \varnothing)$, hence the category of models is equivalent to $\mathbf{2}$.' ), diff --git a/database/data/004_property-assignments/B.sql b/database/data/004_property-assignments/B.sql index b6cc355b..ca8a19a3 100644 --- a/database/data/004_property-assignments/B.sql +++ b/database/data/004_property-assignments/B.sql @@ -61,7 +61,7 @@ VALUES ), ( 'B', - 'multiterminal object', + 'multi-terminal object', FALSE, 'This is trivial.' ), diff --git a/database/data/004_property-assignments/FS.sql b/database/data/004_property-assignments/FS.sql index 0d46d39e..0e632107 100644 --- a/database/data/004_property-assignments/FS.sql +++ b/database/data/004_property-assignments/FS.sql @@ -55,9 +55,9 @@ VALUES ), ( 'FS', - 'multiterminal object', + 'multi-terminal object', TRUE, - 'The empty set and a singleton give a multiterminal object.' + 'The empty set and a singleton give a multi-terminal object.' ), ( 'FS', @@ -125,7 +125,7 @@ VALUES ), ( 'FS', - 'multiinitial object', + 'multi-initial object', FALSE, 'This is trivial.' ), diff --git a/database/data/004_property-assignments/Fld.sql b/database/data/004_property-assignments/Fld.sql index 82e85f44..4337fce6 100644 --- a/database/data/004_property-assignments/Fld.sql +++ b/database/data/004_property-assignments/Fld.sql @@ -31,7 +31,7 @@ VALUES ), ( 'Fld', - 'multialgebraic', + 'multi-algebraic', TRUE, 'See Eg. 4.3(1) in [AR01].' ), @@ -91,7 +91,7 @@ VALUES ), ( 'Fld', - 'multiterminal object', + 'multi-terminal object', FALSE, - 'Every field has a non-trivial extension, for instance, the rational function field over itself in one variable. Hence, a multiterminal object never exists.' + 'Every field has a non-trivial extension, for instance, the rational function field over itself in one variable. Hence, a multi-terminal object never exists.' ); diff --git a/database/data/004_property-assignments/Setne.sql b/database/data/004_property-assignments/Setne.sql index 85116a3f..8fb760e1 100644 --- a/database/data/004_property-assignments/Setne.sql +++ b/database/data/004_property-assignments/Setne.sql @@ -97,9 +97,9 @@ VALUES ), ( 'Setne', - 'multilimits', + 'multi-complete', TRUE, - 'Let $D$ be a diagram in $\mathbf{Set}_{\neq \varnothing}$, and let $L$ be a limit of $D$ in $\mathbf{Set}$. If $L$ is non-empty, it gives a limit in $\mathbf{Set}_{\neq \varnothing}$ as well. If $L$ is the empty set, there is no cone over $D$ in $\mathbf{Set}_{\neq \varnothing}$; hence the empty set of cone gives a multilimit of $D$ in $\mathbf{Set}_{\neq \varnothing}$.' + 'Let $D$ be a diagram in $\mathbf{Set}_{\neq \varnothing}$, and let $L$ be a limit of $D$ in $\mathbf{Set}$. If $L$ is non-empty, it gives a limit in $\mathbf{Set}_{\neq \varnothing}$ as well. If $L$ is the empty set, there is no cone over $D$ in $\mathbf{Set}_{\neq \varnothing}$; hence the empty set of cone gives a multi-limit of $D$ in $\mathbf{Set}_{\neq \varnothing}$.' ), ( 'Setne', diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index 7b4637d1..25127551 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -294,23 +294,23 @@ VALUES FALSE ), ( - 'multilimits_generalize_limits', + 'multi-complete_generalize_limits', '["complete"]', - '["multilimits"]', - 'Limits are precisely multilimits such that the set of cones is singleton.', + '["multi-complete"]', + 'Limits are precisely multi-limits such that the set of cones is singleton.', FALSE ), ( - 'multiterminal_special_case', - '["multilimits"]', - '["multiterminal object"]', + 'multi-terminal_special_case', + '["multi-complete"]', + '["multi-terminal object"]', 'This is trivial.', FALSE ), ( - 'multiterminal_with_connected', - '["connected","multiterminal object"]', + 'multi-terminal_with_connected', + '["connected","multi-terminal object"]', '["terminal object"]', - 'Let $(T_i)_{i\in I}$ be a multiterminal object in a connected category $\mathcal{C}$. By definition of multiterminal objects, for each object $C$, there are a unique index $i_C\in I$ and a unique morphism $C \to T_{i_C}$. Since the index $i_C$ is invariant under connected components, $I$ must be a singleton. The converse is trivial.', + 'Let $(T_i)_{i\in I}$ be a multi-terminal object in a connected category $\mathcal{C}$. By definition of multi-terminal objects, for each object $C$, there are a unique index $i_C\in I$ and a unique morphism $C \to T_{i_C}$. Since the index $i_C$ is invariant under connected components, $I$ must be a singleton. The converse is trivial.', TRUE ); \ No newline at end of file diff --git a/database/data/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index fcb1b8cb..dd7e2ad9 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/database/data/005_implications/007_locally-presentable-implications.sql @@ -161,58 +161,58 @@ VALUES FALSE ), ( - 'locally_multipresentable_definition', - '["locally multipresentable"]', + 'locally_multi-presentable_definition', + '["locally multi-presentable"]', '["accessible", "connected limits"]', 'This is trivial.', TRUE ), ( - 'locally_multipresentable_another_definition', - '["locally multipresentable"]', - '["accessible", "multicolimits"]', + 'locally_multi-presentable_another_definition', + '["locally multi-presentable"]', + '["accessible", "multi-cocomplete"]', 'See Adamek-Rosicky, 4.30.', TRUE ), ( - 'locally_finitely_multipresentable_definition', - '["locally finitely multipresentable"]', + 'locally_finitely_multi-presentable_definition', + '["locally finitely multi-presentable"]', '["finitely accessible", "connected limits"]', 'This is trivial.', TRUE ), ( - 'locally_finitely_multipresentable_another_definition', - '["locally finitely multipresentable"]', - '["finitely accessible", "multicolimits"]', + 'locally_finitely_multi-presentable_another_definition', + '["locally finitely multi-presentable"]', + '["finitely accessible", "multi-cocomplete"]', 'See Adamek-Rosicky, 4.30.', TRUE ), ( - 'locally_polypresentable_definition', - '["locally polypresentable"]', + 'locally_poly-presentable_definition', + '["locally poly-presentable"]', '["accessible", "wide pullbacks"]', 'This is trivial.', TRUE ), ( - 'multialgebraic_implies_locally_finitely_multipresentable', - '["multialgebraic"]', - '["locally finitely multipresentable"]', - 'This follows from the fact that a category is locally finitely multipresentable if and only if it is equivalent to the category of models of an FLC-sketch, where FLC represents finite limits and small coproducts.', + 'multi-algebraic_implies_locally_finitely_multi-presentable', + '["multi-algebraic"]', + '["locally finitely multi-presentable"]', + 'This follows from the fact that a category is locally finitely multi-presentable if and only if it is equivalent to the category of models of an FLC-sketch, where FLC represents finite limits and small coproducts.', FALSE ), ( - 'varieties_are_multialgebraic', + 'varieties_are_multi-algebraic', '["locally strongly finitely presentable"]', - '["multialgebraic"]', + '["multi-algebraic"]', 'This is because that every FP-sketch is an FPC-sketch.', FALSE ), ( - 'multialgebraic_another_definition', - '["multialgebraic"]', - '["generalized variety", "multicolimits"]', + 'multi-algebraic_another_definition', + '["multi-algebraic"]', + '["generalized variety", "multi-cocomplete"]', 'See [AR01, Thm. 4.4].', TRUE ); \ No newline at end of file diff --git a/scripts/expected-data/Ab.json b/scripts/expected-data/Ab.json index fc7001e8..629564fb 100644 --- a/scripts/expected-data/Ab.json +++ b/scripts/expected-data/Ab.json @@ -90,14 +90,14 @@ "finitely accessible": true, "ℵ₁-accessible": true, "generalized variety": true, - "locally finitely multipresentable": true, - "locally multipresentable": true, - "locally polypresentable": true, - "multialgebraic": true, - "multilimits": true, - "multicolimits": true, - "multiterminal object": true, - "multiinitial object": true, + "locally finitely multi-presentable": true, + "locally multi-presentable": true, + "locally poly-presentable": true, + "multi-algebraic": true, + "multi-complete": true, + "multi-cocomplete": true, + "multi-terminal object": true, + "multi-initial object": true, "cartesian closed": false, "locally cartesian closed": false, diff --git a/scripts/expected-data/Set.json b/scripts/expected-data/Set.json index b9c34d9a..f750b77e 100644 --- a/scripts/expected-data/Set.json +++ b/scripts/expected-data/Set.json @@ -85,14 +85,14 @@ "finitely accessible": true, "ℵ₁-accessible": true, "generalized variety": true, - "locally finitely multipresentable": true, - "locally multipresentable": true, - "locally polypresentable": true, - "multialgebraic": true, - "multilimits": true, - "multicolimits": true, - "multiterminal object": true, - "multiinitial object": true, + "locally finitely multi-presentable": true, + "locally multi-presentable": true, + "locally poly-presentable": true, + "multi-algebraic": true, + "multi-complete": true, + "multi-cocomplete": true, + "multi-terminal object": true, + "multi-initial object": true, "Grothendieck abelian": false, "Malcev": false, diff --git a/scripts/expected-data/Top.json b/scripts/expected-data/Top.json index c8879886..5e644c97 100644 --- a/scripts/expected-data/Top.json +++ b/scripts/expected-data/Top.json @@ -65,10 +65,10 @@ "cofiltered": true, "sifted": true, "cosifted": true, - "multilimits": true, - "multicolimits": true, - "multiterminal object": true, - "multiinitial object": true, + "multi-complete": true, + "multi-cocomplete": true, + "multi-terminal object": true, + "multi-initial object": true, "abelian": false, "additive": false, @@ -133,10 +133,10 @@ "finitely accessible": false, "ℵ₁-accessible": false, "generalized variety": false, - "locally finitely multipresentable": false, - "locally multipresentable": false, - "locally polypresentable": false, - "multialgebraic": false, + "locally finitely multi-presentable": false, + "locally multi-presentable": false, + "locally poly-presentable": false, + "multi-algebraic": false, "locally copresentable": false, "coaccessible": false, "countable": false, From ce5ce10b788cb945442ad644db36b46bcfb03fe1 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Mon, 13 Apr 2026 10:44:09 +0900 Subject: [PATCH 11/29] Made several changes based on suggestions. --- database/data/003_properties/008_locally-presentable.sql | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index 2145e503..4c066817 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -27,7 +27,7 @@ VALUES 'locally copresentable', 'is', 'A category is locally copresentable if its opposite category is locally presentable.', - 'https://ncatlab.org/nlab/show/locally+presentable+category', + NULL, 'locally presentable', TRUE ), @@ -67,7 +67,7 @@ VALUES 'coaccessible', 'is', 'A category is coaccessible if its opposite category is accessible.', - 'https://ncatlab.org/nlab/show/locally+presentable+category', + NULL, 'accessible', TRUE ), @@ -90,7 +90,7 @@ VALUES ( 'generalized variety', 'is a', - 'A category is a generalized variety if it has small sifted colimits and there is a (small) set $G$ of strongly finitely presentable objects such that every object is a small sifted colimit of objects from $G$. This notion is defined in [AR01, Def. 3.6].', + 'A category is a generalized variety if it has small sifted colimits and there is a (small) set $G$ of strongly finitely presentable objects such that every object is a small 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 [AR01, Def. 3.6].', NULL, NULL, TRUE @@ -106,7 +106,7 @@ VALUES ( 'locally multi-presentable', 'is', - 'Let $\kappa$ be a regular cardinal. A category is locally $\kappa$-multi-presentable if it is $\kappa$-accessible and has connected limits. It is known that a category is locally $\kappa$-multi-presentable if and only if it is equivalent to the category of models of a limit-coproduct sketch; see Thm. 4.32 in Adamek-Rosicky and the remark below. A category is called locally multi-presentable if it is locally $\kappa$-multi-presentable for some $\kappa$, equivalently, it is accessible and has connected limits.', + 'Let $\kappa$ be a regular cardinal. A category is locally $\kappa$-multi-presentable if it is $\kappa$-accessible and has connected limits. It is known that a category is locally $\kappa$-multi-presentable if and only if it is equivalent to the category of models of a limit-coproduct sketch; see Thm. 4.32 and the remark below in Adamek-Rosicky. A category is called locally multi-presentable if it is locally $\kappa$-multi-presentable for some $\kappa$, equivalently, it is accessible and has connected limits.', 'https://ncatlab.org/nlab/show/locally+multipresentable+category', NULL, TRUE From f1abd65fdbfcb57f24fcdeed71f79950cf754f52 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Mon, 13 Apr 2026 11:40:24 +0900 Subject: [PATCH 12/29] Add related pairs of properties --- .../003_properties/100_related-properties.sql | 69 ++++++++++++++++++- 1 file changed, 68 insertions(+), 1 deletion(-) diff --git a/database/data/003_properties/100_related-properties.sql b/database/data/003_properties/100_related-properties.sql index 724d263d..24b8fef4 100644 --- a/database/data/003_properties/100_related-properties.sql +++ b/database/data/003_properties/100_related-properties.sql @@ -40,22 +40,34 @@ 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', 'locally copresentable'), ('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 +82,7 @@ VALUES ('cokernels', 'conormal'), ('cocomplete', 'coequalizers'), ('cocomplete', 'coproducts'), +('cocomplete', 'multi-cocomplete'), ('products', 'complete'), ('products', 'finite products'), ('products', 'powers'), @@ -122,8 +135,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'), @@ -272,4 +291,52 @@ VALUES ('normal', 'kernels'), ('conormal', 'zero morphisms'), ('conormal', 'epi-regular'), -('conormal', 'cokernels'); \ No newline at end of file +('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', 'coaccessible'), +('ℵ₁-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'), +('locally copresentable', 'locally presentable'), +('coaccessible', 'accessible'); From f49bd9388ca7b2cb71a949277740faeeb044bc9d Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Mon, 13 Apr 2026 23:54:30 +0900 Subject: [PATCH 13/29] Fix typos --- .../data/003_properties/002_limits-colimits-existence.sql | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/003_properties/002_limits-colimits-existence.sql b/database/data/003_properties/002_limits-colimits-existence.sql index ca5b8d9b..9beaa40e 100644 --- a/database/data/003_properties/002_limits-colimits-existence.sql +++ b/database/data/003_properties/002_limits-colimits-existence.sql @@ -345,7 +345,7 @@ VALUES ), ( 'multi-complete', - 'has', + 'is', 'A multi-limit 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', @@ -353,7 +353,7 @@ VALUES ), ( 'multi-cocomplete', - 'has', + 'is', 'A multi-colimit of a diagram $D\colon \mathcal{S} \to \mathcal{C}$ is a set $I$ of cocones over $D$ such that every cocone over $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', From aeac94c8bb214cf879b3c768c1de4d8292a1e366 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Mon, 13 Apr 2026 23:55:07 +0900 Subject: [PATCH 14/29] Add an implication related to multi-completeness --- .../001_limits-colimits-existence-implications.sql | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index 25127551..00936ffd 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -313,4 +313,11 @@ VALUES '["terminal object"]', 'Let $(T_i)_{i\in I}$ be a multi-terminal object in a connected category $\mathcal{C}$. By definition of multi-terminal objects, for each object $C$, there are a unique index $i_C\in I$ and a unique morphism $C \to T_{i_C}$. Since the index $i_C$ is invariant under connected components, $I$ must be a singleton. The converse is trivial.', TRUE +), +( + 'multi-complete_with_finite_coproducts', + '["multi-complete", "finite coproducts"]', + '["complete"]', + 'Let $D\colon \mathcal{S} \to \mathcal{C}$ be a small diagram in a category $\mathcal{C}$, and let $(p^{(i)}\colon \Delta L^{(i)} \Rightarrow D)_{i\in I}$ be a multi-limit of $D$. We will show that the index set $I$ is a singleton. First, $I$ is non-empty because the diagram $D$ admits at least one cone, whose vertex is the initial object. Let $i_0, i_1 \in I$. Taking a coproduct of $L^{(i_0)}$ and $L^{(i_1)}$, we obtain a cone $p\colon \Delta (L^{(i_0)} + L^{(i_1)}) \Rightarrow D$. By the universal property of the multi-limit, there are a unique index $j\in I$ and a unique morphism $k=(k_0,k_1)\colon L^{(i_0)} + L^{(i_1)} \to L^{(j)}$ from $p$ to $p^{(j)}$. We now have morphisms $k_t$ from $p^{(i_t)}$ to $p^{(j)}$ $(t=0,1)$, but the universal property of the multi-limit forces $i_t=j$. Hence $i_0=j=i_1$, and the index set $I$ is a singleton.', + FALSE ); \ No newline at end of file From de3d3e3ff3806f56ad259e08ea0d6c58830bf63a Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Mon, 13 Apr 2026 23:55:52 +0900 Subject: [PATCH 15/29] The categories of finite algebras are countable accessible --- database/data/004_property-assignments/FinAb.sql | 6 ++++++ database/data/004_property-assignments/FinGrp.sql | 6 ++++++ database/data/004_property-assignments/FinSet.sql | 6 ++++++ 3 files changed, 18 insertions(+) diff --git a/database/data/004_property-assignments/FinAb.sql b/database/data/004_property-assignments/FinAb.sql index 7f8d58c1..0969814b 100644 --- a/database/data/004_property-assignments/FinAb.sql +++ b/database/data/004_property-assignments/FinAb.sql @@ -29,6 +29,12 @@ VALUES TRUE, 'This is a simple special case of Pontryagin duality: The functor $\hom(-,\mathbb{Q}/\mathbb{Z})$ provides the equivalence.' ), +( + 'FinAb', + 'ℵ₁-accessible', + TRUE, + 'The inclusion $\mathbf{FinAb} \hookrightarrow \mathbf{Ab}$ is closed under ℵ₁-filtered colimits, because ℵ₁-filtered colimits are computed in the same way as in $\mathbf{Set}$ and any ℵ₁-filtered colimit of finite sets is again finite. Since every finite abelian group is ℵ₁-presentable in $\mathbf{Ab}$, it is still ℵ₁-presentable in $\mathbf{FinAb}$, hence $\mathbf{FinAb}$ is ℵ₁-accessible, where every object is ℵ₁-presentable.' +), ( 'FinAb', 'small', diff --git a/database/data/004_property-assignments/FinGrp.sql b/database/data/004_property-assignments/FinGrp.sql index babb0a4f..2f70092a 100644 --- a/database/data/004_property-assignments/FinGrp.sql +++ b/database/data/004_property-assignments/FinGrp.sql @@ -59,6 +59,12 @@ VALUES TRUE, 'Since epimorphisms are surjective (see below), this is the first isomorphism theorem for finite groups.' ), +( + 'FinGrp', + 'ℵ₁-accessible', + TRUE, + 'The inclusion $\mathbf{FinGrp} \hookrightarrow \mathbf{Grp}$ is closed under ℵ₁-filtered colimits, because ℵ₁-filtered colimits are computed in the same way as in $\mathbf{Set}$ and any ℵ₁-filtered colimit of finite sets is again finite. Since every finite group is ℵ₁-presentable in $\mathbf{Grp}$, it is still ℵ₁-presentable in $\mathbf{FinGrp}$, hence $\mathbf{FinGrp}$ is ℵ₁-accessible, where every object is ℵ₁-presentable.' +), ( 'FinGrp', 'normal', diff --git a/database/data/004_property-assignments/FinSet.sql b/database/data/004_property-assignments/FinSet.sql index 642480c4..d24df1d2 100644 --- a/database/data/004_property-assignments/FinSet.sql +++ b/database/data/004_property-assignments/FinSet.sql @@ -41,6 +41,12 @@ VALUES TRUE, 'The two-element set is a cogenerator.' ), +( + 'FinSet', + 'ℵ₁-accessible', + TRUE, + 'The inclusion $\mathbf{FinSet} \hookrightarrow \mathbf{Set}$ is closed under ℵ₁-filtered colimits, that is, any ℵ₁-filtered colimit of finite sets is again finite. Since every finite set is ℵ₁-presentable in $\mathbf{Set}$, it is still ℵ₁-presentable in $\mathbf{FinSet}$. Therefore, $\mathbf{FinSet}$ is ℵ₁-accessible, where every object is ℵ₁-presentable.' +), ( 'FinSet', 'small', From c946ffca8343f650d7278a9a1a0210620534d589 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Tue, 14 Apr 2026 00:43:35 +0900 Subject: [PATCH 16/29] Resolve errors --- database/data/004_property-assignments/0.sql | 6 ++++++ database/data/004_property-assignments/1.sql | 6 ++++++ database/data/004_property-assignments/2.sql | 6 ++++++ database/data/004_property-assignments/Top_pointed.sql | 6 ++++++ database/data/004_property-assignments/walking_morphism.sql | 6 ++++++ 5 files changed, 30 insertions(+) diff --git a/database/data/004_property-assignments/0.sql b/database/data/004_property-assignments/0.sql index cbbe1462..e15b2183 100644 --- a/database/data/004_property-assignments/0.sql +++ b/database/data/004_property-assignments/0.sql @@ -29,6 +29,12 @@ VALUES TRUE, 'This is trivial.' ), +( + '0', + 'small', + TRUE, + 'This is trivial.' +), ( '0', 'multi-algebraic', diff --git a/database/data/004_property-assignments/1.sql b/database/data/004_property-assignments/1.sql index dede0a97..050857b4 100644 --- a/database/data/004_property-assignments/1.sql +++ b/database/data/004_property-assignments/1.sql @@ -17,6 +17,12 @@ VALUES TRUE, 'This is trivial.' ), +( + '1', + 'small', + TRUE, + 'This is trivial.' +), ( '1', 'discrete', diff --git a/database/data/004_property-assignments/2.sql b/database/data/004_property-assignments/2.sql index 266543cb..74bf9fd8 100644 --- a/database/data/004_property-assignments/2.sql +++ b/database/data/004_property-assignments/2.sql @@ -17,6 +17,12 @@ VALUES TRUE, 'This is trivial.' ), +( + '2', + 'small', + TRUE, + 'This is trivial.' +), ( '2', 'inhabited', diff --git a/database/data/004_property-assignments/Top_pointed.sql b/database/data/004_property-assignments/Top_pointed.sql index 9709b606..f236cda3 100644 --- a/database/data/004_property-assignments/Top_pointed.sql +++ b/database/data/004_property-assignments/Top_pointed.sql @@ -130,6 +130,12 @@ VALUES 'regular quotient object classifier', FALSE, 'We can recycle the proof for the category of pointed sets using discrete topological spaces.' +), +( + 'Top*', + 'coaccessible', + FALSE, + 'We can adjust the proof for $\mathbf{Top}$ as follows: Assume $\mathbf{Top}_*$ is coaccessible. Let $S_0=\{x,*\}$ be the pointed topological space such that $\{*\}$ is the only non-trivial open set, and let $S_1=\{x,*\}$ be the pointed space such that $\{x\}$ is the only non-trivial open set. Let $p_i\colon S_i \to \{x,*\}$ be the identity function to the two-element indiscrete pointed space. Then, a pointed topological space is discrete if and only if it is projective to the morphisms $p_0$ and $p_1$. This implies that the full subcategory spanned by all discrete pointed spaces, which is equivalent to $\mathbf{Set}_*$, is coaccessible by Prop. 4.7 in Adamek-Rosicky. However, since $\mathbf{Set}_*$ is not coaccessible, this is a contradiction.' ); diff --git a/database/data/004_property-assignments/walking_morphism.sql b/database/data/004_property-assignments/walking_morphism.sql index 73c9607b..89328cd8 100644 --- a/database/data/004_property-assignments/walking_morphism.sql +++ b/database/data/004_property-assignments/walking_morphism.sql @@ -23,6 +23,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_morphism', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_morphism', 'infinitary distributive', From c4ba4ed43251c07e46672962b9cea04d1696b317 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Wed, 15 Apr 2026 01:23:13 +0900 Subject: [PATCH 17/29] Add more explanations to "multi-algebraic" and "lsfp" --- .../data/003_properties/008_locally-presentable.sql | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index 4c066817..df8c9c4b 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -47,6 +47,7 @@ VALUES

      1. It is equivalent to the category of models of a many-sorted finitary algebraic theory.
      2. It is equivalent to the category of finite-product-preserving functors to $\mathbf{Set}$ from a small category with finite products (=Lawvere theory).
        3. +
      3. It is equivalent to the category of models of a finite-product sketch.
      4. It is equivalent to the Eilenberg–Moore category of a finitary (=filtered-colimit-preserving) monad on $\mathbf{Set}^S$ for some set $S$.
      5. 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])
      @@ -98,7 +99,16 @@ VALUES ( 'multi-algebraic', 'is', - 'A category is multi-algebraic if it is equivalent to the category of models of an FPC-sketch, where FPC represents finite products and small coproducts. This notion was introduced by Diers.', + 'A category is multi-algebraic if it satisfies one of the following equivalent conditions: +
        +
      1. 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 small sifted colimit of objects from $G$.
        2. +
      2. It is equivalent to the category of models of a (finite product, small coproduct)-sketch, shortly FPC-sketch.
        3. +
      3. It is equivalent to the category of multi-finite-product-preserving functors to $\mathbf{Set}$ from a small category with multi-finite-products (multi-algebraic theory>). Here, multi-finite-products means multi-limits of finite discrete diagrams.
        4. +
      4. It is equivalent to the category of models of a multi-finite-product sketch.
        5. +
      + Multi-algebraic categories are like locally strongly finitely presentable category 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 [AR01a, Lem. 1] and [AR01b, Thm. 4.4]. + This notion was originally introduced by Diers.', NULL, NULL, TRUE From 449e5df7808b0503de04a3c6dfcba65178e8a5ee Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Wed, 15 Apr 2026 01:23:32 +0900 Subject: [PATCH 18/29] The walking span is multi-algebraic --- database/data/004_property-assignments/walking_span.sql | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/database/data/004_property-assignments/walking_span.sql b/database/data/004_property-assignments/walking_span.sql index 7583e21c..97618e02 100644 --- a/database/data/004_property-assignments/walking_span.sql +++ b/database/data/004_property-assignments/walking_span.sql @@ -41,6 +41,12 @@ VALUES TRUE, 'The slice category over $0$ is the trivial category, and the slice category over $1$ is the interval category, which is cartesian closed (see there). The same holds for $2$ by symmetry.' ), +( + 'walking_span', + 'multi-algebraic', + TRUE, + 'We first remark that for a set $X$, the identity span $(\mathrm{id},\mathrm{id})\colon X \leftarrow X \rightarrow X$ exhibits a product if and only if $X$ is either a singleton or the empty set. Therefore, there is a (finite product, coproduct)-sketch whose $\mathbf{Set}$-model is precisely a pair $(X,Y)$ of sets such that each of $X$ and $Y$ is either a singleton or the empty set and the product $X \times Y$ is the empty set. Any $\mathbf{Set}$-model of such a sketch is isomorphic to either $(\varnothing, \varnothing)$, $(\varnothing, 1)$, or $(1, \varnothing)$; hence the category of models is equivalent to the walking span.' +), ( 'walking_span', 'sifted', From f333ab1247c560ea1da628ea0f0ea7432f35139c Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Wed, 15 Apr 2026 10:27:32 +0900 Subject: [PATCH 19/29] Make changes following suggestions --- database/data/003_properties/100_related-properties.sql | 6 +----- .../001_limits-colimits-existence-implications.sql | 2 +- .../006_trivial-categories-implications.sql | 7 +++++++ 3 files changed, 9 insertions(+), 6 deletions(-) diff --git a/database/data/003_properties/100_related-properties.sql b/database/data/003_properties/100_related-properties.sql index 24b8fef4..d1fb6c57 100644 --- a/database/data/003_properties/100_related-properties.sql +++ b/database/data/003_properties/100_related-properties.sql @@ -51,7 +51,6 @@ VALUES ('locally presentable', 'accessible'), ('locally presentable', 'locally multi-presentable'), ('locally presentable', 'locally poly-presentable'), -('locally presentable', 'locally copresentable'), ('locally ℵ₁-presentable', 'cocomplete'), ('locally ℵ₁-presentable', 'locally finitely presentable'), ('locally ℵ₁-presentable', 'locally presentable'), @@ -305,7 +304,6 @@ VALUES ('accessible', 'locally presentable'), ('accessible', 'locally multi-presentable'), ('accessible', 'locally poly-presentable'), -('accessible', 'coaccessible'), ('ℵ₁-accessible', 'accessible'), ('ℵ₁-accessible', 'finitely accessible'), ('ℵ₁-accessible', 'locally ℵ₁-presentable'), @@ -337,6 +335,4 @@ VALUES ('multi-algebraic', 'multi-cocomplete'), ('generalized variety', 'multi-algebraic'), ('generalized variety', 'locally strongly finitely presentable'), -('generalized variety', 'sifted colimits'), -('locally copresentable', 'locally presentable'), -('coaccessible', 'accessible'); +('generalized variety', 'sifted colimits'); diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index 00936ffd..9ad97279 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -318,6 +318,6 @@ VALUES 'multi-complete_with_finite_coproducts', '["multi-complete", "finite coproducts"]', '["complete"]', - 'Let $D\colon \mathcal{S} \to \mathcal{C}$ be a small diagram in a category $\mathcal{C}$, and let $(p^{(i)}\colon \Delta L^{(i)} \Rightarrow D)_{i\in I}$ be a multi-limit of $D$. We will show that the index set $I$ is a singleton. First, $I$ is non-empty because the diagram $D$ admits at least one cone, whose vertex is the initial object. Let $i_0, i_1 \in I$. Taking a coproduct of $L^{(i_0)}$ and $L^{(i_1)}$, we obtain a cone $p\colon \Delta (L^{(i_0)} + L^{(i_1)}) \Rightarrow D$. By the universal property of the multi-limit, there are a unique index $j\in I$ and a unique morphism $k=(k_0,k_1)\colon L^{(i_0)} + L^{(i_1)} \to L^{(j)}$ from $p$ to $p^{(j)}$. We now have morphisms $k_t$ from $p^{(i_t)}$ to $p^{(j)}$ $(t=0,1)$, but the universal property of the multi-limit forces $i_t=j$. Hence $i_0=j=i_1$, and the index set $I$ is a singleton.', + 'Let $D\colon \mathcal{S} \to \mathcal{C}$ be a small diagram in a category $\mathcal{C}$. Since $\mathcal{C} has finite coproducts, the category $\mathbf{Cone}(D)$ of cones over $D$ has finite coproducts. In particular, $\mathbf{Cone}(D)$ is connected, hence a multi-terminal object in it automatically becomes a terminal object.', FALSE ); \ No newline at end of file diff --git a/database/data/005_implications/006_trivial-categories-implications.sql b/database/data/005_implications/006_trivial-categories-implications.sql index fe81e4d6..89749548 100644 --- a/database/data/005_implications/006_trivial-categories-implications.sql +++ b/database/data/005_implications/006_trivial-categories-implications.sql @@ -62,6 +62,13 @@ VALUES 'See Mac Lane, V.2, Prop. 3. The proof works for any category with products.', FALSE ), +( + 'freyd_countable', + '["essentially countable", "countable products"]', + '["thin", "products"]', + 'To see that the category is thin, use Mac Lane, V.2, Prop. 3. The proof can easily be adapted to this case. So the category is equivalent to a countable preordered set. But then products are just infima, so that repetitions of objects do not matter, and every product can be reduced to a countable one.', + FALSE +), ( 'freyd_finite', '["essentially finite", "finite products"]', From 4643987e2e436b5aec387e766364ac6da73374d1 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Wed, 15 Apr 2026 12:24:38 +0900 Subject: [PATCH 20/29] Fix typo --- .../001_limits-colimits-existence-implications.sql | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/data/005_implications/001_limits-colimits-existence-implications.sql b/database/data/005_implications/001_limits-colimits-existence-implications.sql index 9ad97279..8ef2e6c2 100644 --- a/database/data/005_implications/001_limits-colimits-existence-implications.sql +++ b/database/data/005_implications/001_limits-colimits-existence-implications.sql @@ -318,6 +318,6 @@ VALUES 'multi-complete_with_finite_coproducts', '["multi-complete", "finite coproducts"]', '["complete"]', - 'Let $D\colon \mathcal{S} \to \mathcal{C}$ be a small diagram in a category $\mathcal{C}$. Since $\mathcal{C} has finite coproducts, the category $\mathbf{Cone}(D)$ of cones over $D$ has finite coproducts. In particular, $\mathbf{Cone}(D)$ is connected, hence a multi-terminal object in it automatically becomes a terminal object.', + 'Let $D\colon \mathcal{S} \to \mathcal{C}$ be a small diagram in a category $\mathcal{C}$. Since $\mathcal{C}$ has finite coproducts, the category $\mathbf{Cone}(D)$ of cones over $D$ has finite coproducts. In particular, $\mathbf{Cone}(D)$ is connected, hence a multi-terminal object in it automatically becomes a terminal object.', FALSE ); \ No newline at end of file From 0a0652d8fd7fcf477a168461276aa2919b4919c2 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Wed, 15 Apr 2026 12:25:41 +0900 Subject: [PATCH 21/29] Assign smallness --- database/data/004_property-assignments/BG_f.sql | 6 ++++++ .../004_property-assignments/walking_commutative_square.sql | 6 ++++++ .../004_property-assignments/walking_composable_pair.sql | 6 ++++++ database/data/004_property-assignments/walking_fork.sql | 6 ++++++ .../data/004_property-assignments/walking_idempotent.sql | 6 ++++++ .../data/004_property-assignments/walking_isomorphism.sql | 6 ++++++ database/data/004_property-assignments/walking_pair.sql | 6 ++++++ database/data/004_property-assignments/walking_span.sql | 6 ++++++ 8 files changed, 48 insertions(+) diff --git a/database/data/004_property-assignments/BG_f.sql b/database/data/004_property-assignments/BG_f.sql index e5cb2916..f2fd24a6 100644 --- a/database/data/004_property-assignments/BG_f.sql +++ b/database/data/004_property-assignments/BG_f.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'BG_f', + 'small', + TRUE, + 'This is trivial.' +), ( 'BG_f', 'groupoid', diff --git a/database/data/004_property-assignments/walking_commutative_square.sql b/database/data/004_property-assignments/walking_commutative_square.sql index 86551e68..6f3f356a 100644 --- a/database/data/004_property-assignments/walking_commutative_square.sql +++ b/database/data/004_property-assignments/walking_commutative_square.sql @@ -17,6 +17,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_commutative_square', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_commutative_square', 'infinitary distributive', diff --git a/database/data/004_property-assignments/walking_composable_pair.sql b/database/data/004_property-assignments/walking_composable_pair.sql index bbc83274..d0476dba 100644 --- a/database/data/004_property-assignments/walking_composable_pair.sql +++ b/database/data/004_property-assignments/walking_composable_pair.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_composable_pair', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_composable_pair', 'semi-strongly connected', diff --git a/database/data/004_property-assignments/walking_fork.sql b/database/data/004_property-assignments/walking_fork.sql index 970f6844..9cb538b1 100644 --- a/database/data/004_property-assignments/walking_fork.sql +++ b/database/data/004_property-assignments/walking_fork.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_fork', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_fork', 'semi-strongly connected', diff --git a/database/data/004_property-assignments/walking_idempotent.sql b/database/data/004_property-assignments/walking_idempotent.sql index 9b13b5cf..37dcde65 100644 --- a/database/data/004_property-assignments/walking_idempotent.sql +++ b/database/data/004_property-assignments/walking_idempotent.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_idempotent', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_idempotent', 'generator', diff --git a/database/data/004_property-assignments/walking_isomorphism.sql b/database/data/004_property-assignments/walking_isomorphism.sql index 8bfc2e45..e11c8406 100644 --- a/database/data/004_property-assignments/walking_isomorphism.sql +++ b/database/data/004_property-assignments/walking_isomorphism.sql @@ -17,6 +17,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_isomorphism', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_isomorphism', 'skeletal', diff --git a/database/data/004_property-assignments/walking_pair.sql b/database/data/004_property-assignments/walking_pair.sql index e1c0a20b..08e119aa 100644 --- a/database/data/004_property-assignments/walking_pair.sql +++ b/database/data/004_property-assignments/walking_pair.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_pair', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_pair', 'self-dual', diff --git a/database/data/004_property-assignments/walking_span.sql b/database/data/004_property-assignments/walking_span.sql index 97618e02..90a18a94 100644 --- a/database/data/004_property-assignments/walking_span.sql +++ b/database/data/004_property-assignments/walking_span.sql @@ -11,6 +11,12 @@ VALUES TRUE, 'This is trivial.' ), +( + 'walking_span', + 'small', + TRUE, + 'This is trivial.' +), ( 'walking_span', 'skeletal', From 3005178df78e08e24d49416e941489d9ad646987 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Wed, 15 Apr 2026 12:27:03 +0900 Subject: [PATCH 22/29] Clarify sketches are small --- database/data/003_properties/008_locally-presentable.sql | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/database/data/003_properties/008_locally-presentable.sql b/database/data/003_properties/008_locally-presentable.sql index df8c9c4b..4146002f 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -47,7 +47,7 @@ VALUES
      1. It is equivalent to the category of models of a many-sorted finitary algebraic theory.
      2. It is equivalent to the category of finite-product-preserving functors to $\mathbf{Set}$ from a small category with finite products (=Lawvere theory).
        3. -
      3. It is equivalent to the category of models of a finite-product sketch.
        4. +
      4. It is equivalent to the category of models of a small finite-product sketch.
      5. It is equivalent to the Eilenberg–Moore category of a finitary (=filtered-colimit-preserving) monad on $\mathbf{Set}^S$ for some set $S$.
      6. 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])
      @@ -102,9 +102,9 @@ VALUES 'A category is multi-algebraic if it satisfies one of the following equivalent conditions:
      1. 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 small sifted colimit of objects from $G$.
        2. -
      2. It is equivalent to the category of models of a (finite product, small coproduct)-sketch, shortly FPC-sketch.
        3. +
      3. It is equivalent to the category of models of a small (finite product, small coproduct)-sketch, shortly small FPC-sketch.
      4. It is equivalent to the category of multi-finite-product-preserving functors to $\mathbf{Set}$ from a small category with multi-finite-products (multi-algebraic theory>). Here, multi-finite-products means multi-limits of finite discrete diagrams.
        5. -
      5. It is equivalent to the category of models of a multi-finite-product sketch.
        6. +
      6. It is equivalent to the category of models of a small multi-finite-product sketch.
      Multi-algebraic categories are like locally strongly finitely presentable category 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 [AR01a, Lem. 1] and [AR01b, Thm. 4.4]. @@ -116,7 +116,7 @@ VALUES ( 'locally multi-presentable', 'is', - 'Let $\kappa$ be a regular cardinal. A category is locally $\kappa$-multi-presentable if it is $\kappa$-accessible and has connected limits. It is known that a category is locally $\kappa$-multi-presentable if and only if it is equivalent to the category of models of a limit-coproduct sketch; see Thm. 4.32 and the remark below in Adamek-Rosicky. A category is called locally multi-presentable if it is locally $\kappa$-multi-presentable for some $\kappa$, equivalently, it is accessible and has connected limits.', + 'Let $\kappa$ be a regular cardinal. A category is locally $\kappa$-multi-presentable if it is $\kappa$-accessible and has connected limits. It is known that a category is locally $\kappa$-multi-presentable if and only if it is equivalent to the category of models of a small limit-coproduct sketch; see Thm. 4.32 and the remark below in Adamek-Rosicky. A category is called locally multi-presentable if it is locally $\kappa$-multi-presentable for some $\kappa$, equivalently, it is accessible and has connected limits.', 'https://ncatlab.org/nlab/show/locally+multipresentable+category', NULL, TRUE From 40d74cef7f1d3adbb5fc4066899c4ae282cfecea Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Wed, 15 Apr 2026 12:36:16 +0900 Subject: [PATCH 23/29] Change "cocone over" to "cocone under" --- database/data/003_properties/002_limits-colimits-existence.sql | 2 +- static/pdf/walking_parallel_pair_sifted_colimit.tex | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/003_properties/002_limits-colimits-existence.sql b/database/data/003_properties/002_limits-colimits-existence.sql index 9beaa40e..31424109 100644 --- a/database/data/003_properties/002_limits-colimits-existence.sql +++ b/database/data/003_properties/002_limits-colimits-existence.sql @@ -354,7 +354,7 @@ VALUES ( 'multi-cocomplete', 'is', - 'A multi-colimit of a diagram $D\colon \mathcal{S} \to \mathcal{C}$ is a set $I$ of cocones over $D$ such that every cocone over $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.', + 'A multi-colimit 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 diff --git a/static/pdf/walking_parallel_pair_sifted_colimit.tex b/static/pdf/walking_parallel_pair_sifted_colimit.tex index 9bfb0fbc..1dd1896e 100644 --- a/static/pdf/walking_parallel_pair_sifted_colimit.tex +++ b/static/pdf/walking_parallel_pair_sifted_colimit.tex @@ -101,7 +101,7 @@ $D(c)=0$ and there is a morphism from itself sent to $v$ by $D$. \end{enumerate} Now, we have a cocone $(\alpha_c\colon D(c) \to 1)_{c\in\mathcal{C}}$ over $D$ by letting $\alpha_c\coloneqq \mathrm{id}_1$ if $c$ is classified into the first case, $\alpha_c\coloneqq u$ for the second case, and $\alpha_c\coloneqq v$ for the third case. -Moreover, this is a unique cocone over $D$: +Moreover, this is a unique cocone under $D$: If $\beta$ is another cocone, its vertex should be $1$ by the existence of $c_0$. If $c\in\mathcal{C}$ is classified into the first case, $\beta_c$ should be the identity. For the second case, taking a morphism $f\colon c\to x$ such that $D(f)=u$, we can obtain $\beta_c = \beta_x \circ D(f) = D(f) = u$. From 42d8e81534b015d5f5675bfe49ba92407e2f6de1 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Wed, 15 Apr 2026 12:52:05 +0900 Subject: [PATCH 24/29] Fix typo --- 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 4146002f..b8f7ddb4 100644 --- a/database/data/003_properties/008_locally-presentable.sql +++ b/database/data/003_properties/008_locally-presentable.sql @@ -103,7 +103,7 @@ VALUES
      1. 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 small sifted colimit of objects from $G$.
      2. It is equivalent to the category of models of a small (finite product, small coproduct)-sketch, shortly small FPC-sketch.
        3. -
      3. It is equivalent to the category of multi-finite-product-preserving functors to $\mathbf{Set}$ from a small category with multi-finite-products (multi-algebraic theory>). Here, multi-finite-products means multi-limits of finite discrete diagrams.
        4. +
      4. It is equivalent to the category of multi-finite-product-preserving functors to $\mathbf{Set}$ from a small category with multi-finite-products (multi-algebraic theory). Here, multi-finite-products means multi-limits of finite discrete diagrams.
      5. It is equivalent to the category of models of a small multi-finite-product sketch.
      Multi-algebraic categories are like locally strongly finitely presentable category but only with multi-colimits. The relation is similar as between locally finitely multi-presentable and locally finitely presentable categories. From 32d6cf4e35a714b20e6fcf1bee388d9dbb26fc35 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Wed, 15 Apr 2026 15:32:37 +0900 Subject: [PATCH 25/29] Ab_fg is essentially countable --- database/data/004_property-assignments/Ab_fg.sql | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/004_property-assignments/Ab_fg.sql b/database/data/004_property-assignments/Ab_fg.sql index 4533089d..d6c7b429 100644 --- a/database/data/004_property-assignments/Ab_fg.sql +++ b/database/data/004_property-assignments/Ab_fg.sql @@ -13,9 +13,9 @@ VALUES ), ( 'Ab_fg', - 'essentially small', + 'essentially countable', TRUE, - 'Every finitely generated abelian group is isomorphic to a group of the form $\mathbb{Z}^n / U$, where $n \in \mathbb{N}$ and $U$ is a subgroup of $\mathbb{Z}^n$. And these constitute a set.' + 'Every finitely generated abelian group is isomorphic to a group of the form $\mathbb{Z}^n / U$, where $n \in \mathbb{N}$ and $U$ is a subgroup of $\mathbb{Z}^n$. Since $\mathbb{Z}^n$ is Noetherian as a $\mathbb{Z}$-module, $U$ is finitely generated, hence the category $\mathbf{Ab}_\mathrm{fg}$ has only countably many objects up to isomorphism. Furthermore, for any objects $A \cong \mathbb{Z}^n / U$ and $B \cong \mathbb{Z}^m / T$, the hom-set $\mathrm{Hom}(A,B)$ is at most countable. Indeed, precomposition with the quotient map yields an injection $\mathrm{Hom}(A,B) \hookrightarrow \mathrm{Hom}(\mathbb{Z}^n, B) \cong B^n$, and $B^n$ is at most countable.' ), ( 'Ab_fg', From 15d1710d15b4c43835a5df3b3f7ec9bde47395bc Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 08:37:51 +0200 Subject: [PATCH 26/29] Restrict G to be countable for BG --- .../data/001_categories/008_one-object.sql | 8 +++---- .../001_categories/100_related-categories.sql | 8 +++---- database/data/002_tags/002_category-tags.sql | 6 ++--- .../{BG.sql => BG_c.sql} | 24 +++++++++---------- .../002_isomorphisms.sql | 2 +- .../003_monomorphisms.sql | 2 +- .../004_epimorphisms.sql | 2 +- .../005_regular-monomorphisms.sql | 2 +- .../006_regular-epimorphisms.sql | 2 +- 9 files changed, 28 insertions(+), 28 deletions(-) rename database/data/004_property-assignments/{BG.sql => BG_c.sql} (79%) diff --git a/database/data/001_categories/008_one-object.sql b/database/data/001_categories/008_one-object.sql index cfad9bca..74de146d 100644 --- a/database/data/001_categories/008_one-object.sql +++ b/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 ), diff --git a/database/data/001_categories/100_related-categories.sql b/database/data/001_categories/100_related-categories.sql index 19d5395e..bf017838 100644 --- a/database/data/001_categories/100_related-categories.sql +++ b/database/data/001_categories/100_related-categories.sql @@ -13,11 +13,11 @@ VALUES ('Alg(R)', 'Ring'), ('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)'), diff --git a/database/data/002_tags/002_category-tags.sql b/database/data/002_tags/002_category-tags.sql index c501eacd..e48f0b91 100644 --- a/database/data/002_tags/002_category-tags.sql +++ b/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'), diff --git a/database/data/004_property-assignments/BG.sql b/database/data/004_property-assignments/BG_c.sql similarity index 79% rename from database/data/004_property-assignments/BG.sql rename to database/data/004_property-assignments/BG_c.sql index dedf3ec9..61864e12 100644 --- a/database/data/004_property-assignments/BG.sql +++ b/database/data/004_property-assignments/BG_c.sql @@ -6,43 +6,43 @@ INSERT INTO category_property_assignments ( ) VALUES ( - 'BG', + 'BG_c', + 'countable', + TRUE, + 'This is because $G$ is countable.' +), +( + 'BG_c', 'small', TRUE, 'This is trivial.' ), ( - 'BG', + 'BG_c', 'groupoid', TRUE, 'This is trivial.' ), ( - 'BG', + 'BG_c', 'connected', TRUE, 'This is trivial.' ), ( - 'BG', + 'BG_c', 'generator', TRUE, 'The unique object is a generator for trivial reasons.' ), ( - 'BG', + 'BG_c', 'skeletal', TRUE, 'There is just one object.' ), ( - 'BG', - 'trivial', - FALSE, - 'This is trivial.' -), -( - 'BG', + 'BG_c', 'essentially finite', FALSE, 'This is because we choose $G$ to be infinite.' diff --git a/database/data/007_special-morphisms/002_isomorphisms.sql b/database/data/007_special-morphisms/002_isomorphisms.sql index ad35047e..8d26b09e 100644 --- a/database/data/007_special-morphisms/002_isomorphisms.sql +++ b/database/data/007_special-morphisms/002_isomorphisms.sql @@ -51,7 +51,7 @@ VALUES 'This is easy.' ), ( - 'BG', + 'BG_c', 'every morphism', 'It is a groupoid.' ), diff --git a/database/data/007_special-morphisms/003_monomorphisms.sql b/database/data/007_special-morphisms/003_monomorphisms.sql index d4ff8f88..4691ed66 100644 --- a/database/data/007_special-morphisms/003_monomorphisms.sql +++ b/database/data/007_special-morphisms/003_monomorphisms.sql @@ -51,7 +51,7 @@ VALUES 'The unit ball functor $U : \mathbf{Ban} \to \mathbf{Set}$ is faithful and representable (by $\mathbb{C}$), hence reflects and preserves monomorphisms.' ), ( - 'BG', + 'BG_c', 'every morphism', 'This is trivial.' ), diff --git a/database/data/007_special-morphisms/004_epimorphisms.sql b/database/data/007_special-morphisms/004_epimorphisms.sql index f594003e..e3c23503 100644 --- a/database/data/007_special-morphisms/004_epimorphisms.sql +++ b/database/data/007_special-morphisms/004_epimorphisms.sql @@ -46,7 +46,7 @@ VALUES 'Let $f : X \to Y$ be an epimorphism of Banach spaces. The subspace $U := \overline{f(X)} \subseteq Y$ is closed. It is well-known that the quotient $Y/U$ is also a Banach space with a projection $p : Y \to Y/U$. Since $p \circ f = 0 = 0 \circ f$, we infer $p = 0$, so that $U = Y$.' ), ( - 'BG', + 'BG_c', 'every morphism', 'This holds because it is a groupoid.' ), diff --git a/database/data/007_special-morphisms/005_regular-monomorphisms.sql b/database/data/007_special-morphisms/005_regular-monomorphisms.sql index 2939dc7e..6934da0f 100644 --- a/database/data/007_special-morphisms/005_regular-monomorphisms.sql +++ b/database/data/007_special-morphisms/005_regular-monomorphisms.sql @@ -41,7 +41,7 @@ VALUES 'This is because the category is mono-regular.' ), ( - 'BG', + 'BG_c', 'same as monomorphisms', 'This is because the category is mono-regular.' ), diff --git a/database/data/007_special-morphisms/006_regular-epimorphisms.sql b/database/data/007_special-morphisms/006_regular-epimorphisms.sql index db8de608..6ba4c5a9 100644 --- a/database/data/007_special-morphisms/006_regular-epimorphisms.sql +++ b/database/data/007_special-morphisms/006_regular-epimorphisms.sql @@ -46,7 +46,7 @@ VALUES 'This is because the category is epi-regular.' ), ( - 'BG', + 'BG_c', 'same as isomorphisms', 'This is because the category is left cancellative.' ), From 555afe6a729696b93df9f6a4aa23be1325e9330c Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 09:00:14 +0200 Subject: [PATCH 27/29] countable sets can be finite, so we don't need to say "at most" here --- database/data/004_property-assignments/Ab_fg.sql | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/database/data/004_property-assignments/Ab_fg.sql b/database/data/004_property-assignments/Ab_fg.sql index d6c7b429..c0450466 100644 --- a/database/data/004_property-assignments/Ab_fg.sql +++ b/database/data/004_property-assignments/Ab_fg.sql @@ -15,7 +15,7 @@ VALUES 'Ab_fg', 'essentially countable', TRUE, - 'Every finitely generated abelian group is isomorphic to a group of the form $\mathbb{Z}^n / U$, where $n \in \mathbb{N}$ and $U$ is a subgroup of $\mathbb{Z}^n$. Since $\mathbb{Z}^n$ is Noetherian as a $\mathbb{Z}$-module, $U$ is finitely generated, hence the category $\mathbf{Ab}_\mathrm{fg}$ has only countably many objects up to isomorphism. Furthermore, for any objects $A \cong \mathbb{Z}^n / U$ and $B \cong \mathbb{Z}^m / T$, the hom-set $\mathrm{Hom}(A,B)$ is at most countable. Indeed, precomposition with the quotient map yields an injection $\mathrm{Hom}(A,B) \hookrightarrow \mathrm{Hom}(\mathbb{Z}^n, B) \cong B^n$, and $B^n$ is at most countable.' + 'Every finitely generated abelian group is isomorphic to a group of the form $\mathbb{Z}^n / U$, where $n \in \mathbb{N}$ and $U$ is a subgroup of $\mathbb{Z}^n$. Since $\mathbb{Z}^n$ is Noetherian as a $\mathbb{Z}$-module, $U$ is finitely generated, hence the category $\mathbf{Ab}_\mathrm{fg}$ has only countably many objects up to isomorphism. Furthermore, for any objects $A \cong \mathbb{Z}^n / U$ and $B \cong \mathbb{Z}^m / T$, the hom-set $\mathrm{Hom}(A,B)$ is countable. Indeed, precomposition with the quotient map yields an injection $\mathrm{Hom}(A,B) \hookrightarrow \mathrm{Hom}(\mathbb{Z}^n, B) \cong B^n$, and $B^n$ is countable.' ), ( 'Ab_fg', From 258fa8f437c0aec78d93a8fbf5c4b06c35e553fc Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 15 Apr 2026 09:03:38 +0200 Subject: [PATCH 28/29] expand dictionary --- .vscode/settings.json | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index 1fd0af92..c6dd522e 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -17,7 +17,8 @@ "Prost", "SetxSet", "hilberts", - "maxage" + "maxage", + "ndash" ], "cSpell.words": [ "abelian", @@ -39,6 +40,7 @@ "catdat", "clopen", "Clowder", + "coaccessible", "cocartesian", "coclosed", "cocomplete", @@ -70,6 +72,7 @@ "conormal", "copower", "copowers", + "copresentable", "coprime", "coproduct", "coproducts", @@ -92,6 +95,7 @@ "diffeomorphisms", "dualizable", "Dualization", + "Eilenberg", "Engelking", "epimorphic", "epimorphism", @@ -124,6 +128,7 @@ "Kashiwara", "katex", "Kolmogorov", + "Lawvere", "lextensive", "libsql", "Lindelöf", @@ -141,6 +146,7 @@ "Niefield", "nilradical", "nlab", + "Noetherian", "objectwise", "pointwise", "Pontryagin", @@ -148,6 +154,7 @@ "posets", "preadditive", "precomposed", + "precomposition", "preimage", "preimages", "preordered", From f5b35438d8ffb5fbef4da7036bfe08fe70d70e73 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Wed, 15 Apr 2026 18:31:02 +0900 Subject: [PATCH 29/29] Remove the property assignment to Set-op and refine "locally_presentable_thin" --- database/data/004_property-assignments/Set_op.sql | 13 ------------- .../007_locally-presentable-implications.sql | 4 ++-- 2 files changed, 2 insertions(+), 15 deletions(-) delete mode 100644 database/data/004_property-assignments/Set_op.sql diff --git a/database/data/004_property-assignments/Set_op.sql b/database/data/004_property-assignments/Set_op.sql deleted file mode 100644 index d834262b..00000000 --- a/database/data/004_property-assignments/Set_op.sql +++ /dev/null @@ -1,13 +0,0 @@ -INSERT INTO category_property_assignments ( - category_id, - property_id, - is_satisfied, - reason -) -VALUES -( - 'Set_op', - 'accessible', - FALSE, - '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/005_implications/007_locally-presentable-implications.sql b/database/data/005_implications/007_locally-presentable-implications.sql index dd7e2ad9..c375ab86 100644 --- a/database/data/005_implications/007_locally-presentable-implications.sql +++ b/database/data/005_implications/007_locally-presentable-implications.sql @@ -49,9 +49,9 @@ VALUES FALSE ), ( - 'locally_presentable_thin', + 'locally_presentable_essentially_small', '["locally presentable", "locally copresentable"]', - '["thin"]', + '["essentially small"]', 'This follows from Adamek-Rosicky, Thm. 1.64.', FALSE ),