From 90d2f69645b3501546fd94321f571a6779117a30 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 13 Sep 2026 18:19:15 +0200 Subject: [PATCH 01/12] add the category of empty-or-finite pairs of sets --- database/data/categories/SetxSet.yaml | 1 + database/data/categories/SetxSet_0_fin.yaml | 140 ++++++++++++++++++++ shared/structure.history.json | 3 +- 3 files changed, 143 insertions(+), 1 deletion(-) create mode 100644 database/data/categories/SetxSet_0_fin.yaml diff --git a/database/data/categories/SetxSet.yaml b/database/data/categories/SetxSet.yaml index dd98ac1e..6c0416f8 100644 --- a/database/data/categories/SetxSet.yaml +++ b/database/data/categories/SetxSet.yaml @@ -15,6 +15,7 @@ related: - 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..ba766e8a --- /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 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/shared/structure.history.json b/shared/structure.history.json index 97656037..160015a9 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -200,5 +200,6 @@ "Set_family": "2026-09-13", "DiGraph": "2026-09-14", "Bin": "2026-09-14", - "Set_indisc": "2026-09-24" + "Set_indisc": "2026-09-24", + "SetxSet_0_fin": "2026-09-24" } From 32846f9c76ba9966ede3496bcfa1b6b1ad85cf30 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 15 Sep 2026 09:55:59 +0200 Subject: [PATCH 02/12] add the category of directed graphs with finite components --- content/inclusion-functors.md | 4 +- database/data/categories/DiGraph.yaml | 10 +- database/data/categories/DiGraph_fc.yaml | 140 ++++++++++++++++++ database/data/categories/Euclid_coprod.yaml | 5 +- .../extremal cogenerating collection.yaml | 2 +- database/data/macros.yaml | 1 + shared/structure.history.json | 3 +- 7 files changed, 155 insertions(+), 10 deletions(-) create mode 100644 database/data/categories/DiGraph_fc.yaml 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/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..a93c4a39 --- /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 $S$ is essentially small. 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/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 67c441a4..f5a63b4b 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -35,6 +35,7 @@ \op: \mathrm{op} \c: \mathrm{c} \ff: \mathrm{ff} +\fc: \mathrm{fc} \fg: \mathrm{fg} \fp: \mathrm{fp} \ab: \mathrm{ab} diff --git a/shared/structure.history.json b/shared/structure.history.json index 160015a9..6f6c8e75 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -201,5 +201,6 @@ "DiGraph": "2026-09-14", "Bin": "2026-09-14", "Set_indisc": "2026-09-24", - "SetxSet_0_fin": "2026-09-24" + "SetxSet_0_fin": "2026-09-24", + "DiGraph_fc": "2026-09-24" } From 0be4eb3a57d1099984e6492f9af6ee05eb35658b Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 16 Sep 2026 08:47:11 +0200 Subject: [PATCH 03/12] add the category of sequences of sets --- database/data/categories/SeqAb.yaml | 1 + database/data/categories/SeqSet.yaml | 59 +++++++++++++++++++++++++ database/data/categories/Set_arrow.yaml | 1 + database/data/categories/SetxSet.yaml | 1 + shared/structure.history.json | 3 +- 5 files changed, 64 insertions(+), 1 deletion(-) create mode 100644 database/data/categories/SeqSet.yaml 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..62305055 --- /dev/null +++ b/database/data/categories/SeqSet.yaml @@ -0,0 +1,59 @@ +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 + +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/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 6c0416f8..9e916c6a 100644 --- a/database/data/categories/SetxSet.yaml +++ b/database/data/categories/SetxSet.yaml @@ -12,6 +12,7 @@ tags: related: - Set - Set_arrow + - SeqSet - Sh(X) - Set_family - DiGraph diff --git a/shared/structure.history.json b/shared/structure.history.json index 6f6c8e75..3e52f5ec 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -202,5 +202,6 @@ "Bin": "2026-09-14", "Set_indisc": "2026-09-24", "SetxSet_0_fin": "2026-09-24", - "DiGraph_fc": "2026-09-24" + "DiGraph_fc": "2026-09-24", + "SeqSet": "2026-09-24" } From 3eefe2cb084db0d2e3e2ccdbd75651b46822b3a6 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 16 Sep 2026 19:36:18 +0200 Subject: [PATCH 04/12] small correction for accessibility proofs --- database/data/categories/DiGraph_fc.yaml | 2 +- database/data/categories/SetxSet_0_fin.yaml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/database/data/categories/DiGraph_fc.yaml b/database/data/categories/DiGraph_fc.yaml index a93c4a39..08420008 100644 --- a/database/data/categories/DiGraph_fc.yaml +++ b/database/data/categories/DiGraph_fc.yaml @@ -57,7 +57,7 @@ satisfied_properties: 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 $S$ is essentially small. 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}$. + 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$. diff --git a/database/data/categories/SetxSet_0_fin.yaml b/database/data/categories/SetxSet_0_fin.yaml index ba766e8a..1e8149f7 100644 --- a/database/data/categories/SetxSet_0_fin.yaml +++ b/database/data/categories/SetxSet_0_fin.yaml @@ -66,7 +66,7 @@ satisfied_properties: 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 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. + 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: >- From 351992b59ba65dc5e122377bb0f4961add1ea667 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 19 Sep 2026 17:09:35 +0200 Subject: [PATCH 05/12] left adjoints preserve natural numbers objects --- content/natural_numbers_objects.md | 32 ++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) 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. +::: From 067b0bdaa985c246c2cd892b22862cd050d0eac8 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Wed, 16 Sep 2026 19:36:30 +0200 Subject: [PATCH 06/12] add the category of connected sequences of sets --- content/subcategories.md | 16 +- database/data/categories/SeqSet.yaml | 1 + database/data/categories/SeqSet_conn.yaml | 308 ++++++++++++++++++++++ database/data/macros.yaml | 1 + shared/structure.history.json | 3 +- 5 files changed, 322 insertions(+), 7 deletions(-) create mode 100644 database/data/categories/SeqSet_conn.yaml 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/SeqSet.yaml b/database/data/categories/SeqSet.yaml index 62305055..b1d55c16 100644 --- a/database/data/categories/SeqSet.yaml +++ b/database/data/categories/SeqSet.yaml @@ -14,6 +14,7 @@ related: - Set_arrow - SeqAb - SetxSet + - SeqSet_conn satisfied_properties: - property: locally small diff --git a/database/data/categories/SeqSet_conn.yaml b/database/data/categories/SeqSet_conn.yaml new file mode 100644 index 00000000..b4d540b3 --- /dev/null +++ b/database/data/categories/SeqSet_conn.yaml @@ -0,0 +1,308 @@ +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, consisting of those sequences + $$X_0 \to X_1 \to X_2 \to \cdots$$ + whose colimit is a singleton set. Equivalently, the following two conditions are satisfied: (1) There is some $n \geq 0$ such that $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$ and $y$ map to the same element of $X_m$. + + We have added this category as 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 was 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 on colimits. 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 on colimits. Since colimits commute with colimits and 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 that the inclusion functor into 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. This is not immediate because connected sequences are not closed under binary coproducts. In fact, we can prove the stronger statement that the inclusion preserves jointly epimorphic pairs, not necessarily parallel ones. + + 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 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$ eventually become equal in $Z$ and hence in $U$. Thus, $U$ is connected. Therefore, the pushout $P \coloneqq Z \sqcup_U Z$ is also connected. The two coprojections $i_1,i_2 : Z \rightrightarrows P$ satisfy $i_1 \circ f = i_2 \circ f$ and $i_1 \circ g = i_2 \circ g$. Since $f$ and $g$ are jointly epimorphic, we conclude that $i_1 = i_2$, and hence $U = Z$. Thus, + $$Z_n = (f_n)_*(X_n) \cup (g_n)_*(Y_n)$$ + for every $n$, so $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 given 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}$. 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. In other words, if $k$ is the smallest number such that $x_{n+k} \in U_{n+k}$, then $s(k)$ is the smallest number $k'$ such that $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)}$ and, if $\ell < k-1$, then $\ell+1 < k$, so $x_{n+1+\ell} = x_{n+(\ell+1)} \notin U_{n+(\ell+1)}$ by the definition of $k$. + + Thus, $\chi = (\chi_n) : X \to \Omega$ is a 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 such that $x_{n+k} \in U_{n+k}$, where $x_{n+k}$ denotes the image of $x_n$ as before. We claim that + $$\alpha_n(x_n) = k.$$ + For $k=0$, this is clear. Otherwise, we have + $$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}$. Hence + $$\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 obtain + $$\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$ 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$. On the other hand, $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$ for which $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 partially ordered set. + + 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 consisting of 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 a unique $c \in \colim(X)$. Indeed, $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 any $y_n \in Y_n$ and $n \geq 0$. This element is independent of 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$, so $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. Indeed, by the classification of epimorphisms 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. 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 this sequence that distinguishes the two endomorphisms. Hence, $G_0,\dotsc,G_n$ must be empty, while $G_{n+1}$ must be non-empty. Since this holds for every $n$, we obtain 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 were a connected sequence $Y$ admitting morphisms $Y \to X^n$ for every $n \geq 0$, then $Y_0=\cdots=Y_n=\varnothing$ for every $n \geq 0$. Thus, $Y$ would be the empty sequence, which 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 would amount 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 the universal property, for every connected sequence $Y$ and every pair of elements $y,y' \in Y_0$, their images in $Y_k$ must coincide. A 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, but the elements $0,1 \in Y_0$ only become equal in $Y_{k+1}$. + Another counterexample is the subobject classifier $\Omega$, whose elements $0,k+1 \in \Omega_0$ become equal only after $k+1$ steps. + + 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 that maps 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 corresponds to a map $X_n \to S$. In particular, the projection functor is cocontinuous. Hence, any colimit, if it exists, must be computed 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. The claim now follows from the dual of Lemma 1 here. Alternatively, each projection functor $[(\IN,\leq),\Set]_{\conn} \to \Set$, $X \mapsto X_n$, is representable by the sequence just described and hence continuous. + + Thus, it suffices to prove that connected sequences are not closed under countable powers, 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 $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 infinite. + + 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 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 $[(\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 the composite + $$X_k \to X_{k+1} \to \{a,b\}$$ + is constant at $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 at $a$. Hence, $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]}$ (and index $k$ in $B^{[k]}$). A morphism $X \to B^{[k]}$ corresponds to 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\}$ extending $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 consisting of all $U^{[k]} \hookrightarrow V^{[k]}$ together with 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'$ map to $u$ and $v$ maps to $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.$$ + 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$ and $s_0(y)=u'$. Then $f \circ s = g \circ s = \id_B$, so $f,g$ form 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\})$ is a proper subset of $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}$ for which every $f_n$ is bijective + proof: It is a full subcategory of the category of sequences of sets, where isomorphisms are characterized as stated. + monomorphisms: + description: morphisms $f = (f_n)_{n \geq 0}$ for which every $f_n$ is injective + proof: Morphisms with injective components are clearly monomorphisms. Conversely, the inclusion functor into the category of sequences of sets preserves finite limits (by their construction), hence preserves monomorphisms. Since monomorphisms in the category of sequences have injective components, every monomorphism in $[(\IN,\leq),\Set]_{\conn}$ has injective components. + epimorphisms: + description: morphisms $f = (f_n)_{n \geq 0}$ for which every $f_n$ is surjective + proof: Morphisms with surjective components are clearly epimorphisms. Conversely, the inclusion functor into the category of sequences of sets preserves connected colimits (by their construction), and hence pushouts in particular. It therefore preserves epimorphisms. Since epimorphisms in the category of sequences have surjective components, every epimorphism in $[(\IN,\leq),\Set]_{\conn}$ has surjective components. diff --git a/database/data/macros.yaml b/database/data/macros.yaml index f5a63b4b..cd5e5cdb 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -42,6 +42,7 @@ \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 3e52f5ec..f638e3a7 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -203,5 +203,6 @@ "Set_indisc": "2026-09-24", "SetxSet_0_fin": "2026-09-24", "DiGraph_fc": "2026-09-24", - "SeqSet": "2026-09-24" + "SeqSet": "2026-09-24", + "SeqSet_conn": "2026-09-24" } From f629341ef1b2ff9f792497f282f815548385c989 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 24 Sep 2026 12:46:28 +0200 Subject: [PATCH 07/12] add the category of Z-sets --- database/data/categories/M-Set.yaml | 8 ++++---- database/data/categories/R-Mod.yaml | 3 ++- database/data/categories/Z-Set.yaml | 26 ++++++++++++++++++++++++++ shared/structure.history.json | 3 ++- 4 files changed, 34 insertions(+), 6 deletions(-) create mode 100644 database/data/categories/Z-Set.yaml diff --git a/database/data/categories/M-Set.yaml b/database/data/categories/M-Set.yaml index 6fa21d11..6e36a8b6 100644 --- a/database/data/categories/M-Set.yaml +++ b/database/data/categories/M-Set.yaml @@ -34,7 +34,7 @@ unsatisfied_properties: undecidable_properties: - property: semi-strongly connected # TODO: decide if we want to add separate children entries to decide this for some cases. - proof: If this category is semi-strongly connected depends on the choice of $M$. For $M = 1$ it is, for $M = \IZ$ it is not. In general, if $G$ is a group, then $G{-}\Set$ is semi-strongly connected if and only if for all subgroups $H,K \subseteq G$, $H$ is subconjugated to $K$ or $K$ is subconjugated to $H$. If $G$ is abelian, this means that the poset of subgroups is linear, in which case $G$ is either isomorphic to $\IZ/p^n$ or to $\IZ/p^{\infty}$ for a prime $p$. See also MSE/5129804. + proof: If this category is semi-strongly connected depends on the choice of $M$. For $M = 1$ it is, for $M = \IZ$ it is not (see the entry for $\IZ{-}\Set$). In general, if $G$ is a group, then $G{-}\Set$ is semi-strongly connected if and only if for all subgroups $H,K \subseteq G$, $H$ is subconjugated to $K$ or $K$ is subconjugated to $H$. If $G$ is abelian, this means that the poset of subgroups is linear, in which case $G$ is either isomorphic to $\IZ/p^n$ or to $\IZ/p^{\infty}$ for a prime $p$. See also MSE/5129804. special_objects: initial object: @@ -42,11 +42,11 @@ special_objects: terminal object: description: singleton set with the unique action coproducts: - description: disjoint union with obvious $M$-action + description: disjoint union with the obvious action products: - description: direct products with the evident $M$-action + description: direct product with the obvious action special_morphisms: epimorphisms: description: surjective morphisms - proof: More generally, epimorphisms in functor categories $[\C,\Set]$ can be detected pointwise, since pushouts can be constructed pointwise. This is applied here to the one-object category corresponding to $M$. + proof: More generally, epimorphisms in functor categories $[\C,\Set]$ can be detected pointwise, since pushouts can be constructed pointwise. This is applied here to the one-object category corresponding to a monoid. diff --git a/database/data/categories/R-Mod.yaml b/database/data/categories/R-Mod.yaml index f717797b..d7dc616b 100644 --- a/database/data/categories/R-Mod.yaml +++ b/database/data/categories/R-Mod.yaml @@ -10,12 +10,13 @@ tags: - algebra related: - - M-Set - Ab - Vect - grMod_G(R) - Proj_fg(Re) - Free_fg(ZxZ) + - M-Set + - Z-Set satisfied_properties: - property: locally small diff --git a/database/data/categories/Z-Set.yaml b/database/data/categories/Z-Set.yaml new file mode 100644 index 00000000..f75ca940 --- /dev/null +++ b/database/data/categories/Z-Set.yaml @@ -0,0 +1,26 @@ +id: Z-Set +name: category of Z-sets +notation: $\IZ{-}\Set$ +objects: sets with an action of the additive group $\IZ$ +morphisms: maps that are compatible with the action +description: 'This is the special case of the category of $M$-sets, where $M$ is the additive group of integers. Objects can be identified with pairs $(X,\sigma)$, where $X$ is a set and $\sigma : X \to X$ is a permutation on $X$.' +nlab_link: https://ncatlab.org/nlab/show/MSet +parent: M-Set + +tags: + - set theory + - combinatorics + +related: + - Set + - R-Mod + +satisfied_properties: [] + +unsatisfied_properties: + - property: semi-strongly connected + proof: In general, if $G$ is a group and $H,K$ are subgroups of $G$, then there is a morphism of $G$-sets $G/H \to G/K$ if and only if $H$ is contained in a conjugate of $K$. In particular, if $G$ is abelian, this requires $H \subseteq K$. Thus, if $G$ is an abelian group with two subgroups that are not contained in each other, $G{-}\Set$ is not semi-strongly connected. The additive group $\IZ$ has this property; for instance, consider $2\IZ$ and $3\IZ$. See also MSE/5129804. + +special_objects: {} + +special_morphisms: {} diff --git a/shared/structure.history.json b/shared/structure.history.json index f638e3a7..6d129026 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -204,5 +204,6 @@ "SetxSet_0_fin": "2026-09-24", "DiGraph_fc": "2026-09-24", "SeqSet": "2026-09-24", - "SeqSet_conn": "2026-09-24" + "SeqSet_conn": "2026-09-24", + "Z-Set": "2026-09-24" } From 797ed8f87c345bf56d9a5fbb0e853c5d5a852894 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 24 Sep 2026 12:58:42 +0200 Subject: [PATCH 08/12] add the category of finite Z-sets --- database/data/categories/FinSet.yaml | 2 + database/data/categories/Z-FinSet.yaml | 97 ++++++++++++++++++++++++++ database/data/categories/Z-Set.yaml | 4 +- shared/structure.history.json | 3 +- 4 files changed, 104 insertions(+), 2 deletions(-) create mode 100644 database/data/categories/Z-FinSet.yaml diff --git a/database/data/categories/FinSet.yaml b/database/data/categories/FinSet.yaml index b55f78c7..9dbecfb3 100644 --- a/database/data/categories/FinSet.yaml +++ b/database/data/categories/FinSet.yaml @@ -20,6 +20,7 @@ related: - FinSet_even - FinSet_odd - FinSet_power_3 + - Z-FinSet satisfied_properties: - property: locally small @@ -59,6 +60,7 @@ unsatisfied_properties: - property: natural numbers object proof: By Lemma 2 here, if $(N,z,s)$ is a natural numbers object, then $N \cong 1 \sqcup N$. But there is no finite set with this property. + label: FinSet_no_NNO special_objects: initial object: diff --git a/database/data/categories/Z-FinSet.yaml b/database/data/categories/Z-FinSet.yaml new file mode 100644 index 00000000..cacfba17 --- /dev/null +++ b/database/data/categories/Z-FinSet.yaml @@ -0,0 +1,97 @@ +id: Z-FinSet +name: category of finite Z-sets +notation: $\IZ{-}\FinSet$ +objects: finite sets with an action of the additive group $\IZ$, i.e. a permutation +morphisms: maps that are compatible with the action, i.e. commute with the permutation +description: 'This is a full subcategory of the Grothendieck topos $\IZ{-}\Set$, and provides an example of an elementary topos that has no generator and no cogenerator. Objects can be identified with pairs $(X,\sigma)$, where $X$ is a finite set and $\sigma : X \to X$ is a permutation of $X$. A morphism $(X,\sigma) \to (Y,\tau)$ is a map $f : X \to Y$ satisfying $\tau \circ f = f \circ \sigma$.' +nlab_link: null + +tags: + - set theory + - combinatorics + +related: + - Z-Set + - M-Set + - FinSet + - Set + +satisfied_properties: + - property: locally small + proof: It is a full subcategory of $\IZ{-}\Set$, which is locally small. + + - property: locally finite + proof: This follows easily from the fact that $\FinSet$ is locally finite. + + - property: essentially countable + proof: This is because the category is locally small and every object is isomorphic to an object of the form $(\{1,\dotsc,n\},\sigma)$, where $n \in \IN$ and $\sigma$ is a permutation of $\{1,\dotsc,n\}$. + + - property: finitely complete + proof: >- + The category is the functor category $[B\IZ,\FinSet]$, so this follows from the fact that $\FinSet$ is finitely complete. Concretely, a finite limit of finite $\IZ$-sets $(X_i,\sigma_i)$ is constructed using the finite limit of the underlying finite sets $X_i$, equipped with the obvious permutation induced by the $\sigma_i$. + + Remark: The same works with finite colimits. + check_redundancy: false + + - property: cartesian closed + proof: 'We already know that finite products exist. Exponentials exist because $\IZ{-}\Set$ is cartesian closed, and the full subcategory $\IZ{-}\FinSet$ is closed under exponentials. Concretely, the exponential of two $\IZ$-sets $(X,\sigma)$ and $(Y,\tau)$ is $(\Hom(X,Y),\rho)$, where $\Hom(X,Y)$ is the set of maps $f : X \to Y$ and $\rho(f) = \tau \circ f \circ \sigma^{-1}$. If $X,Y$ are finite, then $\Hom(X,Y)$ is finite as well.' + + - property: subobject classifier + proof: 'We already know that finite limits exist. By the description of monomorphisms below, the subobjects of $(X,\sigma)$ are the objects $(U,\sigma|_U)$, where $U \subseteq X$ is a subset such that $\sigma_*(U)=U$, and $\sigma|_U : U \to U$ is the restricted permutation. The subset corresponds to a map of sets $f : X \to \{0,1\}$ with $f^*(\{1\}) = U$, and the condition $\sigma_*(U) = U$ is equivalent to $f$ being a morphism $(X,\sigma) \to (\{0,1\},\id)$. This shows that $(\{0,1\},\id)$ is a subobject classifier in both $\IZ{-}\FinSet$ and $\IZ{-}\Set$.' + + - property: ℵ₁-cofiltered limits + proof: Using that $\FinSet$ is closed under $\aleph_1$-cofiltered limits in $\Set$, and that the forgetful functor $\IZ{-}\Set \to \Set$ is continuous, it follows immediately that $\IZ{-}\FinSet$ is closed under $\aleph_1$-cofiltered limits in $\IZ{-}\Set$. + references: + - finset_aleph1-cofiltered-limits + +unsatisfied_properties: + - property: skeletal + proof: The two terminal objects $(\{0\},\id)$ and $(\{1\},\id)$ are isomorphic, but not equal. + + - property: small + proof: For every set $X$ this category contains the terminal object $(\{X\},\id)$. + + - property: countable + proof: For every set $X$ this category contains the terminal object $(\{X\},\id)$. + + - property: generator + proof: >- + Assume that $(G,\gamma)$ is a generator of $\IZ{-}\FinSet$. Then $G$ cannot be empty, since otherwise $\IZ{-}\FinSet$ would be thin, which is absurd. Choose an element $g \in G$. Since $\gamma$ is a permutation of a finite set, there is some $n \geq 2$ with $\gamma^n(g)=g$. + + Choose a natural number $m \geq 2$ that does not divide $n$ (for example, $m=n+1$), and consider the finite set $X = \{0,1,\dotsc,m-1\}$ equipped with the permutation $\sigma$ defined by $\sigma(x) = (x+1) \bmod m$. Since $(X,\sigma)$ has a non-trivial endomorphism, for example $\sigma$, and $(G,\gamma)$ is a generator, there is a morphism $(G,\gamma) \to (X,\sigma)$. If $x \in X$ denotes the image of $g \in G$, we conclude that $\sigma^n(x)=x$. By construction of $\sigma$, this implies $m \mid n$, which contradicts our assumption on $m$. + + - property: cogenerator + proof: >- + Assume that $(Q,\rho)$ is a cogenerator of $\IZ{-}\FinSet$. Choose $k \geq 1$ with $\rho^k = \id_Q$. Now consider the finite set $X = \{0,1,\dotsc,2k-1\}$ equipped with the permutation $\sigma$ defined by $\sigma(x) = (x+1) \bmod 2k$. The object $(X,\sigma)$ has a non-trivial endomorphism $g$ defined by $g(x) = (x+k) \bmod 2k$, i.e. $g = \sigma^k$. Since $(Q,\rho)$ is a cogenerator, there is a morphism $f : (X,\sigma) \to (Q,\rho)$ with $f \circ g \neq f$. But since $f$ is a morphism, we have + $$f \circ g = f \circ \sigma^k = \rho^k \circ f = f.$$ + + - property: semi-strongly connected + proof: The same reasoning as for $\IZ{-}\Set$ shows that if an abelian group $G$ has two subgroups of finite index that are not contained in each other, then $G{-}\FinSet$ is not semi-strongly connected. Since $\IZ$ has such subgroups, e.g. $2\IZ$ and $3\IZ$, the category $\IZ{-}\FinSet$ is not semi-strongly connected. + references: + - Z-Set_not_semi-strongly_connected + + - property: natural numbers object + proof: We can copy the proof from $\FinSet$. + references: + - FinSet_no_NNO + +special_objects: + initial object: + description: $(\varnothing,\id)$ + terminal object: + description: $(\{\ast\},\id)$ + coproducts: + description: '[finite case] disjoint union with the obvious action' + products: + description: '[finite case] direct product with the obvious action' + +special_morphisms: + isomorphisms: + description: bijective morphisms + proof: This is inherited from $\IZ{-}\Set$. + monomorphisms: + description: injective morphisms + proof: The non-trivial direction follows from the fact that the inclusion functor to the $\IZ{-}\Set$ preserves finite limits (by their construction), hence preserves monomorphisms, and the description of monomorphisms in $\IZ{-}\Set$. + epimorphisms: + description: surjective morphisms + proof: The non-trivial direction follows from the fact that the inclusion functor to the $\IZ{-}\Set$ preserves finite colimits (by their construction), hence preserves epimorphisms, and the description of epimorphisms in $\IZ{-}\Set$. diff --git a/database/data/categories/Z-Set.yaml b/database/data/categories/Z-Set.yaml index f75ca940..03d1ab81 100644 --- a/database/data/categories/Z-Set.yaml +++ b/database/data/categories/Z-Set.yaml @@ -3,7 +3,7 @@ name: category of Z-sets notation: $\IZ{-}\Set$ objects: sets with an action of the additive group $\IZ$ morphisms: maps that are compatible with the action -description: 'This is the special case of the category of $M$-sets, where $M$ is the additive group of integers. Objects can be identified with pairs $(X,\sigma)$, where $X$ is a set and $\sigma : X \to X$ is a permutation on $X$.' +description: 'This is the special case of the category of $M$-sets, where $M$ is the additive group of integers. Objects can be identified with pairs $(X,\sigma)$, where $X$ is a set and $\sigma : X \to X$ is a permutation on $X$. A morphism $(X,\sigma) \to (Y,\tau)$ is a map $f : X \to Y$ satisfying $\tau \circ f = f \circ \sigma$.' nlab_link: https://ncatlab.org/nlab/show/MSet parent: M-Set @@ -12,6 +12,7 @@ tags: - combinatorics related: + - Z-FinSet - Set - R-Mod @@ -20,6 +21,7 @@ satisfied_properties: [] unsatisfied_properties: - property: semi-strongly connected proof: In general, if $G$ is a group and $H,K$ are subgroups of $G$, then there is a morphism of $G$-sets $G/H \to G/K$ if and only if $H$ is contained in a conjugate of $K$. In particular, if $G$ is abelian, this requires $H \subseteq K$. Thus, if $G$ is an abelian group with two subgroups that are not contained in each other, $G{-}\Set$ is not semi-strongly connected. The additive group $\IZ$ has this property; for instance, consider $2\IZ$ and $3\IZ$. See also MSE/5129804. + label: Z-Set_not_semi-strongly_connected special_objects: {} diff --git a/shared/structure.history.json b/shared/structure.history.json index 6d129026..234e1abb 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -205,5 +205,6 @@ "DiGraph_fc": "2026-09-24", "SeqSet": "2026-09-24", "SeqSet_conn": "2026-09-24", - "Z-Set": "2026-09-24" + "Z-Set": "2026-09-24", + "Z-FinSet": "2026-09-24" } From 75800c425fd03effeba106eebaf0ed0bf3a391ae Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 24 Sep 2026 15:51:41 +0200 Subject: [PATCH 09/12] increase the number of recent structures on home page --- src/routes/+page.server.ts | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/routes/+page.server.ts b/src/routes/+page.server.ts index 47b1e6bd..0df7537d 100644 --- a/src/routes/+page.server.ts +++ b/src/routes/+page.server.ts @@ -5,6 +5,8 @@ import { to_placeholders } from '$shared/utils' import { error } from 'node:console' import structure_history from '$shared/structure.history.json' +const NUMBER_RECENT_STRUCTURES = 20 + export const load = () => { const structure_number = db .prepare('SELECT COUNT(*) FROM structures') @@ -91,7 +93,7 @@ export const load = () => { const recent_structures_ids = Object.entries(structure_history) .sort((a, b) => b[1].localeCompare(a[1])) - .slice(0, 10) + .slice(0, NUMBER_RECENT_STRUCTURES) .map((a) => a[0]) const recent_structures = db From 3a7c35dd34f1c37b33f3c52040efd3bcab3a6fef Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 24 Sep 2026 21:07:18 +0200 Subject: [PATCH 10/12] reword definitions of total and cototal categories --- database/data/category-properties/cototal.yaml | 4 ++-- database/data/category-properties/total.yaml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/database/data/category-properties/cototal.yaml b/database/data/category-properties/cototal.yaml index a8046974..539fbab1 100644 --- a/database/data/category-properties/cototal.yaml +++ b/database/data/category-properties/cototal.yaml @@ -6,8 +6,8 @@ description: >-
  • The contravariant Yoneda embedding $$y : \C^{\op} \to [\C, \Set]$$ has a left adjoint. -
  • Every discrete opfibration $X : \I \to \C$ (with $\I$ not necessarily essentially small) whose fibers are bijective to sets has a limit in $\C$. (Recall that $X$ is a discrete opfibration if for every morphism $f : X_i \to Y$ in $\C$ there exists a unique $\alpha : i \to j$ in $\I$ such that $X_\alpha = f$.)
    • -
  • Let $X : \I \to \C$ be a diagram (with $\I$ not necessarily essentially small) such that for each object $Y$ of $\C$, the collection of connected components of the comma category $X \downarrow Y$ is essentially small, i.e. bijective to a set. Then $X$ has a limit in $\C$.
    • +
  • Every discrete opfibration $D : \I \to \C$ (with $\I$ not necessarily essentially small) with the property that each fiber $D^*(\{X\}) = \{i \in \Ob(\C) : D_i = X\}$ is essentially small (bijective to a set), has a limit in $\C$.
    • +
  • Let $D : \I \to \C$ be a diagram (with $\I$ not necessarily essentially small) such that for each object $X$ of $\C$, the collection $\pi_0(D \downarrow X)$ of connected components of the comma category $D \downarrow X$ is essentially small. Then $D$ has a limit in $\C$.
    • The equivalence is proven as Thm. 5.2 and 5.5 in G. M. Kelly, A survey of totality for enriched and ordinary categories. diff --git a/database/data/category-properties/total.yaml b/database/data/category-properties/total.yaml index ef8a1970..54a6f068 100644 --- a/database/data/category-properties/total.yaml +++ b/database/data/category-properties/total.yaml @@ -6,8 +6,8 @@ description: >-
  • The covariant Yoneda embedding $$y : \C \to [\C^{\op}, \Set]$$ has a left adjoint. For a concrete example of how such a left adjoint could look, see here. -
  • Every discrete fibration $X : \I \to \C$ (with $\I$ not necessarily essentially small) whose fibers are bijective to sets has a colimit in $\C$. (Recall that $X$ is a discrete fibration if for every morphism $f : Y \to X_i$ in $\C$ there exists a unique $\alpha : j \to i$ in $\I$ such that $X_\alpha = f$.)
    • -
  • Let $X : \I \to \C$ be a diagram (with $\I$ not necessarily essentially small) such that for each object $Y$ of $\C$, the collection of connected components of the comma category $Y \downarrow X$ is essentially small. Then $X$ has a colimit in $\C$.
    • +
  • Every discrete fibration $D : \I \to \C$ (with $\I$ not necessarily essentially small) with the property that each fiber $D^*(\{X\}) = \{i \in \Ob(\C) : D_i = X\}$ is essentially small (bijective to a set), has a colimit in $\C$.
    • +
  • Let $D : \I \to \C$ be a diagram (with $\I$ not necessarily essentially small) such that for each object $X$ of $\C$, the collection $\pi_0(X \downarrow D)$ of connected components of the comma category $X \downarrow D$ is essentially small. Then $D$ has a colimit in $\C$.
    • The equivalence is proven as Thm. 5.2 and 5.5 in G. M. Kelly, A survey of totality for enriched and ordinary categories. From 0082d16c78694a9219aa2032e65b477067d2db1b Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 24 Sep 2026 21:33:23 +0200 Subject: [PATCH 11/12] mention hypercomplete and hypercocomplete more explicitly in total and cototal proofs but the properties are not added yet --- .cspell.json | 2 ++ content/missing_cogenerator.md | 6 ++++-- database/data/categories/CAlg(R).yaml | 5 +++-- database/data/categories/Cat.yaml | 5 +++-- database/data/categories/Haus.yaml | 8 +++++--- database/data/categories/SemiGrp.yaml | 5 +++-- database/data/categories/Vect_family_mostly_0.yaml | 4 +++- database/data/category-implications/total.yaml | 2 ++ database/data/category-properties/cototal.yaml | 2 +- database/data/category-properties/total.yaml | 2 +- 10 files changed, 27 insertions(+), 14 deletions(-) diff --git a/.cspell.json b/.cspell.json index 46c8ab6c..45d3deb0 100644 --- a/.cspell.json +++ b/.cspell.json @@ -214,8 +214,10 @@ "Hušek", "hypercategories", "hypercategory", + "hypercocomplete", "hypercollection", "hypercollections", + "hypercomplete", "idempotents", "Ieke", "indeterminates", diff --git a/content/missing_cogenerator.md b/content/missing_cogenerator.md index 36a1fee9..3e95430d 100644 --- a/content/missing_cogenerator.md +++ b/content/missing_cogenerator.md @@ -12,11 +12,13 @@ Let $\C$ be a pointed category with a faithful functor $U: \C \to \Set$. Assume 1. For any $X \in \F$ and any $Y \in \C$, every non-zero morphism $f: X \to Y$ is injective on underlying sets. 2. For every $Y \in \C$ there is some object $X \in \F$ such that $\card(U(X)) > \card(U(Y))$. -Then $\C$ does not have a cogenerator. Moreover, $\C$ is not cototal. +Then $\C$ does not have a cogenerator. Moreover, $\C$ is not hypercocomplete, and hence, not cototal. ::: ::: Proof Assume that there is a cogenerator $Y$. By assumption (2) there is an object $X \in \F$ such that $U(X)$ is larger than $U(Y)$ (w.r.t. cardinalities). Since $0,\id_X : X \rightrightarrows X$ are distinct, there is a morphism $f : X \to Y$ with $f \neq 0$. But then $U(f) : U(X) \to U(Y)$ is injective by assumption (1), which contradicts our choice of $X$. -Now assume that $\C$ is cototal. Using the axiom of choice, we may assume that for each small cardinal $\kappa$, there is at most one element $X \in \F$ such that $\card(U(X)) = \kappa$. Treating $\F$ as a discrete diagram in $\C$, assumption (1) implies that for any object $Y$ of $\C$, the collection of cocones $\F \to Y$ is essentially small, since the maps $X \to Y$ with $\card(U(X)) > \card(U(Y))$ must all be zero in such a cocone. Therefore, by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the implication (i) $\Rightarrow$ (iii)), $\C$ must have a coproduct $Y$ of all elements of $\F$. But then by assumption (2), there exists $X \in \F$ such that $\card(U(X)) > \card(U(Y))$; and since $\C$ is pointed, the coprojection $X \to Y$ must be split monic and therefore non-zero. Using assumption (1), we get a contradiction. +Now assume that $\C$ is hypercocomplete. Using the axiom of choice, we may assume that for each small cardinal $\kappa$, there is at most one element $X \in \F$ such that $\card(U(X)) = \kappa$. Treating $\F$ as a discrete diagram in $\C$, assumption (1) implies that for any object $Y$ of $\C$, the collection of cocones $\F \to Y$ is essentially small, since the maps $X \to Y$ with $\card(U(X)) > \card(U(Y))$ must all be zero in such a cocone. Since $\C$ is hypercocomplete, there exists a coproduct $Y$ of all elements of $\F$. But then by assumption (2), there exists $X \in \F$ such that $\card(U(X)) > \card(U(Y))$; and since $\C$ is pointed, the coprojection $X \to Y$ must be split monic and therefore non-zero. Using assumption (1), we get a contradiction. + +Finally, any cototal category is hypercocomplete by Thm. 5.6 in G. M. Kelly, A survey of totality for enriched and ordinary categories. ::: diff --git a/database/data/categories/CAlg(R).yaml b/database/data/categories/CAlg(R).yaml index ad6ebd19..13f8ba7e 100644 --- a/database/data/categories/CAlg(R).yaml +++ b/database/data/categories/CAlg(R).yaml @@ -82,10 +82,11 @@ unsatisfied_properties: In the limit, it induces the inclusion $K[X] \hookrightarrow K[[X]]$, where $K[[X]]$ is the algebra of formal power series over $K$. It is clearly not surjective, but this is not sufficient, we need to argue that it is not an epimorphism in $\CAlg(R)$, or equivalently, in $\CRing$. For a proof, see MSE/2391187. - property: cototal + # TODO: refactor this once we add "hypercocomplete" proof: >- - This proof will be similar to the proof of this lemma. To start, for each infinite cardinal $\kappa \ge \card(U(R))$, choose a field $F_\kappa$ of cardinality $\kappa$ including a quotient field of $R$. (For example, fix some such quotient field $R / \m$ and then let $F_\kappa$ be the extension of $R / \m$ by $\kappa$ many indeterminates.) We first claim that for any commutative $R$-algebra $A$ with $\kappa > \card(U(A))$, there is exactly one $R$-algebra homomorphism $\varphi : R \times F_\kappa \to A$, which can be described as the projection $R \times F_\kappa \to R$ followed by the unique morphism $R \to A$. To see this, note that for any other such morphism $\varphi$, we must have $\varphi(0, 1) \ne 0$. It follows that the rng homomorphism $F_\kappa \to A$ formed by composing $F_\kappa \to R \times F_\kappa$, $x \mapsto (0, x)$, with $\varphi$ is non-zero, and it is therefore injective since $F_\kappa$ was chosen to be a field. This gives a contradiction. + In fact, it is not hypercocomplete, and the proof will be similar to the proof of this lemma. To start, for each infinite cardinal $\kappa \ge \card(U(R))$, choose a field $F_\kappa$ of cardinality $\kappa$ including a quotient field of $R$. (For example, fix some such quotient field $R / \m$ and then let $F_\kappa$ be the extension of $R / \m$ by $\kappa$ many indeterminates.) We first claim that for any commutative $R$-algebra $A$ with $\kappa > \card(U(A))$, there is exactly one $R$-algebra homomorphism $\varphi : R \times F_\kappa \to A$, which can be described as the projection $R \times F_\kappa \to R$ followed by the unique morphism $R \to A$. To see this, note that for any other such morphism $\varphi$, we must have $\varphi(0, 1) \ne 0$. It follows that the rng homomorphism $F_\kappa \to A$ formed by composing $F_\kappa \to R \times F_\kappa$, $x \mapsto (0, x)$, with $\varphi$ is non-zero, and it is therefore injective since $F_\kappa$ was chosen to be a field. This gives a contradiction. - It follows that for any commutative $R$-algebra $A$, the collection of cocones $R \times F_\kappa \to A$ from the discrete diagram on $R \times F_\kappa$ is essentially small. On the other hand, we claim that $\CAlg(R)$ has no coproduct of all $R \times F_\kappa$. This will imply that $\CAlg(R)$ is not cototal, by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the contrapositive of the implication (i) $\Rightarrow$ (iii)). To see this, suppose we had such a coproduct $A$, and choose a cardinal $\kappa$ greater than $\max(\card(U(A)), \card(U(R)), \aleph_0)$. Then the coprojection $R \times F_\kappa \to A$ would be split injective, where we can construct the splitting $A \to R\times F_\kappa$ such that the $\kappa$ component is the identity, whereas for $\lambda \ne \kappa$, the $\lambda$ component is given by the projection $R \times F_\lambda \to R$ composed with the unique morphism $R \to R \times F_\kappa$. However, from this injection, we would get $\card(A) \ge \card(R \times F_\kappa) = \kappa$, giving a contradiction. + It follows that for any commutative $R$-algebra $A$, the collection of cocones $R \times F_\kappa \to A$ from the discrete diagram on $R \times F_\kappa$ is essentially small. On the other hand, we claim that $\CAlg(R)$ has no coproduct of all $R \times F_\kappa$, showing that it is not hypercocomplete. To see this, suppose we had such a coproduct $A$, and choose a cardinal $\kappa$ greater than $\max(\card(U(A)), \card(U(R)), \aleph_0)$. Then the coprojection $R \times F_\kappa \to A$ would be split injective, where we can construct the splitting $A \to R\times F_\kappa$ such that the $\kappa$ component is the identity, whereas for $\lambda \ne \kappa$, the $\lambda$ component is given by the projection $R \times F_\lambda \to R$ composed with the unique morphism $R \to R \times F_\kappa$. However, from this injection, we would get $\card(A) \ge \card(R \times F_\kappa) = \kappa$, giving a contradiction. label: calg_not_cototal special_objects: diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index c1738a25..3a0db17f 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -92,10 +92,11 @@ unsatisfied_properties: is not injective. Therefore, $\Sub_{\reg} : \Cat^{\op} \to \Set^+$ does not preserve pullbacks, so it cannot be representable. - property: cototal + # TODO: refactor this once we add "hypercocomplete" proof: >- - For each infinite cardinal $\kappa$, choose a simple group $G_\kappa$ of cardinality $\kappa$ (such as the alternating group on $\kappa$). Now consider the large span diagram $1 \dottedrightrightarrows B G_\kappa$. Then for any small category $\C$, the collection of cocones $1 \dottedrightrightarrows B G_\kappa \to \C$ is essentially small: to form any such cocone, we must first choose the object $X$ of $\C$ which is the image of the object of $1$. Then, we must choose the morphisms $G_\kappa \to \End_{\C}(X)$; but for $\kappa > \card(\End_{\C}(X))$, the corresponding morphism must be zero. + In fact, it is not hypercocomplete. For each infinite cardinal $\kappa$, choose a simple group $G_\kappa$ of cardinality $\kappa$ (such as the alternating group on $\kappa$). Now consider the large span diagram $1 \dottedrightrightarrows B G_\kappa$. Then for any small category $\C$, the collection of cocones $1 \dottedrightrightarrows B G_\kappa \to \C$ is essentially small: to form any such cocone, we must first choose the object $X$ of $\C$ which is the image of the object of $1$. Then, we must choose the morphisms $G_\kappa \to \End_{\C}(X)$; but for $\kappa > \card(\End_{\C}(X))$, the corresponding morphism must be zero. - On the other hand, we claim that $1 \dottedrightrightarrows B G_\kappa$ does not have a pushout in $\Cat$; by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the contrapositive of the implication (i) $\Rightarrow$ (iii)), this will imply that $\Cat$ is not cototal. To see this, suppose we have a pushout $\C$ of $1 \dottedrightrightarrows B G_\kappa$, and choose a cardinal $\lambda > \card(\Mor(\C))$ (which is possible since $\C$ is a small category). Then the coprojection $i_\lambda : B G_\lambda \to \C$ must be split monic, since we can construct a cocone $1 \dottedrightrightarrows B G_\kappa \to B G_\lambda$ in which $B G_\kappa \to B G_\lambda$ corresponds to the zero map for $\kappa \ne \lambda$, and in which $B G_\lambda \to B G_\lambda$ is the identity. It follows that if $X$ is the image in $\C$ of the object of $B G_\lambda$ under $i_\lambda$, then $i_\lambda$ induces an injective map $G_\lambda \to \End_{\C}(X)$. This gives a contradiction since $\lambda > \card(\End_{\C}(X))$ and $G_\lambda$ has cardinality $\lambda$. + On the other hand, we claim that $1 \dottedrightrightarrows B G_\kappa$ does not have a pushout in $\Cat$, showing that it is not hypercocomplete. To see this, suppose we have a pushout $\C$ of $1 \dottedrightrightarrows B G_\kappa$, and choose a cardinal $\lambda > \card(\Mor(\C))$ (which is possible since $\C$ is a small category). Then the coprojection $i_\lambda : B G_\lambda \to \C$ must be split monic, since we can construct a cocone $1 \dottedrightrightarrows B G_\kappa \to B G_\lambda$ in which $B G_\kappa \to B G_\lambda$ corresponds to the zero map for $\kappa \ne \lambda$, and in which $B G_\lambda \to B G_\lambda$ is the identity. It follows that if $X$ is the image in $\C$ of the object of $B G_\lambda$ under $i_\lambda$, then $i_\lambda$ induces an injective map $G_\lambda \to \End_{\C}(X)$. This gives a contradiction since $\lambda > \card(\End_{\C}(X))$ and $G_\lambda$ has cardinality $\lambda$. label: cat_not_cototal special_objects: diff --git a/database/data/categories/Haus.yaml b/database/data/categories/Haus.yaml index 267fc7dd..a4a41509 100644 --- a/database/data/categories/Haus.yaml +++ b/database/data/categories/Haus.yaml @@ -89,11 +89,13 @@ unsatisfied_properties: The pushout $C \sqcup_A \Gamma$ in $\Haus$ is the Hausdorff reflection of the pushout $Q$ in $\Top$. Notice that $Q$ is the quotient space of $\Gamma$ in which $A_1$ and $A_2$ are each collapsed to a point, denoted by $[A_1]$ and $[A_2]$. The canonical map $C \to Q$ is given by $i \mapsto [A_i]$. Now, $[A_1]$ and $[A_2]$ cannot be separated by disjoint open neighborhoods in $Q$, since such neighborhoods would pull back to disjoint open neighborhoods of $A_1$ and $A_2$ in $\Gamma$. Thus, they are identified in the Hausdorff reflection. This shows that the canonical map $C \to C \sqcup_A \Gamma$ is not injective and hence not a regular monomorphism. - property: cototal - # cspell: disable-next-line + # TODO: refactor this once we add "hypercocomplete" proof: >- - For each cardinal $\kappa$, let $Q_\kappa$ be the product of all Hausdorff topological spaces whose underlying set is a non-empty subset of $\kappa$. By a theorem of Herrlich (Wann sind alle stetigen Abbildungen in Y konstant. Math. Z. 90 (1965): 152-154. EUMDL), there is a regular Hausdorff space $X_\kappa$ with at least two points such that every continuous map $X_\kappa \to Q_\kappa$ is constant. (Note that the result there applies for general $T_1$ spaces $Q$, not just for $Q_\kappa$ as constructed above. In the reference, the author only states that $X_\kappa$ is regular, but actually, $X_\kappa$ is regular and $T_1$, hence Hausdorff.) Choose a base point $x_\kappa \in X_\kappa$ for each $\kappa$. We can form a large span diagram $1 \dottedrightrightarrows X_\kappa$ where each morphism $1 \to X_\kappa$ corresponds to $x_\kappa$. Then for any Hausdorff space $Y$, the collection of cocones $1 \dottedrightrightarrows X_\kappa \to Y$ is essentially small: We must first choose $y \in Y$ corresponding to the morphism $1 \to Y$. Then for each $\kappa \ge \card(U(Y))$, $Y$ is homeomorphic to one of the spaces in the product forming $Q_\kappa$. Therefore, there is a morphism $Y \to Q_\kappa$ splitting the projection map $Q_\kappa \to Y$. It follows that the map $X_\kappa \to Y$ is constant, and in fact it must be the constant map with image $y$. + In fact, it is not hypercocomplete. For each cardinal $\kappa$, let $Q_\kappa$ be the product of all Hausdorff topological spaces whose underlying set is a non-empty subset of $\kappa$. By a theorem of Herrlich (Wann sind alle stetigen Abbildungen in Y konstant. Math. Z. 90 (1965): 152-154. EUMDL), there is a regular Hausdorff space $X_\kappa$ with at least two points such that every continuous map $X_\kappa \to Q_\kappa$ is constant. (Note that the result there applies for general $T_1$ spaces $Q$, not just for $Q_\kappa$ as constructed above. In the reference, the author only states that $X_\kappa$ is regular, but actually, $X_\kappa$ is regular and $T_1$, hence Hausdorff.) - On the other hand, we claim that $1 \dottedrightrightarrows X_\kappa$ does not have a pushout in $\Haus$; by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the contrapositive of the implication (i) $\Rightarrow$ (iii)), this will imply that $\Haus$ is not cototal. To see this, suppose we had a pushout $Y$, and let $\lambda \coloneqq \card(U(Y))$. Then the coprojection $X_\lambda \to Y$ is split monic, since we can construct a cocone $1 \dottedrightrightarrows X_\kappa \to X_\lambda$ where the map $X_\kappa \to X_\lambda$ is the constant map with image $x_\lambda$ when $\kappa \ne \lambda$, and the map $X_\lambda \to X_\lambda$ is the identity. But similarly to the previous paragraph, we can show any morphism $X_\lambda \to Y$ must be constant, giving a contradiction since $X_\lambda$ has at least two points. + Choose a base point $x_\kappa \in X_\kappa$ for each $\kappa$. We can form a large span diagram $1 \dottedrightrightarrows X_\kappa$ where each morphism $1 \to X_\kappa$ corresponds to $x_\kappa$. Then for any Hausdorff space $Y$, the collection of cocones $1 \dottedrightrightarrows X_\kappa \to Y$ is essentially small: We must first choose $y \in Y$ corresponding to the morphism $1 \to Y$. Then for each $\kappa \ge \card(U(Y))$, $Y$ is homeomorphic to one of the spaces in the product forming $Q_\kappa$. Therefore, there is a morphism $Y \to Q_\kappa$ splitting the projection map $Q_\kappa \to Y$. It follows that the map $X_\kappa \to Y$ is constant, and in fact it must be the constant map with image $y$. + + On the other hand, we claim that $1 \dottedrightrightarrows X_\kappa$ does not have a pushout in $\Haus$, showing that it is not hypercocomplete. To see this, suppose we had a pushout $Y$, and let $\lambda \coloneqq \card(U(Y))$. Then the coprojection $X_\lambda \to Y$ is split monic, since we can construct a cocone $1 \dottedrightrightarrows X_\kappa \to X_\lambda$ where the map $X_\kappa \to X_\lambda$ is the constant map with image $x_\lambda$ when $\kappa \ne \lambda$, and the map $X_\lambda \to X_\lambda$ is the identity. But similarly to the previous paragraph, we can show any morphism $X_\lambda \to Y$ must be constant, giving a contradiction since $X_\lambda$ has at least two points. - property: extremal generating collection proof: The proof is the same as the one for $\Top$; there the test spaces we use are of the form $\kappa \sqcup \{ \kappa \}$ and $\kappa + 1$, which are both Hausdorff spaces. diff --git a/database/data/categories/SemiGrp.yaml b/database/data/categories/SemiGrp.yaml index e78e5b83..4830c4d5 100644 --- a/database/data/categories/SemiGrp.yaml +++ b/database/data/categories/SemiGrp.yaml @@ -67,12 +67,13 @@ unsatisfied_properties: - mon_no_effective_cocongruences - property: cototal + # TODO: refactor this once we add "hypercocomplete" proof: >- - The proof is similar to the proof for $\Cat$. For each infinite cardinal $\kappa$, let $G_\kappa$ be a simple group of cardinality $\kappa$ (such as the alternating group on $\kappa$). We can then form the large span diagram $1 \dottedrightrightarrows G_\kappa$ in $\SemiGrp$. For every semigroup $A$, the collection of cocones $1 \dottedrightrightarrows G_\kappa \to A$ is essentially small: for every such cocone, we must first choose an idempotent $e$ of $A$ corresponding to the map $1 \to A$. Then, whenever $\kappa > \card(U(A))$, where $U(-)$ denotes the underlying set, for $f_\kappa : G_\kappa \to A$ in the cocone, we see + In fact, it is not hypercocomplete. The proof is similar to the proof for $\Cat$. For each infinite cardinal $\kappa$, let $G_\kappa$ be a simple group of cardinality $\kappa$ (such as the alternating group on $\kappa$). We can then form the large span diagram $1 \dottedrightrightarrows G_\kappa$ in $\SemiGrp$. For every semigroup $A$, the collection of cocones $1 \dottedrightrightarrows G_\kappa \to A$ is essentially small: for every such cocone, we must first choose an idempotent $e$ of $A$ corresponding to the map $1 \to A$. Then, whenever $\kappa > \card(U(A))$, where $U(-)$ denotes the underlying set, for $f_\kappa : G_\kappa \to A$ in the cocone, we see $$N \coloneqq \{g \in G_\kappa : f_\kappa(g) = e\}$$ is a normal subgroup of $G_\kappa$. It must be non-trivial since otherwise $f_\kappa$ would induce an injective group homomorphism from $G_\kappa$ to a group contained in $A$. Therefore, $N$ is all of $G_\kappa$, so $f_\kappa$ is the constant map with image $e$. - We now claim that $1 \dottedrightrightarrows G_\kappa$ does not have a pushout in $\SemiGrp$; by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the contrapositive of the implication (i) $\Rightarrow$ (iii)), this will imply that $\SemiGrp$ is not cototal. To see this, suppose we had a pushout $A$, and let $\lambda$ be a cardinal strictly greater than $\card(U(A))$. Then the coprojection $G_\lambda\to A$ must be split monic, since we can construct a cocone $1 \dottedrightrightarrows G_\kappa \to G_\lambda$ such that the map $G_\kappa \to G_\lambda$ is the trivial (semi-)group homomorphism if $\kappa \ne \lambda$, while the map $G_\lambda \to G_\lambda$ is the identity. But this contradicts the choice of $\lambda$. + We now claim that $1 \dottedrightrightarrows G_\kappa$ does not have a pushout in $\SemiGrp$, showing that it is not hypercocomplete. To see this, suppose we had a pushout $A$, and let $\lambda$ be a cardinal strictly greater than $\card(U(A))$. Then the coprojection $G_\lambda\to A$ must be split monic, since we can construct a cocone $1 \dottedrightrightarrows G_\kappa \to G_\lambda$ such that the map $G_\kappa \to G_\lambda$ is the trivial (semi-)group homomorphism if $\kappa \ne \lambda$, while the map $G_\lambda \to G_\lambda$ is the identity. But this contradicts the choice of $\lambda$. references: - cat_not_cototal diff --git a/database/data/categories/Vect_family_mostly_0.yaml b/database/data/categories/Vect_family_mostly_0.yaml index 71c59e68..6bbeb1d1 100644 --- a/database/data/categories/Vect_family_mostly_0.yaml +++ b/database/data/categories/Vect_family_mostly_0.yaml @@ -57,10 +57,12 @@ unsatisfied_properties: check_redundancy: false - property: cototal - proof: For $i \in I$ define $E^i \in \Vect^{(I)}_K$ by $E^i_j = 0$ for $j \neq i$ and $E^i_i = K$. This yields a discrete diagram $(E^i)_{i \in I}$. For every $V \in \Vect^{(I)}_K$ the collection of cocones $(E^i \to V)_{i \in I}$ is essentially small, since for $i \notin \supp(V)$ every morphism $E^i \to V$ is zero, so the indices may be restricted to the collection $\supp(V)$, which is essentially small. Assuming $\Vect^{(I)}_K$ is cototal, by G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6 (namely the contrapositive of the implication (i) $\Rightarrow$ (iii)), the coproduct $S \coloneqq \coprod_{i \in I} E^i$ would exist in $\Vect^{(I)}_K$. Since each $E^i$ is a retract of $S$ and $E^i_i \neq 0$, we see that $\supp(S) = I$, which however is not essentially small. + # TODO: refactor this once we add "hypercocomplete" + proof: In fact, it is not hypercocomplete. For $i \in I$ define $E^i \in \Vect^{(I)}_K$ by $E^i_j = 0$ for $j \neq i$ and $E^i_i = K$. This yields a discrete diagram $(E^i)_{i \in I}$. For every $V \in \Vect^{(I)}_K$ the collection of cocones $(E^i \to V)_{i \in I}$ is essentially small, since for $i \notin \supp(V)$ every morphism $E^i \to V$ is zero, so the indices may be restricted to the collection $\supp(V)$, which is essentially small. Assuming $\Vect^{(I)}_K$ is hypercocomplete, the coproduct $S \coloneqq \coprod_{i \in I} E^i$ would exist in $\Vect^{(I)}_K$. Since each $E^i$ is a retract of $S$ and $E^i_i \neq 0$, we see that $\supp(S) = I$, which however is not essentially small. label: Vect_family_not_cototal - property: total + # TODO: refactor this once we add "hypercomplete" proof: We can almost repeat the previous proof that the category is not cototal. The collection of cones $(V \to E^i)_{i \in I}$ is essentially small for every $V$, but $\prod_{i \in I} E^i$ does not exist since it would have support $I$. references: - Vect_family_not_cototal diff --git a/database/data/category-implications/total.yaml b/database/data/category-implications/total.yaml index 74cceba4..f656f1fd 100644 --- a/database/data/category-implications/total.yaml +++ b/database/data/category-implications/total.yaml @@ -12,6 +12,7 @@ - total conclusions: - cocomplete + # TODO: refactor this once we add "hypercocomplete" proof: 'If the category $\C$ is locally small and total, then the Yoneda embedding $y : \C^{\op} \to [\C, \Set]$ makes $\C^{\op}$ into a reflective subcategory of the presheaf category $[\C, \Set]$, where the latter is complete. For a general total category $\C$, use the equivalence to a locally small, total category.' - id: total_complete @@ -19,6 +20,7 @@ - total conclusions: - complete + # TODO: refactor this once we add "hypercomplete" proof: This is proven in G. M. Kelly, A survey of totality for enriched and ordinary categories, Thm. 5.6. # TODO: replace "well-copowered" with "epi-cocomplete" if adding the latter property diff --git a/database/data/category-properties/cototal.yaml b/database/data/category-properties/cototal.yaml index 539fbab1..53cc0f40 100644 --- a/database/data/category-properties/cototal.yaml +++ b/database/data/category-properties/cototal.yaml @@ -9,7 +9,7 @@ description: >-
  • Every discrete opfibration $D : \I \to \C$ (with $\I$ not necessarily essentially small) with the property that each fiber $D^*(\{X\}) = \{i \in \Ob(\C) : D_i = X\}$ is essentially small (bijective to a set), has a limit in $\C$.
  • Let $D : \I \to \C$ be a diagram (with $\I$ not necessarily essentially small) such that for each object $X$ of $\C$, the collection $\pi_0(D \downarrow X)$ of connected components of the comma category $D \downarrow X$ is essentially small. Then $D$ has a limit in $\C$.
    • - The equivalence is proven as Thm. 5.2 and 5.5 in G. M. Kelly, A survey of totality for enriched and ordinary categories. + The equivalence is proven as Thm. 5.2 and 5.5 in G. M. Kelly, A survey of totality for enriched and ordinary categories. Thm. 5.6 in that paper also proves that every cototal category is hypercocomplete, meaning that every diagram $D : \I \to \C$ with the property that for every object $X$ of $\C$ the collection of cocones $\Hom(D,\Delta(X))$ is essentially small, has a colimit. A general category is called cototal if it is equivalent to a locally small category which is cototal. nlab_link: https://ncatlab.org/nlab/show/cototal+category diff --git a/database/data/category-properties/total.yaml b/database/data/category-properties/total.yaml index 54a6f068..49958eed 100644 --- a/database/data/category-properties/total.yaml +++ b/database/data/category-properties/total.yaml @@ -9,7 +9,7 @@ description: >-
  • Every discrete fibration $D : \I \to \C$ (with $\I$ not necessarily essentially small) with the property that each fiber $D^*(\{X\}) = \{i \in \Ob(\C) : D_i = X\}$ is essentially small (bijective to a set), has a colimit in $\C$.
  • Let $D : \I \to \C$ be a diagram (with $\I$ not necessarily essentially small) such that for each object $X$ of $\C$, the collection $\pi_0(X \downarrow D)$ of connected components of the comma category $X \downarrow D$ is essentially small. Then $D$ has a colimit in $\C$.
    • - The equivalence is proven as Thm. 5.2 and 5.5 in G. M. Kelly, A survey of totality for enriched and ordinary categories. + The equivalence is proven as Thm. 5.2 and 5.5 in G. M. Kelly, A survey of totality for enriched and ordinary categories. Thm. 5.6 in that paper also proves that every total category is hypercomplete, meaning that every diagram $D : \I \to \C$ with the property that for every object $X$ of $\C$ the collection of cones $\Hom(\Delta(X),D)$ is essentially small, has a limit. A general category is called total if it is equivalent to a locally small category which is total. nlab_link: https://ncatlab.org/nlab/show/total+category From 1ad571a467ec8d5423115d804dcc1fd36667abcd Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 24 Sep 2026 22:18:30 +0200 Subject: [PATCH 12/12] add the category of F(I)-sets --- database/data/categories/F(I)-Set.yaml | 91 ++++++++++++++++++++++++++ database/data/macros.yaml | 1 + shared/structure.history.json | 3 +- 3 files changed, 94 insertions(+), 1 deletion(-) create mode 100644 database/data/categories/F(I)-Set.yaml diff --git a/database/data/categories/F(I)-Set.yaml b/database/data/categories/F(I)-Set.yaml new file mode 100644 index 00000000..b71b1b39 --- /dev/null +++ b/database/data/categories/F(I)-Set.yaml @@ -0,0 +1,91 @@ +id: F(I)-Set +name: category of F(I)-sets +notation: $F(I){-}\Set$ +objects: sets with an action of a free large group $F(I)$ +morphisms: maps that are compatible with the action +description: Here, $I$ is a collection that is not essentially small, and its free group is constructed in the universe of collections (cf. foundations). Objects can be identified with pairs $(X,\sigma)$, where $X$ is a set and $\sigma = (\sigma_i)_{i \in I}$ is a large family of permutations of $X$, and morphisms are maps of sets that commute with the permutations. This category behaves similarly to $\IZ{-}\Set$, but the most important difference is that it has neither a generating collection nor a cogenerating collection. Moreover, the forgetful functor to $\Set$ is not representable and (hence) has no left adjoint. +nlab_link: null + +tags: + - algebra + +related: + - M-Set + - Z-Set + - Set_family + +comments: + - The category is well-defined in our foundations. For instance, the collection of objects is $\prod_{X \in \SetColl} \prod_{i \in I} \Aut(X)$, which is indeed a collection since collections are closed under the usual operations of set theory. Another explanation is that it is the functor category $[B(F(I)),\Set]$, where $B(F(I))$ is the one-object category associated with $F(I)$. + - The category has appeared in MO/258269. + - The forgetful functor to $\Set$ does not preserve large limits. For $i \in I$ consider the object $X_i = (\{0,1\},\sigma^{[i]})$, where $\sigma^{[i]}_i = (0 ~ 1)$ and $\sigma^{[i]}_j = \id$ for $j \neq i$. One can show that the large product of the family $(X_i)_{i \in I}$ exists and is given by the empty set. + +satisfied_properties: + - property: locally small + proof: The collection $\Hom((X,\sigma),(Y,\tau))$ is contained in the set $\Hom(X,Y)$, and is therefore a set. + + - property: concretizable + proof: The forgetful functor $F(I){-}\Set \to \Set$, $(X,\sigma) \mapsto X$, is faithful. + + - property: complete + proof: The forgetful functor $F(I){-}\Set \to \Set$ creates limits, and $\Set$ is complete. + + - property: cocomplete + proof: The forgetful functor $F(I){-}\Set \to \Set$ creates colimits, and $\Set$ is cocomplete. + check_redundancy: false + + - property: exact filtered colimits + proof: This property is inherited from $\Set$ since the forgetful functor to $\Set$ is continuous, cocontinuous, and conservative. + + - property: subobject classifier + proof: If $G$ is any group, then $\{0,1\}$ equipped with the trivial $G$-action is a subobject classifier of $G{-}\Set$, because a map of sets $X \to \{0,1\}$ lifts to a morphism of $G$-sets if and only if the fiber at $1$ is $G$-stable. The same proof works when $G$ is a large group. + + - property: cartesian closed + proof: If $G$ is a group and $(X,\sigma),(Y,\tau)$ are two $G$-sets, their exponential is $\Hom(X,Y)$ equipped with the $G$-action $(g f)(x) = g f(g^{-1} x)$. The same proof works when $G$ is a large group. + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: semi-strongly connected + proof: Choose an element $i_0 \in I$. There is a fully faithful functor $\IZ{-}\Set \to F(I){-}\Set$ that maps $(X,\sigma) \mapsto (X,\widetilde{\sigma})$, where $\widetilde{\sigma}_{i_0} = \sigma$ and $\widetilde{\sigma}_i = \id_X$ for $i \neq i_0$. Since $\IZ{-}\Set$ is not semi-strongly connected, it follows that $F(I){-}\Set$ is not semi-strongly connected. + + - property: cogenerator + proof: >- + Assume that a cogenerator $(Q,\rho)$ exists. Then $\rho : I \to \Aut(Q)$ is a map which cannot be injective, since otherwise $I$ would be essentially small. Choose elements $i \neq j$ with $\rho_i = \rho_j$. Let $X = \{a,b\}$ and define $\sigma : I \to \Aut(X)$ by $\sigma_i = (a ~ b)$ and $\sigma_k = \id_X$ for all $k \neq i$. Thus, $(X,\sigma)$ is an object of the category, and $\sigma_i : (X,\sigma) \to (X,\sigma)$ is a non-trivial endomorphism since $\sigma_i$ commutes with every $\sigma_k$. Since $(Q,\rho)$ is a cogenerator, there is some morphism $f : (X,\sigma) \to (Q,\rho)$ with $f \circ \sigma_i \neq f$. However, since $f$ is a morphism, we have + $$f \circ \sigma_i = \rho_i \circ f = \rho_j \circ f = f \circ \sigma_j = f.$$ + + - property: total + proof: >- + In fact, we will prove that the category is not hypercomplete. For $i \in I$, consider the object $T_i = (\{0,1,\ast\},t^i)$, where $t^i_i = (0 ~ 1)$ and $t^i_j = \id$ for $j \neq i$. We claim that for every object $(X,\sigma)$, the collection of cones $(f_i : (X,\sigma) \to T_i)_{i \in I}$ is essentially small. Each $f_i$ is a map $X \to \{0,1,\ast\}$ satisfying $f_i \circ \sigma_i = (0 ~ 1) \circ f_i$ and $f_i \circ \sigma_j = f_i$ for $j \neq i$. Thus, for $j \neq i$ with $\sigma_i = \sigma_j$, we have + $$f_i = f_i \circ \sigma_j = f_i \circ \sigma_i = (0 ~ 1) \circ f_i,$$ + so $f_i$ must be the constant map with value $\ast$. The collection + $$I_X \coloneqq \{i \in I : \forall j \neq i \, (\sigma_i \neq \sigma_j)\}$$ + is essentially small since the map $I_X \to \Aut(X)$, $i \mapsto \sigma_i$, is injective, and for every $i \notin I_X$ we have just seen that $f_i \equiv \ast$ is constant. Thus, the collection of cones is isomorphic to the collection of cones over the essentially small family $(T_i)_{i \in I_X}$, proving the claim. + + We will now prove that the family $(T_i)_{i \in I}$ has no product, showing that the category is not hypercomplete. Assume that $(p_i : (X,\sigma) \to T_i)_{i \in I}$ is a product. By what we have seen before, there is an essentially small collection $I_X \subseteq I$ such that $p_i \equiv \ast$ for all $i \in I \setminus I_X$. Since $I$ is not essentially small, we may choose an index $k \in I \setminus I_X$. For every $i \in I$, $i \neq k$, the constant map $\ast : \{0,1,\ast\} \to \{0,1,\ast\}$ lifts to a morphism $T_k \to T_i$, since the maps $t^i_j$ and $t^k_j$ preserve $\ast$. Thus, by the universal property of the product, there is a morphism $f : T_k \to (X,\sigma)$ such that $p_k \circ f = \id_{T_k}$ and $p_i \circ f = \ast$ for $i \neq k$. The first equation shows that $p_k$ is surjective, which contradicts $p_k \equiv \ast$. + + # TODO: once adding "hypercocomplete", add a proof that this category IS hypercocomplete, but not cototal. + + # - property: cototal + # proof: TBA + +special_objects: + initial object: + description: empty set with the unique action + terminal object: + description: singleton set with the unique action + coproducts: + description: disjoint union with the obvious action + products: + description: direct product with the obvious action + +special_morphisms: + isomorphisms: + description: bijective morphisms + proof: This is easy to check. + monomorphisms: + description: injective morphisms + proof: Injective morphisms are clearly monomorphisms. The converse follows since the forgetful functor to $\Set$ preserves limits, pullbacks in particular, and therefore preserves monomorphisms. + epimorphisms: + description: surjective morphisms + proof: Surjective morphisms are clearly epimorphisms. The converse follows since the forgetful functor to $\Set$ preserves colimits, pushouts in particular, and therefore preserves epimorphisms. diff --git a/database/data/macros.yaml b/database/data/macros.yaml index cd5e5cdb..c60d9838 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -56,6 +56,7 @@ \Hom: \operatorname{Hom} \HomInternal: \underline{\operatorname{Hom}} \End: \operatorname{End} +\Aut: \operatorname{Aut} \Bilin: \operatorname{Bilin} \Ob: \operatorname{Ob} \id: \operatorname{id} diff --git a/shared/structure.history.json b/shared/structure.history.json index 234e1abb..32cd7ca9 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -206,5 +206,6 @@ "SeqSet": "2026-09-24", "SeqSet_conn": "2026-09-24", "Z-Set": "2026-09-24", - "Z-FinSet": "2026-09-24" + "Z-FinSet": "2026-09-24", + "F(I)-Set": "2026-09-24" }