Add category of ω-sets

[dschepler]

As discussed in the PR for the effective topos (#353), this PR is working on putting in the subcategory of ω-sets (otherwise known as a special case of the category of assemblies for the partial combinatory algebra also used in constructing the effective topos). The subcategory has simpler definitions that are easier to work with, to work up to the full definition of the effective topos. It can also be useful in an alternate construction of the effective topos, as the ex/reg completion of this category.

[dschepler]

Currently unresolved properties (many similar to the ones that were unresolved for the full effective topos):
is accessible
is Barr-coexact
is coaccessible
has effective cocongruences
has an extremal cogenerating collection
has an extremal cogenerator
has an extremal generating collection
has an extremal generator
is ℵ₁-accessible
has ℵ₁-cofiltered limits
has ℵ₁-filtered colimits

At this point, I think the best way to prove effective cocongruences would be to incorporate the proof from the abandoned quasitopos + SepPsh(X) PR, that regular + extensive + quotients of congruences -> effective cocongruences.

Otherwise, I might be able to adapt the proof from the effective topos PR to show that the $\omega$-sets with underlying sets contained in $\mathbb{N}$ are an extremal generating collection - though I haven't quite gotten the details on that down yet.

[dschepler]

On reviewing it myself, I see a need to improve the wording where I refer to a partial recursive function $\mathbb{N} \dashrightarrow \mathbb{N}$ "being a map as in the definition" for a function between the underlying sets. Maybe we can come up with a good name for that partial recursive map - something like "a realizer tracking map for $f$" perhaps?

[ScriptRaccoon]

On reviewing it myself, I see a need to improve the wording where I refer to a partial recursive function N ⇢ N "being a map as in the definition" for a function between the underlying sets. Maybe we can come up with a good name for that partial recursive map - something like "a realizer tracking map for f " perhaps?

I have no expertise on this category at all, but I would probably call it "a realization function of the morphism", or simply "a realizer of the morphism". Then you can describe morphisms as realizable functions.

EDIT. after reading some of the proofs (still on a superficial level), I think that any term will greatly simplify the exposition; it will be used all the time

[ScriptRaccoon]

Currently unresolved properties [...]

With all of the categories that I have added in the last weeks, I have decided every single property. This was a lot of work, but Gemini Pro has helped me a lot to find the proofs (I can recommend using it), and I think the database has the best value when there are no questions left. But, of course, if something just does not work, leave it open and/or write an issue.

[dschepler]

With all of the categories that I have added in the last weeks, I have decided every single property. This was a lot of work, but Gemini Pro has helped me a lot to find the proofs (I can recommend using it), and I think the database has the best value when there are no questions left. But, of course, if something just does not work, leave it open and/or write an issue.

OK, I'm stuck on the current set of unresolved properties:
is accessible
is coaccessible
has an extremal generator
is ℵ₁-accessible
has ℵ₁-cofiltered limits
has ℵ₁-filtered colimits

I don't have Gemini Pro at the moment; and when I asked free Google AI on some of these questions, it just ended up in the sort of situation where it was just spouting nonsense, and when corrected it just came up with some other nonsense to spout. On a lot of them, it ended up referring again to the van Oosten paper which only proves that a certain set of objects doesn't form a dense subcategory of the effective topos - nothing I could find in that paper that would give direct answers to any of these questions, or even the corresponding questions in the effective topos.

The closest I've come is a pathological-looking ℵ₁-filtered diagram inspired by the van Oosten paper: let $(s_\alpha){\alpha < \omega_1}$ be an $\omega_1$-Aronszajn sequence, which is a sequence of injective functions $\alpha \to \omega_1$ such that whenever $\alpha < \beta$, then $s\beta |{\alpha}$ and $s\alpha$ differ only at finitely many inputs. Now define $X_\alpha$ to be the $\omega$-set with underlying set $\alpha$ and with realizability relation that $n$ realizes $\gamma &lt; \alpha$ if and only if $s_\alpha(\gamma) = n$. Then the almost-compatibility condition implies that only finitely many realizers have to be "reassigned", which is certainly possible to do with a full recursive function; therefore, the inclusion map $\alpha \hookrightarrow \beta$ induces a morphism $X_\alpha \to X_\beta$. Any colimit of this diagram would have to have underlying set bijective with $\omega_1$ (and the cocone maps are equivalent to the inclusions) since the forgetful functor is a left adjoint. But beyond that, I haven't found a proof of a contradiction, nor a construction of a realization relation on $\omega_1$ which makes it a colimit. (Other than the vague idea of using the extremal cogenerator of $P(\mathbb{N}) \setminus {\emptyset}$ to maybe extract some information on what the realizers would have to look like.)

Otherwise, I'm still working on revising the proofs of local cartesian closure and having effective cocongruences, and maybe trying to find a better overview for the category description.

[ScriptRaccoon]

What is the status of the comments I made but that are not resolved yet? Are you planning to work on these? I am basically waiting for that before I continue the review (since this will make it easier for me to digest the other proofs).

EDIT. Nevermind, I just saw the last paragraph in your comment above.

[ScriptRaccoon]

Response to #373 (comment):

I don't have Gemini Pro at the moment;

I also don't pay for Google Gemini, but you get some free credits per day. I have a couple of Google accounts, so that I have even more free credits.

and when I asked free Google AI on some of these questions, it just ended up [...]

Oh yeah, even Gemini Pro also produced a lot of bullshit in the last weeks. Maybe they changed something, but it is also possible that our questions get more complex ... And Google Gemini with the free Flash model is pretty much useless for (advanced) mathematics.

The closest I've come is a pathological-looking ℵ₁-filtered diagram [...]

I see. We can merge this PR without deciding $\aleph_1$-filtered colimits (from my side), but I wonder how we can save this potential counterexample in the repo, so that we or someone else (!) can perhaps later complete it; and find an approach for partial results that also works in future. Maybe just a text file named like the category?

Otherwise, I'm still working on revising the proofs of local cartesian closure and having effective cocongruences, and maybe trying to find a better overview for the category description.

Great!

[dschepler]

FYI, I just posted https://math.stackexchange.com/questions/5150285/what-is-the-motivation-for-the-definition-of-omega-sets to ask about how to motivate the definition or explain how to think about "realizers".

[dschepler]

I've made some more adjustments which should hopefully address the major comments. I also managed to complete the proof that the category does not have $\aleph_1$-filtered colimits, so now it witnesses 3 new combinations:

Directly witnessed:

• locally cartesian closed ∧ ¬ℵ₁-filtered colimits
• quasitopos ∧ ¬ℵ₁-filtered colimits

Dually witnessed:

• locally cocartesian coclosed ∧ ¬ℵ₁-cofiltered limits

[ScriptRaccoon]

Sorry for keeping you waiting. I will review the PR today. Is my understanding correct that it is finished on your side?

[dschepler]

Sorry for keeping you waiting. I will review the PR today. Is my understanding correct that it is finished on your side?

Yes (at least for now, it will of course need rebasing/squashing and resolving conflicts at the very least, eventually).

[ScriptRaccoon]

For the missing proof that $\omega$-Set has no extremal generator, I have asked Claude AI. See the attached document. Use with care since I have not read the proof yet.

omega-set-extremal-generator.pdf

omega-set-extremal-generator.tex.txt

[ScriptRaccoon]

The next batch of comments

[dschepler]

For the missing proof that ω -Set has no extremal generator, I have asked Claude AI. See the attached document. Use with care since I have not read the proof yet.

omega-set-extremal-generator.pdf

omega-set-extremal-generator.tex.txt

I've read through the document and it makes sense to me. I'll see about rewriting it in my own words.

[ScriptRaccoon]

I just wanted to comment that this assumption has been missing all the time. Good that you have fixed it!

[ScriptRaccoon]

I have fixed it now as well in #419

[ScriptRaccoon]

I have fixed the spacing issue on main, so after rebasing you can remove the braces around \id

The same in line 296

[ScriptRaccoon]

It seems you have resolved all my comments. Shall I have another look?
As mentioned, I also haven't looked yet at the proofs of the unsatisfied properties. This comes next.

[dschepler]

It seems you have resolved all my comments. Shall I have another look? As mentioned, I also haven't looked yet at the proofs of the unsatisfied properties. This comes next.

Yes, it should be ready for more review.

[ScriptRaccoon]

The category ω-Set is the first category we have that has block-level elements in the description. This has led to invalid HTML because the description was rendered in a paragraph. In fact, reloading the page gave a 500 error page. I have fixed this in 0a1e767. It also fixes the same rendering issue on the property page, which is actually a live bug on many property pages (finitary algebraic, extensive, ...): directly opening them, or navigating to them and refreshing gives a 500!

EDIT. ok since this is huge bug, I have cherry-picked the commit to main now and deployed. Before rebasing, we can keep the commit here, because only then the page for ω-Set is properly rendered.