Sh(X) never has a generator (unless X has the indiscrete topology)

[dschepler]

It turns out this only resolves the direct assignment plus not being finitary algebraic.

---

• unknown (category, property)-pairs before this PR: 116
• unknown (category, property)-pairs after this PR: 114

[ScriptRaccoon]

Maybe we should even assume that $X$ is sober (a space has the same category of sheaves as its soberification, right?).

If you agree, you can add this right away to the file. Then this weird "not indiscrete" assumption becomes redundant, I assume.

[dschepler]

The new lemma could potentially be used to rewrite the assignments for SetxSet (where $(1,0)$ and $(0,1)$ are each a subterminal object which is not initial or terminal) and for Sp (where I guess for any $n$ the functor assigning 1 for sets of cardinality $n$ and $\varnothing$ otherwise is an intermediate subterminal object). Not sure whether it's worth it for SetxSet (in fact, the proof is easier in general in any situation where the intersection of all intermediate subterminal objects is initial) but in the existing argument for Sp I do see echoes (or foreshadowing) of the general lemma's proof.

[ScriptRaccoon]

Looks very good! Can you please squash your commits into one? Then I will merge.

[ScriptRaccoon]

The new lemma could potentially be used to rewrite the assignments for SetxSet [...] and for Sp

Yes. But let's only add a sentence like "Alternatively, this follows from ..."

[dschepler]

Looks very good! Can you please squash your commits into one? Then I will merge.

Done.