Add quasitopos property

content/separated_objects_quasitopos.md

@@ -0,0 +1,23 @@
+---
+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
+
+### Special Morphisms
+
+::: 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 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._ Recall that $\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.'
 

databases/catdat/data/categories/SepPsh(X).yaml

@@ -0,0 +1,77 @@
+id: SepPsh(X)
+name: category of separated presheaves
+notation: $\SepPsh(X)$
+objects: separated presheaves of sets on a topological space $X$
+morphisms: morphisms of presheaves
+description: Here, we assume that the topological space $X$ is such that there is a non-empty family of open subsets whose union is not in the family, since otherwise this category is almost the category of all presheaves. For a few of the properties, we will strengthen this assumption to the assumption that there are two open subsets $U, V$ such that neither is contained in the other.
+nlab_link: https://ncatlab.org/nlab/show/separated+presheaf
+
+tags:
+  - algebraic geometry
+  - topology
+
+related_categories:
+  - Sh(X)
+  - Set
+
+satisfied_properties:
+  - property: locally small
+    proof: This is easy.
+
+  - property: Grothendieck quasitopos
+    proof: It is equivalent to $\BiSep(\Open(X), J, K)$ where $J$ is the trivial Grothendieck topology and $K$ is the open covering topology.
+
+  - property: cocartesian cofiltered limits
+    proof: 'Let $c : \F \sqcup \lim_{i\in I} \G_i \to \lim_{i\in I} (\F \sqcup \G_i)$ be the comparison map. Using the description of coproducts below, we see that for non-empty $U$, both sides of $c(U)$ can be calculated component-wise. Therefore, for those $U$, the conclusion follows from the corresponding fact in <a href="/category/Set">$\Set$</a>. For $U = \varnothing$, we can see that both sides of $c(\varnothing)$ are empty if and only if $\F(\varnothing) = \varnothing$ and $\G_i(\varnothing) = \varnothing$ for some $i$, and otherwise both sides are a singleton.'
+
+unsatisfied_properties:
+  - property: skeletal
+    proof: Consider the constant presheaves for two non-equal singleton sets.
+
+  - property: disjoint finite coproducts
+    proof: The equalizer of the two coprojections $1 \rightrightarrows 1 + 1$ has value $1$ at $\varnothing$.
+
+  - property: generator
+    proof: 'The subcategory $\Sh(X)$ of $\SepPsh(X)$ is reflective by <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a> Prop A.2.6.12 and A.4.4.4. Therefore, if $\SepPsh(X)$ had a generator then so would <a href="/category/Sh(X)">$\Sh(X)$</a>, which we know is not the case.'
+
+  - property: effective congruences
+    proof: >-
+      Let $\{ U_i : i \in I \}$ be a non-empty family of open sets whose union $U$ is not in the family. In particular, this implies $U \ne \varnothing$. We then consider the relation $\E$ on $\F \coloneqq y_U + y_U '$ where for $x_1, x_2 \in \F(V)$, $(x_1, x_2) \in \E(V)$ if and only if either $x_1 = x_2$ or $V \subseteq U_i$ for some $i \in I$. It is easy to see that $\E$ is a congruence. However, $\E \hookrightarrow \F \times \F$ is not a regular monomorphism: to see this, use the description of regular monomorphisms below, and observe that $(\id_U, \id_U ') \notin \E(U)$ but its restriction is in $\E(U_i)$ for each $i$. On the other hand, any effective congruence would necessarily be an equalizer.
+
+  - property: semi-strongly connected
+    proof: Let $U$ and $V$ be two open subsets such that neither is contained in the other. Then there is neither a morphism $y_U \to y_V$ nor a morphism $y_V \to y_U$.
+
+  - property: co-Malcev
+    proof: >-
+      Let $U$ and $V$ be two open subsets such that neither is contained in the other. We will let $\F \coloneqq y_{U \cup V}$, which represents the functor of sections over $U \cup V$, and then consider the reflexive relation on such sections $a, b \in \G(U \cup V)$ where $a \sim b$ if and only if there exists $c \in \G(U\cup V)$ such that $c |_U = a |_U$ and $c |_V = b |_V$. Note that since $\G$ is separated, such a $z$ is unique if it exists. From this, we can see that this relation is representable by the colimit of a diagram where the objects are $y_U$, $y_V$, and three copies of $y_{U\cup V}$, and the morphisms are canonical morphisms from $y_U$ to the first and third copies of $y_{U\cup V}$ and canonical morphisms from $y_V$ to the second and third copies of $y_{U\cup V}$. In fact, we can see that the presheaf colimit is separated, so this presheaf colimit is also the colimit in $\SepPsh(X)$.
+
+      For a more concrete description of the presheaf colimit $\E$, if $W \not\subseteq U\cup V$, then $\E(W) = \varnothing$. If $W \subseteq U\cup V$ but $W \not\subseteq U$ and $W \not\subseteq V$, then $\E(W) \simeq \{ a_W, b_W, c_W \}$. If $W \subseteq U$ but $W \not\subseteq V$, then $\E(W) \simeq \{ a_W = c_W, b_W \}$; similarly, if $W \subseteq V$ but $W \not\subseteq U$, then $\E(W) \simeq \{ a_W, b_W = c_W \}$. Finally, if $W \subseteq U \cap V$, then $\E(W) \simeq \{ a_W = b_W = c_W \}$. The restriction maps of $\E$ are induced by $a_W \mapsto a_{W'}, b_W \mapsto b_{W'}, c_W \mapsto c_{W'}$.
+
+      Now if $\E$ were cosymmetric, with cosymmetry morphism $s : \E \to \E$, then $c' \coloneqq s(c_{U\cup V}) \in \E(U\cup V)$ would have to satisfy $c' |_U = s(c_{U\cup V} |_U) = s(a_U) = b_U$ and $c' |_V = s(c_{U\cup V} |_V) = s(b_V) = a_V$. However, none of $a_{U\cup V}, b_{U\cup V}, c_{U\cup V}$ satisfies these conditions.
+
+special_objects:
+  initial object:
+    description: empty presheaf sending every open set to $\varnothing$
+  terminal object:
+    description: constant presheaf with value a singleton
+  coproducts:
+    description: take the section-wise disjoint union, and then collapse the value at $\varnothing$ to a singleton if it is non-empty
+  products:
+    description: section-wise defined direct product
+
+special_morphisms:
+  isomorphisms:
+    description: morphisms of separated presheaves that are bijective on every open set
+    proof: This is easy.
+  monomorphisms:
+    description: morphisms of separated presheaves that are injective on every open set
+    proof: This is a corollary of Lemma 1(a) <a href="/content/separated_objects_quasitopos">here</a>.
+  epimorphisms:
+    description: 'morphisms of separated presheaves $\varphi : \F \to \G$ which are "locally surjective": for every local section $g \in \G(U)$ there is an open covering $\bigcup_{i\in I} U_i = U$ such that each $g|_{U_i} \in \G(U_i)$ is contained in the image of $\varphi(U_i) : \F(U_i) \to \G(U_i)$'
+    proof: This is a corollary of Lemma 1(b) <a href="/content/separated_objects_quasitopos">here</a>.
+  regular monomorphisms:
+    description: 'morphisms of separated presheaves $\varphi : \F \hookrightarrow \G$ that are injective on every open set, and such that "every section of $\G$ which is locally in $\F$ is itself in $\F$": if a local section $g \in \G(U)$ has an open covering $\bigcup_{i\in I} U_i = U$ such that each $g|_{U_i} \in \G(U_i)$ is contained in the image of $\varphi(U_i) : \F(U_i) \to \G(U_i)$, then $g$ is contained in the image of $\varphi(U) : \F(U) \to \G(U)$'
+    proof: This is a corollary of Lemma 1(c) <a href="/content/separated_objects_quasitopos">here</a>.
+  regular epimorphisms:
+    description: morphisms of separated presheaves that are surjective on every open set
+    proof: This is a corollary of Lemma 1(d) <a href="/content/separated_objects_quasitopos">here</a>.