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]

These are my comments about the results on extensive categories and cocongruences. I will look at $\omega$-sets later.

[ScriptRaccoon]

Thanks for making this observation. I am not sure if it is best to change the definition though, since I do not want to diverge from the literature (and the nLab article). Maybe it is better to add a new property; we might call it "weakly Malcev". Then, by definition, Malcev = finitely complete + weakly Malcev.

On the other hand, in more classical papers before the book by Mal'cev, protomodular, homological and semi-abelian categories came out, Malcev categories were assumed to be regular, not just finitely complete ...

For example:

• https://www.sciencedirect.com/science/article/pii/002240499190022T
• https://www.sciencedirect.com/science/article/pii/S0022404998001121

This is so confusing.

What's your opinion? This is also very similar to #370.

[ScriptRaccoon]

This PR has two separate topics:

• results on extensive categories
• the category has $\omega$-sets

Let's keep it like this here, but in future, feel free to make smaller or preparatory PRs as soon as it becomes clear that two (or more) topics emerge. (I also do this all the time.)

[ScriptRaccoon]

first batch of comments about $\omega$-sets

[ScriptRaccoon]

I think this proof shows why we insist that encodings are not unique. How do we want to encode an element in a quotient? We take an encoding of a preimage. But which preimage? This does not work if we only allow one encoding. But if we allow multiple encodings, we just take all encodings of all preimages.

I would probably write something like this either here in the proof or as a comment*.

*not a code comment; a comment visible on the page, like in Sh(X).yaml

[dschepler]

Maybe this would become clearer if we also include the category of partitioned $\omega$-sets which presumably doesn't have coequalizers (in fact I think it doesn't have quotients of kernel pairs), and then in the description of this category, or a comment, we can highlight that allowing for multiple realizers of an element changes that.

[ScriptRaccoon]

Yes; something for a separate PR then.

[ScriptRaccoon]

Conceptually, several of the proofs go like

• Set has this property
• Comp (?) has this property
• Hence, $\omega$-Set = (Set @ Comp)/~ has this property as well

I don't know what Comp is. But its objects should definitely not only be natural numbers. And @ is some kind of construction with two categories (not the product obviously).

The pattern is very obvious for finite limits and finite colimits. For cartesian closure, it also happens I guess (but I have not fully understood the proof). Comp (whatever that is) is cartesian closed because we can encode currying (this is exactly what you are doing there).

Maybe we can make this precise.

[dschepler]

Natural numbers are sufficient to encode sequences of bytes, and therefore to encode any computational object which can be serialized to a file. It seems using natural numbers instead of a distinct type is standard in mathematical computation theory.

[dschepler]

As for the rest of it: The usual generalizations are to construct the category of assemblies of a partial combinatory algebra (a generalization of the collection of partial recursive morphisms, though in particular it still requires that any distinction between programs and the data they operate on can be broken when needed) and then the generalization to a simplified version of the tripos-to-topos construction. So for example for binary products, what you're seeing is that we define for each set $X$ an almost-Heyting-algebra structure on the functions $X \to P(\mathbb{N})$ where for example $(f \land g)(x) = { \langle n, m \rangle \mid n \in f(x) \land m \in g(x) }$, and then for two such maps $f,g$ for $X$ and $Y$ we can define such a map for $X\times Y$ via $(p_1^* f) \land (p_2^* g)$. (In fact, it essentially only fails to be a Heyting algebra by failing to be antisymmetric, and you can take the partial order quotients to get actual Heyting algebras. And then you can also define $\exists_f$ and $\forall_f$ adjoints to $f^*$ making the "first-order hyperdoctrine" fragment of the tripos data, and so on.)

But I thought the point here was to avoid jumping straight to the tripos generalization and instead see a concrete version of the construction and proofs.

[ScriptRaccoon]

Natural numbers are sufficient to encode sequences of bytes, and therefore to encode any computational object which can be serialized to a file. It seems using natural numbers instead of a distinct type is standard in mathematical computation theory.

I assume this is a response to my suggestion that Comp should have objects besides N. I was simply saying this because the proofs for products and coproducts also need N + N and N × N and a subset of N → N, and it is kind of awkward to always go back to N.

But I thought the point here was to avoid jumping straight to the tripos generalization and instead see a concrete version of the construction and proofs.

True.

[dschepler]

Thinking about it some more, maybe the category of partitioned $\omega$-sets would be a good candidate for Comp: that's the full subcategory of objects where $R_X$ is the inverse of a functional relation $X \to \mathbb{N}$. Or maybe it could help to restrict to the ones where that function is injective. That might also be related to the fact that $\omega$-Set can be expressed as the reg/lex completion of the category of partitioned $\omega$-sets (thus it's equivalent to a category of formal images of morphisms of partitioned $\omega$-sets). And then in that category $\mathrm{p}{-}\omega{-}\mathbf{Set}$, a serialization function for $X\times Y$ can be constructed as the pairing function composed with the product of the serialization functions for $X$ and $Y$.

[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