diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index 942abdf7..c6d342cc 100644 --- a/database/data/categories/Met.yaml +++ b/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 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 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 $\aleph_1$-accessible. unsatisfied_properties: - property: skeletal proof: This is trivial. @@ -97,7 +104,9 @@ 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: natural numbers object proof: >- diff --git a/database/data/categories/Setne.yaml b/database/data/categories/Setne.yaml index 136deb47..353a88b2 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 94033586..9e8b7719 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 $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 diff --git a/database/data/category-implications/algebraic.yaml b/database/data/category-implications/algebraic.yaml index 16a73ab4..3340b0cf 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