Add quasitopos property

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,64 @@
+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.
+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.'
+
+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: ...
+  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: ...
+  regular monomorphisms:
+    description: 'morphisms of separated presheaves $\varphi : F \hookrightarrow G$ that are injective on every open set, and such that 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: ...
+  regular epimorphisms:
+    description: morphisms of separated presheaves that are surjective on every open set
+    proof: ...

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,49 @@
     - 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
+  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.
+  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)$ so 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 is 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

databases/catdat/data/macros.yaml

@@ -61,6 +61,7 @@
 \cod: \operatorname{cod}
 \rank: \operatorname{rank}
 \Gal: \operatorname{Gal}
+\Open: \operatorname{Open}
 
 # categories
 \Set: \mathbf{Set}
@@ -118,3 +119,5 @@
 \Isom: \mathbf{Isom}
 \Pair: \mathbf{Pair}
 \Span: \mathbf{Span}
+\BiSep: \mathbf{BiSep}
+\SepPsh: \mathbf{SepPsh}

databases/catdat/scripts/expected-data/Ab.json

@@ -169,5 +169,7 @@
 	"subobject-trivial": false,
 	"quotient-trivial": false,
 	"locally finite": false,
-	"pretopos": false
+	"pretopos": false,
+	"quasitopos": false,
+	"Grothendieck quasitopos": false
 }

databases/catdat/scripts/expected-data/Set.json

@@ -112,6 +112,8 @@
 	"ℵ₂-small powers": true,
 	"ℵ₂-small copowers": true,
 	"pretopos": true,
+	"quasitopos": true,
+	"Grothendieck quasitopos": true,
 
 	"Grothendieck abelian": false,
 	"Malcev": false,

databases/catdat/scripts/expected-data/Top.json

@@ -169,5 +169,7 @@
 	"locally finite": false,
 	"Barr-coexact": false,
 	"Barr-exact": false,
-	"pretopos": false
+	"pretopos": false,
+	"quasitopos": false,
+	"Grothendieck quasitopos": false
 }