Determine some accessibilities of Met

database/data/categories/Met.yaml

@@ -62,12 +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 : 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 <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, the category $\Met$ is precisely the cone-injectivity class with respect to the cone $(e_n)_{n \in \IN}$ in $\Met_\infty$. Since <a href="/category/Met_oo">$\Met_\infty$</a> 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 <a href="https://doi.org/10.1016/j.jpaa.2021.106974" target="_blank">Approximate injectivity and smallness in metric-enriched categories</a> 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 $\aleph_1$-accessible.
 unsatisfied_properties:
   - property: skeletal
     proof: This is trivial.
@@ -97,7 +104,9 @@ unsatisfied_properties:
     proof: This is proven in <a href="https://math.stackexchange.com/questions/5131457" target="_blank">MSE/5131457</a>.
 
   - property: filtered-colimit-stable monomorphisms
-    proof: 'The following example is taken from Remark 2.7 in <a href="https://arxiv.org/abs/2006.01399" target="_blank">Approximate injectivity and smallness in metric-enriched categories</a> 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 <a href="/category/PMet">$\PMet$</a> 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 <a href="https://doi.org/10.1016/j.jpaa.2021.106974" target="_blank">Approximate injectivity and smallness in metric-enriched categories</a> 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 <a href="/category/PMet">$\PMet$</a> 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: natural numbers object
     proof: >-

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 <a href="/content/subcategories">here</a> 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$.
 

database/data/category-implications/accessible.yaml

@@ -36,6 +36,14 @@
   proof: Special case of <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, 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 $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
   assumptions:
     - locally finitely presentable

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