diff --git a/content/inclusion-functors.md b/content/inclusion-functors.md index 122dbf62..efd7c190 100644 --- a/content/inclusion-functors.md +++ b/content/inclusion-functors.md @@ -6,7 +6,7 @@ description: We gather results about inclusion functors # Inclusion functors ::: Lemma 1 -Let $\D$ be category that has an extremal cogenerator $Q$. Let $\C \subseteq \D$ be a full subcategory that contains $Q$. Then the inclusion functor $U : \C \hookrightarrow \D$ preserves all colimits that exist in $\C$ and in $\D$. In particular, if $\D$ is cocomplete, $U$ is cocontinuous. +Let $\D$ be category that has an extremal cogenerating collection $S$. Let $\C \subseteq \D$ be a full subcategory that contains every object of $S$. Then the inclusion functor $U : \C \hookrightarrow \D$ preserves all colimits that exist in $\C$ and in $\D$. In particular, if $\D$ is cocomplete, $U$ is cocontinuous. ::: ::: Proof @@ -14,5 +14,5 @@ Let $D : \I \to \C$ be a diagram such that $D$ has a colimit $(u_i : D(i) \to X) $$f^* : \Hom(X,T) \to \Hom(Y,T)$$ -is a bijection; both sides identify with cones $D \to T$. Now apply this to $T \coloneqq Q$ to conclude that $f$ is an isomorphism. +is a bijection; both sides identify with cones $D \to T$. Now apply this to $T \in S$ to conclude that $f$ is an isomorphism. ::: diff --git a/content/natural_numbers_objects.md b/content/natural_numbers_objects.md index a601b9bd..92f7905a 100644 --- a/content/natural_numbers_objects.md +++ b/content/natural_numbers_objects.md @@ -109,3 +109,35 @@ This finishes the proof. _Remark._ Actually, the mentioned [result](/category-implication/parametrized_nno_criterion) and Lemma 4 can be combined into an equivalent characterization as follows: In a category with finite products and countable copowers, the NNO (which exists, see [here](/category-implication/nno_criterion)) is a parametrized NNO if and only if for all objects $A$ the canonical morphism $$\textstyle \coprod_{n \in \IN} A = \coprod_{n \in \IN} (A \times 1) \to A \times \coprod_{n \in \IN} 1$$ is an isomorphism. This is the precise connection to countable distributivity. + +::: Lemma 5 +Let $F : \C \to \D$ be left adjoint to $G : \D \to \C$. Assume that $1_{\C}$ is a terminal object of $\C$ such that $1_{\D} \coloneqq F(1_{\C})$ is a terminal object of $\D$. Then $F$ preserves natural numbers objects. That is, if $(N,z,s)$ is a natural numbers object in $\C$, then its image $(F(N),F(z),F(s))$ is a natural numbers object in $\D$. +::: + +::: Proof +For a category $\C$ with a terminal object $1_{\C}$, let $R(\C)$ denote the category of diagrams +$$1_{\C} \xrightarrow{x_0} X \xrightarrow{r} X$$ +in $\C$. A natural numbers object in $\C$ is precisely an initial object of $R(\C)$. Suppose that $H : \C \to \D$ is a functor between categories with terminal objects that preserves terminal objects. Then $H$ induces a functor $R(H) : R(\C) \to R(\D)$ that maps +$$1_{\C} \xrightarrow{x_0} X \xrightarrow{r} X$$ +to its image +$$1_{\D} \cong H(1_{\C}) \xrightarrow{H(x_0)} H(X) \xrightarrow{H(r)} H(X).$$ + +In the situation of the lemma, we therefore have two functors + +$$ +\begin{align*} +R(F) & : R(\C) \to R(\D),\\ +R(G) & : R(\D) \to R(\C). +\end{align*} +$$ + +Notice that $G$ preserves terminal objects since it is a right adjoint. + +We claim that $R(F)$ is left adjoint to $R(G)$. Indeed, for objects $(X,x_0,r) \in R(\C)$ and $(Y,y_0,s) \in R(\D)$, a morphism $R(F)(X,x_0,r) \to (Y,y_0,s)$ is the same as a morphism $f : F(X) \to Y$ such that +$$f \circ F(x_0) = y_0, \quad s \circ f = f \circ F(r).$$ +Under the adjunction $F \dashv G$, it corresponds to a morphism $\widetilde{f} : X \to G(Y)$ such that +$$\widetilde{f} \circ x_0 = G(y_0), \quad G(s) \circ \widetilde{f} = \widetilde{f} \circ r.$$ +This is precisely a morphism $(X,x_0,r) \to R(G)(Y,y_0,s)$. + +Since $R(F)$ is a left adjoint, it preserves initial objects. This is precisely the statement that $F$ preserves natural numbers objects. +::: diff --git a/content/subcategories.md b/content/subcategories.md index 2dc04ad8..2b25fd78 100644 --- a/content/subcategories.md +++ b/content/subcategories.md @@ -100,15 +100,19 @@ where $U(X) \times_{U(Y)} U(X)$ is the kernel pair of $U(f)$, and $U(\im(f))$ is ::: ::: Lemma 8 -Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has finite limits and coequalizers, and that $U$ preserves inhabited finite limits and coequalizers. If $\D$ has effective congruences, then so does $\C$. +Let $U : \C \to \D$ be a fully faithful functor. Assume that $\C$ has pullbacks and coequalizers, that $U$ preserves pullbacks and coequalizers, and that $U$ preserves jointly monomorphic parallel pairs (which holds, for example, if $\C$ has binary products and $U$ preserves them). If $\D$ has effective congruences, then so does $\C$. ::: ::: Proof -Suppose we have a congruence $E \hookrightarrow X\times X$ in $\C$. We can then form the quotient $X \to X/E$ as a coequalizer, along with the kernel pair $X \times_{X/E} X$ and the comparison map $i$ in the diagram below: -$$E \xrightarrow{i} X \times_{X/E} X \rightrightarrows X \to X/E.$$ -By the assumptions, the image under $U$ is equivalent to the diagram in $\D$: -$$UE \xrightarrow{Ui} UX \times_{U(X/E)} UX \rightrightarrows UX \to U(X/E).$$ -Here, $UE \rightrightarrows UX$ is a congruence: the map $UE \to UX \times UX$ is a monomorphism since $U$ preserves pullbacks and therefore preserves monomorphisms; the reflexivity and symmetry morphisms for $E$ are easily seen to transform under $U$ to reflexivity and symmetry morphisms for $UE$; and similarly, since $U$ preserves pullbacks, the transitivity morphism for $E$ transforms under $U$ to a transitivity morphism for $UE$. This congruence $UE$ of $\D$ is effective, so we must have $Ui$ is an isomorphism. Since $U$ is fully faithful and therefore conservative, we get $i$ is an isomorphism as well, so $E$ is effective. +Suppose we have a congruence $E \rightrightarrows X$ in $\C$. We first observe that its image $U(E) \rightrightarrows U(X)$ is a congruence in $\D$, and therefore effective. It is jointly monomorphic by assumption on $U$; the reflexivity and symmetry morphisms for $E$ are easily seen to transform under $U$ into reflexivity and symmetry morphisms for $U(E)$; and similarly, since $U$ preserves pullbacks, the transitivity morphism for $E$ transforms under $U$ into a transitivity morphism for $U(E)$. + +Now let $X/E$ be the quotient of $E \rightrightarrows X$, i.e. its coequalizer. We will show that the canonical morphism +$$E \to X \times_{X/E} X$$ +is an isomorphism. Since $U$ is fully faithful and preserves pullbacks, it suffices to prove that the canonical morphism +$$U(E) \to U(X) \times_{U(X/E)} U(X)$$ +is an isomorphism, where $U(X/E)$ is the coequalizer of $U(E) \rightrightarrows U(X)$ since $U$ preserves coequalizers. Since the congruence $U(E) \rightrightarrows U(X)$ is effective by the first part of the proof, this follows from [this lemma](/content/effective-congruence-quotients). + +Finally, to prove the parenthetical remark, assume that $\C$ has binary products and that $U$ preserves them. Then $U$ preserves jointly monomorphic parallel pairs, because it preserves monomorphisms (as it preserves pullbacks), and a pair $A \rightrightarrows B$ is jointly monomorphic if and only if the induced morphism $A \to B \times B$ is a monomorphism. ::: ::: Lemma 9 diff --git a/database/data/categories/DiGraph.yaml b/database/data/categories/DiGraph.yaml index 5605af06..f3c7bad8 100644 --- a/database/data/categories/DiGraph.yaml +++ b/database/data/categories/DiGraph.yaml @@ -17,6 +17,7 @@ related: - walking_pair - Cat - Bin + - DiGraph_fc satisfied_properties: - property: locally small @@ -36,7 +37,8 @@ unsatisfied_properties: proof: >- Assume that $G$ is a generator. Consider the edgeless graph $H$ with two vertices. Since it has two distinct endomorphisms $H \rightrightarrows H$, there is a morphism $G \to H$. Since $H$ has no edges, this implies that $G$ has no edges. The directed graph $L$ with a single vertex and two loops has two distinct endomorphisms $L \rightrightarrows L$, but since their maps on vertices agree, every morphism $G \to L$ equalizes them. Thus, $G$ is not a generator. - Alternatively, the claim follows from this result, since the terminal graph (having one vertex and one loop) has a subgraph (having one vertex and no loops) which is neither initial nor terminal. + Alternatively, the claim follows from this result, since the terminal directed graph (having one vertex and one loop) has a subgraph (having one vertex and no loops) which is neither initial nor terminal. + label: DiGraph_no_generator - property: semi-strongly connected proof: Let $G$ be the directed cycle $0 \to 1 \to 0$ and $H$ be the directed cycle $0 \to 1 \to 2 \to 0$. There is no morphism of directed graphs $G \to H$ since $H$ does not contain two edges of the form $x \to y \to x$ (a vertex can only reoccur after $3$ steps). There is also no morphism $H \to G$, because this would amount to a sequence of edges $x \to y \to z \to x$ in $G$. Every edge in $G$ alternates between the two vertices, so if, say, $x=0$, then $y=1$, $z=0$, and then $x=1$, contradicting $x=0$. More generally, if $C_n$ is the directed $n$-cycle, a morphism of directed graphs $C_n \to C_m$ exists if and only if $m \mid n$. @@ -44,11 +46,11 @@ unsatisfied_properties: special_objects: initial object: - description: the graph with no vertices and hence no edges + description: the directed graph with no vertices and hence no edges terminal object: - description: the graph with one vertex and one loop + description: the directed graph with one vertex and one loop coproducts: - description: The coproduct of a family of directed graphs $(V_i,E_i,s_i,t_i)$ is $(\coprod_i V_i, \coprod_i E_i, \coprod_i s_i, \coprod_i t_i)$. Intuitively, we take the disjoint union of the vertices, keep the edges in the individual graphs, and do not add any edges between distinct graphs. + description: The coproduct of a family of directed graphs $(V_i,E_i,s_i,t_i)$ is $(\coprod_i V_i, \coprod_i E_i, \coprod_i s_i, \coprod_i t_i)$. Intuitively, we take the disjoint union of the vertices, keep the edges in the individual directed graphs, and do not add any edges between distinct directed graphs. products: description: The product of a family of directed graphs $(V_i,E_i,s_i,t_i)$ is $(\prod_i V_i, \prod_i E_i, \prod_i s_i, \prod_i t_i)$. diff --git a/database/data/categories/DiGraph_fc.yaml b/database/data/categories/DiGraph_fc.yaml new file mode 100644 index 00000000..08420008 --- /dev/null +++ b/database/data/categories/DiGraph_fc.yaml @@ -0,0 +1,140 @@ +id: DiGraph_fc +name: category of directed graphs with finite components +notation: $\DiGraph_{\fc}$ +objects: directed graphs whose connected components are finite +morphisms: morphisms of directed graphs +description: Here, connected components are understood in the underlying undirected graph, so edges may be traversed in either direction. Thus, the objects are precisely the coproducts of finite directed graphs. We have included this category solely as an example of a category with a subobject classifier that does not have coequalizers. Note that $\DiGraph_{\fc}$ is the free coproduct completion of the category of finite connected directed graphs. +nlab_link: null + +tags: + - graph theory + +related: + - DiGraph + - Euclid_coprod + +satisfied_properties: + - property: locally small + proof: It is a full subcategory of $\DiGraph$, which is locally small. + + - property: finite products + proof: The category $\DiGraph$ has finite products. The full subcategory $\DiGraph_{\fc} \subseteq \DiGraph$ is closed under finite products because every object of $\DiGraph_{\fc}$ is a coproduct of finite directed graphs, $\DiGraph$ is infinitary distributive, and finite products of finite directed graphs are finite. + check_redundancy: false + + - property: equalizers + proof: This follows because $\DiGraph$ has equalizers and $\DiGraph_{\fc} \subseteq \DiGraph$ is closed under subgraphs. Namely, every subgraph of a coproduct of finite directed graphs decomposes as a coproduct of subgraphs of these finite directed graphs, and a subgraph of a finite directed graph is finite. + check_redundancy: false + + - property: subobject classifier + proof: >- + The previous proofs show that $\DiGraph_{\fc} \subseteq \DiGraph$ is closed under finite limits. The subobject classifier $\Omega$ of $\DiGraph$ is finite; see nLab for a detailed description. Hence, $\top : 1 \to \Omega$ is a morphism in $\DiGraph_{\fc}$. If $X \hookrightarrow Y$ is a monomorphism in $\DiGraph_{\fc}$, it is also a monomorphism in $\DiGraph$ since the inclusion functor preserves pullbacks. Hence, there is a unique morphism of directed graphs $Y \to \Omega$ such that + $$\begin{CD} X @>>> Y \\ @V{!}VV @VVV \\ 1 @>>> \Omega \end{CD}$$ + is a pullback square in $\DiGraph$, i.e. a pullback square in $\DiGraph_{\fc}$. + + - property: infinitary extensive + proof: Since $\DiGraph$ is infinitary extensive and $\DiGraph_{\fc} \subseteq \DiGraph$ is closed under coproducts and pullbacks, this follows from Lemma 11 here. + + - property: cokernel pairs + proof: 'We will show that $\DiGraph_{\fc} \subseteq \DiGraph$ is closed under cokernel pairs. More generally, let $f : G \to H$ be a morphism of directed graphs with $H \in \DiGraph_{\fc}$. Write $H = \coprod_i H_i$ as a coproduct of finite directed graphs. Since $\DiGraph$ is infinitary extensive, we have $G = \coprod_i f^*(H_i)$, and $f$ decomposes as a coproduct of morphisms $f_i : f^*(H_i) \to H_i$. Then $H \sqcup_G H = \coprod_i (H_i \sqcup_{f^*(H_i)} H_i)$. Each directed graph $H_i \sqcup_{f^*(H_i)} H_i$ is finite because it is a quotient of the finite directed graph $H_i \sqcup H_i$. Thus, $H \sqcup_G H$ belongs to $\DiGraph_{\fc}$.' + + - property: coequalizers of kernel pairs + proof: 'Let $f : G \to H$ be a morphism in $\DiGraph_{\fc}$. In $\DiGraph$, the coequalizer of the kernel pair of $f$ is simply the image of $f$. Since $\DiGraph_{\fc} \subseteq \DiGraph$ is closed under subgraphs, this image belongs to $\DiGraph_{\fc}$. The universal property of a coequalizer persists in $\DiGraph_{\fc}$.' + + - property: extremal cogenerating collection + proof: >- + We claim that the "chaotic" directed graph $G = (\{a,b\},\{a,b\} \times \{a,b\})$ and the directed graph $H = (\{a\},\{\ell,\ell'\})$ with one vertex and two loops form an extremal cogenerating collection. Indeed, $\Hom(-,G)$ is isomorphic to the contravariant functor $(V,E) \mapsto P(V)$, and $\Hom(-,H)$ is isomorphic to the contravariant functor $(V,E) \mapsto P(E)$. The combined functor $(V,E) \mapsto (P(V),P(E))$ is faithful and conservative because the contravariant power set functor $P : \Set^{\op} \mapsto \Set$ is faithful and conservative. + + Remark: The same proof works for $\DiGraph$. + label: DiGraph_fc_extremal_cogenerators + + - property: well-copowered + proof: This follows immediately from the description of epimorphisms below. + + - property: epi-regular + proof: Any epimorphism $f = (f_V,f_E)$ in $\DiGraph_{\fc}$ has surjective components $f_V,f_E$ by the classification below. Hence, it is the coequalizer of its kernel pair in $\DiGraph$. Since the kernel pair belongs to $\DiGraph_{\fc}$, it is also the coequalizer in $\DiGraph_{\fc}$. + + - property: ℵ₁-accessible + proof: >- + First, we show that $\DiGraph_{\fc} \subseteq \DiGraph$ is closed under $\aleph_1$-filtered colimits. Let $D : \I \to \DiGraph_{\fc}$ be an $\aleph_1$-filtered diagram, and let $C$ be its colimit directed graph in $\DiGraph$. Thus, the set of vertices is given by $V_C = \colim_{i \in \I} V_{D(i)}$, and the set of edges is given by $E_C = \colim_{i \in \I} E_{D(i)}$. Consider a vertex $v$ of $C$. It has a preimage vertex $v_{i_0}$ in some $D(i_0)$. For each morphism $i_0 \to i$, consider its image $v_i$ in $D(i)$, and let $C(i) \subseteq D(i)$ denote the connected component of $v_i$. Then it is easy to see that the connected component of $v$ is identified with $\colim_{i_0 \to i} C(i)$. Since $\FinSet$ is closed under $\aleph_1$-filtered colimits in $\Set$ (the proof is identical to the proof for $\Ab_{\fg}$ in MO/400763), it follows that the collection of finite directed graphs is closed under $\aleph_1$-filtered colimits in $\DiGraph$. Since each $C(i)$ is finite, it follows that the connected component of $v$ is finite, as required. + + Let $S \subseteq \Ob(\DiGraph_{\fc})$ be the collection of directed graphs with countably many components, each of them finite. Note that, up to isomorphism, these constitute a set. (More precisely, there is a set $S' \subseteq S$ such that every object in $S$ is isomorphic to some object in $S'$, so that we may equally work with $S'$.) Each directed graph in $S$ has countably many vertices and edges, and hence is $\aleph_1$-presentable in $\DiGraph$ (either by a direct argument or by using Corollary 3.13 in Adamek-Rosicky). Since the inclusion $\DiGraph_{\fc} \hookrightarrow \DiGraph$ preserves $\aleph_1$-filtered colimits, it follows that each directed graph in $S$ is also $\aleph_1$-presentable in $\DiGraph_{\fc}$. + + Finally, every directed graph $G$ in $\DiGraph_{\fc}$ can be written as $\coprod_{i \in I} G_i$ with finite directed graphs $G_i$, and therefore expressed as the $\aleph_1$-filtered colimit of the directed graphs $\coprod_{i \in C} G_i$ in $S$, where $C$ runs through the countable subsets of $I$. + + - property: ℵ₁-cofiltered limits + proof: >- + We show that $\DiGraph_{\fc} \subseteq \DiGraph$ is closed under $\aleph_1$-cofiltered limits. Let $D : \I \to \DiGraph_{\fc}$ be an $\aleph_1$-cofiltered diagram, and let $L$ be its limit in $\DiGraph$. Consider a vertex $v \in V_L$, and let $C(v) \subseteq L$ denote its connected component. For each $i \in \I$, let $C(v_i) \subseteq D(i)$ be the connected component of $v_i \in V_{D(i)}$. Each transition map $D(i \to j) : D(i) \to D(j)$ maps $C(v_i)$ into $C(v_j)$. Thus, we can construct the directed graph $\lim_{i \in \I} C(v_i)$. It is finite because $\FinSet$ is closed under $\aleph_1$-cofiltered limits in $\Set$. Since each projection map $L \to D(i)$ maps $C(v)$ into $C(v_i)$, there is an embedding $C(v) \hookrightarrow \lim_{i \in \I} C(v_i)$. Hence, $C(v)$ is finite. + references: + - finset_aleph1-cofiltered-limits + + - property: effective cocongruences + proof: More generally, let $G \rightrightarrows H$ be a coreflexive corelation in $\DiGraph_{\fc}$. Since binary coproducts exist and the inclusion functor $\DiGraph_{\fc} \hookrightarrow \DiGraph$ preserves epimorphisms, it is a coreflexive corelation in $\DiGraph$. Since $\DiGraph$ is co-Malcev and has effective cocongruences (by this result), the pair $G \rightrightarrows H$ is the cokernel pair of some morphism $E \to G$ in $\DiGraph$, namely (since equalizers exist, see here) the equalizer of $G \rightrightarrows H$. Since $G$ belongs to $\DiGraph_{\fc}$, also $E$ belongs to $\DiGraph_{\fc}$. It follows that $G \rightrightarrows H$ is also the cokernel pair of $E \to G$ in $\DiGraph_{\fc}$. + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: semi-strongly connected + proof: We can recycle the proof from $\DiGraph$, which only uses finite auxiliary directed graphs. + references: + - DiGraph_not_semi-strongly_connected + + - property: generator + proof: We can recycle the proof from $\DiGraph$, which only uses finite auxiliary directed graphs. + references: + - DiGraph_no_generator + + - property: countable powers + proof: >- + First, note that the forgetful functor $\DiGraph_{\fc} \to \Set$, $(V,E) \mapsto V$, is represented by the directed graph $\bullet$ (one vertex, no edges), and hence preserves limits. Similarly, the forgetful functor $(V,E) \mapsto E$ is represented by the directed graph $\bullet \to \bullet$ (two vertices, one edge), and hence also preserves limits. We conclude that the forgetful functor $\DiGraph_{\fc} \to \DiGraph$ preserves limits. Alternatively, this follows from Lemma 1 here, since $\DiGraph_{\fc}$ contains an extremal generating set of $\DiGraph$, namely the two directed graphs mentioned above. + + Now let $G$ be the directed graph with vertices $a,b$, one loop $a \to a$, and one edge $a \to b$. If the power $G^{\IN}$ exists in $\DiGraph_{\fc}$, it must be the power in $\DiGraph$. It has the vertex $(a,a,\dotsc)$, which admits an edge to every sequence of vertices consisting of $a$ and $b$. Thus, its connected component is infinite, which is a contradiction. + + - property: sequential colimits + proof: >- + First, note that the inclusion functor $\DiGraph_{\fc} \to \DiGraph$ preserves colimits. This is because $\DiGraph$ is cocomplete, $\DiGraph_{\fc}$ contains an extremal cogenerating collection of $\DiGraph$ (by our proof that $\DiGraph_{\fc}$ has one), and Lemma 1 here. Thus, it suffices to show that $\DiGraph_{\fc}$ is not closed under sequential colimits in $\DiGraph$. + + Consider the directed path $P_n$ with $n$ vertices and $n-1$ edges. It is finite, hence belongs to $\DiGraph_{\fc}$, and there is a canonical embedding $P_n \hookrightarrow P_{n+1}$. The colimit of this sequence in $\DiGraph$ is the directed path $P_\infty$ with infinitely many vertices. It is connected but not finite, hence does not belong to $\DiGraph_{\fc}$. + label: DiGraph_fc_no_sequential_colimits + references: + - DiGraph_fc_extremal_cogenerators + + - property: quotients of congruences + proof: Since the category is infinitary extensive and we have just identified a sequence of monomorphisms without a colimit, there is a congruence without a quotient by Lemma 1 here. + references: + - DiGraph_fc_no_sequential_colimits + + - property: coaccessible + proof: >- + The proof is very similar to the proof for $\Top$. Let $D$ be the directed graph with vertices $0,1$ and no edges, and let $I$ be the directed graph with vertices $0,1$ and the four edges $i \to j$ for $i,j \in \{0,1\}$. There is a canonical morphism $p : D \to I$. By definition, a directed graph $G = (V,E)$ is projective to $p$ if the map + $$p_* : \Hom(G,D) \to \Hom(G,I)$$ + is surjective. Note that $\Hom(G,I) \cong \Hom(V,\{0,1\})$ and that + $$\Hom(G,D) \cong \begin{cases} + \Hom(V,\{0,1\}) & E = \varnothing \\ + \varnothing & E \neq \varnothing. + \end{cases}$$ + Thus, $G$ is projective to $p$ if and only if $G$ has no edges, i.e. $G$ is discrete. Every discrete graph belongs to $\DiGraph_{\fc}$. This shows that the full subcategory of directed graphs in $\DiGraph_{\fc}$ that are projective to $p$ is equivalent to $\Set$. Since $\Set$ is not coaccessible, it follows from the dual of Prop. 4.7 in Adamek-Rosicky that $\DiGraph_{\fc}$ is not coaccessible. + references: + - top_not_coaccessible + +special_objects: + initial object: + description: the directed graph with no vertices and hence no edges + terminal object: + description: the directed graph with one vertex and one loop + coproducts: + description: just as in $\DiGraph$ + products: + description: '[finite case] just as in $\DiGraph$' + +special_morphisms: + isomorphisms: + description: morphisms $f = (f_V, f_E)$ such that $f_V$ and $f_E$ are bijective + proof: This description holds in $\DiGraph$. + monomorphisms: + description: morphisms $f = (f_V, f_E)$ such that $f_V$ and $f_E$ are injective + proof: For the non-trivial direction, the construction of finite limits shows that the forgetful functor $\DiGraph_{\fc} \to \DiGraph$ preserves finite limits and hence preserves monomorphisms. The monomorphisms in $\DiGraph$ have the stated description. + epimorphisms: + description: morphisms $f = (f_V, f_E)$ such that $f_V$ and $f_E$ are surjective + proof: >- + For the non-trivial direction, let $f = (f_V,f_E) : (V,E) \to (V',E')$ be an epimorphism. Consider the "chaotic" directed graph $G = (\{a,b\},\{a,b\} \times \{a,b\})$. It is finite, so the map $f^* : \Hom((V',E'),G) \to \Hom((V,E),G)$ is injective. This map identifies with $(f_V)^* : \Hom(V',\{0,1\}) \to \Hom(V,\{0,1\})$. Hence, $f_V$ is surjective. Now consider the directed graph $H = (\{a\},\{\ell,\ell'\})$ with one vertex and two loops. It is finite, so the map $f^* : \Hom((V',E'),H) \to \Hom((V,E),H)$ is injective. This map identifies with $(f_E)^* : \Hom(E',\{\ell,\ell'\}) \to \Hom(E,\{\ell,\ell'\})$. Hence, $f_E$ is surjective. diff --git a/database/data/categories/Euclid_coprod.yaml b/database/data/categories/Euclid_coprod.yaml index 681c5b5c..dc1bb6e1 100644 --- a/database/data/categories/Euclid_coprod.yaml +++ b/database/data/categories/Euclid_coprod.yaml @@ -4,7 +4,7 @@ notation: $\Euclid_{\sqcup}$ objects: coproducts of Euclidean spaces morphisms: continuous functions description: >- - By definition, this is the full subcategory of $\Top$ (or $\Haus$) where every space is isomorphic to $\coprod_{i \in I} \IR^{n_i}$ for a family of natural numbers $(n_i)_{i \in I}$. These are locally Euclidean spaces in the strongest possible sense. This category provides an example of an infinitary distributive category that is not Cauchy complete. Using the fact that Euclidean spaces are connected, it is easy to see that this category is the free coproduct cocompletion of the category of Euclidean spaces. + By definition, this is the full subcategory of $\Top$ (or $\Haus$) where every space is isomorphic to $\coprod_{i \in I} \IR^{n_i}$ for a family of natural numbers $(n_i)_{i \in I}$. These are locally Euclidean spaces in the strongest possible sense. This category provides an example of an infinitary distributive category that is not Cauchy complete. Using the fact that Euclidean spaces are connected, it is easy to see that this category is the free coproduct completion of the category of Euclidean spaces. nlab_link: null tags: - topology @@ -14,6 +14,7 @@ related: - Haus - Man - Met_c + - DiGraph_fc satisfied_properties: - property: locally small @@ -23,7 +24,7 @@ satisfied_properties: proof: This follows since $\Top$ is infinitary distributive and Euclidean spaces are closed under finite products. Namely, $\IR^0=1$ and $\IR^n \times \IR^m \cong \IR^{n+m}$. - property: infinitary extensive - proof: The free coproduct cocompletion of any category is infinitary extensive; for the finite case see Proposition 2.4 in Introduction to extensive and distributive categories by Carboni-Lack-Walters. + proof: The free coproduct completion of any category is infinitary extensive; for the finite case see Proposition 2.4 in Introduction to extensive and distributive categories by Carboni-Lack-Walters. - property: well-powered proof: This is clear from the classification of monomorphisms as injective continuous maps. diff --git a/database/data/categories/SeqAb.yaml b/database/data/categories/SeqAb.yaml index c42c5c9d..d96e99a3 100644 --- a/database/data/categories/SeqAb.yaml +++ b/database/data/categories/SeqAb.yaml @@ -16,6 +16,7 @@ related: - FiltVect - Ch(Ab) - TransSeqAb + - SeqSet satisfied_properties: [] diff --git a/database/data/categories/SeqSet.yaml b/database/data/categories/SeqSet.yaml new file mode 100644 index 00000000..b1d55c16 --- /dev/null +++ b/database/data/categories/SeqSet.yaml @@ -0,0 +1,60 @@ +id: SeqSet +name: category of sequences of sets +notation: $[(\IN,\leq),\Set]$ +objects: sequences of sets $X_0 \to X_1 \to X_2 \to \cdots$ +morphisms: commutative diagrams +description: As a functor category of $\Set$, most properties are inherited from $\Set$, but a notable difference is that it has no generator. +nlab_link: null + +tags: + - set theory + +related: + - Set + - Set_arrow + - SeqAb + - SetxSet + - SeqSet_conn + +satisfied_properties: + - property: locally small + proof: This is obvious. + + - property: Grothendieck topos + proof: This follows from the description as a functor category $[(\IN,\leq),\Set]$. + + - property: finitary algebraic + proof: 'Take the algebraic theory with sorts $S_0,S_1,\dotsc$ and unary operations $S_n \to S_{n+1}$ for every $n \geq 0$.' + + - property: semi-strongly connected + proof: >- + Let $X,Y$ be two sequences. If $X_n = \varnothing$ for every $n \geq 0$, there is a unique morphism $X \to Y$. Likewise, if $Y_m = \varnothing$ for every $m \geq 0$, there is a unique morphism $Y \to X$. Otherwise, choose $n \geq 0$ minimal with $X_n \neq \varnothing$, and choose $m \geq 0$ minimal with $Y_m \neq \varnothing$. Assume without loss of generality that $n \leq m$. Choose an element $x_n \in X_n$. For $k \geq n$, let $x_k \in X_k$ denote its image under the map $X_n \to X_k$, and consider the constant map $Y_k \to X_k$ with value $x_k$. For $k < n \leq m$, define $\varnothing = Y_k \to X_k$ to be the unique map. This defines a morphism of sequences $Y \to X$. + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: generator + proof: >- + Suppose the category of sequences had a generator. Then, by this result, every subterminal object would be either initial or terminal. However, $0 \to 1 \to 1 \to \cdots$ is a subterminal object which is isomorphic to neither the initial object $0 \to 0 \to 0 \to \cdots$ nor the terminal object $1 \to 1 \to 1 \to \cdots$. + +special_objects: + initial object: + description: the constant sequence $0 \to 0 \to \cdots$ + terminal object: + description: the constant sequence $1 \to 1 \to \cdots$ + coproducts: + description: component-wise defined disjoint union + products: + description: component-wise defined direct product + +special_morphisms: + isomorphisms: + description: morphisms $f = (f_n)_{n \geq 0}$ where every $f_n$ is bijective + proof: This is easy to check. It can also be deduced from the fact that isomorphisms in functor categories coincide with natural isomorphisms. + monomorphisms: + description: morphisms $f = (f_n)_{n \geq 0}$ where every $f_n$ is injective + proof: This holds in every functor category $[\C,\Set]$ because the evaluation functors are continuous. + epimorphisms: + description: morphisms $f = (f_n)_{n \geq 0}$ where every $f_n$ is surjective + proof: This holds in every functor category $[\C,\Set]$ because the evaluation functors are cocontinuous. diff --git a/database/data/categories/SeqSet_conn.yaml b/database/data/categories/SeqSet_conn.yaml new file mode 100644 index 00000000..d552c259 --- /dev/null +++ b/database/data/categories/SeqSet_conn.yaml @@ -0,0 +1,305 @@ +id: SeqSet_conn +name: category of connected sequences of sets +notation: $[(\IN,\leq),\Set]_{\conn}$ +objects: 'sequences of sets $X_0 \to X_1 \to X_2 \to \cdots$ that are connected, meaning that $\colim_{n \geq 0} X_n$ is a singleton set' +morphisms: commutative diagrams +description: >- + This is a full subcategory of the category of sequences of sets, containing those sequences + $$X_0 \to X_1 \to X_2 \to \cdots$$ + whose colimit is a singleton set. Equivalently, the following two properties are satisfied: (1) There is some $n \geq 0$ with $X_n \neq \varnothing$. (2) For all $n \geq 0$ and all $x,y \in X_n$, there is some $m \geq n$ such that $x,y$ map to the same element in $X_m$. + + We have added this category to provide an example of a category with a subobject classifier but without an initial object. +nlab_link: null +tags: + - set theory + +related: + - SeqSet + - Setne + +comments: + - This category has been suggested by Jonas Frey at MO/515206. + +satisfied_properties: + - property: locally small + proof: It is a full subcategory of the category of sequences of sets, which is locally small. + + - property: semi-strongly connected + proof: It is a full subcategory of the category of sequences of sets, which is semi-strongly connected. + + - property: finitely complete + proof: 'The category of sequences of sets has (finite) limits, defined pointwise. A sequence of sets $X$ is connected if and only if the unique maps $! : X_n \to \{\ast\}$ induce an isomorphism in the colimit. Since filtered colimits commute with finite limits in $\Set$, a finite limit of connected sequences is again connected.' + check_redundancy: false + + - property: connected colimits + proof: 'The category of sequences of sets has (connected) colimits, defined pointwise. A sequence of sets $X$ is connected if and only if the unique maps $! : X_n \to \{\ast\}$ induce an isomorphism in the colimit. Since colimits commute with (connected) colimits and since a connected colimit of singleton sets is a singleton set, a connected colimit of connected sequences is again connected.' + + - property: exact filtered colimits + proof: Since the subcategory of connected sequences is closed under filtered colimits and finite limits, this follows from the corresponding property of the category of sequences of sets. + + - property: regular + proof: We already know that the category has finite limits and coequalizers, and the inclusion functor to the regular category of sequences of sets is fully faithful and preserves finite limits and coequalizers. Thus, the claim follows from Lemma 7 here. + + - property: effective congruences + proof: Since the category of sequences of sets has effective congruences, finite limits and coequalizers, and the full subcategory of connected sequences is closed under finite limits and coequalizers, this follows from Lemma 8 here. + + - property: effective cocongruences + proof: >- + Since the category of sequences of sets $[(\IN,\leq),\Set]$ has effective cocongruences, pushouts and equalizers, and the full subcategory $[(\IN,\leq),\Set]_{\conn}$ is closed under pushouts and equalizers, this follows from Lemma 8 here as long as we can prove that the inclusion functor + $$[(\IN,\leq),\Set]_{\conn} \hookrightarrow [(\IN,\leq),\Set]$$ + preserves jointly epimorphic parallel pairs, which is not immediate because connected sequences are not closed under binary coproducts. But we can even prove this for non-parallel pairs. + + Let $f : X \to Z$ and $g : Y \to Z$ be jointly epimorphic morphisms in $[(\IN,\leq),\Set]_{\conn}$. We will prove that they are jointly epimorphic even in $[(\IN,\leq),\Set]$. Consider the subsequence $U \subseteq Z$ defined by + $$U_n \coloneqq (f_n)_*(X_n) \cup (g_n)_*(Y_n).$$ + Since $X_n \neq \varnothing$ for some $n$, we also have $U_n \neq \varnothing$ for some $n$. Any two elements of $U_n$ become eventually equally in $Z$ and hence in $U$. Hence, $U$ is connected. Therefore, also the pushout $P \coloneqq Z \sqcup_U Z$ is connected. The two coprojections $i_1,i_2 : Z \rightrightarrows P$ are morphisms with $i_1 \circ f = i_2 \circ f$ and $i_1 \circ g = i_2 \circ g$. Since $f,g$ are jointly epimorphic, we conclude $i_1 = i_2$, i.e. $U = Z$. The equation + $$Z_n = (f_n)_*(X_n) \cup (g_n)_*(Y_n)$$ + shows that $f$ and $g$ are pointwise jointly epimorphic, and therefore jointly epimorphic in $[(\IN,\leq),\Set]$. + + - property: subobject classifier + proof: >- + Define the map ("truncated subtraction") $s : \IN \to \IN$ by $s(k) = \max(0,k-1)$. We claim that the sequence + $$\Omega = \bigl(\IN \xrightarrow{s} \IN \xrightarrow{s} \IN \xrightarrow{s} \cdots\bigr)$$ + is a subobject classifier, where $\top : 1 \to \Omega$ is defined by the elements $0 \in \IN$ in every degree. Clearly, $\Omega$ is connected. Consider a monomorphism $U \to X$. By the classification of monomorphisms below, we may assume that $U \subseteq X$ is a subsequence, i.e. $U_n \subseteq X_n$ for each $n$ and the transition maps $X_n \to X_{n+1}$ restrict to the transition maps $U_n \to U_{n+1}$. + + For $x_n \in X_n$ we claim that there is some $k \geq 0$ such that its image $x_{n+k} \in X_{n+k}$ belongs to $U_{n+k}$. In fact, there is some $u_n \in U_n$, and connectedness of $X$ yields some $k \geq 0$ such that the image of $u_n$ in $X_{n+k}$ is equal to $x_{n+k}$, and this image belongs to $U_{n+k}$. Therefore, the map + $$\chi_n : X_n \to \IN, \quad x_n \mapsto \min \{k \geq 0 : x_{n+k} \in U_{n+k}\}$$ + is well-defined. We claim that the diagram + $$\begin{CD} + X_n @>{x_n \mapsto x_{n+1}}>> X_{n+1} \\ + @V{\chi_n}VV @VV{\chi_{n+1}}V \\ + \IN @>>{s}> \IN + \end{CD}$$ + commutes, i.e. that if $k$ is the smallest number with $x_{n+k} \in U_{n+k}$, then $s(k)$ is the smallest number $k'$ with $x_{n+1+k'} \in U_{n+1+k'}$. If $k=0$, then $x_n \in U_n$, hence $x_{n+1} \in U_{n+1}$, so that $k'=0=s(k)$. Now assume $k > 0$, so that $s(k)=k-1$. Then $k' = k-1$, since $x_{n+1+(k-1)} \in U_{n+1+(k-1)}$ is clear and if $\ell < k-1$, i.e. $\ell+1 < k$, then $x_{n+(\ell+1)} \notin U_{n+(\ell+1)}$ by definition of $k$, or $x_{n+1+\ell} \notin U_{n+1+\ell}$. + + Thus, $\chi = (\chi_n) : X \to \Omega$ is well-defined morphism of sequences. Since $\chi_n^*(\{0\}) = U_n$ for each $n$, the canonical morphism $U \to X \times_{\Omega} 1$ is an isomorphism. It remains to show that $\chi$ is unique with this property. + + Let $\alpha : X \to \Omega$ be another morphism of sequences with $\alpha_n^*(\{0\}) = U_n$ for every $n$, and in particular $(\alpha_n)|_{U_n} = 0$. If $x_n \in X_n$ is any element, choose $k \geq 0$ minimal with $x_{n+k} \in U_{n+k}$, where $x_{n+k}$ denotes the image of $x_n$ as before. We claim + $$\alpha_n(x_n) = k.$$ + For $k=0$, this is clear. Otherwise, we compute + $$0 = \alpha_{n+k}(x_{n+k}) = s(\alpha_{n+k-1}(x_{n+k-1}))$$ + and $\alpha_{n+k-1}(x_{n+k-1}) \neq 0$ since $x_{n+k-1} \notin U_{n+k-1}$, so that + $$\alpha_{n+k-1}(x_{n+k-1})=1.$$ + For any $i \geq 1$, the only preimage of $i$ under $s$ is $i+1$. Hence, by induction on $i \in \{1,\dotsc,k\}$, we see that + $$\alpha_{n+k-i}(x_{n+k-i})=i,$$ + which for $i=k$ gives the desired result. + label: SeqSet_conn_subobject_classifier + + - property: cogenerator + proof: >- + We claim that the subobject classifier $\Omega$ that we have constructed above is a cogenerator. In other words, if $f,g : X \rightrightarrows Y$ are distinct morphisms of connected sequences, then there is a subobject $U \subseteq Y$ such that $f^*(U) \neq g^*(U)$ as subobjects of $X$. + + Choose some $n \geq 0$ and $x_n \in X_n$ such that $f_n(x_n) \neq g_n(x_n)$ in $Y_n$. Define the subsequence $U \subseteq Y$ by + $$U_k = \begin{cases} + \varnothing & k < n \\ + Y_n \setminus \{f_n(x_n)\} & k = n \\ + Y_k & k > n + \end{cases}$$ + Since $U_k = Y_k$ for $k > n$ and $Y$ is connected, it follows that $U$ is connected. Since $f_n(x_n) \notin U_n$, the set $f^*(U)_n = (f_n)^*(U_n)$ does not contain $x_n$. But the set $g^*(U)_n = (g_n)^*(U_n)$ does contain $x_n$ because $g_n(x_n) \in U_n$. Hence, $f^*(U) \neq g^*(U)$. + references: + - SeqSet_conn_subobject_classifier + + - property: finitely accessible + proof: >- + Let $X$ be a sequence of finite sets such that there is some $k \geq 0$ such that $X_n \to X_{n+1}$ is bijective for all $n \geq k$. Then it is easy to check that $X$ is finitely presentable in the category of sequences of sets $[(\IN,\leq),\Set]$, using the fact that finite sets are finitely presentable in $\Set$. (One can show that every finitely presentable object has this form, but we will not need this fact.) It follows that if $X$ is a sequence of finite sets that eventually consists of singletons, i.e. is of the form + $$X_0 \to \cdots \to X_{k-1} \to \{\ast\} \to \{\ast\} \to \cdots,$$ + then $X$ is finitely presentable in $[(\IN,\leq),\Set]_{\conn}$. The collection of isomorphism classes of such sequences is essentially small. It remains to prove that every connected sequence of sets is a filtered colimit of such sequences. + + Let $X$ be any connected sequence. Consider the set $P$ of subsequences $U \subseteq X$ (meaning that $U_n \subseteq X_n$ and the transition maps of $U$ are restrictions of the transition maps of $X$) such that each $U_n$ is finite and there is some $k \geq 0$ such that $U_n$ is a singleton for every $n \geq k$. Then $(P,\subseteq)$ is a partial order. + + Let us check that $(P,\subseteq)$ is directed. First, it is non-empty, because we may choose some element $x_n \in X_n$, and then the sequence + $$\varnothing \to \cdots \to \varnothing \to \{x_n\} \to \{x_{n+1}\} \to \cdots$$ + belongs to $P$, where the empty sets occupy the indices $0,1,\dotsc,n-1$ and $x_m$ denotes the image of $x_n$ in $X_m$ for any $m \geq n$. + + Now let $U,V \in P$. There is some $k \geq 0$ such that both $U_n$ and $V_n$ are singletons for every $n \geq k$. Write $U_k = \{u_k\}$ and $V_k = \{v_k\}$. Then $u_k,v_k \in X_k$, so there is some $m \geq k$ such that $u_k$ and $v_k$ have the same image $x_m \in X_m$. Since $U \subseteq X$ and $V \subseteq X$ are subsequences, we have $x_m \in U_m$ and $x_m \in V_m$, so $U_m = \{x_m\}$ and $V_m = \{x_m\}$. Define $W \subseteq X$ by $W_n = U_n \cup V_n$ for $n \leq m$ and $W_n = \{x_n\}$ for $n \geq m$, where $x_n$ denotes the image of $x_m$ in $X_n$. Then $W \in P$, and clearly $U \subseteq W$ and $V \subseteq W$, as required. + + We claim that the canonical morphism + $$\colim_{U \in P} U \to X$$ + induced by the inclusion maps $U \hookrightarrow X$ is an isomorphism. In other words, for every $n \geq 0$, the component + $$\colim_{U \in P} U_n \to X_n$$ + is an isomorphism. It is injective since $(P,\leq)$ is directed and each $U_n \hookrightarrow X_n$ is injective. To show surjectivity, let $x_n \in X_n$. As before, consider the sequence $U$ defined by + $$\varnothing \to \cdots \to \varnothing \to \{x_n\} \to \{x_{n+1}\} \to \cdots.$$ + It belongs to $P$, and the element $x_n \in U_n$ induces an element of $\colim_{U \in P} U_n$ that maps to $x_n \in X_n$. + + - property: multi-complete + proof: 'We will prove that the inclusion functor $[(\IN,\leq),\Set]_{\conn} \hookrightarrow [(\IN,\leq),\Set]$ has a right multi-adjoint, so that multi-limits in the category $[(\IN,\leq),\Set]_{\conn}$ can be constructed by applying this adjoint to multi-limits in the category $[(\IN,\leq),\Set]$ (which is even complete). For a sequence of sets $X$ (not necessarily connected) and an element $c \in \colim(X)$, let $X^c \subseteq X$ be the subsequence containing those elements that map to $c$ in the colimit. That is, if $(u_n : X_n \to \colim(X))_{n \geq 0}$ is the colimit cocone, we define $(X^c)_n \coloneqq (u_n)^*(\{c\})$. It is easy to see that $X^c$ is connected. We claim that the family of inclusion maps $(X^c \to X)_{c \in \colim(X)}$ is multi-universal, i.e. that every morphism $f : Y \to X$ from a connected sequence $Y$ to $X$ factors uniquely through $X^c \hookrightarrow X$ for some unique $c \in \colim(X)$. This is because $f$ induces a map $\{\ast\} = \colim(Y) \to \colim(X)$, which corresponds to an element $c \in \colim(X)$, namely $u_n(f_n(y_n))$ for $y_n \in Y_n$ and $n \geq 0$. This element does not depend on the choice of $y_n$ and $n$. Hence, we have $f_n(y_n) \in (u_n)^*(\{c\})$ for all $y_n \in Y_n$ and $n \geq 0$, meaning that $f$ factors through $X^c \hookrightarrow X$.' + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: locally finite + proof: The endomorphisms of the sequence $\IN \to \{\ast\} \to \{\ast\} \to \cdots$ correspond to the endomorphisms of the set $\IN$. + + - property: disjoint finite products + proof: >- + If $X,Y$ are connected sequences with $X_0 = \varnothing$ and $Y_0 \neq \varnothing$, for example + $$\begin{align*} + X & = \bigl(\varnothing \to \{\ast\} \to \{\ast\} \to \cdots\bigr), \\ + Y & = \bigl(\{\ast\} \to \{\ast\} \to \{\ast\} \to \cdots\bigr), + \end{align*}$$ + then the projection $X \times Y \to Y$ is not an epimorphism. In fact, by their classification below, this would require $X_0 \times Y_0 \to Y_0$ to be surjective, which is not the case. + + - property: generator + proof: >- + Assume that $G$ is a generator sequence. For every $n \geq 0$ consider the sequence + $$\varnothing \to \cdots \to \varnothing \to \IN \to \{\ast\} \to \{\ast\} \to \cdots,$$ + where the empty sets occupy the indices $0,1,\dotsc,n$. It is connected and has a non-trivial endomorphism. Thus, there must be a morphism from $G$ to that sequence that distinguishes the two endomorphisms. Thus, $G_0,\dotsc,G_n$ are empty, while $G_{n+1}$ must be non-empty. Since this holds for all $n$, we get a contradiction. + + - property: ℵ₁-cofiltered + proof: >- + For every $n \geq 0$ consider the sequence $X^n$ defined by + $$\varnothing \to \cdots \to \varnothing \to \{\ast\} \to \{\ast\} \to \cdots,$$ + where the empty sets occupy the indices $0,1,\dotsc,n$. Clearly, $X^n$ is connected. If there is some connected sequence $Y$ admitting morphisms $Y \to X^n$ for every $n \geq 0$, this implies $Y_0=\cdots=Y_n=\varnothing$ for every $n \geq 0$. Thus, $Y$ is the empty sequence, which however is not connected. Therefore, the countable family $(X^n)_{n \geq 0}$ has no cone. + + - property: binary copowers + proof: >- + We show that the coproduct $1+1$ does not exist in $[(\IN,\leq),\Set]_{\conn}$, where $1$ denotes the terminal object, the constant sequence with value $\{\ast\}$. Since a morphism $1 \to X$ corresponds to an element of $X_0$, this amounts to a universal connected sequence of sets $X$ equipped with two elements $x,x' \in X_0$. Choose $k \geq 0$ such that their images in $X_k$ coincide. Then, by virtue of the universal property, for every connected sequence $Y$ and every pair of elements $y,y' \in Y_0$, their images in $Y_k$ coincide. The smallest counterexample is the sequence $Y$ defined by + $$\{0,1\} \xrightarrow{\id} \cdots \xrightarrow{\id} \{0,1\} \xrightarrow{!} \{0\} \xrightarrow{!} \{0\} \xrightarrow{!} \cdots,$$ + where $Y_k = \{0,1\}$ and $Y_{k+1}=\{\ast\}$. It is connected, and the elements $0,1 \in Y_0$ become only equal in $Y_{k+1}$. + Another counterexample is the subobject classifier $\Omega$ with the elements $0,k+1 \in \Omega_0$. + + Here is an alternative proof that the coproduct $1+1$, and in fact most coproducts do not exist: The projection functor $[(\IN,\leq),\Set]_{\conn} \to \Set$, $X \mapsto X_n$ has a right adjoint mapping a set $S$ to the connected sequence + $$S \xrightarrow{\id} \cdots \xrightarrow{\id} S \xrightarrow{!} \{\ast\} \xrightarrow{!} \{\ast\} \xrightarrow{!} \cdots,$$ + where the singleton sets start at index $n+1$, because a morphism from $X$ to this sequence identifies with a map $X_n \to S$. In particular, the projection functor is cocontinuous. This means that any colimit, if it exists, must be pointwise. Since the pointwise coproduct $1+1$ is not connected, it does not exist in $[(\IN,\leq),\Set]_{\conn}$. + references: + - SeqSet_conn_subobject_classifier + + - property: countable powers + proof: >- + First, we prove that the inclusion functor $[(\IN,\leq),\Set]_{\conn} \hookrightarrow [(\IN,\leq),\Set]$ is continuous. By the Yoneda Lemma, the Hom-functors $\Hom(n,-)$ for $n \geq 0$ form an extremal generating collection of the functor category $[(\IN,\leq),\Set]$. The corresponding sequence is + $$\varnothing \to \cdots \to \varnothing \to \{\ast\}\to \{\ast\} \to \cdots,$$ + where $\{\ast\}$ starts at index $n$, and this sequence is clearly connected. Now the claim follows from the dual of Lemma 1 here. + + Thus, it suffices to prove that connected sequences are not closed under countable powers of sequences, which are defined pointwise. Consider the subobject classifier + $$\Omega = \bigl(\IN \xrightarrow{s} \IN \xrightarrow{s} \IN \xrightarrow{s} \cdots\bigr)$$ + with $s(k) = \max(0,k-1)$. We will prove that $\Omega^{\IN}$ is not connected. For the two elements $n,0 \in \Omega_0 = \IN$, their images in $\Omega_k = \IN$ coincide if and only if $k \geq n$. It follows that the two elements $(0,1,2,\dotsc)$ and $(0,0,\dotsc)$ of $\Omega_0^{\IN}$ have the same image in $\Omega_k^{\IN}$ if and only if $k \geq n$ for every $n \geq 0$. Thus, no such number $k$ exists, and $\Omega^{\IN}$ is not connected. + references: + - SeqSet_conn_subobject_classifier + + - property: natural numbers object + proof: >- + Assume that a natural numbers object $(N,z,s)$ exists in $[(\IN,\leq),\Set]_{\conn}$. The morphism $z : 1 \to N$ corresponds to an element $z \in N_0$. The functor + $$[(\IN,\leq),\Set]_{\conn} \to \Set, \quad X \mapsto X_0$$ + has a right adjoint mapping a set $S$ to the connected sequence + $$S \xrightarrow{!} \{\ast\} \xrightarrow{!} \{\ast\} \xrightarrow{!} \cdots,$$ + and it preserves terminal objects. Thus, by Lemma 5 here, the triple $(N_0,z,s_0)$ is a natural numbers object of $\Set$, and therefore isomorphic to the standard natural numbers object $(\IN, 0, x \mapsto x+1)$. In particular, $N_0$ is an infinite set. + + For every $k \geq 0$ consider the connected sequence $X$ defined by + $$N_0 \xrightarrow{\id} \cdots \xrightarrow{\id} N_0 \xrightarrow{!} \{\ast\} \xrightarrow{!} \{\ast\} \xrightarrow{!} \cdots,$$ + where the singleton sets start at index $k+1$. The element $z \in N_0 = X_0$ induces a morphism $z : 1 \to X$. We define the endomorphism $r : X \to X$ by using the map $s_0 : N_0 \to N_0$ at indices $0,\dotsc,k$ and the unique maps at indices $> k$. Since $(N,z,s)$ is a natural numbers object, there is a (unique) morphism of sequences $f : N \to X$ such that $f_0(z)=z$ and $r \circ f = f \circ s$. Evaluating this equation at index $0$ yields $s_0 \circ f_0 = f_0 \circ s_0$, so that $f_0 = \id_{N_0}$. Furthermore, naturality of $f : N \to X$ for $0 \to k$ shows that the diagram + $$\begin{CD} + N_0 @>{N_{0 \to k}}>> N_k \\ + @V{\id}VV @VV{f_k}V \\ + N_0 @>>{\id}> N_0 + \end{CD}$$ + commutes. In particular, each transition map $N_0 \to N_k$ is injective. It follows that also the induced map $N_0 \to \colim_k N_k$ is injective. But this contradicts the fact that $N_0$ is infinite and $\colim_k N_k$ is a singleton set. + + - property: coaccessible + proof: >- + We will find a family of morphisms in $[(\IN,\leq),\Set]_{\conn}$ such that an object $X$ is projective to the family if and only if $X_k \to X_{k+1}$ is an isomorphism for each $k \geq 1$. Then $X_k$ is a singleton for each $k \geq 1$, and the full subcategory of such objects is equivalent to $\Set$, which is not coaccessible. It will then follow from the dual of Prop. 4.7 in Adamek-Rosicky that also $[(\IN,\leq),\Set]_{\conn}$ is not coaccessible. + + Let $k \geq 1$. Consider the monomorphism of connected sequences $U^{[k]} \hookrightarrow V^{[k]}$ defined by + $$\begin{CD} + \{a\} @>>> \cdots @>>> \{a\} @>>> \{a\} @>>> \{a\} @>>> \cdots \\ + @VVV @. @VVV @VVV @VVV @. \\ + \{a\} @>>> \cdots @>>> \{a\} @>>> \{a, b\} @>>> \{a\} @>>> \cdots + \end{CD}$$ + with the evident maps, where $\{a,b\}$ has index $k+1$ in $V^{[k]}$. Given a sequence $X$, a morphism $X \to V^{[k]}$ is the same as a map $X_{k+1} \to \{a,b\}$ such that $X_k \to X_{k+1} \to \{a,b\}$ is constant $a$. + $$\begin{CD} + X_k @>>> X_{k+1} \\ + @VVV @VVV \\ + \{a\} @>>> \{a, b\} + \end{CD}$$ + It lifts to a morphism $X \to U^{[k]}$ if and only if the map $X_{k+1} \to \{a,b\}$ is constant $a$. Hence, we see that $X$ is projective to $U^{[k]} \hookrightarrow V^{[k]}$ if and only if $X_k \to X_{k+1}$ is surjective. + + Next, consider the epimorphism of connected sequences $A^{[k]} \twoheadrightarrow B^{[k]}$ defined by + $$\begin{CD} + \{a,b\} @>>> \cdots @>>> \{a,b\} @>>> \{a,b\} @>>> \{a\} @>>> \cdots \\ + @VVV @. @VVV @VVV @VVV @. \\ + \{a,b\} @>>> \cdots @>>> \{a,b\} @>>> \{a\} @>>> \{a\} @>>> \cdots, + \end{CD}$$ + where the last $\{a,b\}$ has index $k+1$ in $A^{[k]}$ (resp. $k$ in $B^{[k]}$). A morphism $X \to B^{[k]}$ identifies with a map $X_k \to \{a,b\}$, and it lifts to a morphism $X \to A^{[k]}$ if and only if there is a map $X_{k+1} \to \{a,b\}$ that extends $X_k \to \{a,b\}$. Thus, $X$ is projective to $A^{[k]} \twoheadrightarrow B^{[k]}$ if and only if the map + $$\Hom(X_{k+1},\{a,b\}) \to \Hom(X_k,\{a,b\})$$ + induced by $X_k \to X_{k+1}$ is surjective, which is equivalent to $X_k \to X_{k+1}$ being injective. + + Therefore, the family of all $U^{[k]} \hookrightarrow V^{[k]}$ joined with the family of all $A^{[k]} \twoheadrightarrow B^{[k]}$ has the desired property. + + - property: generalized variety + proof: >- + First, we will show that every strongly finitely presentable object $X$ of $[(\IN,\leq),\Set]_{\conn}$ has injective transition maps (and hence is subterminal). The proof is rather long, but elementary. + + Suppose that $X \in [(\IN,\leq),\Set]_{\conn}$ is strongly finitely presentable, meaning that $\Hom(X,-)$ preserves sifted colimits. For ease of exposition, we will only show that the second transition map $t : X_1 \to X_2$ is injective; evident modifications of the sequences $A,B$ below show that every transition map $X_k \to X_{k+1}$ is injective. + + Define $A$ to be the connected sequence + $$\begin{CD} + \{u,u',v\} @>{\id}>> \{u,u',v\} @>>> \{u,v\} @>{!}>> \{\ast\} @>{!}>> \cdots + \end{CD}$$ + where $u,u' \mapsto u$ and $v \mapsto v$. Define $B$ to be the connected sequence + $$\begin{CD} + \{x,y\} @>{\id}>> \{x,y\} @>{!}>> \{\ast\} @>{!}>> \{\ast\} @>{!}>> \cdots. + \end{CD}$$ + Define a morphism $f : A \to B$ by the diagram + $$\begin{CD} + \{u,u',v\} @>{\id}>> \{u,u',v\} @>>> \{u,v\} @>{!}>> \{\ast\} @>{!}>> \cdots \\ + @VV{f_0}V @VV{f_0}V @VV{!}V @VV{!}V @. \\ + \{x,y\} @>{\id}>> \{x,y\} @>{!}>> \{\ast\} @>{!}>> \{\ast\} @>{!}>> \cdots, + \end{CD}$$ + where + $$f_0(u)=x, \quad f_0(u')=y, \quad f_0(v)=x.$$ + We define $g : A \to B$ similarly, but with + $$g_0(u)=x, \quad g_0(u')=y, \quad g_0(v)=y.$$ + Define a morphism $s : B \to A$ by the diagram + $$\begin{CD} + \{x,y\} @>{\id}>> \{x,y\} @>{!}>> \{\ast\} @>{!}>> \{\ast\} @>{!}>> \cdots.\\ + @VV{s_0}V @VV{s_0}V @VV{u}V @VV{!}V @. \\ + \{u,u',v\} @>{\id}>> \{u,u',v\} @>>> \{u,v\} @>{!}>> \{\ast\} @>{!}>> \cdots, + \end{CD}$$ + where $s_0(x)=u$, $s_0(y)=u'$. Then $f \circ s = g \circ s = \id_B$, so $f,g$ is a reflexive pair. Since $X$ is strongly finitely presentable, $\Hom(X,-)$ preserves reflexive coequalizers in particular, so the canonical map + $$\coeq(\Hom(X,f),\Hom(X,g)) \to \Hom(X,\coeq(f,g))$$ + is an isomorphism. The coequalizer of $f,g$ can be computed pointwise. It is obtained from $B$ by identifying $x$ with $y$, and hence is the terminal sequence. In particular, $\Hom(X,\coeq(f,g))$ is a singleton set. Hence, the coequalizer of + $$\Hom(X,f),\Hom(X,g) : \Hom(X,A) \rightrightarrows \Hom(X,B)$$ + is also a singleton set. We will next describe this coequalizer. + Morphisms $X \to B$ can be identified with maps $X_1 \to \{x,y\}$, and thus with subsets of $X_1$ by taking the fiber over $x$. + $$\begin{CD} + X_0 @>>> X_1 @>>> X_2 @>>> X_2 @>>> \cdots \\ + @VVV @VVV @VV{!}V @VV{!}V @. \\ + \{x,y\} @>{\id}>> \{x,y\} @>{!}>> \{\ast\} @>{!}>> \{\ast\} @>{!}>> \cdots + \end{CD}$$ + Morphisms $X \to A$ can be identified with commutative squares + $$\begin{CD} + X_1 @>{t}>> X_2 \\ + @VVV @VVV \\ + \{u,u',v\} @>>> \{u,v\}. + \end{CD}$$ + The map $X_2 \to \{u,v\}$ corresponds to a subset $V \subseteq X_2$ by taking the fiber over $u$, and the map $X_1 \to \{u,u',v\}$ corresponds to a pair of subsets $U \subseteq U' \subseteq X_1$ by taking the preimages of $\{u\}$ and $\{u,u'\}$, respectively. The commutativity of the diagram means that $t^*(V) = U'$. Thus, the data of a morphism $X \to A$ can be identified with a pair of subsets $U \subseteq X_1$, $V \subseteq X_2$ satisfying $U \subseteq t^*(V)$, i.e. $t_*(U) \subseteq V$. + + Under these identifications, one can easily check that $\Hom(X,f)$ sends a pair $(U,V)$ to $U \cup (X_1 \setminus t^*(V))$, while $\Hom(X,g)$ sends this pair to $U$. Hence, the coequalizer of $\Hom(X,f)$ and $\Hom(X,g)$ is the quotient of the power set $P(X_1)$ by the equivalence relation $\sim$ generated by + $$U \sim U \cup (X_1 \setminus t^*(V))$$ + for all $U \subseteq X_1$ and $V \subseteq X_2$ satisfying $U \subseteq t^*(V)$. By replacing $V$ with $X_2 \setminus V$, this can also be described as the equivalence relation generated by + $$U \sim U \cup t^*(V)$$ + whenever $U \cap t^*(V) = \varnothing$. + + Consider the following property of a subset $U \subseteq X_1$: there is some fiber $t^*(\{y\})$ such that $U \cap t^*(\{y\})$ is a non-empty proper subset of $t^*(\{y\})$. We claim that this property is invariant under $\sim$, i.e. that, for equivalent sets $U$ and $U' \coloneqq U \cup t^*(V)$ as above, $U$ satisfies this property if and only if $U'$ does. Assume first that $U$ has the property. Then $U' \cap t^*(\{y\})$ is non-empty (since $U \subseteq U'$). Choose $x \in t^*(\{y\}) \setminus U$. If $x \in U'$, then $x \in t^*(V)$, so $y \in V$, but then $U \cap t^*(\{y\}) \subseteq U \cap t^*(V) = \varnothing$, a contradiction. Thus, $x \notin U'$, showing that $U' \cap t^*(\{y\}) \neq t^*(\{y\})$, and hence $U'$ has the property. Conversely, assume that $U'$ has the property. Then $U \cap t^*(\{y\})$ is a proper subset of $t^*(\{y\})$ (since $U \subseteq U'$). Choose $x \in U' \cap t^*(\{y\})$. Since $x \in U'$, either $x \in U$, in which case we are done, or $x \in t^*(V)$. In the latter case, $y \in V$, and hence $t^*(\{y\}) \subseteq t^*(V) \subseteq U'$, contradicting the assumption on $U'$. Thus, $U$ has the property. + + Since the coequalizer of $\Hom(X,f)$ and $\Hom(X,g)$ is a singleton set, all pairs of subsets of $X_1$ are equivalent. Moreover, the subset $\varnothing$ does not have the property discussed above. It follows that no subset of $X_1$ has the property. In particular, if $x \in X_1$, then $\{x\}$ does not have the property for $y=t(x)$, i.e. $\{x\} \cap t^*(\{y\}) = t^*(\{y\})$, so $t^*(\{y\}) = \{x\}$. Therefore, $t$ is injective. + + This finishes the proof that every strongly finitely presentable object $X$ has injective transition maps. Then each $X_n$ embeds into $\colim(X)$, which is a singleton. Thus, each set $X_n$ is subterminal, and it follows easily that $X$ is isomorphic to one of the sequences + $$\varnothing \to \cdots \to \varnothing \to \{\ast\} \to \{\ast\} \to \cdots$$ + which are the representable functors $(\IN,\leq) \to \Set$. In $\Set$, a connected colimit of subterminal sets is again subterminal. It follows that the strongly finitely presentable objects of $[(\IN,\leq),\Set]_{\conn}$ are closed under connected colimits, and hence also under sifted colimits. Since not every connected sequence is of this form, $[(\IN,\leq),\Set]_{\conn}$ cannot be a generalized variety. + +special_objects: + terminal object: + description: the constant sequence $\{\ast\} \to \{\ast\} \to \cdots$ + products: + description: '[finite case] component-wise defined direct product' + +special_morphisms: + isomorphisms: + description: morphisms $f = (f_n)_{n \geq 0}$ where every $f_n$ is bijective + proof: It is a full subcategory of the category of sequences of sets, where isomorphisms are described as stated. + monomorphisms: + description: morphisms $f = (f_n)_{n \geq 0}$ where every $f_n$ is injective + proof: Morphisms with injective components are clearly monomorphisms. To prove the converse, use that the inclusion functor into the category of sequences of sets preserves finite limits (by their construction), hence preserves monomorphisms, and that monomorphisms of the category of sequences have injective components. + epimorphisms: + description: morphisms $f = (f_n)_{n \geq 0}$ where every $f_n$ is surjective + proof: Morphisms with surjective components are clearly epimorphisms. To prove the converse, use that the inclusion functor into the category of sequences of sets preserves connected colimits, hence preserves pushouts in particular, and therefore preserves epimorphisms, and that epimorphisms of the category of sequences have surjective components. diff --git a/database/data/categories/Set_arrow.yaml b/database/data/categories/Set_arrow.yaml index 1a71f485..763766cc 100644 --- a/database/data/categories/Set_arrow.yaml +++ b/database/data/categories/Set_arrow.yaml @@ -21,6 +21,7 @@ related: - SetxSet - Sh(X) - Mono + - SeqSet satisfied_properties: - property: locally small diff --git a/database/data/categories/SetxSet.yaml b/database/data/categories/SetxSet.yaml index dd98ac1e..9e916c6a 100644 --- a/database/data/categories/SetxSet.yaml +++ b/database/data/categories/SetxSet.yaml @@ -12,9 +12,11 @@ tags: related: - Set - Set_arrow + - SeqSet - Sh(X) - Set_family - DiGraph + - SetxSet_0_fin satisfied_properties: - property: locally small diff --git a/database/data/categories/SetxSet_0_fin.yaml b/database/data/categories/SetxSet_0_fin.yaml new file mode 100644 index 00000000..1e8149f7 --- /dev/null +++ b/database/data/categories/SetxSet_0_fin.yaml @@ -0,0 +1,140 @@ +id: SetxSet_0_fin +name: category of empty-or-finite pairs of sets +notation: $(\Set \times \Set)_{\varnothing,\fin}$ +objects: pairs $(A,B)$ of sets $A$ and $B$ such that $A$ is empty or $B$ is finite +morphisms: pairs of functions +description: This is a rather random full subcategory of $\Set \times \Set$. We have included it solely as an example of a category with a subobject classifier that does not have binary coproducts. +nlab_link: null + +tags: + - set theory + +related: + - Set + - SetxSet + - FinSet + +satisfied_properties: + - property: locally small + proof: It is a full subcategory of $\Set \times \Set$, which is locally small. + + - property: finite products + proof: We show that the category is closed under finite products in $\Set \times \Set$. Let $(A_i,B_i)_{i \in I}$ be a finite family in $(\Set \times \Set)_{\varnothing,\fin}$. The product in $\Set \times \Set$ is $(\prod_{i \in I} A_i, \prod_{i \in I} B_i)$. If $\prod_{i \in I} A_i$ is non-empty, every $A_i$ is non-empty. Hence, every $B_i$ is finite, and therefore $\prod_{i \in I} B_i$ is finite. + check_redundancy: false + label: SetxSet_0_fin_finite_products + + - property: equalizers + proof: In fact, $(\Set \times \Set)_{\varnothing,\fin}$ is closed under subobjects in $\Set \times \Set$, which has equalizers. Let $(C,D) \hookrightarrow (A,B)$ be a monomorphism in $\Set \times \Set$ with $(A,B) \in (\Set \times \Set)_{\varnothing,\fin}$. If $C$ is non-empty, then $A$ is non-empty, so $B$ is finite, and hence $D$, which injects into $B$, is finite. + check_redundancy: false + label: SetxSet_0_fin_equalizers + + - property: coequalizers + proof: In fact, $(\Set \times \Set)_{\varnothing,\fin}$ is closed under quotients in $\Set \times \Set$, which has coequalizers. Let $(A,B) \twoheadrightarrow (C,D)$ be an epimorphism in $\Set \times \Set$ with $(A,B) \in (\Set \times \Set)_{\varnothing,\fin}$. If $C$ is non-empty, then $A$ is non-empty since $A \to C$ is surjective. Thus, $B$ is finite. Since $B \to D$ is surjective, it follows that $D$ is finite. + + - property: strict initial object + proof: Since $(\varnothing, \varnothing)$ is clearly a strict initial object of $\Set \times \Set$ and belongs to $(\Set \times \Set)_{\varnothing,\fin}$, it is also a strict initial object of $(\Set \times \Set)_{\varnothing,\fin}$. + + - property: finite copowers + proof: In fact, $(\Set \times \Set)_{\varnothing,\fin}$ is closed under finite copowers in $\Set \times \Set$. That is, if $(A,B) \in (\Set \times \Set)_{\varnothing,\fin}$ and $I$ is a finite set, then $\coprod_{i \in I} (A,B) = (\coprod_{i \in I} A, \coprod_{i \in I} B)$ belongs to $(\Set \times \Set)_{\varnothing,\fin}$. Namely, if $\coprod_{i \in I} A$ is non-empty, then $A$ is non-empty, so $B$ is finite, and hence $\coprod_{i \in I} B$ is finite. + + - property: cokernel pairs + proof: 'Let $(f,g) : (A,B) \to (C,D)$ be a morphism in $(\Set \times \Set)_{\varnothing,\fin}$. We show that the pointwise pushout $(C,D) \sqcup_{(A,B)} (C,D) = (C \sqcup_A C, D \sqcup_B D)$ in $\Set \times \Set$ also belongs to $(\Set \times \Set)_{\varnothing,\fin}$. If $C = \varnothing$, then $C \sqcup_A C = \varnothing$, and the claim holds. Otherwise, $D$ is finite, and hence $D \sqcup_B D$ is finite.' + + - property: subobject classifier + proof: Using the classification of monomorphisms as pairs of injective maps (see below) and the fact that $\{0,1\}$ is a subobject classifier of $\Set$, it is clear that the pair $(\{0,1\}, \{0,1\})$ is a subobject classifier. + + - property: cogenerator + proof: The pair $(\{0,1\}, \{0,1\})$ is a cogenerator of $\Set \times \Set$ by this lemma and belongs to $(\Set \times \Set)_{\varnothing,\fin}$. + + - property: epi-regular + proof: Every epimorphism is the coequalizer of its kernel pair. In fact, this is true in $\Set$, hence also in $\Set \times \Set$. It remains to use that $(\Set \times \Set)_{\varnothing,\fin}$ is closed under finite limits in $\Set \times \Set$, as shown above, and that epimorphisms are pairs of surjective maps (proven below). + check_redundancy: false + references: + - SetxSet_0_fin_equalizers + - SetxSet_0_fin_finite_products + + - property: regular + proof: By the previous properties, it suffices to prove that epimorphisms are stable under pullback. Since they are pairs of surjective maps and pullbacks are constructed pointwise, this follows immediately from the corresponding property of $\Set$. + + - property: effective congruences + proof: Let $(R,S) \rightrightarrows (A,B)$ be a congruence in $(\Set \times \Set)_{\varnothing,\fin}$. Since finite limits are constructed pointwise, it is also a congruence in $\Set \times \Set$, and therefore a pair of congruences in $\Set$. Thus, the congruence is the kernel pair of $(A,B) \to (A/R,B/S)$ in $\Set \times \Set$. It remains to show that $(A/R,B/S)$ belongs to $(\Set \times \Set)_{\varnothing,\fin}$. If $A$ is empty, then $A/R$ is empty, and the claim holds. Otherwise, $B$ is finite, and hence $B/S$ is finite. + + - property: effective cocongruences + proof: More generally, let $(A,B) \rightrightarrows (R,S)$ be a coreflexive corelation in $(\Set \times \Set)_{\varnothing,\fin}$. Since binary copowers exist and the forgetful functor to $\Set \times \Set$ preserves epimorphisms (see their classification below), it is a coreflexive corelation in $\Set \times \Set$. Any coreflexive corelation in $\Set \times \Set$ is an effective cocongruence (by this result). Therefore, using this result, $(A,B) \rightrightarrows (R,S)$ is the cokernel pair of its equalizer. Since the equalizer belongs to $(\Set \times \Set)_{\varnothing,\fin}$, we are done. + + - property: ℵ₁-accessible + proof: >- + First, we will show that $(\Set \times \Set)_{\varnothing,\fin}$ is closed under $\aleph_1$-filtered colimits in $\Set \times \Set$. Let $D : \I \to (\Set \times \Set)_{\varnothing,\fin}$ be an $\aleph_1$-filtered diagram. Write $D(i) = (A(i),B(i))$, so that $\colim(D) = (\colim(A),\colim(B))$. If every $A(i)$ is empty, then $\colim(A)$ is empty, and we are done. Otherwise, there is some $i \in \I$ such that $A(i)$ is non-empty, and by passing to a final subcategory of $\I$, we may assume that $A(i)$ is non-empty for every $i \in \I$. Since $D(i) \in (\Set \times \Set)_{\varnothing,\fin}$, this means that each $B(i)$ is finite. Since $\FinSet$ is closed under $\aleph_1$-filtered colimits in $\Set$ (the proof is identical to the proof for $\Ab_{\fg}$ in MO/400763), we conclude that $\colim(B)$ is finite. Hence, $(\colim(A), \colim(B))$ is an object of $(\Set \times \Set)_{\varnothing,\fin}$. + + Countable sets are precisely the $\aleph_1$-presentable objects of $\Set$. It follows that for every countable set $C$ and every finite set $E$, the objects $(C,E)$ and $(\varnothing,C)$ are $\aleph_1$-presentable objects of $(\Set \times \Set)_{\varnothing,\fin}$. The collection of isomorphism classes of such objects is essentially small. Any object of $(\Set \times \Set)_{\varnothing,\fin}$ is either of the form $(\varnothing,X)$ for some set $X$ and therefore expressible as $\colim_{C \in P_{<\aleph_1}(X)} (\varnothing,C)$, where $P_{<\aleph_1}(X)$ is the $\aleph_1$-filtered poset of countable subsets of $X$, or of the form $(X,E)$ for a set $X$ and a finite set $E$ and therefore expressible as $\colim_{C \in P_{<\aleph_1}(X)} (C,E)$. In each case, we have expressed the object as an $\aleph_1$-filtered colimit of the selected $\aleph_1$-presentable objects. + + - property: ℵ₁-cofiltered limits + proof: >- + We will show that $(\Set \times \Set)_{\varnothing,\fin}$ is closed under $\aleph_1$-cofiltered limits in $\Set \times \Set$. Let $D : \I \to (\Set \times \Set)_{\varnothing,\fin}$ be an $\aleph_1$-cofiltered diagram. Write $D(i) = (A(i),B(i))$, so that $\lim(D) = (\lim(A),\lim(B))$. If some $A(i)$ is empty, then $\lim(A)$ is empty, and we are done. If not, since $D(i) \in (\Set \times \Set)_{\varnothing,\fin}$, each $B(i)$ is finite. Since we know that $\FinSet$ is closed under $\aleph_1$-cofiltered limits in $\Set$, we conclude that $\lim(B)$ is finite. Hence, $(\lim(A), \lim(B))$ is an object of $(\Set \times \Set)_{\varnothing,\fin}$. + references: + - finset_aleph1-cofiltered-limits + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: locally finite + proof: The object $(\IN,\varnothing)$ is valid and has infinitely many endomorphisms. + + - property: semi-strongly connected + proof: If $X$ is a non-empty set, there is no map between $(\varnothing,X)$ and $(X,\varnothing)$. + + - property: countable powers + proof: >- + The first projection functor $(\Set \times \Set)_{\varnothing,\fin} \to \Set$ mapping $(A,B)$ to $A$ is right adjoint to $A \mapsto (A,\varnothing)$ (which is a valid object), and hence preserves limits. Likewise, the second projection functor $(\Set \times \Set)_{\varnothing,\fin} \to \Set$ mapping $(A,B)$ to $B$ is right adjoint to $B \mapsto (\varnothing,B)$ (which is a valid object), and hence preserves limits. It follows that any limits in $(\Set \times \Set)_{\varnothing,\fin}$, if they exist, are computed pointwise. + + Therefore, to show that countable powers do not exist, it suffices to note that $(\{0\},\{0,1\})$ is a valid object, whereas $(\{0\},\{0,1\})^{\IN} = (\{0\}^{\IN},\{0,1\}^{\IN})$ is not, since $\{0,1\}^{\IN}$ is infinite. + label: SetxSet_0_fin_countable_powers + + - property: binary coproducts + proof: 'We will prove that the objects $(\{0\},\varnothing)$ and $(\varnothing,\IN)$ have no coproduct in $(\Set \times \Set)_{\varnothing,\fin}$, i.e. that there is no initial cocone. The category of cocones is isomorphic to the product category $\Set_* \times \IN / \FinSet$. If it has an initial object, then $\IN / \FinSet$ would have an initial object as well. Assume that $f : \IN \to X$ is initial in $\IN / \FinSet$. Let $n,m \in \IN$ with $n \neq m$. There is a map $g : \IN \to \{0,1\}$ with $g(n)=0$ and $g(m)=1$. Since $f$ is initial, there is a unique map $h : X \to \{0,1\}$ with $h \circ f = g$. Since $g(n) \neq g(m)$, it follows that $f(n) \neq f(m)$. Thus, $f : \IN \to X$ is injective, which contradicts the fact that $X$ is finite.' + + - property: generator + proof: Assume that $(A,B)$ is a generator. Since it has to distinguish the three endomorphisms of $(\{0,1\},\varnothing)$ (which is a valid object), we see that $A$ is non-empty and $B$ is empty. Using the object $(\varnothing,\{0,1\})$ (which is also valid), we see that $B$ is non-empty and $A$ is empty. This is a contradiction. + + - property: natural numbers object + proof: >- + Assume that $N = (N_A,N_B)$ is a natural numbers object of $(\Set \times \Set)_{\varnothing,\fin}$ equipped with morphisms $z : (1,1) \to N$ and $s : N \to N$, i.e. elements $z_A \in N_A$, $z_B \in N_B$, and maps $s_A : N_A \to N_A$ and $s_B : N_B \to N_B$. Since $N_A$ is non-empty, $N_B$ is finite. We claim that $(N_B, z_B, s_B)$ is a natural numbers object of $\FinSet$, which we know does not exist. + + Let $X$ be a finite set, $x_0 \in X$, and $r : X \to X$ be a map. Then $(N_A,X)$ is a valid object of $(\Set \times \Set)_{\varnothing,\fin}$, and we have morphisms $(z_A,x_0) : (1,1) \to (N_A,X)$ and $(s_A,r) : (N_A,X) \to (N_A,X)$. Since $(N_A,N_B)$ is a natural numbers object, there is a unique pair of maps $(f,g) : (N_A,N_B) \to (N_A,X)$ such that $f$ satisfies $f(z_A) = z_A$ and $f \circ s_A = s_A \circ f$, and $g$ satisfies $g(z_B) = x_0$ and $g \circ s_B = r \circ g$. These conditions are independent, and a cartesian product $P \times Q$ is a singleton if and only if both $P$ and $Q$ are singletons. Thus, there is a unique map $g : N_B \to X$ satisfying $g(z_B) = x_0$ and $g \circ s_B = r \circ g$. This proves that $(N_B, z_B, s_B)$ is a natural numbers object, as claimed. + + - property: coaccessible + proof: >- + Assume that the category is $\kappa$-coaccessible for a regular cardinal $\kappa$. In particular, every object is a limit of $\kappa$-copresentable objects. We claim that every $\kappa$-copresentable object $(A,B)$ satisfies $A \cong \{\ast\}$, so that a limit of such objects also has this property (since the projection functor is continuous, as shown before), and hence does not include every object. + + Assume that $(A,B)$ is $\kappa$-copresentable. Since $\kappa$ is regular, $(\kappa,\leq)$ is $\kappa$-filtered, so its dual $(\kappa,\geq)$ is $\kappa$-cofiltered. Consider the diagram $D : (\kappa,\geq) \to (\Set \times \Set)_{\varnothing,\fin}$ defined by $D(\alpha) = ({[\alpha,\kappa[}, \varnothing)$ on objects. If $\alpha \geq \beta$, the morphism $D(\alpha) \to D(\beta)$ is induced by the inclusion map ${[\alpha,\kappa[} \subseteq {[\beta,\kappa[}$. We have $\lim_\alpha D(\alpha) = (\varnothing,\varnothing)$. Since $(A,B)$ is $\kappa$-copresentable, the canonical map + $$\textstyle \Hom(\lim_\alpha D(\alpha),(A,B)) \to \lim_\alpha \Hom(D(\alpha),(A,B))$$ + is an isomorphism. Thus, + $$\textstyle \{\ast\} \cong \lim_\alpha \Hom({[\alpha,\kappa[},A).$$ + Since $A$ embeds into $\Hom({[\alpha,\kappa[},A)$ via constant functions, and hence into the limit, we see that $\card(A) \leq 1$. But $A = \varnothing$ is not possible, since then the limit would also be empty. Thus, $A \cong \{\ast\}$. + references: + - SetxSet_0_fin_countable_powers + +special_objects: + initial object: + description: $(0,0)$ + terminal object: + description: $(1,1)$ + products: + description: '[finite case] component-wise direct product' + +special_morphisms: + isomorphisms: + description: pairs of bijective maps + proof: This is trivial. + monomorphisms: + description: pairs of injective maps + proof: For the non-trivial direction, the construction of finite limits shows that the two projection functors to $\Set$ preserve finite limits and hence preserve monomorphisms. + epimorphisms: + description: pairs of surjective maps + proof: >- + For the non-trivial direction, let $(f,g) : (A,B) \to (C,D)$ be an epimorphism. Assume for contradiction that $f : A \to C$ is not surjective. Since $\{0,1\}$ cogenerates, then there are distinct maps $u,v : C \rightrightarrows \{0,1\}$ with $u \circ f = v \circ f$. The set $C$ is non-empty, so $D$ is finite, and $(\{0,1\},D)$ is a valid object. Then + $$(u,\id_D), (v,\id_D) : (C,D) \rightrightarrows (\{0,1\},D)$$ + are distinct morphisms satisfying $(u,\id_D) \circ (f,g) = (v,\id_D) \circ (f,g)$. This contradicts the assumption that $(f,g)$ is an epimorphism. Thus, $f$ is surjective. Now assume that $g$ is not surjective. Then there are distinct maps $u,v : D \rightrightarrows \{0,1\}$ with $u \circ g = v \circ g$. Then + $$(\id_C,u), (\id_C,v) : (C,D) \rightrightarrows (C,\{0,1\})$$ + are distinct morphisms satisfying $(\id_C,u) \circ (f,g) = (\id_C,v) \circ (f,g)$, contradicting the assumption that $(f,g)$ is an epimorphism. diff --git a/database/data/category-properties/extremal cogenerating collection.yaml b/database/data/category-properties/extremal cogenerating collection.yaml index bca930a2..ddd63a10 100644 --- a/database/data/category-properties/extremal cogenerating collection.yaml +++ b/database/data/category-properties/extremal cogenerating collection.yaml @@ -2,7 +2,7 @@ id: extremal cogenerating collection relation: has an description: >- This property refers to the existence of an extremal cogenerating collection. A collection of objects $S \subseteq \Ob(\C)$ in a category $\C$ is called an extremal cogenerating collection if it is a cogenerating collection and for every morphism $f : A \to B$, $f$ is an isomorphism if and only if for every object $Q \in S$ we have ${-} \circ f : \Hom(B, Q) \to \Hom(A, Q)$ is a bijection. Equivalently, the functor - $(\Hom(-,Q))_{Q \in S} : \C^{\op} \to (\Set^+)^S$ + $$(\Hom(-,Q))_{Q \in S} : \C^{\op} \to (\Set^+)^S$$ is faithful and conservative. If $\C$ is locally essentially small and has products, it is also equivalent to the condition that the canonical morphism $$\textstyle A \to \prod_{Q\in S} \prod_{f\in\Hom(A,Q)} Q$$ is an extremal monomorphism for every object $A$, explaining the terminology (see Prop. 5.3 at the nLab). The term "extremal cogenerating set" is more common, but within our foundations, the collection $S$ is not necessarily a set; it is just isomorphic to a set. diff --git a/database/data/macros.yaml b/database/data/macros.yaml index 6908efc6..9bf7efe1 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -35,12 +35,14 @@ \op: \mathrm{op} \c: \mathrm{c} \ff: \mathrm{ff} +\fc: \mathrm{fc} \fg: \mathrm{fg} \fp: \mathrm{fp} \ab: \mathrm{ab} \reg: \mathrm{reg} \fin: \mathrm{fin} \noiso: \mathrm{noiso} +\conn: \mathrm{conn} # standard collections \SetColl: \mathrm{Set} diff --git a/shared/structure.history.json b/shared/structure.history.json index e4d98386..d6a8a5ae 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -199,5 +199,9 @@ "Set_family_mostly_0": "2026-09-12", "Set_family": "2026-09-13", "DiGraph": "2026-09-14", - "Bin": "2026-09-14" + "Bin": "2026-09-14", + "SetxSet_0_fin": "2026-09-14", + "DiGraph_fc": "2026-09-15", + "SeqSet": "2026-09-16", + "SeqSet_conn": "2026-09-16" }