Add category of ω-sets

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 <a href="/category/Set">$\Set$</a>, 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.
-
-      <strong>Case 1.</strong> 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).$$
-      <strong>Case 2.</strong> We have $p = i_2(x)$ and $q = i_2(x')$. This is symmetric to Case 1.
-
-      <strong>Case 3.</strong> 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.
-
-      <strong>Case 4.</strong> 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.

database/data/categories/Cat.yaml

@@ -45,9 +45,6 @@ unsatisfied_properties:
   - property: balanced
     proof: Since we know that <a href="/category/Mon">$\Mon$</a> 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 <a href="https://ncatlab.org/nlab/show/regular+category" target="_blank">nLab</a>.
-
   - property: coregular
     proof: 'We already know that <a href="/category/Mon">$\Mon$</a> 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 (<a href="https://math.stackexchange.com/questions/574745" target="_blank">MSE/574745</a>), hence it preserves regular monomorphisms. It also preserves pushouts (<a href="https://math.stackexchange.com/questions/5130854" target="_blank">MSE/5130854</a>), 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:

database/data/categories/LRS_R.yaml

@@ -88,9 +88,6 @@ unsatisfied_properties:
   - property: cartesian filtered colimits
     proof: This is Corollary 4(b) <a href="/content/Top-embeds-in-LRS">here</a>.
 
-  - property: regular
-    proof: This is Corollary 4(c) <a href="/content/Top-embeds-in-LRS">here</a>.
-
   - property: cofiltered-limit-stable epimorphisms
     proof: This is Corollary 4(d) <a href="/content/Top-embeds-in-LRS">here</a>.
 

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 <a href="https://ncatlab.org/nlab/show/regular+epimorphism">nLab</a>), 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 <a href="https://link.springer.com/book/10.1007/978-3-540-34514-5" target="_blank">Measure theory</a> $\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 <a href="/category/Top">$\Top$</a>. 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$.

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 <a href="/category/PMet">$\PMet$</a>.
-    references:
-      - pmet_not_regular
-
   - property: regular subobject classifier
     proof: The same proof as for <a href="/category/Met">$\Met$</a> works.
     references:

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

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 <a href="https://ncatlab.org/nlab/show/regular+category" target="_blank">nLab</a>.
-
   - property: Malcev
     proof: 'Consider the subposet $\{(a,b) : a \leq b \}$ of $\IN^2$.'
 

database/data/categories/PreOrd.yaml

@@ -53,9 +53,6 @@ satisfied_properties:
       Finally, by <a href="/content/generator_construction">this result</a>, 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 <a href="https://ncatlab.org/nlab/show/regular+category" target="_blank">nLab</a>.
-
   - property: skeletal
     proof: This is trivial.
 

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 <a href="https://math.stackexchange.com/questions/1255678" target="_blank">MSE/1255678</a>.'
 
-  - property: regular
-    proof: See Example 3.14 at the <a href="https://ncatlab.org/nlab/show/regular+category" target="_blank">nLab</a>.
-
   - 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 <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>. However, since <a href="/category/Set">$\Set$</a> is not coaccessible, this is a contradiction.'
     label: top_not_coaccessible