Add quasitopos property

content/separated_objects_quasitopos.md

@@ -0,0 +1,41 @@
+---
+title: Quasitopoi of Separated Objects
+description: Some results concerning the full subcategory of separated objects for a Lawvere-Tierney topology on a topos
+author: Daniel Schepler
+---
+
+## Results Concerning Quasitopoi of Separated Objects
+
+Let $\T$ be an elementary topos with a <a href="https://ncatlab.org/nlab/show/Lawvere-Tierney+topology" target="_blank">Lawvere-Tierney topology</a> $j$. Recall that by definition, a subobject $V \hookrightarrow U$ is $j$-dense if $\cl_{j,U}(V) = U$, and it is $j$-closed if $\cl_{j,U}(V) = V$. Also, an object $X$ is $j$-separated if for each $j$-dense subobject $V \hookrightarrow U$, the composition function $\Hom(U, X) \to \Hom(V, X)$ is injective; or equivalently, if the diagonal subobject $\Delta_X : X \hookrightarrow X \times X$ is $j$-closed. In terms of the internal language of a topos, this last condition is equivalent to $1 \models \forall x, y : X, j(x=y) \rightarrow x=y$.
+
+### Reflective Subcategory
+
+::: Lemma 1
+Let $\T$ be an elementary topos with a <a href="https://ncatlab.org/nlab/show/Lawvere-Tierney+topology" target="_blank">Lawvere-Tierney topology</a> $j$. Then for each object $X$ of $\T$, $\cl_{j,X\times X}(\Delta_X)$ is a congruence whose quotient $X_{\sep}$ is $j$-separated. Moreover, this operation forms a reflector functor making the full subcategory $\Sep(j)$ of $j$-separated objects a reflective category; and this reflector functor preserves finite products and monomorphisms.
+:::
+
+_Proof._ For generalized elements $x, y \in X(U)$, we see that $(x, y) \in \cl_{j,X\times X}(\Delta_X)$ if and only if $U \models j(x=y)$. This makes it easy to show the closure of the diagonal is a congruence: for reflexivity, we certainly have $U \models x=x$ and $(x=x) \le j(x=x)$. For symmetry, if $U \models j(x=y)$, then $(x=y) = (y=x)$, so $j(x=y) = j(y=x)$ and $U \models j(y=x)$ also. For transitivity, suppose $U \models j(x=y)$ and $U \models j(y=z)$. Then $U \models j(x=y) \land j(y=z)$, whereas $j(x=y) \land j(y=z) = j(x=y \land y=z)$. Also, $(x=y \land y=z) \le (x=z)$, so $j(x=y \land y=z) \le j(x=z)$, implying that $U \models j(x=z)$.
+
+To see the quotient is separated, suppose we have generalized elements $\bar x, \bar y \in X_{sep}(U)$ such that $U \models j(\bar x = \bar y)$. Then since the quotient morphism $p : X \to X_{sep}$ is an epimorphism, there exists an epimorphism $\alpha : U' \to U$ and generalized elements $x, y \in X(U')$ such that $p(x) = \alpha^* \bar x$ and $p(y) = \alpha^* \bar y$. Since the quotient is effective, we have $\alpha^*(\bar x = \bar y) = (p(x) = p(y)) = j(x=y)$. Therefore, $\top = \alpha^*(j(\bar x = \bar y)) = j(\alpha^*(\bar x = \bar y)) = j(j(x=y)) = j(x=y)$, implying that $\alpha^*(\bar x = \bar y) = \top$. Since $\alpha$ is an epimorphism, that implies $\bar x = \bar y$. We have thus established that $1 \models \forall \bar x, \bar y : X_{\sep}, j(\bar x=\bar y) \rightarrow \bar x = \bar y$.
+
+To see this forms a left adjoint to the forgetful functor $\Sep(j) \to \T$, suppose we have a morphism $f : X \to Y$ in $\T$ with $Y$ $j$-separated. Then $f$ factors through the projection morphism $p_X : X \to X_{\sep}$ if and only if $1 \models \forall x_1, x_2 : X, j(x_1 = x_2) \rightarrow f(x_1) = f(x_2)$. However, for generalized elements $x_1, x_2 \in X(U)$, we certainly have $(x_1 = x_2) \le (f(x_1) = f(x_2)$, so $j(x_1 = x_2) \le j(f(x_1) = f(x_2)) \le (f(x_1) = f(x_2))$ by the assumption that $Y$ is $j$-separated. We thus see $f$ does factor through the projection morphism $p_X : X \to X_{\sep}$, and the uniqueness of the factor $X_{\sep} \to Y$ is automatic since $p_X$ is an epimorphism. This implies that there is a unique functor extension of $X \mapsto X_{\sep}$ which forms a left adjoint, with the projection morphisms $p_X : X \to X_{\sep}$ serving as the unit of the adjunction.
+
+To see that the reflector preserves monomorphisms, suppose we have a monomorphism $f : X \to Y$. Now, suppose we have two generalized elements $\bar x_1, \bar x_2 \in X_{\sep}(U)$ such that $f_{\sep}(\bar x_1) = f_{\sep}(\bar x_2)$ in $Y_{\sep}(U)$. Since $X \to X_{\sep}$ is an epimorphism, there exists an epimorphism $\alpha : U' \to U$ and $x_1, x_2 \in X(U')$ such that $\alpha^* \bar x_i = p_X(x_i)$, $i=1,2$. Then since $f_{\sep}(\alpha^* \bar x_1) = f_{\sep}(\alpha^* \bar x_2)$, we have $p_Y(f(x_1)) = p_Y(f(x_2))$. It follows that $U' \models j(f(x_1) = f(x_2))$. However, since $f$ is a monomorphism, $(f(x_1) = f(x_2)) \le (x_1 = x_2)$, so $j(f(x_1) = f(x_2)) \le j(x_1 = x_2)$, so $U' \models j(x_1 = x_2)$ also. Therefore, $p_X(x_1) = p_X(x_2)$, so $\alpha^* \bar x_1 = \alpha^* \bar x_2$. Since $\alpha$ is an epimorphism, this implies $\bar x_1 = \bar x_2$.
+
+Finally, to see that the reflector preserves finite products, suppose we have objects $X_1, \ldots, X_n$ of $\T$. Then we have an epimorphism $\prod_{i=1}^n X_i \to \prod_{i=1}^n (X_i)_{\sep}$. In order to show the reflector preserves this finite product, it suffices to show the kernel pair of this epimorphism agrees with the $j$-closure of the diagonal on $\prod_{i=1}^n X_i$. That kernel pair is precisely the relation of pairs $(x = (x_1, \ldots, x_n), x' = (x_1', \ldots, x_n'))$ such that $\bigwedge_{i=1}^n j(x_i = x_i')$. However, since $j(\top) = \top$ and $j(p \land q) = j(p) \land j(q)$, we see $j$ preserves finite conjunctions, so this is equivalent to $j \left( \bigwedge_{i=1}^n (x_i = x_i') \right) = j(x = x')$, as required. <span class="qed">$\square$</span>
+
+### Special Morphisms
+
+::: Lemma 2
+Let $\T$ be an elementary topos with a <a href="https://ncatlab.org/nlab/show/Lawvere-Tierney+topology" target="_blank">Lawvere-Tierney topology</a> $j$. Then in the full subcategory $\Sep(j)$ of $j$-separated objects:<br>
+(a) The monomorphisms are the morphisms whose image in $\T$ are monomorphisms.<br>
+(b) The epimorphisms are the morphisms whose image in $\T$ are $j$-dominant (i.e. the image calculated in $\T$ is a $j$-dense subobject of the codomain).<br>
+(c) The regular monomorphisms are the morphisms whose image in $\T$ are $j$-closed monomorphisms.<br>
+(d) The regular epimorphisms are the morphisms whose image in $\T$ are epimorphisms.
+:::
+
+_Proof._ By the above, $\Sep(j)$ is a reflective subcategory of $\T$, where the reflector takes an object $X$ to the quotient $X_{\sep}$ of $X$ by the congruence defined by the $j$-closure of the diagonal in $X\times X$. Also recall that the equalizer of $j, \id : \Omega_\T \rightrightarrows \Omega_\T$ is a $j$-separated object $\Omega_j$ which serves as the regular subobject classifier in $\Sep(j)$, and since $j$ is idempotent, this can also be described as the image (in $\T$) of $j$.<br>
+(a) ($\Rightarrow$) This follows from the fact that $\Sep(j)$ is a reflective subcategory of $\T$. ($\Leftarrow$) This is trivial for any subcategory.<br>
+(b) ($\Rightarrow$) Given a morphism $f : X \to Y$, form the image $\im(f)$ in $\T$, which corresponds to a morphism $\chi_{\im(f)} : Y \to \Omega_\T$. Then $j \circ \chi_{\im(f)} \circ f = j\circ \top_X = \top_X = \top_Y \circ f$ as morphisms $Y \to \Omega_j$, so if $f$ is an epimorphism in $\Sep(j)$, then we conclude $j \circ \chi_{\im(f)} = \top_Y$. However, $j \circ \chi_{\im(f)} : Y \to \Omega_j \hookrightarrow \Omega$ is the characteristic morphism of the $j$-closure of $\im(f)$, so we conclude that $j$-closure is all of $Y$. ($\Leftarrow$) Given a morphism $f : X \to Y$ of $j$-separated objects whose image in $\T$ is $j$-dense, suppose we have two morphisms $g, h : Y \rightrightarrows Z$ with $g \circ f = h \circ f$. Then since $Z$ is $j$-separated, the equalizer of $g$ and $h$ is $j$-closed; it also contains the image of $f$ and thus is $j$-dense. We conclude that the equalizer is all of $Y$.<br>
+(c) ($\Rightarrow$) Any equalizer in $\T$ of $f, g : X \rightrightarrows Y$ with $Y$ $j$-separated is a $j$-closed subobject of $X$. If $X$ is $j$-separated as well, then that equalizer subobject is automatically separated, and agrees with the equalizer in $\Sep(j)$. ($\Leftarrow$) For a $j$-closed subobject $f : X \hookrightarrow Y$, we see that the characteristic morphism in $\T$, $\chi_X : Y \to \Omega_\T$, factors through $\Omega_j$. Now $X$ is the equalizer of $\chi_X, \top : Y \rightrightarrows \Omega_j$.<br>
+(d) ($\Rightarrow$) We can calculate the coequalizer of $f, g : X \rightrightarrows Y$ in $\Sep(j)$ by taking the coequalizer $Z$ in $\T$ and then applying the reflector to get $Z_{sep}$. We see that both $Y \to Z$ and $Z \to Z_{sep}$ are epimorphisms in $\T$. ($\Leftarrow$) Suppose $f : X \to Y$ is an epimorphism in $\T$ of $j$-separated objects. Then the subcategory inclusion functor preserves the kernel pair $X \times_Y X \rightrightarrows X$, and since $f$ is a regular epimorphism in $\T$, this kernel pair has coequalizer $f : X \to Y$ in $\T$. Since $Y$ was already $j$-separated, the kernel pair also has coequalizer $f : X \to Y$ in $\Sep(j)$. <span class="qed">$\square$</span>

databases/catdat/data/categories/Cat.yaml

@@ -43,9 +43,6 @@ unsatisfied_properties:
   - property: cogenerating set
     proof: 'Assume that $S$ is a cogenerating set in $\Cat$. Then one checks that the set of monoids $\{\End(X) : X \in \C \in S\}$ is a cogenerating set in <a href="/category/Mon">$\Mon$</a>, which we know does not exist.'
 
-  - 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 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.'
 

databases/catdat/data/categories/LRS_R.yaml

@@ -62,6 +62,7 @@ unsatisfied_properties:
 
   - property: regular
     proof: This is Corollary 4(c) <a href="/content/Top-embeds-in-LRS">here</a>.
+    check_redundancy: false
 
   - property: cofiltered-limit-stable epimorphisms
     proof: This is Corollary 4(d) <a href="/content/Top-embeds-in-LRS">here</a>.

databases/catdat/data/categories/Meas.yaml

@@ -56,9 +56,6 @@ unsatisfied_properties:
   - property: balanced
     proof: Take a set $X$ with two different $\sigma$-algebras $\A \subset \B$ (for example, $\A = \{\varnothing,X\}$ and $\B = P(X)$ when $X$ has at least $2$ elements), then the identity map $(X,\B) \to (X,\A)$ provides a counterexample.
 
-  - property: Malcev
-    proof: Use that <a href="/category/Set">$\Set$</a> is not Malcev and endow sets with the trivial $\sigma$-algebra.
-
   - property: cartesian filtered colimits
     proof: See <a href="https://math.stackexchange.com/questions/5027218" target="_blank">MSE/5027218</a>.
 
@@ -68,9 +65,6 @@ unsatisfied_properties:
   - property: effective cocongruences
     proof: 'The proof is similar to the one for <a href="/category/Top">$\Top$</a>: Use the trivial $\sigma$-algebra on a two-point set.'
 
-  - property: regular
-    proof: A proof can be found <a href="/content/Meas_not_regular">here</a>.
-
 special_objects:
   initial object:
     description: empty set with the unique $\sigma$-algebra

databases/catdat/data/categories/Met_oo.yaml

@@ -60,9 +60,6 @@ unsatisfied_properties:
   - property: effective cocongruences
     proof: The same counterexample as for <a href="/category/Met">$\Met$</a> works here. The difference in this case is that a binary copower of two copies of $(0,1)$ does exist in $\Met_\infty$. However, this would assign a distance of $\infty$ between points in $(-1,0)$ and points in $(0,1)$, which does not agree with the chosen subspace metric on $(-1,0) \cup (0,1)$.
 
-  - property: regular
-    proof: We can take the same counterexample as for <a href="/category/PMet">$\PMet$</a>.
-
 special_objects:
   initial object:
     description: empty metric space

databases/catdat/data/categories/Pos.yaml

@@ -45,9 +45,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$.'
 

databases/catdat/data/categories/Prost.yaml

@@ -41,18 +41,12 @@ satisfied_properties:
     proof: The set $\{0,1\}$ with the chaotic preorder $(0 \leq 1$, $1 \leq 0)$ is a regular subobject classifier since order-preserving maps $P \to \{0,1\}$ correspond to subsets of $P$.
 
 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: 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: skeletal
     proof: This is trivial.
 
-  - property: Malcev
-    proof: 'Consider the subproset $\{(a,b) : a \leq b \}$ of $\IN^2$.'
-
   - property: co-Malcev
     proof: 'See <a href="https://mathoverflow.net/questions/509552">MO/509552</a>: Consider the forgetful functor $U : \Prost \to \Set$ and the relation $R \subseteq U^2$ defined by $R(A) \coloneqq \{(a,b) \in U(A)^2 : a \leq b\}$. Both are representable: $U$ by the singleton preordered set and $R$ by $\{0 \leq 1 \}$. It is clear that $R$ is reflexive, but not symmetric.'
 

databases/catdat/data/categories/Rng.yaml

@@ -55,9 +55,6 @@ unsatisfied_properties:
   - property: CSP
     proof: Assume that $\coprod_n \IZ \to \prod_n \IZ$ is an epimorphism in $\Rng$. Then $((\coprod_n \IZ)^+)^{\ab} \to \prod_n \IZ$ would be an epimorphism in $\CRing$, where $(-)^+$ denotes the unitalization and $(-)^{\ab}$ the abelianization. But if $R \to S$ is an epimorphism of commutative rings, then $\card(S) \leq \card(R)$ by <a href="https://stacks.math.columbia.edu/tag/04W0" target="_blank">SP/04W0</a>. Since $((\coprod_n \IZ)^+)^{\ab}$ is countable and $\prod_n \IZ$ is not, we get a contradiction.
 
-  - property: regular subobject classifier
-    proof: 'Assume that $\Rng$ has a subobject classifier $\Omega$. Since $0$ is a zero object, every regular subobject $R \subseteq S$ would be the kernel of some homomorphism $S \to \Omega$. In particular, it would be an ideal. Now take any pair of homomorphisms $f,g : S \rightrightarrows T$ in $\Ring$. Their equalizer $R \subseteq S$ is also the equalizer in $\Rng$, and it contains $1 \in S$. If it was an ideal, then $R = S$, and hence $f = g$, which is absurd.'
-
   - property: coregular
     proof: 'We can copy the proof for <a href="/category/Ring">$\Ring$</a>. In short, the inclusion of diagonal matrices $\IQ^2 \hookrightarrow M_2(\IQ)$ is a regular monomorphism, but becomes zero after taking the pushout with $p_1 : \IQ^2 \twoheadrightarrow \IQ$ because $M_2(\IQ)$ is simple.'