diff --git a/database/data/categories/Bin.yaml b/database/data/categories/Bin.yaml index e6dd1b73..bf8df09d 100644 --- a/database/data/categories/Bin.yaml +++ b/database/data/categories/Bin.yaml @@ -65,40 +65,6 @@ satisfied_properties: $$(0,1) = (h(x),h(x')) = (g(f(x)),g(f(x'))) \in R_Q,$$ which is a contradiction. - - 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/Cat.yaml b/database/data/categories/Cat.yaml index c1738a25..1072f5dc 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 which is 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 51c09ea0..ee69d7c9 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 fa3c0cbf..b0c8cb45 100644 --- a/database/data/categories/Meas.yaml +++ b/database/data/categories/Meas.yaml @@ -126,29 +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 Theorem 6.5.7 in Bogachev's Measure theory $\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 bdf90725..e8c1a660 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 289702b6..601f91fc 100644 --- a/database/data/categories/Mono.yaml +++ b/database/data/categories/Mono.yaml @@ -89,6 +89,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 6ce59799..e5906f45 100644 --- a/database/data/categories/Pos.yaml +++ b/database/data/categories/Pos.yaml @@ -56,9 +56,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 a66f3b37..d6f078e7 100644 --- a/database/data/categories/PreOrd.yaml +++ b/database/data/categories/PreOrd.yaml @@ -53,9 +53,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/Top.yaml b/database/data/categories/Top.yaml index 7e4b7519..da8381cb 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 Sierpinski 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 Prop. 4.7 in Adamek-Rosicky. 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 00000000..bc4d6ec0 --- /dev/null +++ b/database/data/categories/omega-Set.yaml @@ -0,0 +1,172 @@ +id: omega-Set +name: category of ω-sets +notation: $\omega{-}\Set$ +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 transformer compatible with $f$: this is a partial recursive function $\varphi : \IN \dashrightarrow \IN$ such that for every $(n,x) \in R_X$, the value $\varphi(n)$ is defined and $(\varphi(n),f(x)) \in R_Y$' +description: >- + The category of $\omega$-sets is mostly useful as a dense subcategory of the effective topos consisting of objects which are simpler to work with. Namely, the effective topos can be constructed as the ex/reg completion of $\omega{-}\Set$. + + 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 full recursive pairing function $\langle {-}, {-} \rangle : \IN^2 \to \IN$ with full 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$.) + + For a few of the properties, we also fix a choice of admissible numbering of the partial recursive functions. We will use the notation that $p \cdot n \downarrow$ if the $p$th partial recursive function is unary $\varphi_p : \IN \dashrightarrow \IN$, $\varphi_p(n)$ exists, and in this case we will write $p \cdot n$ for its value. +nlab_link: https://ncatlab.org/nlab/show/assembly +tags: + - logic + +related: + - Set + +satisfied_properties: + - property: locally small + proof: There is a forgetful functor $\omega{-}\Set \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_{\omega{-}\Set}((X, R_X), (Y, R_Y))$, where we can choose the compatible realizer transformer $\varphi : \IN \dashrightarrow \IN$ to be the full recursive function with constant value $n_0$. Otherwise, if $Y$ is empty, then the unique function $Y \to X$ is a morphism in $\Hom_{\omega{-}\Set}((Y, R_Y), (X, R_X))$, and in fact any partial recursive function $\IN \dashrightarrow \IN$ is a compatible realizer transformer.' + + - 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 $(1, \IN \times 1)$ is terminal. Namely, for any object $(X, R_X)$, the unique function $! : X \to 1$ is a morphism $(X, R_X) \to (1, \IN \times 1)$, since for example any total recursive function $\varphi : \IN \to \IN$ forms a compatible realizer transformer.' + 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 full 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 $\varphi, \psi : \IN \dashrightarrow \IN$ be realizer transformers compatible with $f$ and $g$, respectively. Then $\langle {-}, {-} \rangle \circ (\varphi, \psi)$ is a realizer transformer 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$ be the equalizer of the underlying functions. We then claim that $(E, R_X \cap (\IN \times X'))$ is an equalizer of $f$ and $g$, with the morphism $(E, R_X \cap (\IN \times X')) \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 transformer. 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 transformer compatible with $h$ is also compatible with $\bar h$. From here, it is easy to conclude that $\bar h : (E, R_X \cap X') \to (X, R_X)$ is indeed an equalizer of $f$ and $g$. + 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 $\varphi : \IN \dashrightarrow \IN$ is vacuously a compatible realizer transformer.' + 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 full 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 $\varphi, \psi : \IN \dashrightarrow \IN$ be realizer transformers compatible with $f$ and $g$, respectively. Then there is a unique partial recursive function which sends $2n \mapsto \varphi(n)$ (if the latter exists) and $2n+1 \mapsto \psi(n)$ (if the latter exists), and it forms a realizer transformer compatible with $f+g : X\sqcup Y \to Z$ 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 $Q$ be the coequalizer of the underlying functions with projection $p : Y \twoheadrightarrow Q$. Also, let + $$R_Q \coloneqq ({\id_{\IN}} \times p)_*(R_Y) = \{ (n, p(y)) \mid (n, y) \in R_Y \}.$$ + We claim that $(Q, R_Q)$ is a coequalizer of $f$ and $g$ with $p$ as the projection morphism $(Y, R_Y) \to (Q, R_Q)$. First, the identity function $\IN \to \IN$ is a realizer transformer 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 transformer compatible with $h$ is also compatible with $\bar h$. + + - property: cartesian closed + proof: >- + 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_{\omega{-}\Set}((X, R_X), (Y, R_Y))$. The realization relation will be that $n \in \IN$ realizes $f : (X, R_X) \to (Y, R_Y)$ if and only if $n$ is the code for a unary partial recursive function $\varphi_n : \IN \dashrightarrow \IN$ which is a realizer transformer compatible with $f$. + + In order to check that this is indeed an exponential in $\omega{-}\Set$, we first define the evaluation morphism + $$ev : [(X, R_X), (Y, R_Y)] \times (X, R_X) \to (Y, R_Y), (f, x) \mapsto f(x).$$ + To show that this is in fact a morphism of $\omega$-sets, note that there is a partial recursive function $\varepsilon : \IN \dashrightarrow \IN$ such that $\varepsilon(\langle p, n \rangle)$ exists if and only $p \cdot n \downarrow$, and in this case $\varepsilon(\langle p, n \rangle) = p \cdot n$. This $\varepsilon$ is then a realizer transformer compatible with $ev$. + + Now, suppose we have a morphism $h : (U, R_U) \times (X, R_X) \to (Y, R_Y)$, with compatible realizer transformer $\varphi_h : \IN \dashrightarrow \IN$. We can then curry $\varphi_h$ into a full recursive function $\varphi_h ' : \IN \to \IN$, such that $\varphi_h '(n) \cdot m \downarrow$ if and only if $\varphi_h(\langle n, m \rangle)$ exists, and in that case $\varphi_h '(n) \cdot m = \varphi_h(\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 $\varphi_j(\langle n, {-} \rangle)$ as a compatible realizer transformer; thus, $u \mapsto h(u, {-})$ induces a function $\lambda_h : U \to \Hom_{\omega{-}\Set}((X, R_X), (Y, R_Y))$. Furthermore, $\varphi_h '$ is a compatible realizer transformer for $\lambda_h$, so in fact we get a morphism $\lambda_h : (U, R_U) \to \Hom_{\omega{-}\Set}((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: >- + Suppose we have two morphisms $f : (X, R_X) \to (Z, R_Z)$ and $g : (Y, R_Y) \to (Z, R_Z)$. Let $[X, Y]_Z$ be the relative exponential of $f$ and $g$ in $\Set$, with function $h : [X, Y]_Z \to Z$ coming from $[X, Y]_Z$ being an object of $\Set/Z$. We will then define a realization relation between $\IN$ and $[X, Y]_Z$ such that $\langle n, p \rangle$ realizes $\varphi \in [X, Y]_Z$ if and only if $n$ realizes $h(\varphi) \in Z$, and for every $x\in X$ such that $f(x) = h(\varphi)$ and every $m \in \IN$ such that $m$ realizes $x$, then $p \cdot m \downarrow$ and $p \cdot m$ realizes $\varphi(x) \in Y$. Finally, let $E$ be the subset of $[X, Y]_Z$ consisting of elements which are realized by some $\langle n, p \rangle\in \IN$. We then claim that $E$ with the restriction $R_E$ of the above realization relation forms a relative exponential of $f$ and $g$ in $\omega{-}\Set$. + + First, it is easy to see that the restriction of $h$ to $E$ is a morphism of $\omega$-sets $(E, R_E) \to (Z, R_Z)$, with $p_1 : \IN \to \IN$ working as the partial recursive function in the definition. This is the morphism we will use to consider $(E, R_E)$ as an object of $\omega{-}\Set / (Z, R_Z)$. + + The next step is to define an evaluation morphism $(E, R_E) \times_{(Z, R_Z)} (X, R_X) \to (Y, R_Y)$. Note that from the above descriptions of binary products and equalizers, we can describe the pullback as $E \times_Z X$ with realization relation that $\langle n, m \rangle$ realizes $(e, x) \in E \times_Z X$ if and only if $n$ realizes $e$ and $m$ realizes $x$. We will then define the evaluation map to be the restriction of the set-level evaluation map $[X, Y]_Z \times_Z X \to Y$ to $E \times_Z X \to Y$. The fact that this is a morphism of $\omega$-sets follows from the fact that there is a partial recursive function $\IN \dashrightarrow \IN$ which sends $\langle \langle n', p \rangle, m \rangle$ to $p \cdot m$ if the latter exists. + + Finally, suppose we have a morphism $d : (U, R_U) \to (Z, R_Z)$ and a morphism $j : (U, R_U) \times_{(Z, R_Z)} (X, R_X) \to (Y, R_Y)$ in $\omega{-}\Set / (Z, R_Z)$. Choose realizer transformers $\varphi_d : \IN \dashrightarrow \IN$ and $\varphi_j : \IN \dashrightarrow \IN$ compatible with $d$ and $j$, respectively. Then we can curry $\varphi_j$ into a full recursive function $\varphi_j ' : \IN \to \IN$, such that $\varphi_j '(n) \cdot m \downarrow$ if and only if $\varphi_j(\langle n, m \rangle)$ exists, and in that case $\varphi_j '(n) \cdot m = \varphi_j(\langle n, m \rangle)$. It is now straightforward to check that $n \mapsto \langle \varphi_d(n), \varphi_j'(n) \rangle$ is a partial recursive function, and it shows that the function $\tilde j : U \to [X, Y]_Z$ coming from $[X, Y]_Z$ being a relative exponential in $\Set$ factors through $E$, and it induces a morphism $(U, R_U) \to (E, R_E)$. + + - 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 $\omega{-}\Set \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 $\omega{-}\Set \to \Set$ which is clearly faithful. (For the nontrivial direction of the isomorphism between $\Hom_{\omega{-}\Set}((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 full recursive function given by the constant function with image $n$ forms a realizer transformer 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 not a bijection, 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 \coloneqq \{ f(x_\psi) \}$ 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 transformer. 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 $\varphi : \IN \dashrightarrow \IN$ were a compatible realizer transformer, then we would have that $n_\varphi$ realizes $f(x_{\varphi})\in U$, and therefore $\varphi(n_\varphi)$ exists and $\varphi(n_\varphi)$ realizes $g(f(x_\varphi)) = x_\varphi\in X$, contradicting the choice of $n_\varphi$ and $x_\varphi$. + + 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, so $(U, R_U)$ is isomorphic to a member of the given collection (and in fact structurally isomorphic, not just isomorphic in $\omega{-}\Set$). + + - property: extremal cogenerator + proof: >- + We first claim that $(2, \IN\times 2)$ and $(P(\IN) \setminus \{ \varnothing \}, {\in}_{\IN})$ form an extremal cogenerating collection. To see this, we first consider morphisms to the first member $(2, \IN\times 2)$ of the family. Note that $\Hom_{\omega{-}\Set}({-}, (2, \IN \times 2)) \cong \Hom_{\Set}(U{-}, 2)$, where $U : \omega{-}Set \to \Set$ is the forgetful functor. (For the nontrivial direction of this isomorphism, note that for any function $f : X \to 2$, then we can choose any total recursive function as the compatible realizer transformer, showing that $f$ indeed induces a morphism of $\omega$-sets $(X, R_X) \to (2, \IN \times 2)$.) Therefore, $\Hom_{\omega{-}\Set}({-}, (2, \IN \times 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 $(2, \IN\times 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), (2, \IN\times 2)) \to \Hom((X, R_X), (2, \IN\times 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 transformer). 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 transformer $\varphi_h : \IN \dashrightarrow \IN$. Then for any $x\in X$, if $n$ realizes $f(x)$, then $\varphi_h(n)$ exists and $\varphi_h(n)$ realizes $h(f(x)) = g(x)$. Thus, by definition of $g$, $\varphi_h(n)$ is in the set of realizers of $x$, i.e. $\varphi_h(n)$ realizes $x$. From the characterization of isomorphisms below, this implies that $f$ is an isomorphism. + + Finally, since $(2, \IN\times 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 $\omega{-}\Set$ is semi-strongly connected). Therefore, by this result, the product of these two objects is an extremal cogenerator. + + - property: natural numbers object + proof: >- + We claim that $N \coloneqq (\IN, \Delta_{\IN})$ is a natural numbers object. 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 $a : 1 \to (X, R_X)$ and $g : (X, R_X) \to (X, R_X)$, and choose realizer transformers $\varphi_a : \IN \dashrightarrow \IN$ and $\varphi_g : \IN \dashrightarrow \IN$ compatible with $a$ and $g$, respectively. Then there is a partial recursive function $\psi : \IN \dashrightarrow \IN$ which sends $n$ to $\varphi_g^n(\varphi_a(0))$; and an easy induction shows that in fact this is a full recursive function, and also that $\psi(n) = \varphi_g^n(\varphi_a(0))$ realizes $g^n(a(0))$. Therefore, if we define $\Phi : \IN \to X$, $n \mapsto g^n(a(0))$, then $\Phi$ also induces a morphism of $\omega$-sets $N \to (X, R_X)$ with the required properties. + +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: There is a fully faithful (and therefore conservative) functor $\Set \to \omega{-}\Set$ which sends a set $X$ to $(X, \IN \times X)$. + + - property: locally finite + proof: 'There is a fully faithful functor $\nabla : \Set \to \omega{-}\Set$ which sends a set $X$ to $(X, \IN \times X)$. Therefore, for example, $\Hom_{\omega{-}\Set}(\nabla 1, \nabla \IN) \simeq \Hom_{\Set}(1, \IN)$ is infinite.' + + - property: balanced + proof: 'Define $\nabla \IN \coloneqq (\IN, \IN \times \IN)$ and $N \coloneqq (\IN, \Delta_{\IN})$. Then 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 transformer. 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 transformer $\varphi$, we have that $0$ realizes both $0$ and $1$ in $\nabla \IN$. Therefore, $\varphi(0)$ would have to exist and realize both $0$ and $1$ in $N$, which is impossible. (Alternately, $\Hom_{\omega{-}\Set}(\nabla \IN, \nabla \IN) \simeq \Hom_{\Set}(\IN, \IN)$ is uncountable. On the other hand, it is easy to see that $\Hom_{\omega{-}\Set}(N, N)$ is exactly the full recursive functions, since a compatible realizer transformer would have to agree with the underlying function. Therefore, $\Hom_{\omega{-}\Set}(N, N)$ is countable.)' + check_redundancy: false + + - property: co-Malcev + proof: 'Consider the two possible morphisms $f, g : (1, \IN \times 1) \rightrightarrows (2, \IN \times 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 transformers $\varphi_n : \IN \dashrightarrow \IN$ compatible with $f_n$. It follows that $\varphi_n(m)$ is defined and $\varphi_n(m) = f_n(x)$ for each $n$. Therefore, the image of $g$ is contained in the set of sequences $(\varphi_n(m))_{n\in N}$ where $m \in \IN$ is such that $\varphi_n(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. + +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 $\omega{-}\Set$. + monomorphisms: + description: Morphisms of $\omega$-sets whose underlying set function is injective + proof: This follows from the fact that the forgetful functor $\omega{-}\Set \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, note that $\Hom_{\Set}(X, Z) \cong \Hom_{\omega{-}\Set}((X, E_X), (Z, \IN \times Z))$. Hence, the forgetful functor 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 5803dd83..19c3135f 100644 --- a/database/data/category-implications/congruences.yaml +++ b/database/data/category-implications/congruences.yaml @@ -126,6 +126,34 @@ 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 Example 2.2.18 in Malcev, protomodular, homological and semi-abelian categories. 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: >- + Suppose $p : X+X' \twoheadrightarrow E$ is a cocongruence, with coreflexivity morphism $r : E \to X$ and cotransitivity morphism $t : E \to E +_X E'$. (Here $X'$ is an isomorphic copy of $X$; $E'$ is an isomorphic copy of $E$; and $E +_X E'$ is the coproduct modulo the relations $p(x') = p(x)'$, i.e. it is equivalent to the pushout of $E \xleftarrow{p\circ i_2} X \xrightarrow{p\circ i_1} E$. Since both these morphisms are (split) monomorphisms, the pushout exists by this result.) + + We now claim that we have pullback diagrams + $$\begin{CD} + X @> p \circ i_1 >> E @. \quad @. X' @> p \circ i_2 >> E \\ + @V p \circ i_1 VV @VV t V @. @V p \circ i_2 VV @VV t V \\ + E @> i_1 >> E +_X E' @. \quad @. E' @> i_2 >> E +_X E'. + \end{CD}$$ + For the left diagram, suppose we have generalized elements $e_1, e_2 \in E$ such that $t(e_1) = i_1(e_2) \in E +_X E'$. Then we have two retractions of $t$, $s_1 : E +_X E' \to E$, defined by $e \mapsto p(r(e)), e' \mapsto e'$; and $s_2 : E +_X E' \to E$, defined by $e \mapsto e, e' \mapsto p(r(e)')$. To check for instance that $s_1$ is a retraction, note that $s_1(t(p(x))) = s_1(p(x)) = p(r(p(x)) = p(x)$ and $s_1(t(p(x'))) = s_1(p(x')') = p(x')$ and then use the assumption that $p$ is an epimorphism; the proof for $s_2$ is similar. Therefore, $e_1 = s_1(t(e_1)) = s_1(i_1(e_2)) = p(r(e_2))$. On the other hand, $e_1 = s_2(t(e_1)) = s_2(i_1(e_2)) = e_2$. Therefore, $e_1 = e_2 = p(r(e_2))$, so the generalized element $r(e_2)$ of $X$ maps to $e_1$ and $e_2$ respectively as required. On the other hand, since $p\circ i_1 : X \to E$ is a (split) monomorphism, the uniqueness of the generalized element of $X$ is automatic, completing the proof that the left diagram is a pullback square. The proof for the right diagram is similar. + + Now, using extensivity, we can combine these into a pullback diagram + $$\begin{CD} + X+X' @> p >> E \\ + @VVV @VV t V \\ + E+E' @>>> E +_X E'. + \end{CD}$$ + Since both morphisms $X \to E$ and $X \to E'$ used in the pushout are monomorphisms, by the construction here, the morphism $E+E' \to E +_X E'$ is a regular epimorphism. Therefore, by the assumption that the category is regular, we have that $p$ is in fact a regular epimorphism. + + From here, this proof shows that $E$ is effective. This proof applies since the assumption that the category is epi-regular has only been used to make sure that $p$ is a regular epimorphism. + - id: pretopos_balanced assumptions: - effective congruences diff --git a/database/data/config.yaml b/database/data/config.yaml index 0546f4f5..e51f9001 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 - set theory diff --git a/shared/structure.history.json b/shared/structure.history.json index e4d98386..5e9b8982 100644 --- a/shared/structure.history.json +++ b/shared/structure.history.json @@ -199,5 +199,6 @@ "Set_family_mostly_0": "2026-09-12", "Set_family": "2026-09-13", "DiGraph": "2026-09-14", - "Bin": "2026-09-14" + "Bin": "2026-09-14", + "omega-Set": "2026-09-14" }