Current priority: reduce the number of unknown properties

[ScriptRaccoon]

This issue is partially a duplicate of other issues (or more like a parent), but I want to make it more visible that this should have a priority right now (when it comes to additions to the data). Do not add new properties and do not add new categories before we have decided most (or at least some) of the unknown properties of the categories which look doable. Exceptions: new properties that help to decide the given ones and where all categories will be decided directly (those that create no new unknowns).

In particular, decide all properties of (at least):

category	done
CMon	❌
FinOrd	✅
FinGrp	✅
B	✅
FS	✅
Rel	✅
Set_f	✅
Cat	✅
Man	✅
BG_f	✅
walking_fork	✅
walking_pair	✅
walking_span	✅
BG_c	✅

The following are currently open:

• CMon has 1 unknown property. MO question: https://mathoverflow.net/questions/511792

All these look doable. A PR can tackle one property or one category at a time.

Related:

• Decide if CMon and FinGrp have effective cocongruences #151
• Decide accessible etc. for various categories #91

PRs working on this issue:

• Small groupoids are generalized varieties and finitely accessible #195
• Decide multi-completeness for remaining categories #196
• Add criterion for sifted colimits #197
• Decide some properties of FS and Rel #198
• Some coaccessibility proofs #201
• Decide all properties for the category of Hausdorff spaces #202
• Handle undecidable properties as assignments #203 (sort of)
• Cat does not have a regular subobject classifier #209
• Meas is not regular #216
• Sh(X) never has a generator (unless X has the indiscrete topology) #210
• Add missing proofs for FinGrp, FS, Met #217
• LRS does not have a small generating set #225

Development of the number of unknown (category, property)-pairs:

151 --> 145 --> 139 --> 136 --> 133 --> 125 --> 118 --> 116 --> 115 (--> 117) --> 116 --> 114 --> 108 ---> 97

[varkor]

(The links are to localhost, rather than the website.)

[ScriptRaccoon]

Yes, on purpose :). It's easier for development.

[dschepler]

I think probably my proof at https://math.stackexchange.com/questions/1742667/is-the-category-of-categories-a-topos/3121774#3121774 that Cat does not have a subobject classifer could easily be adapted to a proof that it does not have a regular subobject classifier. All you would have to do would be to verify that all the subcategories involved are equalizers, which looks straightforward.

[dschepler]

I'm planning to submit a PR on the Cat assignment later today. The basic idea will be to recast the proof in terms of expressing ${ 0 \to 1 \to 2 }$ as a pushout of ${ 0 \to 1 }$ and ${ 1 \to 2 }$, and constructing two distinct equalizers on ${ 0 \to 1 \to 2 }$ whose restrictions to ${ 0 \to 1 }$ and ${ 1 \to 2 }$ are both the same. Therefore, $\mathrm{Sub}_{\mathrm{reg}} : \mathbf{Cat}^{\mathrm{op}} \to \mathbf{Set}^+$ does not preserve pullbacks, so it cannot be representable.

I might also be able to submit a PR to prove Sh(X) never has a generator (unless X has the trivial topology, which is excluded). Not sure how many other properties that will resolve - it should for example also show Sh(X) is not finitary algebraic.

[ScriptRaccoon]

Thanks!

Yes adding not having a generator for Sh(X) resolves finitary algebraic, but unfortunately nothing else (I just tried).

Remark: Sh(X,Ab) does have a generator. And both have a generating set. So the issue must be a form of connectedness.

[dschepler]

For FS being a generalized variety: Maybe every object is strongly finitely presentable, since in a sifted colimit, there is some $i$ for which $X_i$ has minimum cardinality; and then for such an $i$, you might be able to prove $X_i$ is the colimit by a proof similar to the one for sifted colimits in groupoids? (Not at all sure about this, since I haven't studied sifted colimits before. But if you can find a counterexample where the sifted colimit is not some $X_i$ of minimum cardinality, then that sifted colimit in fact would not be strongly finitely presentable.)

Hmm... yes, looking at lemma 1 in http://localhost:5173/content/sifted-colimits-in-groupoids it does appear the proof should go through with minimal changes if we revise the statement to: Suppose $i_0 \in \mathcal{I}$ is such that for every $f : i_0 \to j$, $D(f)$ is an isomorphism. Then $D(i_0)$ is a colimit object of $D$. (About the only thing to add would be maybe a short justification for using $D(f)^{-1}$ in the third display, where $D(f)$ being an isomorphism is automatic from $f$ fitting into a diagram $i_0 \to k \to k'$.)

[ScriptRaccoon]

Thanks! I will try to work this out and add it to #217.

[ScriptRaccoon]

@dschepler You may have a look since I could improve that content page and the proofs for FS a lot.

[ScriptRaccoon]

The only category that remains (as for this issue) is CMon. I have asked on MO:

https://mathoverflow.net/questions/511792/is-every-cocongruence-in-mathbfcmon-effective