From 9a8315aa6a783e44a9d1ac95905e183afaf2ec53 Mon Sep 17 00:00:00 2001 From: ykawase5048 Date: Fri, 17 Jul 2026 19:37:54 +0900 Subject: [PATCH 1/4] Determine some accessibilities of Met --- database/data/categories/Met.yaml | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index 942abdf78..1535301d7 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -68,6 +68,18 @@ satisfied_properties: - property: well-copowered proof: 'If $f : X \to Y$ is an epimorphism, then $f(X)$ is dense in $Y$ (see below). Hence, there is an injective map $Y \to X^{\IN}$, which bounds the size of $Y$.' + - property: ℵ₁-accessible + proof: >- + For $\alpha=n$ or $\alpha=\infty$, let $I_\alpha$ denote the metric space (with $\infty$ allowed) consisting of exactly two points at distance $\alpha$. + Let $e_n\colon I_\infty \to I_n$ be the identity-on-points morphism in $\Met_\infty$. + Then, the category $\Met$ is precisely the cone-injectivity class with respect to the cone $\{e_n\}_{n\in\mathbb{N}}$ (cf. Section 4.B of Adamek-Rosicky), that is, $M\in\Met_\infty$ belongs to $\Met$ iff every morphism $I_\infty \to M$ is factorized by some $e_n$. + (This implies $\Met$ is accessible, but an additional argument below is needed to show $\aleph_1$-accessibility.) + + It is known that an object in $\Met_\infty$ is $\aleph_1$-presentable iff the underlying set is countable (see Lem. 2.6 in AR22). + In particular, the metric spaces $I_\alpha$ are $\aleph_1$-presentable in $\Met_\infty$, which straightforwardly implies that the cone-injectivity class $\Met\subseteq\Met_\infty$ is closed under $\aleph_1$-filtered colimits. + Then, countable metric spaces in $\Met$ are $\aleph_1$-presentable not only in $\Met_\infty$. + On the other hand, every object in $\Met_\infty$ is an $\aleph_1$-filtered colimit of its countable isometric subspaces, and the same is true in $\Met$. + Hence, $\Met$ is ℵ₁-accessible. unsatisfied_properties: - property: skeletal proof: This is trivial. @@ -120,6 +132,18 @@ unsatisfied_properties: - property: regular proof: We can take the same counterexample as for $\PMet$. + - property: finitely accessible + proof: >- + The following proof is due to Rem. 2.7 in AR22. + Consider a sequence $I_1 \to I_{\frac{1}{2}} \to I_\frac{1}{3} \to\cdots$ in $\Met$, where $I_{\frac{1}{n}}$ is the metric space consisting of exactly two points at distance $\frac{1}{n}$, and where each morphism in the sequence is the identity on the underlying set. + While the (filtered) colimit of the sequence is the singleton, for every non-empty metric space $M\in\Met$, the colimit $\colim_n \Hom(M,I_{\frac{1}{n}})$ has at least two distinct element. + Hence, $M\in\Met$ is finitely presentable iff it is empty. + Clearly, non-empty metric spaces are never filtered colimits of the empty one; hence $\Met$ is not finitely accessible. + + - property: generalized variety + proof: >- + Since every filtered colimit are in particular sifted and every strongly finitely presentable object is finitely presentable, the same argument showing that $\Met$ is not finitely accessible still works in this case. + special_objects: initial object: description: empty metric space From 3368f0a1840f5b534af17c7a016ffc69b0e0908a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Fri, 17 Jul 2026 16:48:19 +0200 Subject: [PATCH 2/4] revise proofs for accessibility of metric spaces --- database/data/categories/Met.yaml | 43 ++++++++++++++----------------- 1 file changed, 20 insertions(+), 23 deletions(-) diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index 1535301d7..c72dbf1fb 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -62,24 +62,19 @@ satisfied_properties: $$d(x_j,y_j) \geq d(x_{i_n},y_{i_n}) \geq n$$ for every $n \in \IN$. This is impossible since the metric on $D(j)$ takes only finite values. - - property: well-powered - proof: This follows since monomorphisms are injective. - - property: well-copowered proof: 'If $f : X \to Y$ is an epimorphism, then $f(X)$ is dense in $Y$ (see below). Hence, there is an injective map $Y \to X^{\IN}$, which bounds the size of $Y$.' - property: ℵ₁-accessible proof: >- For $\alpha=n$ or $\alpha=\infty$, let $I_\alpha$ denote the metric space (with $\infty$ allowed) consisting of exactly two points at distance $\alpha$. - Let $e_n\colon I_\infty \to I_n$ be the identity-on-points morphism in $\Met_\infty$. - Then, the category $\Met$ is precisely the cone-injectivity class with respect to the cone $\{e_n\}_{n\in\mathbb{N}}$ (cf. Section 4.B of Adamek-Rosicky), that is, $M\in\Met_\infty$ belongs to $\Met$ iff every morphism $I_\infty \to M$ is factorized by some $e_n$. - (This implies $\Met$ is accessible, but an additional argument below is needed to show $\aleph_1$-accessibility.) + Let $e_n : I_\infty \to I_n$ be the identity-on-points morphism in $\Met_\infty$. Then $M \in \Met_\infty$ belongs to $\Met$ iff every morphism $I_\infty \to M$ factors through some $e_n$. In other words, using the terminology from Section 4.B of Adamek-Rosicky, the category $\Met$ is precisely the cone-injectivity class with respect to the cone $(e_n)_{n \in \IN}$ in $\Met_\infty$. Since $\Met_\infty$ is accessible, this already implies that $\Met$ is accessible by Prop. 4.16 in loc. cit., but an additional argument below is needed to show $\aleph_1$-accessibility. - It is known that an object in $\Met_\infty$ is $\aleph_1$-presentable iff the underlying set is countable (see Lem. 2.6 in AR22). - In particular, the metric spaces $I_\alpha$ are $\aleph_1$-presentable in $\Met_\infty$, which straightforwardly implies that the cone-injectivity class $\Met\subseteq\Met_\infty$ is closed under $\aleph_1$-filtered colimits. - Then, countable metric spaces in $\Met$ are $\aleph_1$-presentable not only in $\Met_\infty$. + It is known that an object in $\Met_\infty$ is $\aleph_1$-presentable iff the underlying set is countable (see Lem. 2.6 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky). + In particular, the metric space $I_\infty$ is $\aleph_1$-presentable in $\Met_\infty$, which straightforwardly implies that the cone-injectivity class $\Met\subseteq\Met_\infty$ is closed under $\aleph_1$-filtered colimits. + Then, countable metric spaces in $\Met$ are $\aleph_1$-presentable not only in $\Met_\infty$, but also in $\Met$. On the other hand, every object in $\Met_\infty$ is an $\aleph_1$-filtered colimit of its countable isometric subspaces, and the same is true in $\Met$. - Hence, $\Met$ is ℵ₁-accessible. + Hence, $\Met$ is $\aleph_1$-accessible. unsatisfied_properties: - property: skeletal proof: This is trivial. @@ -109,7 +104,21 @@ unsatisfied_properties: proof: This is proven in MSE/5131457. - property: filtered-colimit-stable monomorphisms - proof: 'The following example is taken from Remark 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky: For $n \geq 1$ let $X_n$ denote the metric space with underlying set $\{0,1\}$ in which $0,1$ have distance $1/n$. We have bijective non-expansive maps $X_n \to X_{n+1}$, $x \mapsto x$. The colimit of this sequence in $\PMet$ is $\{0,1\}$ where $0,1$ have distance $0$, so the colimit in $\Met$ collapses to $\{0\}$. Therefore, the colimit of the monomorphisms $X_0 \to X_n$, $x \mapsto x$ is the non-injective map $X_0 \to \{0\}$.' + proof: >- + The following example is taken from Rem. 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky. + For $n \geq 1$ let $X_n$ denote the metric space with underlying set $\{0,1\}$ in which $0,1$ have distance $1/n$. We have bijective non-expansive maps $X_n \to X_{n+1}$, $x \mapsto x$. The colimit of this sequence in $\PMet$ is $\{0,1\}$ where $0,1$ have distance $0$, so the colimit in $\Met$ collapses to $\{0\}$. Therefore, the colimit of the monomorphisms $X_1 \to X_n$, $x \mapsto x$ is the non-injective map $X_1 \to \{0\}$. + + - property: finitely accessible + proof: >- + The following proof is due to Rem. 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky. + For $n \geq 1$ let $X_n$ denote the metric space with underlying set $\{0,1\}$ in which $0,1$ have distance $1/n$. Consider the sequence of identity-on-points maps + $$X_1 \to X_2 \to X_3 \to \cdots$$ + in $\Met$. We already saw above that the colimit of this sequence is the singleton space. Hence, for every metric space $M$, the set $\Hom(M,\colim_n X_n)$ is a singleton set. But if $M$ is non-empty, the colimit $\colim_n \Hom(M,X_n)$ has at least two distinct elements (consider the two constant maps $0,1 : M \rightrightarrows X_1$). + Hence, $M \in \Met$ is finitely presentable iff it is empty. + Clearly, a non-empty metric space is never a filtered colimit of the empty one; hence $\Met$ is not finitely accessible. + + - property: generalized variety + proof: 'We have just proven that every finitely presentable object is empty. It follows that also every strongly finitely presentable object is empty. Clearly, a non-empty metric space is never a sifted colimit of the empty one; hence $\Met$ is not a generalized variety.' - property: natural numbers object proof: >- @@ -132,18 +141,6 @@ unsatisfied_properties: - property: regular proof: We can take the same counterexample as for $\PMet$. - - property: finitely accessible - proof: >- - The following proof is due to Rem. 2.7 in AR22. - Consider a sequence $I_1 \to I_{\frac{1}{2}} \to I_\frac{1}{3} \to\cdots$ in $\Met$, where $I_{\frac{1}{n}}$ is the metric space consisting of exactly two points at distance $\frac{1}{n}$, and where each morphism in the sequence is the identity on the underlying set. - While the (filtered) colimit of the sequence is the singleton, for every non-empty metric space $M\in\Met$, the colimit $\colim_n \Hom(M,I_{\frac{1}{n}})$ has at least two distinct element. - Hence, $M\in\Met$ is finitely presentable iff it is empty. - Clearly, non-empty metric spaces are never filtered colimits of the empty one; hence $\Met$ is not finitely accessible. - - - property: generalized variety - proof: >- - Since every filtered colimit are in particular sifted and every strongly finitely presentable object is finitely presentable, the same argument showing that $\Met$ is not finitely accessible still works in this case. - special_objects: initial object: description: empty metric space From 972d8c188870f203cb89b5e3e0aef29c1f216b36 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 18 Jul 2026 12:10:59 +0200 Subject: [PATCH 3/4] finitely accessible categories have filtered-colimit-stable monos --- database/data/categories/Met.yaml | 9 --------- database/data/categories/Setne.yaml | 3 --- database/data/category-implications/accessible.yaml | 8 ++++++++ 3 files changed, 8 insertions(+), 12 deletions(-) diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index c72dbf1fb..5a95f6496 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -108,15 +108,6 @@ unsatisfied_properties: The following example is taken from Rem. 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky. For $n \geq 1$ let $X_n$ denote the metric space with underlying set $\{0,1\}$ in which $0,1$ have distance $1/n$. We have bijective non-expansive maps $X_n \to X_{n+1}$, $x \mapsto x$. The colimit of this sequence in $\PMet$ is $\{0,1\}$ where $0,1$ have distance $0$, so the colimit in $\Met$ collapses to $\{0\}$. Therefore, the colimit of the monomorphisms $X_1 \to X_n$, $x \mapsto x$ is the non-injective map $X_1 \to \{0\}$. - - property: finitely accessible - proof: >- - The following proof is due to Rem. 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky. - For $n \geq 1$ let $X_n$ denote the metric space with underlying set $\{0,1\}$ in which $0,1$ have distance $1/n$. Consider the sequence of identity-on-points maps - $$X_1 \to X_2 \to X_3 \to \cdots$$ - in $\Met$. We already saw above that the colimit of this sequence is the singleton space. Hence, for every metric space $M$, the set $\Hom(M,\colim_n X_n)$ is a singleton set. But if $M$ is non-empty, the colimit $\colim_n \Hom(M,X_n)$ has at least two distinct elements (consider the two constant maps $0,1 : M \rightrightarrows X_1$). - Hence, $M \in \Met$ is finitely presentable iff it is empty. - Clearly, a non-empty metric space is never a filtered colimit of the empty one; hence $\Met$ is not finitely accessible. - - property: generalized variety proof: 'We have just proven that every finitely presentable object is empty. It follows that also every strongly finitely presentable object is empty. Clearly, a non-empty metric space is never a sifted colimit of the empty one; hence $\Met$ is not a generalized variety.' diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index 136deb47b..353a88b24 100644 --- a/database/data/categories/Setne.yaml +++ b/database/data/categories/Setne.yaml @@ -50,9 +50,6 @@ satisfied_properties: - property: natural numbers object proof: Any natural numbers object in $\Set$, such as $(\IN,0,n \mapsto n+1)$, is clearly also one in $\Setne$. - - property: filtered-colimit-stable monomorphisms - proof: This follows from Lemma 2 here applied to the forgetful functor to $\Set$. - - property: multi-complete proof: Let $D$ be a diagram in $\Setne$, and let $L$ be a limit of $D$ in $\Set$. If $L$ is non-empty, it gives a limit in $\Setne$ as well. If $L$ is the empty set, there is no cone over $D$ in $\Setne$; hence the empty set of cones gives a multi-limit of $D$ in $\Setne$. diff --git a/database/data/category-implications/accessible.yaml b/database/data/category-implications/accessible.yaml index 94033586c..6f4d89241 100644 --- a/database/data/category-implications/accessible.yaml +++ b/database/data/category-implications/accessible.yaml @@ -36,6 +36,14 @@ proof: Special case of Adamek-Rosicky, Prop. 1.59 with $\lambda = \aleph_0$. is_equivalence: false +- id: finitely_accessible_stable_monos + assumptions: + - finitely accessible + conclusions: + - filtered-colimit-stable monomorphisms + proof: 'Let $\C$ be a finitely accessible category and let $\C_{\fp}$ be its full subcategory of finitely presentable objects. Consider the restricted Yoneda embedding $\C \hookrightarrow [\C_{\fp}^{\op},\Set]$. It preserves filtered colimits (essentially by the definition of a finitely presentable object) and all limits, in particular monomorphisms. It also reflects monomorphisms since $\C_{\fp}$ is a generating set. Therefore, since $\Set$ and hence the functor category has filtered-colimit-stable monomorphisms, this is also true for $\C$.' + is_equivalence: false + - id: locally_finitely_presentable_raise assumptions: - locally finitely presentable From 7bd0674713e4e0dd832e63e296e452c44b890e4a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 19 Jul 2026 09:16:44 +0200 Subject: [PATCH 4/4] generalized varieties have filtered-colimit-stable monos --- database/data/categories/Met.yaml | 3 --- database/data/category-implications/accessible.yaml | 2 +- database/data/category-implications/algebraic.yaml | 8 ++++++++ 3 files changed, 9 insertions(+), 4 deletions(-) diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index 5a95f6496..c6d342ccc 100644 --- a/database/data/categories/Met.yaml +++ b/database/data/categories/Met.yaml @@ -108,9 +108,6 @@ unsatisfied_properties: The following example is taken from Rem. 2.7 in Approximate injectivity and smallness in metric-enriched categories by Adamek-Rosicky. For $n \geq 1$ let $X_n$ denote the metric space with underlying set $\{0,1\}$ in which $0,1$ have distance $1/n$. We have bijective non-expansive maps $X_n \to X_{n+1}$, $x \mapsto x$. The colimit of this sequence in $\PMet$ is $\{0,1\}$ where $0,1$ have distance $0$, so the colimit in $\Met$ collapses to $\{0\}$. Therefore, the colimit of the monomorphisms $X_1 \to X_n$, $x \mapsto x$ is the non-injective map $X_1 \to \{0\}$. - - property: generalized variety - proof: 'We have just proven that every finitely presentable object is empty. It follows that also every strongly finitely presentable object is empty. Clearly, a non-empty metric space is never a sifted colimit of the empty one; hence $\Met$ is not a generalized variety.' - - property: natural numbers object proof: >- If $(N,z,s)$ is a natural numbers object in $\Met$, then diff --git a/database/data/category-implications/accessible.yaml b/database/data/category-implications/accessible.yaml index 6f4d89241..9e8b77193 100644 --- a/database/data/category-implications/accessible.yaml +++ b/database/data/category-implications/accessible.yaml @@ -41,7 +41,7 @@ - finitely accessible conclusions: - filtered-colimit-stable monomorphisms - proof: 'Let $\C$ be a finitely accessible category and let $\C_{\fp}$ be its full subcategory of finitely presentable objects. Consider the restricted Yoneda embedding $\C \hookrightarrow [\C_{\fp}^{\op},\Set]$. It preserves filtered colimits (essentially by the definition of a finitely presentable object) and all limits, in particular monomorphisms. It also reflects monomorphisms since $\C_{\fp}$ is a generating set. Therefore, since $\Set$ and hence the functor category has filtered-colimit-stable monomorphisms, this is also true for $\C$.' + proof: 'Let $\C$ be a finitely accessible category and let $G$ be a set of finitely presentable objects which generates $\C$ under filtered colimits. Consider $G$ as a full subcategory and consider the restricted Yoneda embedding $\C \hookrightarrow [G^{\op},\Set]$. It preserves filtered colimits (essentially by the definition of a finitely presentable object) and all limits, in particular monomorphisms. It also reflects monomorphisms since $G$ is a generating set. Therefore, since $\Set$ and hence the functor category has filtered-colimit-stable monomorphisms, this is also true for $\C$.' is_equivalence: false - id: locally_finitely_presentable_raise diff --git a/database/data/category-implications/algebraic.yaml b/database/data/category-implications/algebraic.yaml index 16a73ab41..3340b0cf6 100644 --- a/database/data/category-implications/algebraic.yaml +++ b/database/data/category-implications/algebraic.yaml @@ -62,6 +62,14 @@ Now let $G$ be a set of finitely presentable objects in $\C$ generating all objects via filtered colimits. The claim follows because every filtered colimit is sifted and the objects in $G$ are strongly finitely presentable. is_equivalence: false +- id: generalized_variety_stable_monos + assumptions: + - generalized variety + conclusions: + - filtered-colimit-stable monomorphisms + proof: 'Let $\C$ be a generalized variety and let $G$ be a set of strongly finitely presentable objects which generates $\C$ under sifted colimits. Consider $G$ as a full subcategory of $\C$ and consider the restricted Yoneda embedding $\C \hookrightarrow [G^{\op},\Set]$. It preserves sifted colimits (essentially by the definition of a strongly finitely presentable object) and therefore filtered colimits. It also preserves all limits, in particular monomorphisms, and it reflects monomorphisms since $G$ is a generating set. Therefore, since $\Set$ and hence the functor category has filtered-colimit-stable monomorphisms, this is also true for $\C$.' + is_equivalence: false + - id: multi-algebraic_implies_locally_finitely_multi-presentable assumptions: - multi-algebraic