diff --git a/.cspell.json b/.cspell.json index 5fc8c1bd..e5826a8c 100644 --- a/.cspell.json +++ b/.cspell.json @@ -64,6 +64,7 @@ "coexponentials", "cofiltered", "cofiltering", + "cofinal", "cofinitary", "cofull", "cogenerates", @@ -125,6 +126,7 @@ "extremal", "fieldification", "finitary", + "foundedness", "Freyd", "functor", "functorial", @@ -265,5 +267,8 @@ ".netlify", "build" ], - "ignoreRegExpList": ["\\$[^$]*\\$", "\\$\\$[^$]*\\$\\$"] + "ignoreRegExpList": [ + "\\$[^$]*\\$", + "\\$\\$[^$]*\\$\\$" + ] } diff --git a/databases/catdat/data/categories/BN.yaml b/databases/catdat/data/categories/BN.yaml index 5e895b3b..0f56c227 100644 --- a/databases/catdat/data/categories/BN.yaml +++ b/databases/catdat/data/categories/BN.yaml @@ -40,6 +40,45 @@ satisfied_properties: - property: locally cartesian closed reason: The slice category $B\IN / *$ is isomorphic to the poset $(\IN,\geq)$ (not to $(\IN,\leq)$). This category is thin and and semi-strongly connected, hence cartesian closed. + - property: ℵ₁-filtered colimits + reason: >- + Let $D : \I \to B\IN$ be an $\aleph_1$-filtered diagram. Every two parallel morphisms $i \rightrightarrows j$ are mapped to the same morphism in $B \IN$, because they are coequalized by some morphism and $(\IN,+)$ is cancellative. Hence, $D$ factors through the preorder reflection of $\I$, and we may therefore assume that $\I$ itself is a preorder. Thus, the diagram consists of numbers $D(i,j) \in \IN$ for all $i \leq j$ satisfying + $$D(j,k) + D(i,j) = D(i,k)$$ + for all $i \leq j \leq k$. In particular, $D(i,j) \leq D(i,k)$. + + Let $i \in \I$. The set of natural numbers $\{D(i,k) : k \geq i\}$ is bounded above. Otherwise, for every $n \in \IN$ we could find $k_n \in \I$ with $k_n \geq i$ and $D(i,k_n) \geq n$. Since $\I$ is $\aleph_1$-filtered, the family $(k_n)_{n \in \IN}$ has an upper bound $k_\infty \in \I$. But then + $$D(i, k_\infty) = D(k_n,k_\infty) + D(i, k_n) \geq D(i, k_n) \geq n$$ + for all $n \in \IN$, contradicting the fact that $D(i,k_\infty) \in \IN$. + + Therefore, the maximum + $$u_i \coloneqq \max \{D(i,k) : k \geq i\} \in \IN$$ + is well-defined, which we regard as a morphism in $B\IN$. For $i \leq j$ we compute + $$\begin{align*} + u_i & = \max \{D(i,k) : k \geq i\} \\ + & = \max \{D(i,k) : k \geq j\} \\ + & = \max \{ D(j,k) + D(i,j) : k \geq j\} \\ + & = \max \{D(j,k) : k \geq j\} + D(i,j)\\ + & = u_j + D(i,j), + \end{align*}$$ + showing that $(u_i)$ defines a cocone. It is universal: let $(v_i)$ be another cocone, i.e. $v_i \in \IN$ and $v_i = v_j + D(i,j)$ for all $i \leq j$. Then $v_i \geq D(i,j)$ for all $i \leq j$, hence $v_i \geq u_i$. Write $v_i = w_i + u_i$ for some uniquely determined $w_i \in \IN$. For $i \leq j$ we compute + $$w_j + u_j + D(i,j) = v_j + D(i,j) = v_i = w_i + u_i = w_i + u_j + D(i,j),$$ + hence $w_j = w_i$. Therefore, the $w_i$ are constant, and the required factorization follows. + check_redundancy: false + + - property: ℵ₁-accessible + reason: >- + We continue the proof that $\aleph_1$-filtered colimits exist. It remains to show that the unique object $*$ is $\aleph_1$-presentable, i.e. that for every diagram $D : \I \to B\IN$ as above, the canonical map + $$\alpha : \colim_{i \in \I} \Hom(*,D(i)) \to \Hom(*,\colim_{i \in \I} D(i))$$ + is bijective. On objects, we necessarily have $D(i)=*$ and $\colim_{i \in \I} D(i)=*$. Hence, the codomain of $\alpha$ is simply $\IN$, while the domain consists of equivalence classes $[i,n]$ of pairs $(i,n) \in \I \times \IN$, where $(i,n) \sim (j,m)$ iff there exists some $k \geq i,j$ such that + $$D(i,k) + n = D(j,k) + m.$$ + By the construction of the colimit cocone, we have + $$\alpha([i,n]) = u_i + n = \max \{D(i,j) : j \geq i\} + n.$$ + (1) The map $\alpha$ is surjective: Pick some $i \in \I$. Choose $j \geq i$ such that $u_i = D(i,j)$. For all $k \geq j$ we then have + $$u_i \geq D(i,k) = D(j,k) + D(i,j) = D(j,k) + u_i,$$ + hence $D(j,k)=0$. Therefore, $u_j=0$, and thus $\alpha([j,n]) = n$ for all $n \in \IN$. + + (2) The map $\alpha$ is injective: Assume that $[i,n]$ and $[j,m]$ have the same image. Since $\I$ is filtered, we may assume $i=j$. The condition then becomes $u_i + n = u_i + m$, and therefore $n=m$. This completes the proof. + unsatisfied_properties: - property: one-way reason: This is trivial. diff --git a/databases/catdat/data/categories/BOn.yaml b/databases/catdat/data/categories/BOn.yaml index ea77a211..a998ea05 100644 --- a/databases/catdat/data/categories/BOn.yaml +++ b/databases/catdat/data/categories/BOn.yaml @@ -41,6 +41,47 @@ satisfied_properties: - property: locally cartesian closed reason: The slice category $B\On / *$ is isomorphic to the poset $(\On,\geq)$ (not to $(\On,\leq)$). This category is thin and and semi-strongly connected, hence cartesian closed. + - property: ℵ₁-filtered colimits + reason: >- + The proof is similar to $B\IN$. Let $\I$ be an $\aleph_1$-filtered small category and $D : \I \to B\On$ a diagram. A cocone $\lambda = (\lambda_i)_{i \in \I}$ for $D$ is a family of ordinals satisfying $\lambda_i = \lambda_j + D(f)$ for every morphism $f: i \to j$ in $\I$. + + + We first observe that $D$ factors uniquely through the preorder reflection of $\I$. Indeed, any two parallel morphisms in $\I$ are coequalized by some morphism, and $B\On$ is left cancellative. Thus, we may assume that $\I$ is a preorder. Each inequality $i \leq j$ in $\I$ is mapped to an ordinal number $\alpha_{i,j} \coloneqq D(i \to j)$, and these numbers satisfy + $$\alpha_{i,k} = \alpha_{j,k} + \alpha_{i,j}$$ + for all $i \leq j \leq k$. In particular, $\alpha_{i,j} \leq \alpha_{i,k}$. + + + For fixed $i \in \I$, the collection $\{\alpha_{i,j} : j \geq i\}$ is a set of ordinals because $\I$ is small, hence bounded above in $\On$. We claim that it has a maximum element. Otherwise, we can find a countable chain $i = j_0 \leq j_1 \leq j_2 \leq \dotsc$ in $\I$ such that $\alpha_{i,j_n} < \alpha_{i,j_{n+1}}$ for all $n \in \IN$. Since $\I$ is $\aleph_1$-filtered, there is an upper bound $j_\infty \in \I$ of $(j_n)_{n \in \IN}$. For each $n \in \IN$, the equation + $$\alpha_{i,j_{n+1}} = \alpha_{j_n,j_{n+1}} + \alpha_{i,j_n}$$ + implies that $\alpha_{j_n,j_{n+1}} > 0$. Hence, + $$\alpha_{j_n,j_\infty} = \alpha_{j_{n+1},j_\infty} + \alpha_{j_n,j_{n+1}} > \alpha_{j_{n+1},j_\infty},$$ + so $(\alpha_{j_n,j_\infty})_{n \in \IN}$ is a strictly decreasing infinite sequence of ordinals, contradicting the well-foundedness of $\On$. Thus, the maximum + $$u_i \coloneqq \max \{ \alpha_{i,j} : j \geq i \}$$ + is a well-defined ordinal number, which we regard as a morphism in $B\On$. The family $(u_i)_{i \in \I}$ forms a cocone for $D$, since for all $i \leq j$ we have + $$\begin{align*} + u_i & = \max \{ \alpha_{i,k} : k \geq i \} \\ + & = \max \{ \alpha_{i,k} : k \geq j \} \\ + & = \max \{ \alpha_{j,k} + \alpha_{i,j} : k \geq j \} \\ + & = \max \{ \alpha_{j,k} : k \geq j \} + \alpha_{i,j} \\ + & = u_j + \alpha_{i,j}. + \end{align*}$$ + To establish the universal property, let $(\lambda_i)_{i \in \I}$ be any cocone for $D$, so that $\lambda_i = \lambda_j + \alpha_{i,j}$ for all $i \leq j$. The cocone relation $u_i = u_j + \alpha_{i,j}$ implies that $u_i \geq u_j$ whenever $i \leq j$. By the well-foundedness of $\On$, there exists $i_0 \in \I$ such that $u_j = u_{i_0}$ for all $j \geq i_0$. For such $j$, the relation + $$u_{i_0} = u_j + \alpha_{i_0,j} = u_{i_0} + \alpha_{i_0,j}$$ + forces $\alpha_{i_0,j} = 0$. Consequently, + $$u_{i_0} = \max \{ \alpha_{i_0,j} : j \geq i_0 \} = 0.$$ + Define the mediating morphism to be the ordinal $\kappa \coloneqq \lambda_{i_0}$. We must show that $\lambda_i = \kappa + u_i$ for all $i \in \I$. Choose $j \in \I$ with $j \geq i$ and $j \geq i_0$. Since $j \geq i_0$, we have $u_j = 0$ and $\alpha_{i_0,j} = 0$. The cocone condition for $\lambda$ gives + $$\kappa = \lambda_{i_0} = \lambda_j + \alpha_{i_0,j} = \lambda_j.$$ + Applying the cocone conditions for $u$ and $\lambda$ to $i \leq j$, we obtain + $$u_i = u_j + \alpha_{i,j} = 0 + \alpha_{i,j} = \alpha_{i,j}$$ + and + $$\lambda_i = \lambda_j + \alpha_{i,j} = \kappa + \alpha_{i,j} = \kappa + u_i.$$ + This proves the existence of the mediating morphism. + + + For uniqueness, suppose $\kappa'$ is any ordinal satisfying $\lambda_i = \kappa' + u_i$ for all $i \in \I$. Evaluating at $i_0$ yields + $$\lambda_{i_0} = \kappa' + u_{i_0} = \kappa' + 0 = \kappa',$$ + hence $\kappa' = \kappa$. Therefore, the cocone $(u_i)_{i \in \I}$ is the colimit of $D$ in $B\On$. + unsatisfied_properties: - property: initial object reason: This is trivial. diff --git a/databases/catdat/data/categories/FinAb.yaml b/databases/catdat/data/categories/FinAb.yaml index 4b868950..5f583a90 100644 --- a/databases/catdat/data/categories/FinAb.yaml +++ b/databases/catdat/data/categories/FinAb.yaml @@ -31,9 +31,6 @@ satisfied_properties: - property: self-dual reason: 'This is a simple special case of Pontryagin duality: The functor $\Hom(-,\IQ/\IZ)$ provides the equivalence.' - - property: ℵ₁-accessible - reason: The proof works exactly as for $\FinSet$. - unsatisfied_properties: - property: small reason: Even the collection of trivial groups is not small. diff --git a/databases/catdat/data/categories/FinGrp.yaml b/databases/catdat/data/categories/FinGrp.yaml index ab9d68df..1fdcf3f6 100644 --- a/databases/catdat/data/categories/FinGrp.yaml +++ b/databases/catdat/data/categories/FinGrp.yaml @@ -46,9 +46,6 @@ satisfied_properties: - property: regular reason: The category is Malcev and hence finitely complete, and it has all coequalizers. The regular epimorphisms coincide with the surjective group homomorphisms (see below), hence are clearly stable under pullbacks. - - property: ℵ₁-accessible - reason: The proof works exactly as for $\FinSet$. - unsatisfied_properties: - property: small reason: Even the collection of trivial groups is not small. diff --git a/databases/catdat/data/categories/FinSet.yaml b/databases/catdat/data/categories/FinSet.yaml index 820d795a..ea764b5d 100644 --- a/databases/catdat/data/categories/FinSet.yaml +++ b/databases/catdat/data/categories/FinSet.yaml @@ -41,9 +41,6 @@ satisfied_properties: - property: elementary topos reason: This follows easily from the fact that sets form an elementary topos. - - property: ℵ₁-accessible - reason: The inclusion $\FinSet \hookrightarrow \Set$ is closed under ℵ₁-filtered colimits, that is, any ℵ₁-filtered colimit of finite sets is again finite. Since every finite set is ℵ₁-presentable in $\Set$, it is still ℵ₁-presentable in $\FinSet$. Therefore, $\FinSet$ is ℵ₁-accessible, where every object is ℵ₁-presentable. - unsatisfied_properties: - property: small reason: Even the collection of all singletons is not a set. diff --git a/databases/catdat/data/categories/FreeAb.yaml b/databases/catdat/data/categories/FreeAb.yaml index de14a680..fdb0bd42 100644 --- a/databases/catdat/data/categories/FreeAb.yaml +++ b/databases/catdat/data/categories/FreeAb.yaml @@ -54,6 +54,9 @@ unsatisfied_properties: - property: sequential colimits reason: See MO/509715. + - property: ℵ₁-filtered colimits + reason: It is shown in MO/511426 that the $\aleph_1$-filtered diagram of countable subgroups of $\IZ^{\IN}$ does not have a colimit in $\FreeAb$. + category_property_comments: - property: accessible comment: The question if this category is accessible is undecidable in ZFC. See MSE/720885. diff --git a/databases/catdat/data/categories/Grp_c.yaml b/databases/catdat/data/categories/Grp_c.yaml index 7c8fac0a..ce9a5114 100644 --- a/databases/catdat/data/categories/Grp_c.yaml +++ b/databases/catdat/data/categories/Grp_c.yaml @@ -85,7 +85,7 @@ unsatisfied_properties: - property: cogenerator reason: 'Assume that a cogenerator $Q$ exists in $\Grp_\c$. There are only countably many finitely generated subgroups of $Q$. But there are continuum many finitely generated simple groups; this follows from Corollary 1.5 in Finitely generated infinite simple groups of homeomorphisms of the real line by J. Hyde and Y. Lodha. Hence, there is a finitely generated (and hence countable) simple group $H$ which does not embed into $Q$. Since $H$ is simple, any homomorphism $H \to Q$ must be trivial then. But then $\id_H, 1 : H \rightrightarrows H$ are not separated by a homomorphism $H \to Q$.' - - property: ℵ₁-accessible + - property: ℵ₁-filtered colimits reason: 'We can almost copy the proof from $\Set_\c$ to show that $\Grp_\c$ does not have $\aleph_1$-filtered colimits: Fix an uncountable set $X$, let $P_\c(X)$ be the poset of countable subsets of $X$, which is $\aleph_1$-filtered, and consider the functor $P_\c(X) \to \Grp_\c$ taking a subset $Y \subseteq X$ to the free group $F(Y)$. The colimit of this diagram in $\Grp$ is given by $F(X)$ itself, so if $G$ were a colimit in $\Grp_\c$, then $\Hom(G, C_2) \cong \Hom(F(X),C_2) \cong \{0,1\}^X$. But the former has cardinality at most $2^{\aleph_0}$ and the latter has cardinality $2^{\card(X)}$, so we have obtained a contradiction if we pick $X$ large enough (e.g. $\card(X)=2^{\aleph_0}$).' special_objects: diff --git a/databases/catdat/data/categories/Man.yaml b/databases/catdat/data/categories/Man.yaml index 37f73027..afca53ec 100644 --- a/databases/catdat/data/categories/Man.yaml +++ b/databases/catdat/data/categories/Man.yaml @@ -71,7 +71,7 @@ unsatisfied_properties: - property: sequential colimits reason: If $\Man$ had sequential colimits, then by this lemma there would be a manifold $M$ that admits a split epimorphism $M \to \IR^n$ for every $n$. But then $M$ will have an infinite-dimensional tangent space, which is a contradiction. - - property: ℵ₁-accessible + - property: ℵ₁-filtered colimits reason: 'We already know that $\Set_\c$ does not have $\aleph_1$-filtered colimits. The functor $\pi_0: \Man \to \Set_\c$ is well-defined (because manifolds are second-countable), and it admits a fully faithful right adjoint (regarding a countable set as a discrete manifold). Therefore, $\Man$ does not have $\aleph_1$-filtered colimits.' - property: quotients of congruences diff --git a/databases/catdat/data/categories/Met_c.yaml b/databases/catdat/data/categories/Met_c.yaml index 3bbc433c..cd7dc052 100644 --- a/databases/catdat/data/categories/Met_c.yaml +++ b/databases/catdat/data/categories/Met_c.yaml @@ -48,7 +48,7 @@ satisfied_properties: reason: This follows from the existence of coproducts and finite products, and from the fact that $\Top$ is infinitary extensive. - property: effective cocongruences - reason: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Met_\c$. Then the image in $\Haus$ is a coreflexive corelation (since epimorphisms in both categories are continuous maps with dense image). By MO/509548, that implies that image is of the form $X +_S X$ for a closed subset $S$ of $X$. Since $S$ is metrizable, and the functor $\Met_\c \to \Haus$ is fully faithful and therefore reflects colimits, we conclude that $E$ is effective in $\Met_\c$.' + reason: 'Suppose we have a cocongruence $f, g : X \rightrightarrows E$ in $\Met_c$. Then the image in $\Haus$ is a coreflexive corelation (since epimorphisms in both categories are continuous maps with dense image). By MO/509548, that implies that image is of the form $X +_S X$ for a closed subset $S$ of $X$. Since $S$ is metrizable, and the functor $\Met_c \to \Haus$ is fully faithful and therefore reflects colimits, we conclude that $E$ is effective in $\Met_c$.' unsatisfied_properties: - property: skeletal @@ -67,7 +67,10 @@ unsatisfied_properties: reason: 'We recycle the proof from $\Haus$: Assume that there is a regular subobject classifier $\Omega$. By the classification of regular monomorphisms, we would have an isomorphism between $\Hom(X,\Omega)$ and the set of closed subsets of $X$ for any metric space $X$. If we take $X = 1$ we see that $\Omega$ has two points. Since $\Omega$ is Hausdorff, $\Omega \cong 1 + 1$ must be discrete. But then $\Hom(X,\Omega)$ is isomorphic to the set of all clopen subsets of $X$, of which there are usually far fewer than closed subsets (consider $X = [0,1]$).' - property: sequential colimits - reason: See MO/510316. + reason: See MO/510316 for a proof that the diagram $\IN \to \Met_c$, $n \mapsto \IR^n$ does not have a colimit. + + - property: ℵ₁-filtered colimits + reason: See MO/511433 for a proof that the diagram $\omega_1 \to \Met_c$, $\alpha \mapsto \IR^\alpha$ does not have a colimit. - property: quotients of congruences reason: If $\Met_c$ had quotients of congruences, then by this lemma it would have sequential colimits of sequences of monomorphisms. This contradicts MO/510316. diff --git a/databases/catdat/data/categories/Set_c.yaml b/databases/catdat/data/categories/Set_c.yaml index e949660d..fc228389 100644 --- a/databases/catdat/data/categories/Set_c.yaml +++ b/databases/catdat/data/categories/Set_c.yaml @@ -69,8 +69,8 @@ unsatisfied_properties: - property: countable powers reason: Since the forgetful functor $\Set_\c \to \Set$ is representable, it preserves (countable) products. Therefore, if the power $\{0,1\}^{\IN}$ exists in $\Set_\c$, it must be the ordinary cartesian product, which however is uncountable. - - property: ℵ₁-accessible - reason: 'In fact, $\Set_\c$ does not have $\aleph_1$-filtered colimits: Fix an uncountable set $X$, let $P_\c(X)$ be the poset of countable subsets of $X$, which is $\aleph_1$-filtered, and consider the functor $P_\c(X) \to \Set_\c$ taking a subset $Y \subseteq X$ to $Y$. The colimit of this diagram in $\Set$ is given by $X$ itself, so if $X_c$ were a colimit in $\Set_\c$, then $\Hom(X_c, \{0,1\}) \cong \Hom(X, \{0,1\})$. But the former has cardinality at most $2^{\aleph_0}$ and the latter has cardinality $2^{\card(X)}$, so we have obtained a contradiction if we pick $X$ large enough (e.g. $\card(X)=2^{\aleph_0}$).' + - property: ℵ₁-filtered colimits + reason: 'Fix an uncountable set $X$, let $P_\c(X)$ be the poset of countable subsets of $X$, which is $\aleph_1$-filtered, and consider the functor $P_\c(X) \to \Set_\c$ taking a subset $Y \subseteq X$ to $Y$. The colimit of this diagram in $\Set$ is given by $X$ itself, so if $X_c$ were a colimit in $\Set_\c$, then $\Hom(X_c, \{0,1\}) \cong \Hom(X, \{0,1\})$. But the former has cardinality at most $2^{\aleph_0}$ and the latter has cardinality $2^{\card(X)}$, so we have obtained a contradiction if we pick $X$ large enough (e.g. $\card(X)=2^{\aleph_0}$).' special_objects: initial object: diff --git a/databases/catdat/data/categories/Sp.yaml b/databases/catdat/data/categories/Sp.yaml index 62c23aef..b210f840 100644 --- a/databases/catdat/data/categories/Sp.yaml +++ b/databases/catdat/data/categories/Sp.yaml @@ -23,6 +23,9 @@ satisfied_properties: - property: cogenerator reason: 'This follows from $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$, this lemma, and the fact that if $G$ is a (finite) group, the power set $P(G)$ with the evident $G$-action is a weakly terminal cogenerator in $G{-}\Set$ (resp. $G{-}\FinSet$). For the proof, notice that $\varnothing,G \in P(G)$ are fixed points, yielding two $G$-maps $1 \rightrightarrows P(G)$. In particular, $P(G)$ is weakly terminal. If $X$ is a $G$-set with distinct points $x,y$, we construct a $G$-map $f : X \to P(G)$ that separates $x,y$: First, $X$ is a coproduct of orbits. If $x,y$ lie in different orbits, let $f|_{Gx}$ be constant $\varnothing$, $f|_{Gy}$ be constant $G$, and, say, $f$ be constant $\varnothing$ on all other orbits. If $x,y$ lie in the same orbit, say $y = g_0 x$, define $f|_{Gx} : Gx \to P(G)$ by $f(x) = G_x$ (stabilizer), which is well-defined, and choose $f$ to be $\varnothing$ on all other orbits. Then $f(y) = g_0 G_x \neq G_x = f(x)$.' + - property: ℵ₁-accessible + reason: We know that $\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable. It follows that for every $n \in \IN$ also $\Sigma_n{-}\FinSet$ has $\aleph_1$-filtered colimits and that every object is $\aleph_1$-presentable. From this it follows formally that $\Sp \simeq \prod_{n \geq 0} \Sigma_n{-}\FinSet$ also has these properties. In particular, $\Sp$ is $\aleph_1$-accessible. + unsatisfied_properties: - property: skeletal reason: This is trivial. diff --git a/databases/catdat/data/categories/walking_idempotent.yaml b/databases/catdat/data/categories/walking_idempotent.yaml index 68b3a491..ba0e99ce 100644 --- a/databases/catdat/data/categories/walking_idempotent.yaml +++ b/databases/catdat/data/categories/walking_idempotent.yaml @@ -39,8 +39,8 @@ satisfied_properties: - property: preadditive reason: The monoid $\{1,e\}$ with $e^2=e$ is the underlying multiplicative monoid of the ring $\IZ/2$, where $e=0$. Thus, the (unique) preadditive structure is given by $1 + e = e + 1 = 1$, $e + e = e$ and $1 + 1 = e$. - - property: filtered - reason: The pair $\id,e$ is coequalized by $e$ (non-universally). + - property: ℵ₁-filtered + reason: 'In fact, the walking idempotent is $\kappa$-filtered for every regular infinite cardinal $\kappa$: Every diagram $D : \I \to \Idem$ has the cocone $(e : D(i) \to 0)_{i \in \I}$.' unsatisfied_properties: - property: terminal object diff --git a/databases/catdat/data/category-implications/accessible.yaml b/databases/catdat/data/category-implications/accessible.yaml index c0018f04..e9c3b3e9 100644 --- a/databases/catdat/data/category-implications/accessible.yaml +++ b/databases/catdat/data/category-implications/accessible.yaml @@ -132,6 +132,7 @@ - ℵ₁-accessible conclusions: - accessible + - ℵ₁-filtered colimits reason: This is trivial. is_equivalence: false @@ -148,7 +149,7 @@ - accessible conclusions: - Cauchy complete - reason: This is because the walking idempotent is $\kappa$-filtered for any regular cardinal $\kappa$. + reason: This is because the walking idempotent is $\kappa$-filtered for any regular cardinal $\kappa$. See also Makkai-Pare, Prop. 2.2.1. is_equivalence: false - id: small_accessible_characterization @@ -160,13 +161,59 @@ reason: See Makkai-Pare, Thm. 2.2.2. is_equivalence: false -- id: countably_accessible_thin +- id: countably_accessible_criterion assumptions: - essentially countable - - thin + - locally finite + - Cauchy complete conclusions: - ℵ₁-accessible - reason: 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. + reason: >- + The proof is similar to Thm. 2.2.2 in Makkai-Pare (which only establishes $\aleph_2$-accessibility) and to MO/509853 (which concerns $\aleph_0$-accessibility in the finite case). + + + Let $\C$ be a category that is locally finite, essentially countable, and Cauchy complete. By replacing $\C$ with an equivalent category if necessary, we may assume that it is countable and that all Hom-sets are finite sets. Let $\I$ be an $\aleph_1$-filtered category and let $D : \I \to \C$ be a diagram. We will prove that the colimit of $D$ exists and is a retract of some $D(i)$, in fact for arbitrarily large $i$. (Note that one cannot in general prove that it is isomorphic to some $D(i)$; this is false.) It follows that $\aleph_1$-filtered colimits exist and that every object of $\C$ is $\aleph_1$-presentable. + + + Let $X \in \C$ be a fixed object. Then + $$F \coloneqq \Hom(X,D(-)) : \I \to \FinSet$$ + is a diagram of finite sets. Regard it as a diagram in $\Set$ and let $L \in \Set$ be its colimit. Thus, for every $i \in \I$ we have maps $u_i : F(i) \to L$ that are jointly surjective, and two elements in $F(i)$ and $F(j)$ become equal in $L$ iff there exists a cospan $i \to k \leftarrow j$ such that these elements map to the same element in $F(k)$. + + + We claim that $L$ is finite. Otherwise, there would exist infinitely many pairwise distinct elements $l_1,l_2,\dotsc$ in $L$. Choose objects $i_1,i_2,\dotsc \in \I$ such that $l_n$ has a preimage in $F(i_n)$. Since $\I$ is $\aleph_1$-filtered, there exists a cocone $(i_n \to j)_{n \geq 1}$ in $\I$. We then obtain preimages $a_1,a_2,\dotsc$ in $F(j)$, which must be pairwise distinct because $l_1,l_2,\dotsc$ are pairwise distinct. This contradicts the finiteness of $F(j)$. Therefore, $L$ is finite. + + + For every element of the finite set $L$, choose a preimage in some $F(i)$. Since $\I$ is filtered, there exists $i \in \I$ that works for all elements simultaneously. Equivalently, the canonical map $F(i) \to L$ is surjective. + + + Now consider the free cocompletion $Y : \C \hookrightarrow \widehat{\C} = [\C^{\op},\Set]$ and the colimit $D_\infty \in \widehat{\C}$ of the diagram $Y \circ D$. Since colimits in $\widehat{\C}$ are computed objectwise, + $$D_\infty(X) = \colim_{i \in \I} \Hom(X,D(i)).$$ + We have shown above that $D_\infty(X)$ is finite and that there exists some $i_X \in \I$ such that the canonical map + $$u_{i_X}(X) : \Hom(X,D(i_X)) \to D_\infty(X)$$ + is surjective. Since $\C$ is countable and $\I$ is $\aleph_1$-filtered, there exists a cocone $(i_X \to j)_{X \in \C}$ in $\I$. It follows that + $$u_j(X) : \Hom(X,D(j)) \to D_\infty(X)$$ + is surjective for all $X \in \C$. Equivalently, $u_j : Y(D(j)) \to D_\infty$ is an epimorphism in $\widehat{\C}$. For every morphism $j \to j'$, the map $u_{j'}$ is likewise an epimorphism. We will now show that some $u_{j'}$ is in fact a split epimorphism in $\widehat{\C}$. + + + For every $X \in \C$, since $u_j(X)$ is a surjective map of finite sets, there exists a map + $$v(X) : D_\infty(X) \to \Hom(X,D(j))$$ + such that $u_j(X) \circ v(X) = \id_{D_\infty(X)}$. The issue is that $v$ need not be natural in $X$. To analyze this, let $f : X \to Y$ be a morphism in $\C$. Then we have a diagram of finite sets: + $$\begin{CD} + D_\infty(Y) @>{v(Y)}>> \Hom(Y,D(j)) @>{u_j(Y)}>> D_\infty(Y) \\ + @V{f^*}VV @V{f^*}VV @VV{f^*}V \\ + D_\infty(X) @>>{v(X)}> \Hom(X,D(j)) @>>{u_j(X)}> D_\infty(X) + \end{CD}$$ + The outer rectangle commutes, and the square on the right commutes. Hence, the square on the left commutes after composition with $u_j(X)$. Since $D_\infty(Y)$ is finite, it follows that there exists some morphism $j \to j'$ such that the left square commutes after composition with + $$\Hom(X,D(j \to j')) : \Hom(X,D(j)) \to \Hom(X,D(j')).$$ + A priori, the index $j'$ depends on the morphism $f : X \to Y$. However, since $\I$ is $\aleph_1$-filtered and $\C$ has only countably many morphisms, we may choose $j'$ independently of $f$. Thus, by construction, + $$w(X) \coloneqq \Hom(X,D(j \to j')) \circ v(X) : D_\infty(X) \to \Hom(X,D(j'))$$ + is natural in $X$. Moreover, + $$\begin{align*} + u_{j'}(X) \circ w(X) & = u_{j'}(X) \circ \Hom(X,D(j \to j')) \circ v(X) \\ + & = u_j(X) \circ v(X) = \id_{D_\infty(X)}. + \end{align*}$$ + Therefore, $u_{j'}$ is a split epimorphism in $\widehat{\C}$. Since $\C$ is Cauchy complete, it follows that $D_\infty$ is representable, represented by a retract of $D(j')$. Since $Y$ is fully faithful, this object is a colimit of $D$. + is_equivalence: false - id: locally_presentable_another_definition diff --git a/databases/catdat/data/category-implications/filtered + sifted.yaml b/databases/catdat/data/category-implications/filtered + sifted.yaml index 1b1f2b3c..ce37ad89 100644 --- a/databases/catdat/data/category-implications/filtered + sifted.yaml +++ b/databases/catdat/data/category-implications/filtered + sifted.yaml @@ -39,27 +39,64 @@ where $f=g$; hence when the category is also sifted, all cospans must be of this form, and so any two parallel morphisms are equal. is_equivalence: false -- id: terminal_object_yields_filtered +- id: filtered_criterion assumptions: - - terminal object + - finitely cocomplete + conclusions: + - filtered + reason: Every finite diagram even admits a universal cocone. + is_equivalence: false + +- id: filtered_via_coequalizers + assumptions: + - coequalizers + - semi-strongly connected conclusions: - filtered reason: This is obvious. is_equivalence: false -- id: filtered_criterion +- id: aleph1-filtered-consequence assumptions: - - finitely cocomplete + - ℵ₁-filtered conclusions: - filtered - reason: Every finite diagram even admits a universal cocone. + reason: This is trivial. is_equivalence: false -- id: filtered_via_equalizers +- id: aleph1-filtered_criterion assumptions: - coequalizers - - semi-strongly connected + - countable coproducts conclusions: - - filtered + - ℵ₁-filtered + reason: Every countable diagram even admits a universal cocone. + is_equivalence: false + +- id: terminal_object_yields_kappa_filtered + assumptions: + - terminal object + conclusions: + - ℵ₁-filtered reason: This is obvious. is_equivalence: false + +- id: filtered-finite-thin + assumptions: + - thin + - filtered + - essentially finite + conclusions: + - terminal object + reason: Let $\C$ be a thin, filtered, and w.l.o.g. finite category. The identity diagram $\C \to \C$ admits a cocone. That is, there is an object $T$ with a morphism $A \to T$ for all $A \in \C$. Then $T$ is terminal. + is_equivalence: false + +- id: aleph1-filtered-countable-thin + assumptions: + - thin + - ℵ₁-filtered + - essentially countable + conclusions: + - terminal object + reason: Let $\C$ be a thin, $\aleph_1$-filtered, and w.l.o.g. countable category. The identity diagram $\C \to \C$ admits a cocone. That is, there is an object $T$ with a morphism $A \to T$ for all $A \in \C$. Then $T$ is terminal. + is_equivalence: false diff --git a/databases/catdat/data/category-implications/filtered colimits.yaml b/databases/catdat/data/category-implications/filtered colimits.yaml index 5e3ff90a..5b93a253 100644 --- a/databases/catdat/data/category-implications/filtered colimits.yaml +++ b/databases/catdat/data/category-implications/filtered colimits.yaml @@ -61,6 +61,22 @@ reason: We may assume that the category $\C$ is finite and Cauchy complete. The answer at MO/509853 shows that every filtered colimit in $\C$ exists, in fact it is a retract of one of the objects in the diagram. Now apply this to the morphism category of $\C$. It follows that for every filtered diagram of morphisms $X_i \to Y_i$ their colimit $X_\infty \to Y_\infty$ exists, which is a retract of one of the $X_i \to Y_i$. Therefore, if every $X_i \to Y_i$ is a monomorphism, also $X_\infty \to Y_\infty$ is a monomorphism. is_equivalence: false +- id: aleph1-filtered-colimits-include-filtered-colimits + assumptions: + - filtered colimits + conclusions: + - ℵ₁-filtered colimits + reason: Every $\aleph_1$-filtered category is also $\aleph_0$-filtered, i.e. filtered. Therefore, every $\aleph_1$-filtered diagram is also a filtered diagram, hence has a colimit by assumption. + is_equivalence: false + +- id: kappa-filtered-colimits_require_Cauchy_complete + assumptions: + - ℵ₁-filtered colimits + conclusions: + - Cauchy complete + reason: More generally, if $\kappa$ is any infinite regular cardinal, a category with $\kappa$-filtered colimits must be Cauchy cocomplete. This is because the walking idempotent is $\kappa$-filtered. See also Makkai-Pare, Prop. 2.2.1. + is_equivalence: false + - id: sifted_categories_are_connected assumptions: - connected colimits diff --git a/databases/catdat/data/category-properties/aleph1-accessible.yaml b/databases/catdat/data/category-properties/aleph1-accessible.yaml index 23532d7a..6b3d96c2 100644 --- a/databases/catdat/data/category-properties/aleph1-accessible.yaml +++ b/databases/catdat/data/category-properties/aleph1-accessible.yaml @@ -1,6 +1,6 @@ id: ℵ₁-accessible relation: is -description: This is the special case of the notion of $\kappa$-accessible categories, where $\kappa = \aleph_1$ is the first uncountable cardinal. +description: This is the special case of the notion of a $\kappa$-accessible category, where $\kappa = \aleph_1$ is the first uncountable cardinal. Concretely, a category is $\aleph_1$-accessible when it has $\aleph_1$-filtered colimits and there is a small set $G$ of $\aleph_1$-presentable objects such that every object is a $\aleph_1$-filtered colimit of objects in $G$. nlab_link: https://ncatlab.org/nlab/show/accessible+category invariant_under_equivalences: true @@ -8,3 +8,4 @@ related_properties: - accessible - finitely accessible - locally ℵ₁-presentable + - ℵ₁-filtered colimits diff --git a/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml b/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml new file mode 100644 index 00000000..1a583f6a --- /dev/null +++ b/databases/catdat/data/category-properties/aleph1-filtered colimits.yaml @@ -0,0 +1,12 @@ +id: ℵ₁-filtered colimits +relation: has +description: A category has $\aleph_1$-filtered colimits if it has colimits of diagrams indexed by small $\aleph_1$-filtered categories. This is the special case of having small $\kappa$-filtered colimits for $\kappa=\aleph_1$, the first uncountable cardinal. +nlab_link: https://ncatlab.org/nlab/show/filtered+colimit +dual_property: null +invariant_under_equivalences: true + +related_properties: + - cocomplete + - filtered colimits + - ℵ₁-accessible + - ℵ₁-filtered diff --git a/databases/catdat/data/category-properties/aleph1-filtered.yaml b/databases/catdat/data/category-properties/aleph1-filtered.yaml new file mode 100644 index 00000000..52183594 --- /dev/null +++ b/databases/catdat/data/category-properties/aleph1-filtered.yaml @@ -0,0 +1,11 @@ +id: ℵ₁-filtered +relation: is +description: A category is $\aleph_1$-filtered if every countable diagram admits a cocone. This is the special case of the notion of a $\kappa$-filtered category for $\kappa = \aleph_1$, the first uncountable cardinal. An equivalent characterization is given as Theorem 2.2 at the nLab. +nlab_link: https://ncatlab.org/nlab/show/filtered+category +dual_property: null +invariant_under_equivalences: true + +related_properties: + - filtered + - ℵ₁-filtered colimits + - cocomplete diff --git a/databases/catdat/data/category-properties/filtered colimits.yaml b/databases/catdat/data/category-properties/filtered colimits.yaml index ebab748e..9cc8bc4f 100644 --- a/databases/catdat/data/category-properties/filtered colimits.yaml +++ b/databases/catdat/data/category-properties/filtered colimits.yaml @@ -10,3 +10,4 @@ related_properties: - directed colimits - filtered - sifted colimits + - ℵ₁-filtered colimits diff --git a/databases/catdat/data/category-properties/filtered.yaml b/databases/catdat/data/category-properties/filtered.yaml index 938bdf4a..7ce6254b 100644 --- a/databases/catdat/data/category-properties/filtered.yaml +++ b/databases/catdat/data/category-properties/filtered.yaml @@ -1,10 +1,12 @@ id: filtered relation: is -description: A category is filtered if every finite diagram admits a cocone. Equivalently, it is inhabited, for every two objects $x,y$ there is a cospan $x \rightarrow s \leftarrow y$ (not necessarily universal), and every parallel pair $x \rightrightarrows y$ is coequalized by some morphism $y \to c$ (not necessarily universal). +description: A category is filtered if every finite diagram admits a cocone. Equivalently, it is inhabited, for every two objects $x,y$ there is a cospan $x \rightarrow s \leftarrow y$ (not necessarily universal), and every parallel pair $x \rightrightarrows y$ is coequalized by some morphism $y \to c$ (not necessarily universal). This is the special case of the notion of a $\kappa$-filtered category for $\kappa = \aleph_0$. nlab_link: https://ncatlab.org/nlab/show/filtered+category dual_property: cofiltered invariant_under_equivalences: true related_properties: + - ℵ₁-filtered - filtered colimits - - finitely cocomplete + - cocomplete + - sifted diff --git a/databases/catdat/scripts/expected-data/Ab.json b/databases/catdat/scripts/expected-data/Ab.json index 5adbeb58..42c0cb6a 100644 --- a/databases/catdat/scripts/expected-data/Ab.json +++ b/databases/catdat/scripts/expected-data/Ab.json @@ -79,6 +79,7 @@ "finite copowers": true, "binary copowers": true, "filtered": true, + "ℵ₁-filtered": true, "cofiltered": true, "sifted": true, "cosifted": true, @@ -89,6 +90,7 @@ "accessible": true, "finitely accessible": true, "ℵ₁-accessible": true, + "ℵ₁-filtered colimits": true, "generalized variety": true, "locally finitely multi-presentable": true, "locally multi-presentable": true, diff --git a/databases/catdat/scripts/expected-data/Set.json b/databases/catdat/scripts/expected-data/Set.json index 1b231c2e..b2ab6e58 100644 --- a/databases/catdat/scripts/expected-data/Set.json +++ b/databases/catdat/scripts/expected-data/Set.json @@ -77,12 +77,14 @@ "finite copowers": true, "binary copowers": true, "filtered": true, + "ℵ₁-filtered": true, "cofiltered": true, "sifted": true, "cosifted": true, "accessible": true, "finitely accessible": true, "ℵ₁-accessible": true, + "ℵ₁-filtered colimits": true, "generalized variety": true, "locally finitely multi-presentable": true, "locally multi-presentable": true, diff --git a/databases/catdat/scripts/expected-data/Top.json b/databases/catdat/scripts/expected-data/Top.json index d3febb98..f0292620 100644 --- a/databases/catdat/scripts/expected-data/Top.json +++ b/databases/catdat/scripts/expected-data/Top.json @@ -61,6 +61,7 @@ "finite copowers": true, "binary copowers": true, "filtered": true, + "ℵ₁-filtered": true, "cofiltered": true, "sifted": true, "cosifted": true, @@ -137,6 +138,7 @@ "accessible": false, "finitely accessible": false, "ℵ₁-accessible": false, + "ℵ₁-filtered colimits": true, "generalized variety": false, "locally finitely multi-presentable": false, "locally multi-presentable": false,