Add quasitopos property

[dschepler]

Adds properties: quasitopos, Grothendieck quasitopos
As a prototypical example of the latter, adds the category of separated presheaves on a topological space

[ScriptRaccoon]

Thank you for the PR! I made some minor comments. I haven't checked out the code yet in my editor, I will do that tomorrow.

---

Related issue: #18

[dschepler]

Actually, could you check Johnstone C2.2.13 for the exact statement, and if it matches what's on the nLab page, could you check whether the definition of "generating set" he uses matches the one we use? If so, then I'd think the category of pseudotopological spaces would be a counterexample to the first statement: it's certainly a locally small quasitopos; it's cocomplete (for arbitrary coproducts, take the disjoint union and set the convergent filters to be exactly the ones containing an image of a convergent filter in one of the components); and it has a generating set (in fact it's even well-pointed). I suspect that the correct statement of the first one would have to replace "generating set" with "small dense subcategory".

If that's the case, then we don't currently have all the component properties of either formulation. Though I guess I could approximate it with a combination of the two, "Grothendieck quasitopos <-> quasitopos + locally small + locally presentable". EDIT: Actually I guess locally presentable -> locally essentially small so that becomes Grothendieck quasitopos <-> quasitopos + locally presentable.

[ScriptRaccoon]

I don't understand the context of your comment. Are you reviewing something which is already in the PR? Is there something wrong? What do you mean with "first statement" in "If so, then I'd think the category of pseudotopological spaces would be a counterexample to the first statement"?

Are you thinking of adding the result C2.2.13 to the implications?

Here is the definition (urgh...)

[dschepler]

The context was that I was considering adding "Grothendieck quasitopos" property to the PR, and then the example of SepPsh(X) as an example of a Grothendieck quasitopos which is not an elementary topos (under the assumption that the topology on X is not totally ordered under inclusion). So I wanted to evaluate what would be a correct equivalent condition, hopefully using existing properties.

The "first statement" was referring to the restatement of this theorem on the nLab quasitopos page, which corresponds to the equivalence (ii) <=> (iii) in Johnstone's theorem.

So, it does look like Johnstone's definition of "generating set" is different from ours (which he calls "separating set"). Johnstone's version certainly seems related to being able to express objects as colimits of generating objects, though I'm not sure of the exact relation off the top of my head.

[ScriptRaccoon]

I understand. But I won't be able to help with that, I am afraid. Maybe it's also necessary to edit the nLab article or reach out to the authors since it "misquotes" (because of Johnstone's weird terminology) the theorem.

[dschepler]

Right now, I think the major property to be resolved is whether it has effective cocongruences. I'm pretty convinced, using that the sheafification is effective, that the comparison morphism $X \sqcup_Y X \to R$ is both monic and epic. So, if I could somehow use the cotransitivity morphism $R \to R \sqcup_{i_2,X,i_1} R$ to show the map $X \sqcup_Y X \to R$ is either regular monic or regular epic, or even that it's strong monic, then that would finish off the proof. I haven't found anything yet along those lines, though.

For the opposite approach, a non-effective equivalence relation I can think of would be something like: say $x \sim y$ for $x,y$ compatible collections of sections over $U_i$ if ($x$ has a gluing if and only if $y$ has a gluing). Or, if that statement in the internal language is satisfied, which is equivalent to: for each $V$, ${x_i}|_{U_i \cap V}$ has a gluing if and only if ${y_i} |_{U_i \cap V}$ has a gluing. It seems pretty clear that's not functorial, though: it should be pretty easy to add a gluing of $x$ without adding a gluing of $y$.

But in any case, any counterexample would have to be roughly of this form "equality when restricted to a regular subobject, augmented by existence of something where that something is forced to be unique if it exists".

Edit: Fixed MathJax formulas

[dschepler]

I think I have a rough proof now: Since $X+X' \to E$ is an epimorphism, that means any section $e \in E(U)$ is locally in one of the copies of $X$. Now $e = r(e)$ is a regular subobject of $y_U$, which must be some $y_V$; and similarly the equalizer of $e = r(e)'$ is some $y_W$. The epimorphism condition implies $U = V \cup W$. We also have that $V \cap W$ is equivalent to $r(e) \in Y$. Now, since $R+R \to R+_X R$ is a regular epimorphism, $t(e)$ must either be in the first or second copy of $R$. If it's in the first copy, then using a splitting of $R \to R +_X R$, we can see it's in fact equal to $i_1(e)$. But then on $W$, we can calculate that $t(e) = i_1(e)$ implies $r(e) = r(e)'$, so $W \subseteq V \cup W$. Thus, $e$ is in the image of $X+X$. And a similar proof holds if $t(e) = i_2(e)$. This shows that $X+X \to E$ is in fact a regular epimorphism; and the category is also regular (any quasitopos is, as the automated deductions suffice to show), so $E$ is effective.

In fact, this should pretty easily generalize to the category of separated objects of a Lawvere-Tierney topology. The only thing that makes it not as easy to generalize to an arbitrary quasitopos is the involvement of regular epimorphisms.

[ScriptRaccoon]

Do we want to add separate entries for the cases $X = \emptyset$ and $X = *$? It seems like these give categories not already present in the database.

EDIT. Ok maybe the case $X = \emptyset$ gives the interval category. For $X = *$ we get Set with a formally adjoined initial object, right?

[dschepler]

The brief introduction to Lawvere-Tierney topologies I would give is: It's just an abstraction of the important properties of the "locally" qualifier on topological spaces. Namely, if $\mathcal{F}' \hookrightarrow \mathcal{F}$ is a sub-presheaf, we say $x \in \mathcal{F}(U)$ is locally in $\mathcal{F}'$ if there exists an open cover $\bigcup_{i\in I} U_i = U$ such that $x|_{U_i} \in \mathcal{F}'(U_i)$ for each $i$. It is easy to check that the collection of sections satisfying this property is again a sub-presheaf of $\mathcal{F}$, which we might call the "locally"-closure of $\mathcal{F}'$ in $\mathcal{F}$", $cl_{\mathcal{F}}(\mathcal{F'})$. We say $\mathcal{F}'$ is "locally"-closed in $\mathcal{F}$ if that closure is $\mathcal{F}'$, and it is "locally"-dense in $\mathcal{F}$ if that closure is $\mathcal{F}$.

