Add quasitopos property

content/separated_objects_special_morphisms.md

@@ -0,0 +1,21 @@
+---
+title: Special Morphisms of a Quasitopos of Separated Objects
+description: A classification of the special morphisms in the full subcategory of separated objects for a Lawvere-Tierney topology on a topos
+author: Daniel Schepler
+---
+
+## Special Morphisms of a Quasitopos of Separated Objects
+
+::: Lemma
+Let $\T$ be an elementary topos with a Lawvere-Tierney topology $j$. Then in the full subcategory 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 this subcategory is reflective, where the reflector takes an object $X$ to the quotient 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 the subcategory, 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 the subcategory is reflective. ($\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 = \top_Y \circ f$ as morphisms $Y \to \Omega_j$, so if $f$ is an epimorphism in the subcategory, then we conclude $j \circ \chi_{\im(f)} = \top_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 the subcategory. ($\Leftarrow$) For a $j$-closed subobject $f : X \hookrightarrow Y$, we see that the characteristic morphism in $\T$, $\chi_X : Y \to \Omega$, 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 the subcategory 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 the subcategory. <span class="qed">$\square$</span>

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>.
 

databases/catdat/data/categories/Prost.yaml

@@ -50,9 +50,6 @@ unsatisfied_properties:
   - 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,70 @@
+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)
+
+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: For non-empty $U$, both sides of $X \sqcup \lim_{i\in I} Y_i \to \lim_{i\in I} (X \sqcup Y_i)$ can be calculated component-wise. Therefore, for those $U$, the conclusion follows from the corresponding fact in $\Set$. For $U = \varnothing$, we can see that both sides are empty if and only if $X(\varnothing) = \varnothing$ and $Y_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 2.6.12 and A4.4. Therefore, if $\SepPsh(X)$ had a generator then so would $\Sh(X)$, 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. We then consider the relation $E$ on $X \coloneqq y_U + y_U$ where for $x_1, x_2 \in X(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 X \times X$ is not a regular monomorphism, whereas 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 $X \coloneqq y_{U \cup V}$, which represents the functor of sections over $U \cup V$, and then consider the reflexive relation on such sections $x, y \in F(U \cup V)$ where $x \sim y$ if and only if there exists $z \in F(U\cup V)$ such that $z |_U = x |_U$ and $z |_V = y |_V$. Note that since $F$ 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)$. Thus, we conclude that this corelation is not cosymmetric.
+
+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 (a) <a href="/content/separated_objects_special_morphisms">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 (b) <a href="/content/separated_objects_special_morphisms">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 (c) <a href="/content/separated_objects_special_morphisms">here</a>.
+  regular epimorphisms:
+    description: morphisms of separated presheaves that are surjective on every open set
+    proof: This is a corollary of (d) <a href="/content/separated_objects_special_morphisms">here</a>.

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

@@ -14,6 +14,7 @@ related_categories:
   - Set
   - SetxSet
   - Sh(X,Ab)
+  - SepPsh(X)
 
 comments:
   - It is likely that none of the currently remaining unknown properties (locally ℵ₁-presentable, exact filtered colimits, etc.) are satisfied for a <i>generic</i> space $X$, but we need to make this precise by adding additional requirements to $X$. Maybe we need to create separate entries for specific spaces $X$.

databases/catdat/data/categories/Top.yaml

@@ -72,9 +72,6 @@ unsatisfied_properties:
   - 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.'
 
-  - property: Malcev
-    proof: This is clear since <a href="/category/Set">$\Set$</a> is not Malcev and can be interpreted as the subcategory of discrete spaces.
-
   - property: co-Malcev
     proof: 'See <a href="https://mathoverflow.net/questions/509548" target="_blank">MO/509548</a>. We can also phrase the proof as follows: Consider the forgetful functor $U : \Top \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) \coloneqq \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the singleton and $R$ by the Sierpinski space. It is clear that $R$ is reflexive, but not symmetric.'
 

