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]

I think it makes sense to merge the two pages.

[ScriptRaccoon]

Let's add a link to https://ncatlab.org/nlab/show/Lawvere-Tierney+topology

[ScriptRaccoon]

I must say that I do not understand this proof.

1. Can you make more clear where the quasitopos properties are used? (I must admit that this was also a weakness in my proof before for elementary toposes.)
2. Why is $0 \to \lim_n N_{\geq n}$ an epi? Don't we need to take morphisms on the limit for that? Why do you consider $N_{\geq n} \to X$?
3. There seems to be a typo in $i_{n'} : 1 \to N_{\geq n}$. It should be $n'$.
4. Please write out domain and codomains in $\top \circ {!}_X$. Like $X \to 1 \to \Omega$.

[ScriptRaccoon]

Please add a reference for the equivalence.

[ScriptRaccoon]

Do we need / want tags for properties? Then we can tag this and related properties with topos theory. It will easier to find all properties within one tag. Other tags can be existence of limits, existence of colimits, compatibility of limits and colimits, morphism behavior, size, etc. (Similar to the folders we once had before properties got separate files, but these folders were internal only.) Maybe then also tags for implications?

[ScriptRaccoon]

We can also add Grothendieck quasitopos

[ScriptRaccoon]

Maybe we need a short remark that Johnstone uses a different definition of a generating set, namely a strong generating set, but that any locally presentable category has a strong generating set by Adamek-Rosicky, Theorem 1.20 in Chapter 1?

[ScriptRaccoon]

"In order to calculate colimits [...]" --- Can you add a reference / proof why colimits look like this?

What is the " $K$ closure of the diagonal relation"? And the relation on which object?

Notice that it's the first time for me reading about all these concepts (quasitopos, Grothendieck quasitopos, Lawvere-Tierney topology, etc.), so basically I cannot follow. Can we make the proof accessible to people like me? Can you perhaps add more references in general here?

[ScriptRaccoon]

Suggested change

	Let $\T$ be an elementary topos with a Lawvere-Tierney topology $j$. Then in the full subcategory of $j$-separated objects, every cocongruence is effective.
	Let $\T$ be an elementary topos with a Lawvere-Tierney topology $j$. Then in the full subcategory $E$ of $j$-separated objects, every cocongruence is effective.

I assume?

[ScriptRaccoon]

To clarify this proof, either describe binary coproducts first or even add property: binary coproducts with proof before. This will also be useful for disjoint finite coproducts below.

[ScriptRaccoon]

... or refer to the description of coproducts below

[ScriptRaccoon]

$X$ is already taken. Let us use "sheaf-notation" $F$ and $G_i$.

Also, let's write "both sides ... on $U$".

Replace $\Set$ by <a href="/category/Set">$\Set$</a> since there the proof can be found. Alternatively, link to the implication extensive_cocartesian_cofiltered_limits.

[ScriptRaccoon]

Let's add Set.

[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?

[ScriptRaccoon]

I just noticed that \Sh: \operatorname{Sh} is inconsistent. Can you change this to mathbf?

[ScriptRaccoon]

Suggested change

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

[ScriptRaccoon]

$X$ is already taken.

[ScriptRaccoon]

Why is $E \to X \times X$ not regular?

[ScriptRaccoon]

$X$ is already taken

[ScriptRaccoon]

Why is this relation not cosymmetric?

[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?