Then the observation which relates this to separatedness and sheaves is: a presheaf $\mathcal{F}$ is separated if and only if for each "locally"-dense inclusion $\mathcal{G}' \hookrightarrow \mathcal{G}$, the restriction function $Hom(\mathcal{G}, \mathcal{F}) \to Hom(\mathcal{G}', \mathcal{F})$ is injective; and $\mathcal{F}$ is a sheaf if and only if for each such "locally"-dense inclusion, the restriction function is bijective. (The forward implication in both cases is a straightforward exercise; the reverse implication can be gotten by considering $\mathcal{G} := y_U$ and $\mathcal{G}' := \bigcup_{i\in I} y_{U_i}$, where a morphism $\mathcal{G}' \to \mathcal{F}$ can be checked to be equivalent to a compatible collection of sections in $\mathcal{F}(U_i)$.)

A commonly used equivalent condition to separatedness is: a presheaf $\mathcal{F}$ is separated if and only if the diagonal subsheaf $\Delta_{\mathcal{F}} \hookrightarrow \mathcal{F} \times \mathcal{F}$ is "locally"-closed. This condition can be informally interpreted as: "if two sections are locally equal, then the sections themselves are equal". A less commonly used equivalent condition to being a sheaf, which you might sometimes see (for example in Toposes, Triples, and Theories) is: $\mathcal{F}$ is a sheaf if and only if it is separated and for each separated presheaf $\mathcal{G}$ which is an extension of $\mathcal{F}$, then $\mathcal{F}$ is "locally"-closed in $\mathcal{G}$.

The "locally" Lawvere-Tierney topology just extends this to subobjects considered as equivalence classes of monomorphisms as usual. It's also straightforward to generalize this to a Grothendieck site, of course. One of the conditions of a Lawvere-Tierney topology is that the closure operation commutes with pullbacks, so it induces an endomorphism of the Sub functor, and thus a morphism $j : \Omega \to \Omega$ satisfying certain conditions.

[dschepler]