databases/catdat/data/category-implications/topos.yaml

@@ -32,10 +32,10 @@
 
 - id: topos_implies_coregular
   assumptions:
-    - elementary topos
+    - quasitopos
   conclusions:
     - coregular
-  proof: This is proven in <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, A2.6.3 (for every quasitopos).
+  proof: This is proven in <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, A2.6.3.
   is_equivalence: false
 
 - id: grothendieck_topos_definition
@@ -70,12 +70,13 @@
 
 - id: topos_no_stable_epis
   assumptions:
-    - elementary topos
+    - quasitopos
     - cofiltered-limit-stable epimorphisms
     - countable coproducts
   conclusions:
-    - trivial
-  proof: Let $N \coloneqq \coprod_{m \in \IN} 1$ and consider for every $n \in \IN$ the subobject $N_{\geq n} = \coprod_{m \geq n} 1$ of $N$. For $n \leq n'$ we have $N_{\geq n'} \subseteq N_{\geq n}$. There is a (unique, split) epimorphism $N_{\geq n} \to 1$ for every $n$. By assumption, their limit $\lim_n N_{\geq n} \to 1$ is also an epimorphism. But $\lim_n N_{\geq n} = \bigcap_{n} N_{\geq n} = 0$. Thus, $0 \to 1$ is an epimorphism. It must be a regular epimorphism, but $0$ is strict initial, so that $0 \to 1$ is an isomorphism. Hence, $X \cong X \times 1 \cong X \times 0 \cong 0$ for all $X$.
+    - thin
+  proof: >-
+    Let $N \coloneqq \coprod_{m \in \IN} 1$ and consider for every $n \in \IN$ the subobject $N_{\geq n} = \coprod_{m \geq n} 1$ of $N$. For $n \leq n'$ we have $N_{\geq n'} \subseteq N_{\geq n}$. There is a (unique, split) epimorphism $N_{\geq n} \to 1$ for every $n$. By assumption, their limit $\lim_n N_{\geq n} \to 1$ is also an epimorphism. But $0 \to \lim_n N_{\geq n}$ is also an epimorphism since any morphism $N_{\geq n} \to X$ factors through one of the coprojections $i_{n'} : 1 \to N_{\geq n}$ and therefore does not extend to a map $N_{\geq n'+1} \to X$. Thus, $0 \to 1$ is an epimorphism. It follows that for any parallel pair $f, g : X \rightrightarrows Y$, the characteristic morphism of the equalizer is equal to $\top \circ {!}_X$ so that $f = g$.
   is_equivalence: false
 
 - id: pretopos_definition
@@ -86,3 +87,53 @@
     - extensive
   proof: This is true by definition.
   is_equivalence: true
