diff --git a/.cspell.json b/.cspell.json index 0a2477ec4..c8b761ff6 100644 --- a/.cspell.json +++ b/.cspell.json @@ -34,6 +34,7 @@ "algebraicity", "algébriques", "anneaux", + "Aronszajn", "Artin", "Auslander", "Axiomatising", @@ -169,6 +170,7 @@ "deloopings", "Demazure", "Diers", + "diagonalization", "diffeomorphism", "diffeomorphisms", "disjointness", @@ -244,6 +246,7 @@ "irreflexive", "Isbell", "isos", + "Jaap", "Johnstone", "Jónsson", "Kashiwara", @@ -291,6 +294,7 @@ "Noetherian", "Noncommutative", "objectwise", + "Oosten", "opfibration", "Perrone", "pointwise", diff --git a/content/cocongruences_in_extensive_categories.md b/content/cocongruences_in_extensive_categories.md new file mode 100644 index 000000000..8d890e9a4 --- /dev/null +++ b/content/cocongruences_in_extensive_categories.md @@ -0,0 +1,173 @@ +--- +title: Cocongruences in extensive categories +description: This gives some results on cocongruences in extensive categories with various extra hypotheses. +--- + +# Cocongruences in extensive categories + +We start with a general fact which is easier to visualize for the dual case of congruences. + +::: Lemma 1 +Let $q_1, q_2 : E \rightrightarrows X$ be a congruence such that the pullback $E \times_X E$ of $q_2$ and $q_1$ exists, and let $t : E \times_X E \to E$ be the transitivity morphism. Then we have pushout diagrams + +$$ +\begin{CD} +E \times_X E @> p_1 >> E @. \quad @. E \times_X E @> p_2 >> E \\ +@V t VV @VV q_1 V @. @V t VV @VV q_2 V \\ +E @> q_1 >> X @. \quad @. E @> q_2 >> X. +\end{CD} +$$ + +::: + +::: Proof +Suppose we have a commutative square + +$$ +\begin{CD} +E \times_X E @> p_1 >> E \\ +@V t VV @VV f V \\ +E @> g >> T. +\end{CD} +$$ + +Then for any generalized element $(x, y)$ of $E$, consider the generalized elements $((x, x), (x, y))$ and $((x, y), (y, y))$ of $E \times_X E$. From the commutativity of the square acting on these generalized elements, we have +$$f(x, x) = g(x, y)$$ +and +$$f(x, y) = g(x, y).$$ +Therefore, if we define $h : X \to T$ on generalized elements by $h(x) \coloneqq f(x, x)$, we must have $f = h \circ q_1$ and $g = h \circ q_1$. Conversely, if $h$ is a morphism with $f = h \circ q_1$, we have $h(x)=f(x,y)$ for all $(x,y) \in E$, which for $y=x$ yields $h(x)=f(x,x)$. + +This concludes the proof that the first diagram is a pushout diagram; the proof for the second is similar. +::: + +::: Lemma 2 +Suppose we have two pullback diagrams + +$$ +\begin{CD} +A_1 @> f_1 >> B @. \quad @. A_2 @> f_2 >> B \\ +@V g_1 VV @VV h V @. @V g_2 VV @VV h V \\ +C_1 @> k_1 >> D @. \quad @. C_2 @> k_2 >> D +\end{CD} +$$ + +in an extensive category. Then we can combine these into a pullback diagram + +$$ +\begin{CD} +A_1 + A_2 @> (f_1; f_2) >> B \\ +@V g_1 + g_2 VV @VV h V \\ +C_1 + C_2 @> (k_1; k_2) >> D. +\end{CD} +$$ + +::: + +::: Proof +Suppose we have compatible maps $T \to B$ and $T \to C_1 + C_2$. Then using extensivity, we can find a decomposition of the latter into morphisms $T_1 \to C_1$ and $T_2 \to C_2$ where $T \cong T_1 + T_2$. Using the individual pullback diagrams, we can then construct morphisms $T_1 \to A_1$ and $T_2 \to A_2$ with the corresponding projections to $B, C_1, C_2$. The sum $T \cong T_1 + T_2 \to A_1 + A_2$ then gives the required morphism for the desired pullback diagram. On the other hand, the uniqueness of this morphism $T \to A_1 + A_2$ follows from the uniqueness conditions for $T_1 \to A_1$ and $T_2 \to A_2$ from the assumed pullback diagrams, along with the disjointness of the coproduct $C_1 + C_2$ (to be exact, the fact that the coprojections $C_1 \to C_1 + C_2$ and $C_2 \to C_1 + C_2$ are monomorphisms). +::: + +::: Corollary 3 +Let $j_1, j_2 : X \rightrightarrows E$ be a cocongruence in an extensive category such that the pushout $E +_X E$ of $j_2$ and $j_1$ exists, and let $t : E \to E +_X E$ be the corresponding cotransitivity morphism. Then we have a pullback diagram + +$$ +\begin{CD} +X + X @> (j_1; j_2) >> E \\ +@V j_1 + j_2 VV @VV t V \\ +E + E @>>> E +_X E. +\end{CD} +$$ + +In particular, if the category also has pullback-stable regular epimorphisms, then for any cocongruence $j_1, j_2 : X \rightrightarrows E$, the corresponding morphism $(j_1; j_2) : X + X \to E$ is a regular epimorphism. +::: + +::: Proof +The pullback diagram comes from using Lemma 2 on the two pullback diagrams from the dual of Lemma 1. For the other conclusion, all we need to establish is that $E + E \to E +_X E$ is a regular epimorphism. This follows from the construction of the pushout $E +_X E$ of monomorphisms (in fact, split monomorphisms with the coreflexivity morphism being the left inverse) as a quotient of a congruence on $E + E$ here. +::: + +In the following results, define a regular corelation to be a corelation $j_1, j_2 : X \rightrightarrows E$ such that the binary copower of $X$ exists, and $(j_1; j_2) : X + X \to E$ is a regular epimorphism. + +::: Lemma 4 +In an extensive category, every regular coreflexive corelation $j_1, j_2 : X \rightrightarrows E$ such that the equalizer of $j_1$ and $j_2$ exists is an effective cocongruence. +::: + +::: Proof +Let $e : Y \hookrightarrow X$ be the equalizer of $j_1$ and $j_2$. We will prove that the parallel pair + +$$ +\begin{align*} +(i_1; i_1 \circ e; i_2 \circ e; i_2) & ,\\ +(i_1; i_2 \circ e; i_1 \circ e; i_2) & : X + Y + Y + X \rightrightarrows X + X. +\end{align*} +$$ + +is a kernel pair of $(j_1; j_2) : X + X \to E$. +Informally, we can think of this as the subobject of $(X + X)^2 \cong \sum_{i,j=1}^2 X^2$ which is the diagonal of $X$ in the first and fourth quadrants, and the diagonal of $Y$ in the second and third quadrants. + +To see this, note that since $j_1$ is a (split) monomorphism, we have a pullback diagram + +$$ +\begin{CD} +X @> \id >> X \\ +@V \id VV @VV j_1 V \\ +X @>> j_1 > E. +\end{CD} +$$ + +Similarly, since $e$ is formed as a coreflexive equalizer, we have a pullback diagram + +$$ +\begin{CD} +Y @> e >> X \\ +@V e VV @VV j_1 V \\ +X @>> j_2 > E. +\end{CD} +$$ + +(See here.) + +Combining these using Lemma 2, we get a pullback diagram + +$$ +\begin{CD} +X+Y @> (\id; e) >> X \\ +@V \id + e VV @VV j_1 V \\ +X+X @>> (j_1; j_2) > E. +\end{CD} +$$ + +Similarly, we get a pullback diagram + +$$ +\begin{CD} +Y+X @> (e; \id) >> X \\ +@V e + \id VV @VV j_2 V \\ +X+X @>> (j_1; j_2) > E. +\end{CD} +$$ + +Now, combining those two using Lemma 2 (transposed), we get a pullback diagram + +$$ +\begin{CD} +(X+Y)+(Y+X) @> (\id; e) + (e; \id) >> X+X \\ +@V (\id+e; e+\id) VV @VV (j_1; j_2) V \\ +X+X @>> (j_1; j_2) > E. +\end{CD} +$$ + +However, under the canonical isomorphism $(X+Y)+(Y+X) \cong X+Y+Y+X$, we see that $(\id; e) + (e; \id)$ corresponds to +$$(i_1; i_1\circ e; i_2\circ e; i_2) : X+Y+Y+X \to X+X,$$ +whereas $(\id+e; e+\id)$ corresponds to +$$(i_1; i_2\circ e; i_1\circ e; i_2) : X+Y+Y+X \to X+X.$$ + +Therefore, since $(j_1; j_2) : X + X \to E$ is a regular epimorphism, it is a coequalizer of this kernel pair. However, this coequalizer is exactly the congruence quotient in the construction here of $X +_Y X$. Thus, we see that the original corelation is equivalent to the cokernel pair of $e$. +::: + +::: Corollary 5 +In an extensive and regular category with quotients of congruences, every cocongruence is effective. +::: + +::: Proof +This follows by combining Corollary 3 and Lemma 4, using the existence of quotients of congruences so that $E +_X E$ always exists by this result. +::: diff --git a/database/data/categories/Bin.yaml b/database/data/categories/Bin.yaml index 4157f7629..975cf900c 100644 --- a/database/data/categories/Bin.yaml +++ b/database/data/categories/Bin.yaml @@ -90,40 +90,6 @@ satisfied_properties: which is a contradiction. label: Bin_extremal_cogenerator - - property: effective cocongruences - proof: >- - Let $q_1,q_2 : (X,R) \rightrightarrows (Y,S)$ be a cocongruence. Since the forgetful functor $\Bin \to \Set$ is cocontinuous, the pair $q_1,q_2 : X \rightrightarrows Y$ is a cocongruence in $\Set$, which has effective cocongruences and equalizers. Thus, if $E \subseteq X$ denotes the equalizer of $q_1,q_2$, the canonical map - $$\alpha : X \sqcup_E X \to Y,\qquad i_1(x) \mapsto q_1(x),\quad i_2(x) \mapsto q_2(x)$$ - is bijective. This is the underlying map of the canonical morphism - $$\alpha : (X,R) \sqcup_{(E,R|_E)} (X,R) \to (Y,S),$$ - and it remains to prove that $\alpha$ is relation-reflecting. By the construction of colimits, the pushout is given by - $$(X \sqcup_E X, i_1(R) \cup i_2(R)),$$ - where $i_k(R)$ is shorthand for $\{(i_k(x),i_k(x')) : (x,x') \in R\}$. Thus, we need to show that for all elements $p,q \in X \sqcup_E X$ with $(\alpha(p),\alpha(q)) \in S$, we have $(p,q) \in i_1(R) \cup i_2(R)$. Since $p$ and $q$ are contained in $i_1(X) \cup i_2(X)$, there are four cases to consider. - - Case 1. We have $p = i_1(x)$ and $q = i_1(x')$. Thus, - $$(q_1(x),q_1(x')) = (\alpha(p),\alpha(q)) \in S.$$ - Applying the retraction $r : (Y,S) \to (X,R)$, we obtain $(x,x') \in R$. Thus, - $$(p,q) = (i_1(x),i_1(x')) \in i_1(R) \subseteq i_1(R) \cup i_2(R).$$ - Case 2. We have $p = i_2(x)$ and $q = i_2(x')$. This is symmetric to Case 1. - - Case 3. We have $p = i_1(x)$ and $q = i_2(x')$. Thus, - $$(q_1(x),q_2(x')) = (\alpha(p),\alpha(q)) \in S.$$ - Consider the set - $$Z \coloneqq X \sqcup_E X \sqcup_E X.$$ - There are three canonical injective maps - $$u_i : X \to Z$$ - satisfying $u_i(x) = u_j(x') \iff x = x' \in E$ for $i \neq j$. Because $(u_1)|_E = (u_2)|_E$, there is a unique map $f : Y \to Z$ with $f q_1 = u_1$ and $f q_2 = u_2$. Likewise, there is a unique map $g : Y \to Z$ with $g q_1 = u_2$ and $g q_2 = u_3$. Consider the binary relation $T \coloneqq f(S) \cup g(S)$ on $Z$. Then $f$ and $g$ induce morphisms $f,g : (Y,S) \rightrightarrows (Z,T)$ satisfying $f q_2 = g q_1$. Since $q_1,q_2$ is cotransitive, there is a morphism - $$h : (Y,S) \to (Z,T)$$ - satisfying $h q_1 = f q_1 = u_1$ and $h q_2 = g q_2 = u_3$. Since $(q_1(x),q_2(x')) \in S$ and $h$ is a morphism, we have - $$(u_1(x),u_3(x')) \in T = f(S) \cup g(S).$$ - Assume first that $(u_1(x),u_3(x')) \in f(S)$. Then - $$u_3(x') \in \im(f) \subseteq \im(u_1) \cup \im(u_2),$$ - so that $x' \in E$. But then $p = i_1(x)$ and $q = i_1(x')$, so that we are in Case 1. Next, assume that $(u_1(x),u_3(x')) \in g(S)$. Then - $$u_1(x) \in \im(g) \subseteq \im(u_2) \cup \im(u_3),$$ - so that $x \in E$. But then $p = i_2(x)$ and $q = i_2(x')$, so that we are in Case 2. - - Case 4. We have $p = i_2(x)$ and $q = i_1(x')$. This is symmetric to Case 3. - unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Bin_refl.yaml b/database/data/categories/Bin_refl.yaml index aa9a4e284..db37f83d6 100644 --- a/database/data/categories/Bin_refl.yaml +++ b/database/data/categories/Bin_refl.yaml @@ -99,9 +99,6 @@ satisfied_properties: references: - Bin_extremal_cogenerator - - property: effective cocongruences - proof: This follows from the corresponding fact for $\Bin$ and the dual of Lemma 8 here. - unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Bin_symm.yaml b/database/data/categories/Bin_symm.yaml index 8c2cd9f4e..4fcd80a7c 100644 --- a/database/data/categories/Bin_symm.yaml +++ b/database/data/categories/Bin_symm.yaml @@ -86,9 +86,6 @@ satisfied_properties: references: - Bin_extremal_cogenerator - - property: effective cocongruences - proof: This follows from the corresponding fact for $\Bin$ and the dual of Lemma 8 here. - unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Bin_symm_refl.yaml b/database/data/categories/Bin_symm_refl.yaml index 441a0131b..4de8ab5a9 100644 --- a/database/data/categories/Bin_symm_refl.yaml +++ b/database/data/categories/Bin_symm_refl.yaml @@ -87,9 +87,6 @@ satisfied_properties: references: - Bin_extremal_cogenerator - - property: effective cocongruences - proof: This follows from the corresponding fact for $\Bin$ and the dual of Lemma 8 here. - unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Cat.yaml b/database/data/categories/Cat.yaml index cc24d2f7b..7ca234742 100644 --- a/database/data/categories/Cat.yaml +++ b/database/data/categories/Cat.yaml @@ -45,9 +45,6 @@ unsatisfied_properties: - property: balanced proof: Since we know that $\Mon$ is not balanced, there is a monoid map $M \to N$ which is a monomorphism and an epimorphism, but not an isomorphism. Then $B(M) \to B(N)$ has the corresponding properties. - - property: regular - proof: See Example 3.14 at the nLab. - - property: coregular proof: 'We already know that $\Mon$ is not coregular; in fact we have shown that there is a regular monomorphism $M \to N$ of monoids and a morphism $M \to K$ such that $K \to K \sqcup_M N$ is not a monomorphism. The delooping functor $B : \Mon \to \Cat$ has a left adjoint (MSE/574745), hence it preserves regular monomorphisms. It also preserves pushouts (MSE/5130854), and it reflects monomorphisms since it is faithful. Therefore, $B(M) \to B(N)$ provides the desired counterexample of a non-stable regular monomorphism of categories.' references: diff --git a/database/data/categories/LRS_R.yaml b/database/data/categories/LRS_R.yaml index 6e10dc953..cae018ac2 100644 --- a/database/data/categories/LRS_R.yaml +++ b/database/data/categories/LRS_R.yaml @@ -88,9 +88,6 @@ unsatisfied_properties: - property: cartesian filtered colimits proof: This is Corollary 4(b) here. - - property: regular - proof: This is Corollary 4(c) here. - - property: cofiltered-limit-stable epimorphisms proof: This is Corollary 4(d) here. diff --git a/database/data/categories/Meas.yaml b/database/data/categories/Meas.yaml index 249542cce..72abf4af7 100644 --- a/database/data/categories/Meas.yaml +++ b/database/data/categories/Meas.yaml @@ -126,24 +126,6 @@ unsatisfied_properties: references: - Top_no_effective_cocongruences - - property: regular - proof: >- - In a regular category, regular epimorphisms are stable under pullbacks and compositions (see Prop. 3.7 at the nLab), which implies that for every regular epimorphism $f : X \to Y$ also $f \times f : X \times X \to Y \times Y$ is a regular epimorphism. We will show that this fails in $\Meas$. - - Let $X \coloneqq [0, 1)$ equipped with the standard Borel $\sigma$-algebra $\B$. Consider the equivalence relation $x \sim y \iff x-y \in \IQ$, let $Y \coloneqq X /{\sim}$ be the set of equivalence classes, and $f: X \to Y$ be the natural projection map. Equip $Y$ with the quotient $\sigma$-algebra $\Sigma_Y$, so that $f$ is a regular epimorphism. - - Now consider the diagonal in the quotient space $\Delta_Y \coloneqq \{(y, y) \mid y \in Y\}$. Then - $$\textstyle (f \times f)^{-1}(\Delta_Y) = \{(x_1, x_2) \in [0, 1)^2 \mid x_1 - x_2 \in \IQ\} \eqqcolon \bigcup_{q \in \IQ} L_q$$ - where each $L_q$ is the intersection of the diagonal level sets of $x_1 - x_2$ with $[0, 1)^2$. Because each line is closed in $\IR^2$, its intersection with $[0, 1)^2$ is a Borel set in $X \times X$. Since a countable union of Borel sets is Borel, $(f \times f)^{-1}(\Delta_Y) \in \B \otimes \B$. - - Now take any set $B \in \Sigma_Y$. Its preimage $f^{-1}(B)$ is a Borel set in $[0, 1)$ that is invariant under rational translations modulo 1. Because the action of $\IQ / \IZ$ on $[0, 1)$ is ergodic, the Lebesgue measure $\lambda(f^{-1}(B))$ must be exactly $0$ or $1$. Assume for contradiction that $\Sigma_Y$ is countably separated, i.e. there exists a countable sequence of measurable sets $(B_n)_{n \geq 1}$ in $\Sigma_Y$ that separates the points of $Y$. Let $A_n \coloneqq f^{-1}(B_n)$. Every $A_n$ has $\lambda(A_n) = 0$ or $\lambda(A_n) = 1$. - - Define a "bad set" $N \subseteq [0, 1)$ as - $$\textstyle N \coloneqq \left( \bigcup_{\lambda(A_n)=0} A_n \right) \cup \left( \bigcup_{\lambda(A_n)=1} A_n^c \right)$$ - Because $N$ is a countable union of sets with measure $0$, we have $\lambda(N) = 0$, and thus $\lambda([0, 1) \setminus N)=1$. For any two points $x, y \in [0, 1) \setminus N$, clearly $x \in A_n \iff y \in A_n$ for every $n$. Consequently, the sequence $(B_n)$ fails to separate $f(x)$ and $f(y)$. Hence, $x \sim y$. Since $[0, 1) \setminus N$ has measure $1$, it is uncountable. Because each equivalence class is only countable, these uncountably many points must belong to uncountably many different equivalence classes. Thus, we can easily pick $x, y \in [0, 1) \setminus N$ where $x \not\sim y$. Thus $\Sigma_Y$ is not countably separated. - - Hence by Bogachev, Theorem 6.5.7, $\Delta_Y \notin \Sigma_Y \otimes \Sigma_Y$. We have identified a non-measurable subset of $Y \times Y$ whose preimage under $f \times f$ is measurable. Therefore, $f \times f$ is not a regular epimorphism. - - property: extremal generating collection proof: >- The proof is similar to the one for $\Top$. In this case, suppose $\kappa$ is an uncountable regular cardinal. We can then define $\M_\kappa$ to be the collection of subsets $E \subseteq \kappa + 1$ such that there exists an ordinal $\alpha < \kappa$ such that for each $\beta \in [\alpha, \kappa)$, $\beta \in E$ if and only if $\kappa \in E$. This is easily checked to be a $\sigma$-algebra on $\kappa + 1$. Similarly, define $\M_\kappa'$ to be the $\sigma$-algebra generated by $\M_\kappa \cup \{ \{ \kappa \} \}$; this can be described as the set of $E \subseteq \kappa + 1$ such that there exists an ordinal $\alpha < \kappa$ such that for each $\beta, \gamma \in [\alpha, \kappa)$, $\beta \in E$ if and only if $\gamma \in E$. diff --git a/database/data/categories/Met_oo.yaml b/database/data/categories/Met_oo.yaml index 83cbebce1..041c0d232 100644 --- a/database/data/categories/Met_oo.yaml +++ b/database/data/categories/Met_oo.yaml @@ -70,11 +70,6 @@ unsatisfied_properties: references: - Met_no_effective_cocongruences - - property: regular - proof: We can take the same counterexample as for $\PMet$. - references: - - PMet_not_regular - - property: regular subobject classifier proof: The same proof as for $\Met$ works. references: diff --git a/database/data/categories/Mono.yaml b/database/data/categories/Mono.yaml index a1821fa25..9b4b72aab 100644 --- a/database/data/categories/Mono.yaml +++ b/database/data/categories/Mono.yaml @@ -91,6 +91,7 @@ satisfied_properties: - property: effective cocongruences proof: 'See the proof that $\Mono$ is co-Malcev: It shows that in fact any coreflexive corelation is equivalent to an effective cocongruence $X \sqcup X \twoheadrightarrow X \sqcup_Y X$.' + check_redundancy: false unsatisfied_properties: - property: skeletal diff --git a/database/data/categories/Pos.yaml b/database/data/categories/Pos.yaml index 5fae25783..94a3ecd77 100644 --- a/database/data/categories/Pos.yaml +++ b/database/data/categories/Pos.yaml @@ -58,9 +58,6 @@ unsatisfied_properties: - property: balanced proof: The inclusion $\{0,1\} \to \{0 < 1\}$ provides a counterexample (where in the domain there is no relation between $0$ and $1$). - - property: regular - proof: See Example 3.14 at the nLab. - - property: Malcev proof: 'Consider the subposet $\{(a,b) : a \leq b \}$ of $\IN^2$.' diff --git a/database/data/categories/PreOrd.yaml b/database/data/categories/PreOrd.yaml index 31190a912..8ee261070 100644 --- a/database/data/categories/PreOrd.yaml +++ b/database/data/categories/PreOrd.yaml @@ -56,9 +56,6 @@ satisfied_properties: Finally, by this result, we can conclude that the product of $\{0,1\}_c$ and $\{0<1\}$ is an extremal cogenerator. unsatisfied_properties: - - property: regular - proof: See Example 3.14 at the nLab. - - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Set_family_mostly_0.yaml b/database/data/categories/Set_family_mostly_0.yaml index 135f396de..aad49077a 100644 --- a/database/data/categories/Set_family_mostly_0.yaml +++ b/database/data/categories/Set_family_mostly_0.yaml @@ -74,12 +74,6 @@ satisfied_properties: - property: effective congruences proof: Let $R \rightrightarrows X$ be a congruence in $\Set^{(I)}_0$. We claim that it is the kernel pair of its coequalizer $X \twoheadrightarrow X/R$. This certainly holds in $\Set$, and for every $i \in I$, the pair $R_i \rightrightarrows X_i$ is a congruence in $\Set$. Therefore, the claim follows since kernel pairs (in fact, all connected limits) and coequalizers (in fact, all colimits) are constructed pointwise. - - property: effective cocongruences - proof: Let $X \rightrightarrows R$ be a cocongruence in $\Set^{(I)}_0$. We claim that it is the cokernel pair of its equalizer $E \hookrightarrow X$. This certainly holds in $\Set$, and for every $i \in I$, the pair $X_i \rightrightarrows R_i$ is a cocongruence in $\Set$. Therefore, the claim follows since cokernel pairs (in fact, all colimits) and equalizers (in fact, all connected limits) are constructed pointwise. - - - property: co-Malcev - proof: Since colimits are constructed pointwise, this property is inherited from $\Set$. - unsatisfied_properties: - property: skeletal proof: This is trivial. diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index 5a6473169..0521ce0e2 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -79,9 +79,6 @@ unsatisfied_properties: - property: cartesian filtered colimits proof: 'The functor $\IQ \times - : \Top \to \Top$ does not preserve sequential colimits; see MSE/1255678.' - - property: regular - proof: See Example 3.14 at the nLab. - - property: coaccessible proof: 'Assume $\Top$ is coaccessible. Let $p : S \to I$ be the identity map from the Sierpiński space to the two-element indiscrete space. Then, a topological space is discrete if and only if it is projective to the morphism $p$. This implies that the full subcategory spanned by all discrete spaces, which is equivalent to $\Set$, is coaccessible by Adámek–Rosický, Prop. 4.7. However, since $\Set$ is not coaccessible, this is a contradiction.' label: Top_not_coaccessible diff --git a/database/data/categories/omega-Set.yaml b/database/data/categories/omega-Set.yaml new file mode 100644 index 000000000..854949578 --- /dev/null +++ b/database/data/categories/omega-Set.yaml @@ -0,0 +1,296 @@ +id: omega-Set +name: category of ω-sets +notation: $\omegaSet$ +objects: pairs $(X, R_X)$ where $X$ is a set and $R_X \subseteq \IN \times X$ is a "realization" relation such that $(p_2)_*(R_X) = X$ +morphisms: 'a morphism $(X, R_X) \to (Y, R_Y)$ is a function $f : X \to Y$ such that there exists a realizer tracker compatible with $f$: this is a partial recursive function $\ulcorner f \urcorner : \IN \dashrightarrow \IN$ such that for every $(n,x) \in R_X$, the value $\ulcorner f \urcorner(n)$ is defined and $(\ulcorner f \urcorner(n),f(x)) \in R_Y$' +description: >- + An $\omega$-set represents a mathematical set with computational encodings of its elements; and similarly, a morphism of $\omega$-sets is a mathematical function such that roughly speaking, there is a computer program which translates encodings in the domain to encodings in the codomain (at least theoretically, if run on a computer with unlimited storage capacity and given an unlimited though finite time to work). In particular, if we consider $(n, x) \in R_X$ roughly to express a notion of $n$ being a serialization of a valid representation of $x$, then: + + + In many of the proofs to follow, we will use the phrase "$n$ realizes $x$" to mean $(n, x) \in R_X$. + + + Note that in several of the properties below, we will fix a choice of a total recursive pairing function $\langle {-}, {-} \rangle : \IN^2 \to \IN$ with total recursive inverses $p_1, p_2 : \IN \to \IN$. (Standard examples of such a pairing function include $\langle m, n \rangle \coloneqq \binom{m+n+1}{2} + m$, or the function intertwining the binary representations of $m$ and $n$.) +nlab_link: https://ncatlab.org/nlab/show/assembly +tags: + - logic + +related: + - Set + +comments: + - 'Note that the realizer tracker $\ulcorner f \urcorner$ is not part of the data of a morphism $f : (X, R_X) \to (Y, R_Y)$; only the existence of at least one realizer tracker is required.' + - 'The forgetful functor $U : \omegaSet \to \Set$ has a right adjoint $\nabla : \Set \to \omegaSet$ mapping a set $X$ to the $\omega$-set $(X, \IN \times X)$.' + +satisfied_properties: + - property: locally small + proof: There is a forgetful functor $\omegaSet \to \Set$ and $\Set$ is locally small. + + - property: semi-strongly connected + proof: 'Suppose we have two objects $(X, R_X)$ and $(Y, R_Y)$. If $Y$ is non-empty, suppose $y_0 \in Y$, and find $n_0 \in \IN$ such that $n_0$ realizes $y_0$. Then it is easy to see that the constant function with value $y_0$ is a morphism in $\Hom_{\omegaSet}((X, R_X), (Y, R_Y))$, where we can choose the compatible realizer tracker $\ulcorner y_0 \urcorner : \IN \dashrightarrow \IN$ to be the total recursive function with constant value $n_0$. Otherwise, if $Y$ is empty, then the unique function $Y \to X$ is a morphism in $\Hom_{\omegaSet}((Y, R_Y), (X, R_X))$, and in fact any partial recursive function $\IN \dashrightarrow \IN$ is a compatible realizer tracker.' + label: omega_Set_ssc + + - property: well-powered + proof: If $(X, R_X) \hookrightarrow (Y, R_Y)$ is a monomorphism, then by the description below, this implies the underlying function $X \to Y$ is injective. Therefore, we can find an equivalent subobject $(X, R_X) \cong (Y', R_{Y'})$ where $Y' \subseteq Y$ by transporting $R_X$ to the image of the underlying function. The collection of possible $Y'$ is then small, and for each $Y'$, the collection of possible $R_{Y'}$ is also small. + + - property: well-copowered + proof: If $(X, R_X) \twoheadrightarrow (Y, R_Y)$ is an epimorphism, then by the description below, this implies the underlying function $X \to Y$ is surjective. Therefore, if $E$ is the kernel pair of this underlying function, then we can find an equivalent quotient object $(X / E, R_{X / E})$ by transporting $R_X$ to $X / E$. The collection of possible equivalence relations $E$ is then small, and for each $E$, the collection of possible $R_{X / E}$ is also small. + + - property: terminal object + proof: 'The $\omega$-set $\nabla 1 = (1, \IN \times 1)$ is terminal, since $\nabla$ is a right adjoint and therefore preserves terminal objects.' + check_redundancy: false + + - property: binary products + proof: >- + We claim that for $\omega$-sets $(X, R_X)$ and $(Y, R_Y)$, then $(X \times Y, R_{X\times Y})$ is a binary product where + $$R_{X\times Y} \coloneqq \{ (\langle n, m \rangle, (x, y)) \mid (n, x) \in R_X \land (m, y) \in R_Y \}$$ + and the two projections are the standard set-level projections $\pi_1 : X\times Y \to X$ and $\pi_2 : X\times Y \to Y$. First, those projections are indeed morphisms of $\omega$-sets, since $p_1, p_2 : \IN \to \IN$ are assumed to be total recursive functions. Also, for any two morphisms $f : (U, R_U) \to (X, R_X)$ and $g : (U, R_U) \to (Y, R_Y)$, let $\ulcorner f \urcorner, \ulcorner g \urcorner : \IN \dashrightarrow \IN$ be realizer trackers compatible with $f$ and $g$, respectively. Then $\langle {-}, {-} \rangle \circ (\ulcorner f \urcorner, \ulcorner g \urcorner)$ is a realizer tracker compatible with $(f, g) : U \to X \times Y$, showing that $(f, g)$ induces a morphism $(U, R_U) \to (X\times Y, R_{X\times Y})$. + check_redundancy: false + + - property: equalizers + proof: >- + Let $f, g : (X, R_X) \rightrightarrows (Y, R_Y)$ be two parallel morphisms, and let $E \subseteq X$ be the equalizer of the underlying functions. We then claim that $(E, R_X \cap (\IN \times E))$ is an equalizer of $f$ and $g$, with the morphism $(E, R_X \cap (\IN \times E)) \hookrightarrow (X, R_X)$ being the inclusion map. First, to see this indeed gives a morphism of $\omega$-sets, note that the identity function is a compatible realizer tracker. Now, if we have $h : (U, R_U) \to (X, R_X)$ such that $h \circ f = h \circ g$, then it is easy to see that the induced function $\bar h : U \to E$ to the equalizer in $\Set$ induces a morphism $(U, R_U) \to (E, R_X \cap (\IN \times X'))$ since any realizer tracker compatible with $h$ is also compatible with $\bar h$. + check_redundancy: false + + - property: initial object + proof: 'The $\omega$-set $(\varnothing, \varnothing)$ is initial. Namely, for any object $(X, R_X)$, the unique function $! : \varnothing \to X$ is a morphism $(\varnothing, \varnothing) \to (X, R_X)$. In fact, any partial recursive function $\IN \dashrightarrow \IN$ is vacuously a compatible realizer tracker.' + check_redundancy: false + + - property: binary coproducts + proof: >- + We claim that for $\omega$-sets $(X, R_X)$ and $(Y, R_Y)$, then $(X \sqcup Y, R_{X\sqcup Y})$ is a binary coproduct where + $$R_{X\sqcup Y} \coloneqq \{ (2n, x) \mid (n, x) \in R_X \} \cup \{ (2n+1, y) \mid (n, y) \in R_Y \}$$ + and the two coprojections are the standard set-level coprojections $i_1 : X \hookrightarrow X \sqcup Y$ and $i_2 : Y \hookrightarrow X \sqcup Y$. First, those coprojections are indeed morphisms of $\omega$-sets, since the functions $n \mapsto 2n$ and $n \mapsto 2n+1$ are total recursive functions $\IN \to \IN$. Also, for any two morphisms $f : (X, R_X) \to (Z, R_Z)$ and $g : (Y, R_Y) \to (Z, R_Z)$, let $\ulcorner f \urcorner, \ulcorner g \urcorner : \IN \dashrightarrow \IN$ be realizer trackers compatible with $f$ and $g$, respectively. Then there is a unique partial recursive function which sends $2n \mapsto \ulcorner f \urcorner(n)$ (if the latter exists) and $2n+1 \mapsto \ulcorner g \urcorner(n)$ (if the latter exists), and it forms a realizer tracker compatible with $(f; g) : X\sqcup Y \to Z$. Therefore, $(f; g)$ induces a morphism $(X\sqcup Y, R_{X\sqcup Y}) \to (Z, R_Z)$. + check_redundancy: false + + - property: coequalizers + proof: >- + Let $f, g : (X, R_X) \rightrightarrows (Y, R_Y)$ be two parallel morphisms, and let $p : Y \twoheadrightarrow Q$ be the coequalizer of the underlying functions. Also, let + $$R_Q \coloneqq ({\id_{\IN}} \times p)_*(R_Y) = \{ (n, p(y)) \mid (n, y) \in R_Y \}.$$ + We claim that $p : (Y, R_Y) \to (Q, R_Q)$ is a coequalizer of $f$ and $g$. First, the identity function $\IN \to \IN$ is a realizer tracker compatible with $p$, so $p$ is indeed a morphism of $\omega$-sets. Now, suppose we have a morphism $h : (Y, R_Y) \to (Z, R_Z)$ with $h\circ f = h\circ g$. Let $\bar h : Q \to Z$ be the function induced by $Q$ being the coequalizer in $\Set$. We then claim that $\bar h : (Q, R_Q) \to (Z, R_Z)$ is also a morphism of $\omega$-sets. This follows since it is easy to see that any realizer tracker compatible with $h$ is also compatible with $\bar h$. + + - property: cartesian closed + proof: >- + First, fix an admissible numbering $(\varphi_n)_{n \in \IN}$ of the partial recursive functions. + + Let $(X, R_X)$ and $(Y, R_Y)$ be two $\omega$-sets. We will define the exponential $[(X, R_X), (Y, R_Y)]$ to have underlying set $\Hom_{\omegaSet}((X, R_X), (Y, R_Y))$. The realization relation will be that $p \in \IN$ realizes $f : (X, R_X) \to (Y, R_Y)$ if and only if the $p$th partial recursive function $\varphi_p$ is unary and is a realizer tracker compatible with $f$. + + In order to check that this is indeed an exponential in $\omegaSet$, we first define the evaluation morphism + $$\ev : [(X, R_X), (Y, R_Y)] \times (X, R_X) \to (Y, R_Y), \quad (f, x) \mapsto f(x).$$ + To show that this is in fact a morphism of $\omega$-sets, note that using the evaluation axiom of the admissible numbering, there is a partial recursive function $\varepsilon : \IN \dashrightarrow \IN$ such that $\varepsilon(\langle p, n \rangle)$ exists if and only $\varphi_p(n)$ exists, and in this case $\varepsilon(\langle p, n \rangle) = \varphi_p(n)$. This $\varepsilon$ is then a realizer tracker compatible with $\ev$. + + Now, suppose we have a morphism $h : (U, R_U) \times (X, R_X) \to (Y, R_Y)$, with compatible realizer tracker $\ulcorner h \urcorner : \IN \dashrightarrow \IN$. Using the currying axiom of the admissible numbering, we can then curry $\ulcorner h \urcorner$ into a total recursive function $\ulcorner \lambda_h \urcorner : \IN \to \IN$, such that each $\varphi_{\ulcorner \lambda_h \urcorner(n)}$ is unary; $\varphi_{\ulcorner \lambda_h \urcorner(n)}(m)$ exists if and only if $\ulcorner h \urcorner(\langle n, m \rangle)$ exists; and in that case + $$\varphi_{\ulcorner \lambda_h \urcorner(n)}(m) = \ulcorner h \urcorner(\langle n, m \rangle).$$ + This implies that for each $u\in U$, if we find a realizer $n$ of $u$, then $h(u, {-}) : X \to Y$ has $\ulcorner h \urcorner(\langle n, {-} \rangle)$ as a compatible realizer tracker; thus, $u \mapsto h(u, {-})$ induces a function + $$\lambda_h : U \to \Hom_{\omegaSet}((X, R_X), (Y, R_Y)).$$ + Furthermore, $\ulcorner \lambda_h \urcorner$ is a compatible realizer tracker for $\lambda_h$, so in fact we get a morphism + $$\lambda_h : (U, R_U) \to [(X, R_X), (Y, R_Y)].$$ + + From here, it is straightforward to show that $\lambda_h$ is the unique morphism such that $ev \circ (\lambda_h \times \id_X) = h$. + check_redundancy: false + + - property: locally cartesian closed + proof: >- + This proof will be an adaptation of the proof above that the category is cartesian closed. As in the previous proof, we first fix an admissible numbering $(\varphi_n)_{n \in \IN}$ of the partial recursive functions. + + As a preliminary, suppose we have a morphism $f : (X, R_X) \to (Z, R_Z)$ and an element $z\in Z$. Then we will define $f_z$ to be the $\omega$-set with underlying set $f^*(\{ z \})$ and with realization relation $R_X \cap (\IN \times f^*(\{ z \}))$. + + As another preliminary, suppose we have a span + $$(X, R_X) \xrightarrow{f} (Z, R_Z) \xleftarrow{g} (Y, R_Y).$$ + Then from the above descriptions of binary products and equalizers, we can describe the pullback in $\omegaSet$ as having underlying set given by the pullback of underlying sets $f \times_Z g$, with realization relation + $$\{ (\langle n, m \rangle, (x, y)) \mid f(x) = g(y) \land (n, x) \in R_X \land (m, y) \in R_Y \}.$$ + + Now, suppose we have two morphisms $f : (X, R_X) \to (Z, R_Z)$ and $g : (Y, R_Y) \to (Z, R_Z)$. Then the relative exponential $[f, g]_Z$ will have underlying set + $$\bigsqcup_{z\in Z} \Hom_{\omegaSet}(f_z, g_z).$$ + The realization relation will be that $\langle n, p \rangle$ realizes $\alpha \in \Hom_{\omegaSet}(f_z, g_z)$ if $n$ realizes $z$, and $p$ is the code for a unary partial recursive function $\varphi_p : \IN \dashrightarrow \IN$ which is a realizer tracker compatible with $\alpha$. + + First, it is easy to see that the projection to $Z$ is a morphism of $\omega$-sets $[f, g]_Z \to (Z, R_Z)$, since $p_1 : \IN \to \IN$ is a compatible realizer tracker. This is the morphism we will use to consider $[f, g]_Z$ as an object of $\omegaSet / (Z, R_Z)$. + + The next step is to define an evaluation morphism + $$\ev_Z : [f, g]_Z \times_{(Z, R_Z)} (X, R_X) \to (Y, R_Y).$$ + We will define this as the function + $$\bigsqcup_{z\in Z} \left( \Hom(f_z, g_z) \times X_z \right) \to Y, (z, (\alpha, x)) \mapsto \alpha(x).$$ + The fact that this is a morphism of $\omega$-sets follows from the fact that using the evaluation axiom of the admissible numbering, there is a partial recursive function $\IN \dashrightarrow \IN$ which sends $\langle \langle n, p \rangle, m \rangle \rangle$ to $\varphi_p(m)$ if the latter exists; and it gives a compatible realizer tracker. + + Finally, suppose we have a morphism $h : (U, R_U) \to (Z, R_Z)$ and a morphism $j : h \times_{(Z, R_Z)} f \to g$ in $\omegaSet / (Z, R_Z)$. Choose realizer trackers $\ulcorner h \urcorner : \IN \dashrightarrow \IN$ and $\ulcorner j \urcorner : \IN \dashrightarrow \IN$ compatible with $h$ and $j$, respectively. We can then use the currying axiom of the admissible numbering to construct a total recursive function $\ulcorner \lambda_j \urcorner : \IN \to \IN$, such that $\varphi_{\ulcorner \lambda_j \urcorner(n)}(m)$ exists if and only if $\ulcorner j \urcorner(\langle n, m \rangle)$ exists, and in that case + $$\varphi_{\ulcorner \lambda_j \urcorner(n)}(m) = \ulcorner j \urcorner(\langle n, m \rangle).$$ + This implies that for each $u\in U$, if we find a realizer $n$ of $u$, then $j(u, {-}) : f_{h(u)} \to g_{h(u)}$ has $\ulcorner j \urcorner(\langle n, {-} \rangle)$ as a compatible realizer tracker. Thus, $u \mapsto j(u, {-})$ induces a function + $$\lambda_j : U \to \bigsqcup_{z\in Z} \Hom_{\omegaSet}(f_z, g_z).$$ + Furthermore, $n \mapsto \langle \ulcorner h \urcorner(n), \ulcorner \lambda_j \urcorner(n) \rangle$ is a partial recursive function, and it gives a compatible realizer tracker for $\lambda_j$. + + From here, it is straightforward to show that $\lambda_j$ is the unique morphism such that $\ev_Z \circ (\lambda_j \times_{(Z, R_Z)} \id_f) = j$. + + - property: regular subobject classifier + proof: >- + We claim that $\Omega \coloneqq (2, \IN \times 2)$ is a regular subobject classifier, with $\top : 1 \to \Omega$ being the morphism whose underlying set function is $0 \mapsto 1$. To see this, note that from the construction of equalizers above, any regular subobject of $(X, R_X)$ is equivalent to $(X', R_X \cap (\IN \times X'))$ for some $X' \subseteq X$. It is then straightforward to check that the characteristic function $\chi_{X'} : X \to 2$ induces a morphism $(X, R_X) \to \Omega$, and that $(X', R_X \cap (\IN \times X'))$ is also the pullback of $\chi_{X'}$ and $\top$. + + - property: disjoint finite coproducts + proof: This follows from the fact that the forgetful functor $\omegaSet \to \Set$ preserves finite coproducts from the construction above; the fact that finite coproducts are disjoint in $\Set$; and the fact that the forgetful functor reflects initial objects. + + - property: generator + proof: The terminal object $(1, \IN \times 1)$ represents the forgetful functor $\omegaSet \to \Set$ which is clearly faithful. (For the nontrivial direction of the isomorphism between $\Hom_{\omegaSet}((1, \IN \times 1), (X, R_X))$ and $X$, suppose we have $x \in X$. Then there exists $n \in \IN$ such that $n$ realizes $x$; therefore, the total recursive function given by the constant function with image $n$ forms a realizer tracker compatible with the corresponding function $1 \to X$.) + + - property: extremal generating collection + proof: >- + We claim that the collection of $\omega$-sets $(U, R_U)$ with $U\subseteq \IN$ is an extremal generating collection. To see this, note that the terminal object is isomorphic to the object $(\{ 0 \}, \IN \times \{ 0 \})$, and we saw above that it is a generator, so the given collection is certainly a generating collection. + + To see it is extremal, suppose we have a morphism $f : (X, R_X) \to (Y, R_Y)$ which is not an isomorphism. If this is because the underlying function $f : X \to Y$ is not a bijection, then that implies + $$f \circ {-} : \Hom((\{0\}, \IN\times\{0\}), (X, R_X)) \to \Hom((\{0\}, \IN\times\{0\}), (Y, R_Y))$$ + is not a bijection. Otherwise, if the underlying function is a bijection, but $f$ is not an isomorphism, then by the description of isomorphisms below, for each partial recursive function $\psi : \IN \dashrightarrow \IN$, there exist $n_\psi \in \IN$ and $x_\psi \in X$ such that $n_\psi$ realizes $f(x_\psi)\in Y$, but either $\psi(n_\psi)$ does not exist, or $\psi(n_\psi)$ does not realize $x_\psi\in X$. Choose one such pair of $n_\psi$ and $x_\psi$ for each unary partial recursive function $\psi$. We will then define $U$ to be the collection of all $f(x_\psi)$ where $\psi$ is a unary partial recursive function, and $R_U \coloneqq R_Y \cap (\IN \times U)$. + + Then $(U, R_U)$ is an $\omega$-set, and the inclusion map $i : U \hookrightarrow Y$ induces a morphism $i : (U, R_U) \hookrightarrow (Y, R_Y)$ of $\omega$-sets, since the identity function $\IN \to \IN$ is a compatible realizer tracker. However, we claim there can be no morphism $g : (U, R_U) \to (X, R_X)$ such that $f \circ g = i$. In fact, if such $g$ existed, then the underlying function would have to send $f(x_{\psi}) \mapsto x_{\psi}$. On the other hand, if $\ulcorner g \urcorner : \IN \dashrightarrow \IN$ were a compatible realizer tracker, then we would have that $n_{\ulcorner g \urcorner}$ realizes $f(x_{\ulcorner g \urcorner})\in U$, and therefore $\ulcorner g \urcorner(n_{\ulcorner g \urcorner})$ exists and $\ulcorner g \urcorner(n_{\ulcorner g \urcorner})$ realizes $g(f(x_{\ulcorner g \urcorner})) = x_{\ulcorner g \urcorner}\in X$, contradicting the choice of $n_{\ulcorner g \urcorner}$ and $x_{\ulcorner g \urcorner}$. + + This shows that + $$f \circ {-} : \Hom((U, R_U), (X, R_X)) \to \Hom((U, R_U), (Y, R_Y))$$ + is not surjective, and therefore not bijective. However, since there are only countably many partial recursive functions, $U$ is countable. Hence $(U, R_U)$ is isomorphic to a member of the given collection, which we can construct by choosing a subset of $\IN$ bijective to $U$, and then transporting $R_U$ to that subset. + + - property: extremal cogenerator + proof: >- + We first claim that $\nabla 2$ and $(P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$ form an extremal cogenerating collection. To see this, we first consider morphisms to the first member $\nabla 2$ of the family. Note that + $$\Hom_{\omegaSet}({-}, \nabla 2) \cong \Hom_{\Set}(U{-}, 2),$$ + where $U : \omegaSet \to \Set$ is the forgetful functor. Therefore, $\Hom_{\omegaSet}({-}, \nabla 2)$ is isomorphic to the composition of $U$ and the power set functor $P : \Set^{\op} \to \Set$, both of which are faithful. This shows that $\nabla 2$ is a cogenerator, so the collection is also a cogenerating collection. + + To show the collection is an extremal cogenerating collection, suppose we have a morphism $f : (X, R_X) \to (Y, R_Y)$ such that ${-} \circ f$ induces bijections of morphism sets to both members of the collection. From the first assumption that + $${-} \circ f : \Hom((Y, R_Y), \nabla 2) \to \Hom((X, R_X), \nabla 2)$$ + is a bijection, we see that + $${-} \circ f : \Hom_{\Set}(Y, 2) \to \Hom_{\Set}(X, 2)$$ + is a bijection. Since $2$ is an extremal cogenerator of $\Set$, we conclude that the underlying function of $f$ is a bijection. + + Now, consider the morphism + $$g : (X, R_X) \to (P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$$ + which sends $x \in X$ to its set of realizers (with the identity function $\IN \to \IN$ as the compatible realizer tracker). From the hypothesis, there exists a morphism + $$h : (Y, R_Y) \to (P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$$ + such that $g = h \circ f$. Choose a compatible realizer tracker $\ulcorner h \urcorner : \IN \dashrightarrow \IN$. Then for any $x\in X$, if $n$ realizes $f(x)$, then $\ulcorner h \urcorner(n)$ exists and $\ulcorner h \urcorner(n)$ realizes $h(f(x)) = g(x)$. Thus, by definition of $g$, $\ulcorner h \urcorner(n)$ is in the set of realizers of $x$, i.e. $\ulcorner h \urcorner(n)$ realizes $x$. From the characterization of isomorphisms below, this implies that $f$ is an isomorphism. + + Finally, since $\nabla 2$ and $(P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$ both have non-empty underlying sets, they form a strongly connected family (see the proof above that $\omegaSet$ is semi-strongly connected). Therefore, by this result, the product of these two objects is an extremal cogenerator. + references: + - omega_Set_ssc + - Set_extremal_cogenerator + + - property: parametrized natural numbers object + proof: >- + We claim that $N \coloneqq (\IN, \Delta_{\IN})$, where $\Delta_{\IN}$ is the diagonal, is a parametrized natural numbers object. (In other words, the realization relation is that $m$ realizes $n$ if and only if $m = n$.) First, the zero function $z : 1 \to \IN$ and the successor function $s : \IN \to \IN$ clearly induce morphisms of $\omega$-sets $z : 1 \to N$ and $s : N \to N$. Now, suppose we have $f : (A, R_A) \to (X, R_X)$ and $g : (X, R_X) \to (X, R_X)$. Choose compatible realizer trackers $\ulcorner f \urcorner, \ulcorner g \urcorner : \IN \dashrightarrow \IN$. Also, let $\Phi : A \times \IN \to X$ be the function $(a, n) \mapsto g^n(f(a))$. Then since the collection of partial recursive functions is closed under primitive recursion, we can also construct a partial recursive function $\ulcorner \Phi \urcorner$ such that + $$\ulcorner \Phi \urcorner(\langle b, 0 \rangle) = \ulcorner f \urcorner(b)$$ + and + $$\ulcorner \Phi \urcorner(\langle b, n+1 \rangle) = \ulcorner g \urcorner(\ulcorner \Phi \urcorner(\langle b, n \rangle)).$$ + Now suppose $m$ realizes $a \in A$; then an easy induction shows that for each $n$, $\ulcorner \Phi \urcorner(\langle m, n \rangle)$ exists and realizes $\Phi(a, n)$. This shows that $\Phi$ induces a morphism of $\omega$-sets $(A, R_A) \times N \to (X, R_X)$ with the required properties. + + Uniqueness of $\Phi$ follows from the uniqueness part of $\IN$ being a parametrized natural numbers object in $\Set$. + +unsatisfied_properties: + - property: skeletal + proof: Consider $(X, \IN \times X)$ and $(Y, \IN \times Y)$ for $X$ and $Y$ bijective but unequal sets. + + - property: essentially small + proof: 'The right adjoint $\nabla : \Set \to \omegaSet$ to the forgetful functor is fully faithful, and therefore conservative.' + + - property: locally finite + proof: >- + The right adjoint $\nabla : \Set \to \omegaSet$ to the forgetful functor is fully faithful. Therefore, for example, + $$\Hom_{\omegaSet}(\nabla 1, \nabla \IN) \cong \Hom_{\Set}(1, \IN)$$ + is infinite. + + - property: balanced + proof: 'The identity map $\IN \to \IN$ induces a morphism of $\omega$-sets $N \to \nabla \IN$, since the identity map is also a compatible realizer tracker. It is both a monomorphism and an epimorphism by the characterizations below. However, it is not an isomorphism: an inverse $\nabla \IN \to N$ would have to have the identity map $\IN \to \IN$ as its underlying function. But for any compatible realizer tracker $\psi$, we have that $0$ realizes both $0$ and $1$ in $\nabla \IN$. Therefore, $\psi(0)$ would have to exist and realize both $0$ and $1$ in $N$, which is impossible. (Alternately, $\Hom_{\omegaSet}(\nabla \IN, \nabla \IN) \cong \Hom_{\Set}(\IN, \IN)$ is uncountable. On the other hand, it is easy to see that $\Hom_{\omegaSet}(N, N)$ is exactly the total recursive functions, since a compatible realizer tracker would have to agree with the underlying function. Therefore, $\Hom_{\omegaSet}(N, N)$ is countable.)' + check_redundancy: false + + - property: co-Malcev + proof: 'Consider the two possible morphisms $f, g : \nabla 1 \rightrightarrows \nabla 2$. This defines a cocongruence representing the functor which to $(X, E_X)$ assigns the binary relation on $X$ of two elements having a common realizer. That shows that this cocongruence is coreflexive, since by definition any element of an $\omega$-set has a realizer. However, it is easy to see that it is not cotransitive; for example, in $(3, \{ (0, 0), (0, 1), (1, 1), (1, 2) \})$, $0$ and $1$ have a common realizer, as do $1$ and $2$; but $0$ and $2$ do not have a common realizer.' + + - property: countable powers + proof: >- + Let $N \coloneqq (\IN, \Delta_{\IN})$ be the natural numbers object. For any $\omega$-set $(X, R_X)$ with a sequence of morphisms $f_n : (X, R_X) \to N$, we can define a function $g : X \to \IN^{\IN}$ which sends $x \in X$ to the sequence $(f_n(x))_{n\in \IN}$. We claim that $g$ has countable image. To see this, suppose $x\in X$. Then there exists $m\in \IN$ such that $m$ realizes $x$. We can also choose realizer trackers $\ulcorner f_n \urcorner : \IN \dashrightarrow \IN$ compatible with $f_n$. It follows that $\ulcorner f_n \urcorner(m)$ is defined and $\ulcorner f_n \urcorner(m) = f_n(x)$ for each $n$. Therefore, the image of $g$ is contained in the set of sequences $(\ulcorner f_n \urcorner(m))_{n\in N}$ where $m \in \IN$ is such that $\ulcorner f_n \urcorner(m)$ is defined for each $n$. + + From this, we see that there can be no $\aleph_0$-indexed power of $N$. Indeed, if $X$ were such a power, then for any sequence $(a_n) \in \IN^{\IN}$, we would have a corresponding sequence of morphisms $1 \to \IN$, inducing a morphism $1 \to X$ and thus an element $x$ of the underlying set. The corresponding function $g : X \to \IN^{\IN}$ would then have to have value $g(x) = (a_n)$. Thus, $g$ would be surjective, contradicting the previous paragraph. + + - property: ℵ₁-filtered colimits + proof: >- + This counterexample is inspired by the construction in Jaap van Oosten, Filtered colimits in the effective topos. Here, first choose an $\omega_1$-Aronszajn sequence: this is a sequence $(s_\alpha)_{\alpha \in \omega_1}$ of injective functions $\alpha \to \IN$ such that whenever $\beta < \alpha < \omega_1$, then $s_\beta$ and $s_\alpha |_\beta$ agree except at finitely many points. We then let $X_\alpha$ be the $\omega$-set whose underlying set is $\alpha$, equipped with the realization relation that $n$ realizes $\beta \in \alpha$ if and only if $s_\alpha(\beta) = n$. + + Whenever $\beta < \alpha$, the inclusion map $\beta \hookrightarrow \alpha$ induces a morphism $X_\beta \to X_\alpha$. This is because by the above condition, a compatible realizer tracker only needs to "reassign" finitely many realizers, which is certainly possible to achieve with a total recursive function. It is easy to see that this makes $(X_\alpha)_{\alpha \in \omega_1}$ into an ℵ₁-filtered diagram. + + However, this diagram cannot have a colimit. If it did have a colimit $Y$, it would have to have underlying set equivalent to $\omega_1$, since the forgetful functor $\omegaSet \to \Set$ is a left adjoint. Thus, we may assume $Y$ has underlying set equal to $\omega_1$, with the cocone maps $X_\alpha \to Y$ being the inclusion maps. Also, for any $\gamma_0 \in \omega_1$, we can construct morphisms $X_\alpha \to N$ such that $\beta \mapsto 0$ except that $\gamma_0 \mapsto 1$ if $\gamma_0 \in \alpha$. To see this, if $\gamma_0 \not\in \alpha$, then we can use the constant function with value 0 as the compatible realizer tracker. On the other hand, if $\gamma_0 \in \alpha$, then we can use the total recursive function which sends all natural numbers to 0, except that it sends $s_\alpha(\gamma_0)$ to 1. It is easy to see that this gives a cocone of $(X_\alpha)_{\alpha \in \omega_1}$, so it induces a morphism $f : Y \to N$. Furthermore, we must have $f(\gamma_0) = 1$ while $f(\gamma ') = 0$ for $\gamma ' \ne \gamma_0$. + + From this, examining the conditions on a compatible realizer tracker for $f$, we can conclude that for $\gamma ' \ne \gamma_0$, $\gamma_0$ and $\gamma '$ cannot have any common realizers in $Y$. Thus, the realization relation on $Y$ induces a surjective function from a subset of $\IN$ to $\omega_1$, giving a contradiction. + + - property: extremal generator + proof: >- + Suppose we had an extremal generator $(G, R_G)$. + + + Step 1: We construct an $\omega$-set $(T, R_T)$ such that $T$ is infinite, but any morphism $(G, R_G) \to (T, R_T)$ has finite image. + + + In order to do this, first let $\Gamma \coloneqq (p_1)_*(R_G)$ be the set of realizers of elements of $G$. Also fix an enumeration $(\varphi_n)_{n\in \IN}$ of the unary partial recursive morphisms $\IN \dashrightarrow \IN$ (which does not need to be an admissible numbering for this application). We will then construct an increasing sequence of finite subsets $I_n, O_n \subseteq \IN$ such that $I_n \cap O_n = \varnothing$ for each $n$. We start with $I_0 = O_0 = \varnothing$. Now for each $n$, if $(\varphi_n)_*(\Gamma) \subseteq I_n \cup O_n$, then we set $O_{n+1} \coloneqq O_n$; otherwise, we let $O_{n+1} \coloneqq O_n \cup \{ b_n \}$ where we choose + $$b_n \in (\varphi_n)_*(\Gamma) \setminus (I_n \cup O_n).$$ + We then let $I_{n+1} \coloneqq I_n \cup \{ a_n \}$ where we choose + $$a_n \in \IN \setminus (I_n \cup O_{n+1}).$$ + + Once we have this sequence, we let $T \coloneqq \bigcup_{n\in \IN} I_n$, and $R_T \coloneqq \Delta_T \subseteq \IN \times T$. + + + Step 2: Proof that $(T, R_T)$ has the properties stated in Step 1. + + + First, since $\card(I_{n+1}) = n$ for each $n$, then $T$ must certainly be infinite. Now, suppose we have a morphism $f : (G, R_G) \to (T, R_T)$, and choose $n$ such that $\varphi_n$ is a compatible realizer tracker. Then whenever $m$ realizes $x \in X$, we must have $f(x) = \varphi_n(m)$; from this fact, it is easy to see that the image of $f$ is equal to $(\varphi_n)_*(\Gamma)$. However, if we had the second case at stage $n$ in the above construction, then we would have $b_n \in O_m$ whenever $m > n$; hence $b_n \notin T$. On the other hand, $b_n \in (\varphi_n)_*(\Gamma)$ by construction, and $(\varphi_n)_*(\Gamma) \subseteq T$, giving a contradiction. + + + Thus, we must have had the first case at stage $n$ in the above construction. In other words, $(\varphi_n)_*(\Gamma) \subseteq I_n \cup O_n$, and the latter is finite. + + + Step 3: Construction of a function $c : T \to \IN$ which is not the restriction of any partial recursive function $\IN \dashrightarrow \IN$. + + + This is an easy adaptation of the standard diagonalization construction of a non-recursive function. We use the enumeration $(\varphi_n)_{n\in \IN}$ of the unary partial recursive morphisms as above, along with an enumeration $(t_n)_{n\in \IN}$ of the countably infinite set $T$. We now set + $$c(t_n) \coloneqq \begin{cases} + 1, & t_n\in \dom(\varphi_n) \land \varphi_n(t_n) = 0, \\ + 0, & \mathrm{otherwise}. + \end{cases}$$ + By construction, $c \ne (\varphi_n) |_T$ for each $n$ since they disagree at $t_n\in T$ (either $\varphi_n(t_n)$ is not defined whereas $c(t_n)$ is defined, or they are both defined but have different values). + + + Step 4: Construction of a non-isomorphism $f : (T, R_T ') \to (T, R_T)$. + + + We first set + $$R_T' \coloneqq \{ (\langle n, c(n) \rangle, n) \mid n \in T \}.$$ + Then $f$ will have the identity map on $T$ as its underlying set function, which has $\ulcorner f \urcorner \coloneqq p_1$ as a compatible realizer tracker. We claim $f$ is not an isomorphism. To see this, any inverse $f^{-1}$ must have the identity map on $T$ as its underlying set function. Also, any compatible realizer tracker $\ulcorner f^{-1} \urcorner : \IN \dashrightarrow \IN$ must be defined at each element of $T$ with $\ulcorner f^{-1} \urcorner(n) = \langle n, c(n) \rangle$ for each $n\in T$. Therefore, $p_2 \circ \ulcorner f^{-1} \urcorner$ would be a partial recursive function whose restriction to $T$ is equal to $c$. This contradicts the construction of $c$. + + + Step 5: Proof that $(G, R_G)$ sees $f$ as an isomorphism. + + + Since $f$ is a monomorphism, certainly + $$f \circ {-} : \Hom((G, R_G), (T, R_T ')) \to \Hom((G, R_G), (T, R_T))$$ + must be injective. To see it is surjective, suppose we have a morphism $g : (G, R_G) \to (T, R_T)$, and choose a compatible realizer tracker $\ulcorner g \urcorner$. By the construction above, $g$ must have finite image. Therefore, there is a partial recursive function $c' : \IN \dashrightarrow \IN$ such that $c' |_{\im(g)} = c |_{\im(g)}$, which we could implement in any Turing-complete programming language using a lookup table for example. Now we let $h : (G, R_G) \to (T, R_T ')$ have the same underlying function as $g$. This also forms a morphism of $\omega$-sets because + $$\ulcorner h \urcorner \coloneqq n \mapsto \langle \ulcorner g \urcorner(n), c'(\ulcorner g \urcorner(n)) \rangle$$ + is a compatible realizer tracker. Furthermore, we certainly have $f \circ h = g$. + +special_objects: + initial object: + description: $(\varnothing, \varnothing)$ + terminal object: + description: $(1, \IN \times 1)$ + coproducts: + description: '[binary case] The binary coproduct of $(X, R_X)$ and $(Y, R_Y)$ is $X \sqcup Y$ with realization relation $$R_{X\sqcup Y} \coloneqq \{ (2n, x) \mid (n, x) \in R_X \} \cup \{ (2n+1, y) \mid (n, y) \in R_Y \}.$$' + products: + description: '[binary case] The binary product of $(X, R_X)$ and $(Y, R_Y)$ is $X \times Y$ with realization relation $$R_{X\times Y} \coloneqq \{ (\langle n, m \rangle, (x, y)) \mid (n, x) \in R_X \land (m, y) \in R_Y \}.$$' + +special_morphisms: + isomorphisms: + description: 'A morphism $f : (X, R_X) \to (Y, R_Y)$ is an isomorphism if and only if the underlying function $X \to Y$ is a bijection, and there also exists a partial recursive function $\psi : \IN \dashrightarrow \IN$ such that whenever we have $n\in\IN, x\in X$ such that $n$ realizes $f(x)\in Y$, then $\psi(n)$ exists and $\psi(n)$ realizes $x\in X$' + proof: This is easy, since the condition on the existence of $\psi$ just says that the set-level inverse of $f$ is also a morphism in $\omegaSet$. + monomorphisms: + description: Morphisms of $\omega$-sets whose underlying set function is injective + proof: This follows from the fact that the forgetful functor $\omegaSet \to \Set$ is clearly faithful, and it is representable by the terminal object $(1, \IN \times 1)$. + regular monomorphisms: + description: 'A morphism $f : (X, R_X) \to (Y, R_Y)$ is a regular monomorphism if and only if the underlying function $X \to Y$ is injective, and there exists a partial recursive function $\psi : \IN \dashrightarrow \IN$ such that whenever we have $n\in \IN$ and $x\in X$ such that $n$ realizes $f(x) \in Y$, then $\psi(n)$ exists and $\psi(n)$ realizes $x\in X$' + proof: 'Following the constructions above, we can see that for any morphism $f : (X, R_X) \to (Y, R_Y)$, the equalizer of the cokernel pair of $f$ is $(\im(f), R_Y \cap (\IN \times \im(f)))$; and the condition above is equivalent to the condition that the canonical map $X \to \im(f)$ induces an isomorphism of $\omega$-sets $(X, R_X) \to (\im(f), R_Y \cap (\IN \times \im(f)))$.' + epimorphisms: + description: Morphisms of $\omega$-sets whose underlying set function is surjective + proof: Sufficiency of this condition is trivial. For necessity, use the fact that the forgetful functor $\omegaSet$ is a left adjoint, and therefore preserves epimorphisms. + regular epimorphisms: + description: 'A morphism $f : (X, R_X) \to (Y, R_Y)$ is a regular epimorphism if and only if there exists a partial recursive function $\psi : \IN \dashrightarrow \IN$ such that whenever we have $n\in \IN$ and $y\in Y$ such that $n$ realizes $y$, then $\psi(n)$ exists, and there exists $x\in X$ such that $f(x) = y$ and $\psi(n)$ realizes $x$' + proof: 'Following the constructions above, we can see that for any morphism $f : (X, R_X) \to (Y, R_Y)$, the coequalizer of the kernel pair of $f$ is $(\im(f), ({\id_{\IN}} \times f)_*(R_X))$; and the condition above is equivalent to the condition that the canonical map $\im(f) \to Y$ induces an isomorphism of $\omega$-sets $(\im(f), (\id_{\IN} \times f)_*(R_X)) \to (Y, R_Y)$.' diff --git a/database/data/category-implications/congruences.yaml b/database/data/category-implications/congruences.yaml index ad5a60b86..94b3fdd98 100644 --- a/database/data/category-implications/congruences.yaml +++ b/database/data/category-implications/congruences.yaml @@ -105,26 +105,34 @@ - quotients of congruences proof: We assume that every congruence is effective, and the regularity condition implies that every effective congruence has a quotient. +# TODO: The "finitely cocomplete" assumption is only needed to satisfy the preconditions of co-Malcev; thus, if we +# revise the definition of "Malcev" not to require a finitely complete category, then that condition can be dropped. +# (In particular, this will allow us to conclude that the category Set_ff of sets with finite-to-one maps +# satisfies the more general definition of co-Malcev.) - id: regular_epi-regular_extensive_consequences assumptions: - epi-regular - extensive - - regular + - equalizers + - finitely cocomplete conclusions: - co-Malcev - effective cocongruences proof: >- - Suppose we have a coreflexive corelation - $$X+X' \xtwoheadrightarrow{p} E \xtwoheadrightarrow{r} X$$ - on $X$, where we let $X'$ be an isomorphic copy of $X$ for clarity below. Let $Y$ be the equalizer of $p\circ i_1, p\circ i_2 : X \rightrightarrows E$. That means that for a generalized element $x \in X(T)$, $x \in Y(T)$ if and only if $p(x) = p(x')$. Then by the assumptions $p$ is a regular epimorphism. By regularity, $p$ is the coequalizer of its kernel pair, which can be expressed as the equalizer $K$ of - $$p \circ \pi_1,\, p\circ \pi_2 : (X+X') \times (X+X') \rightrightarrows E,$$ - where $\pi_1, \pi_2$ are the projections. By distributivity and extensivity, it is sufficient to calculate the equalizer on each "quadrant" of $(X+X') \times (X+X')$, i.e. the four copies of $X \times X$. - - On the $X\times X$ quadrant, for generalized elements $x_1, x_2 \in X(T)$, we have $(x_1, x_2) \in K(T)$ if and only if $p(x_1) = p(x_2)$. Since $p\circ i_1$ is a split monomorphism, this is equivalent to $x_1 = x_2$. Thus, the $X\times X$ quadrant of $K$ is the diagonal of $X$. On the $X\times X'$ quadrant, we have $(x_1, x_2')\in K(T)$ if and only if $p(x_1) = p(x_2')$. Since $r(p(x_1)) = x_1$ and $r(p(x_2')) = x_2$, this condition implies $x_1 = x_2$; and then by definition of $Y$, $x_1 = x_2 \in Y(T)$. The converse is straightforward. Thus, the $X\times X'$ quadrant of $K$ is the diagonal of $Y$. Similarly, the $X'\times X$ quadrant of $K$ is the diagonal of $Y$, and the $X'\times X'$ quadrant of $K$ is the diagonal of $X$. - Thus, we get that a morphism $h : X+X' \to Z$ factors through $E$ if and only if $h(x) = h(x)$ for every generalized element $x \in X$; $h(y) = h(y')$ for every $y \in Y$; $h(y') = h(y)$ for every $y\in Y$; and $h(x') = h(x')$ for every $x \in X$. Clearly this is equivalent to $h(y) = h(y')$ for every $y\in Y$, so in fact $E$ is the cokernel pair of $i_1 \circ \inc_Y$ and $i_2 \circ \inc_Y$. This means that $E$ is an effective cocongruence. + This is a consequence of Lemma 4 here, since every coreflexive corelation is regular and has an equalizer by the assumptions. Remark: The assumptions are satisfied in particular for every elementary topos. Therefore, every elementary topos has effective cocongruences and is co-Malcev. This special case is treated in Borceux–Bourn, Example 2.2.18. An alternative proof of this special case is given later in A.5.17. +- id: regular_extensive_consequences + assumptions: + - extensive + - regular + - quotients of congruences + conclusions: + - effective cocongruences + proof: >- + This is proved as Corollary 5 here. + - id: pretopos_balanced assumptions: - effective congruences diff --git a/database/data/config.yaml b/database/data/config.yaml index 38bc22558..a73597d9a 100644 --- a/database/data/config.yaml +++ b/database/data/config.yaml @@ -5,6 +5,7 @@ structure_tags: - category theory - combinatorics - graph theory + - logic - number theory - order theory - relational structures diff --git a/database/data/macros.yaml b/database/data/macros.yaml index 260044b89..e0c008c56 100644 --- a/database/data/macros.yaml +++ b/database/data/macros.yaml @@ -95,6 +95,7 @@ \Open: \operatorname{Open} \Id: \operatorname{Id} \Br: \operatorname{Br} +\dom: \operatorname{dom} \rightrightrightarrows: \mathrel{\substack{\rightarrow\\[-0.6ex]\rightarrow\\[-0.6ex]\rightarrow}} \dottedrightrightarrows: \mathrel{\substack{\rightarrow\\[-0.6ex]\cdots\\[-0.6ex]\rightarrow}} @@ -171,3 +172,4 @@ \Mono: \mathbf{Mono} \Sh: \mathbf{Sh} \Proj: \mathbf{Proj} +\omegaSet: \omega{-}\Set diff --git a/shared/structure.history.json b/shared/structure.history.json index dbe579f93..dbb29d6de 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -214,5 +214,6 @@ "Bin_symm", "Bin_symm_refl", "Set_bij", - "Set_family_bij" + "Set_family_bij", + "omega-Set" ]