I was thinking of modifying the proof of the special morphisms to start with a calculation that the image in Sep(j) is the same as the image as calculated in $\mathcal{T}$, whereas the coimage in Sep(j) (i.e. the equalizer of the cokernel pair) is the j-closure of the image as calculated in $\mathcal{T}$. Then, the rest would be automatic from the fact that in a regular category, $f : X \to Y$ is a monomorphism if and only if $X \to im(f)$ is an isomorphism, and $f : X \to Y$ is a regular epimorphism if and only if $im(f) \to Y$ is an isomorphism; and similarly we have the dual result for coregular categories and coimages.

Does this revision sound good to you?

[dschepler]

Incidentally, the search http://localhost:5173/category-search/results?satisfied=regular%7Ecoregular&unsatisfied=thin%7Ebalanced also returned the example of TorsFreeAb where the description of special morphisms looked very similar, just with saturation in place of "locally"-closure or $j$-closure. I wonder if there might be some more general result that would encompass both cases. I guess I can make the observation that an abelian group is torsion-free if and only if the diagonal is saturated, and the reflector in that case can also be viewed as taking the quotient by the saturation of the diagonal.

[ScriptRaccoon]

The brief introduction to Lawvere-Tierney topologies I would give is: [...]

Thanks a lot!

I was thinking of modifying the proof of the special morphisms [...]

I don't have an opinion on this right now.

[...] I wonder if there might be some more general result that would encompass both cases. [...]

Can we perhaps move this to a separate issue or PR?

As for the review, I need to postpone this a few days. I need some pause from this project.

[ScriptRaccoon]

"... general situation ..." - Please add a reference why it is a reflective subcategory, and for the claim that the reflector preserves finite limits.

[ScriptRaccoon]

Maybe write X_{sep} since this notation is used below.

[ScriptRaccoon]

I must admit that I am not able to review this PR. Too much is unclear to me, especially in this paragraph.

[ScriptRaccoon]

Several options:

1. We merge this PR either way, I don't need to understand everything.
2. We find another person that checks the details.
3. More details are added to make it self-contained.

[dschepler]

I think I've found a proof that a general quasitopos has effective cocongruences. In fact, the core of the argument seemed to generalize to a proof that regular + extensive + quotients of congruences -> effective cocongruences (which doesn't directly apply to SepPsh(X) for example, but the failure to have disjoint coproducts is controlled enough that a cocongruence lives within a subcategory where you can apply that result).

Interestingly, this seems to have made several "not regular" assignments redundant: for LRS_R, Meas, Met_oo, Pos, Prost, Cat, Top. Essentially, I guess the proof provides a way to take a non-effective cocongruence, and construct a pullback diagram where the bottom row is a regular epimorphism but the top row is not. That pullback diagram, more concretely, has the cocongruence $X+X'\to R$ as top row; $X+X'\to E+E'$ as left column; the cotransitivity morphism $t : E\to E+_X E'$ as right column; and $E+E' \to E+_X E'$ as bottom row.

[dschepler]

Before this is ready to be merged, there are a couple references that need to be completed. One is to the decomposition of an arbitrary quasitopos into a comma category of a Heyting algebra and a solid quasitopos. The other is to the fact that a solid quasitopos has disjoint finite coproducts and is therefore extensive (though this one is easy enough to prove by hand, if needed). However, I don't have a copy of Johnstone to search for these references.

If you want another reviewer still, after the refactoring of the "quasitopos -> effective cocongruences" implication, then the reviewer I could think of inviting would be Vladimir Sotirov at MSE. He's the author of the proof there that "strong quasitopos <-> regular quasitopos" and has also given answers to some of my questions there that on review are referencing generalizations of my questions to quasitopoi. If you would want him as a reviewer, is there some way we could provide an interim rendering of the PR branch for him to browse, without his needing to set up the repo and pnpm on one of this machines?

[ScriptRaccoon]

Ok, I don't even know what a solid quasi-topos is.

Yes let's invite another reviewer.

Netlify offers branch deployments with preview URLs, so a reviewer can check out the URL directly. But this doesn't work with branches in forks. But for the review process I can just copy the branch into the repository itself etc. so this will be doable. (The only issue is that syncing is not so straightforward.)

Just let me know when I should do that.

[dschepler]

In brief, for a quasitopos, TFAE: (1) The category has disjoint finite coproducts. (2) The category is extensive. (3) The unique morphism $0 \to 1$ is a regular monomorphism. The term "solid quasitopos" is defined as option (3) probably because it's the easiest to check.