+
+- id: quasitopos_definition
+  assumptions:
+    - quasitopos
+  conclusions:
+    - finitely complete
+    - finitely cocomplete
+    - locally cartesian closed
+    - regular subobject classifier
+  proof: This is true by definition.
+  is_equivalence: true
+
+- id: balanced_quasitopos_is_topos
+  assumptions:
+    - quasitopos
+    - balanced
+  conclusions:
+    - elementary topos
+  proof: This is proven in <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, A2.6.3.
+  is_equivalence: false
+
+- id: Giraud_for_quasitopos
+  assumptions:
+    - Grothendieck quasitopos
+  conclusions:
+    - quasitopos
+    - locally presentable
+  proof: See <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, C2.2.13.
+  is_equivalence: true
+
+- id: Malcev_quasitopos_is_thin
+  assumptions:
+    - regular subobject classifier
+    - Malcev
+  conclusions:
+    - thin
+  proof: 'By a proof similar to <a href="/category-implication/subobject_classifier_disallows_malcev">this</a> we conclude that every regular monomorphism is an isomorphism. Applying this to the equalizer of any parallel pair $f, g : X \rightrightarrows Y$, we conclude that $f = g$.'
+  is_equivalence: false
+
+- id: Grothendieck_quasitopos_consequences
+  assumptions:
+    - Grothendieck quasitopos
+  conclusions:
+    - exact filtered colimits
+    - cogenerator
+  proof: >-
+    In order to calculate colimits in $\BiSep(\C, J, K)$, we can first calculate the colimit in the Grothendieck topos $\Sh(\C, J)$, and then take the presheaf quotient of the $K$-closure of the diagonal relation. (Note that since this closure is also a $J$-closed congruence on a $J$-sheaf, its presheaf quotient is still in $\Sh(\C, J)$.) We already know that filtered colimits in $\Sh(\C, J)$ commute with finite limits, and similarly the $K$-separated quotient functor commuts with finite limits. We conclude that filtered colimits in $\BiSep(\C, J, K)$ also commute with finite limits.
+
+    As for having a cogenerator: we have that $\Sh(\C, K)$ is a reflective subcategory of $\BiSep(\C, J, K)$, and the unit of the reflection adjunction is a monomorphism. It follows that the reflector is faithful, and thus that a cogenerator of $\Sh(\C, K)$ is also a cogenerator of $\BiSep(\C, J, K)$.
+  is_equivalence: false

databases/catdat/data/category-properties/Grothendieck quasitopos.yaml

@@ -0,0 +1,10 @@
+id: Grothendieck quasitopos
+relation: is a
+description: Given a small category $\C$ with a pair of Grothendieck topologies $J \subseteq K$, we define $\BiSep(\C, J, K)$ to be the full subcategory of presheaves on $\C$ which are both a sheaf for the $J$ topology and also separated for the $K$ topology. A <i>Grothendieck quasitopos</i> is a category which is equivalent to $\BiSep(\C, J, K)$ for some $\C, J, K$. Equivalently, a category is a Grothendieck quasitopos if and only if it is equivalent to the full subcategory of separated objects for a Lawvere-Tierney topology on a Grothendieck topos.
+nlab_link: https://ncatlab.org/nlab/show/quasitopos
+invariant_under_equivalences: true
+
+related_properties:
+  - quasitopos
+  - Grothendieck topos
+  - locally presentable

databases/catdat/data/category-properties/Grothendieck topos.yaml

@@ -6,3 +6,4 @@ invariant_under_equivalences: true
 
 related_properties:
   - elementary topos
+  - Grothendieck quasitopos

databases/catdat/data/category-properties/elementary topos.yaml

@@ -11,3 +11,4 @@ related_properties:
   - natural numbers object
   - subobject classifier
   - pretopos
+  - quasitopos

databases/catdat/data/category-properties/quasitopos.yaml

@@ -0,0 +1,17 @@
+id: quasitopos
+relation: is a
+description: >-
+  A <i>quasitopos</i> is a category which is finitely complete, finitely cocomplete, locally cartesian closed, and has a regular subobject classifier. This gives the category properties similar to those of an elementary topos; a major difference is that a quasitopos need not be balanced.
+
+  Note that some authors use a strong subobject classifier in place of a regular subobject classifier in the definition, i.e. a morphism $\top : 1 \to \Omega$ which classifies strong monomorphisms. For the equivalence of these definitions, see <a href="https://math.stackexchange.com/q/4335533" target="_blank">MSE/4335533</a>.
+nlab_link: https://ncatlab.org/nlab/show/quasitopos
+invariant_under_equivalences: true
+
+related_properties:
+  - finitely complete
+  - finitely cocomplete
+  - locally cartesian closed
+  - regular subobject classifier
+  - elementary topos
+  - Grothendieck quasitopos
+  - balanced

databases/catdat/data/category-properties/regular subobject classifier.yaml

@@ -12,3 +12,4 @@ invariant_under_equivalences: true
 related_properties:
   - finitely complete
   - subobject classifier
+  - quasitopos