(The proof: (1) <=> (2) is of course because the quasitopos is locally cartesian closed. (1) => (3): $1+1$ being a disjoint coproduct implies $0$ is the equalizer of the two coinclusion morphisms $1 \to 1+1$. (3) => (1): Since $0$ is a strict initial object, we have a pullback square $(0 \to X) \to (0 \to 1)$, so every $!_X : 0 \to X$ is a regular monomorphism. So, since the category is coregular, in the pushout square $(0 \to X) \to (Y \to X+Y)$, the morphisms $X \to X+Y$ and $Y \to X+Y$ are (regular) monomorphisms. That pushout is also a pullback by Johnstone A2.6.3 (or, use the fact that $0 \to 1$ being regular monic implies it's the equalizer of its cokernel pair $1 \rightrightarrows 1+1$, and we have a map $X+Y \to 1+1$). )

Anyway, I have plans for this evening, but hopefully tomorrow I'll be able to sync the PR branch with main and do another cleanup pass.

[dschepler]

I discovered that my previous supposed proof that a Grothendieck quasitopos has exact filtered colimits was incorrect: in general, the reflector from a topos T to Sep(j) does not preserve equalizers. And in fact, for any topological space $X$ which has a non-compact open subset, then SepPsh(X) does not have exact filtered colimits. That's because if we have a directed set of open subsets whose union $U$ is not in the set, then we can take the directed diagram of parallel pairs $1 \rightrightarrows 1 +{y_V} 1$ for $V$ in the set. The directed colimit is $1 \rightrightarrows 1 +{y_U} 1$, with equalizer $y_U$. On the other hand, the equalizers are $y_V$, and the directed colimit of these equalizers is $\bigcup_V y_V$.

I think if every open subset is compact, then SepPsh(X) does have exact filtered colimits.

How do we want to handle putting this observation in the database? It seems more of a specialized assumption than the ones about the topology not being totally ordered by inclusion, or that there are nontrivial open covers, to assume that there is a non-compact open subset (since for instance separated presheaf categories on finite discrete spaces are still interesting).

[ScriptRaccoon]

How do we want to handle putting this observation in the database? [...]

This problem is essentially #7. I don't have a good final answer. But one option is to just specify $X$ to be a very concrete space, say the real numbers. I would say that we don't necessarily need to cover all cases for all parameterized categories, but rather list interesting examples of categories. In particular, I think SepPSh(X) has been added for the purpose of having a quasi-topos which is not a topos, right? For this purpose, it should be fine to specify $X$. And in the proofs, you can decide if you want to make explicit which step uses which property of $X$ (or none at all).

Obviously, I would not say the same for the category of $R$-modules for a ring $R$, since it is used in all sorts of places for general $R$, and here we should cover many cases.

[ScriptRaccoon]

Meta comment: consider splitting this PR into smaller chunks, since otherwise merging will be delayed, the review becomes difficult, and rebasing becomes cumbersome.

• add SepPSh(X) (not all properties have to be decided at once)
• add quasi-topos property (only what's necessary to decide the property for many categories)
• add Grothendieck quasi-topos property (only what's necessary to decide the property for many categories)
• fill in the gaps

for example.

[dschepler]

OK, if we want to start off with an example of a quasitopos which is neither an elementary topos nor thin, then I could start off with a simpler and more concrete example, such as:

• The category of subsequential spaces.
• The category of pseudotopological spaces. (Simpler definition if you use the formulation in terms of a limit relation between ultrafilters on $X$ and $X$ including that the principal ultrafilter at $x$ has limit $x$, but maybe a bit more complex to show why it's locally cartesian closed.)
• The category of simple (undirected) graphs.
• The category of binary relations (objects are a set $X$ equipped with a binary relation $R \subseteq X$, morphisms are then functions $X \to Y$ respecting the relations).
• The category Mono of injective functions of sets, with morphisms being commutative squares.

Any one of these jump out at you as an example you'd like to get in? Personally, I'd lean more towards the graph example as an expansion into a new "graph-theory" tag.

[ScriptRaccoon]

Mono > Rel* > Graph would be my personal preference.

*Need a different notation.