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

I have finally read everything. I added the commit d8a0a91 which adds details to some proofs of unsatisfied properties. (Claude did this for me, I simply asked for clarification at some steps.)

Below, I will post two AI reviews.

[ScriptRaccoon]

Claude's review of the proofs for $\omega$-sets

I reviewed database/data/categories/omega-Set.yaml, all 25 proofs in it.

Overall: Most of the arguments hold up, including the long ones: cartesian closed, locally cartesian closed, the extremal generating collection, the extremal cogenerator, ℵ₁-filtered colimits, extremal generator, and countable powers. The local definitions I checked agree with how they are used: co-Malcev, the extremal (co)generating notions, disjoint finite coproducts, the regular subobject classifier, and the lemma in content/generator_construction.md. One proof doesn't prove its claim. The other findings are small gaps.

Findings

1. essentially small (unsatisfied), proof at omega-Set.yaml:187. Severity: major.
The proof stops at "∇ is fully faithful, and therefore conservative." Nothing gets from there to "not essentially small."

• Conservativity is the wrong property to use. It says that a morphism is an iso when its image is. It doesn't say that an isomorphism ∇X ≅ ∇Y comes from a bijection X ≅ Y.
• What is needed: ∇ is fully faithful, so it is injective on isomorphism classes. Set has a proper class of isomorphism classes, so ωSet has one too.
• The full faithfulness of ∇ is also not proved anywhere in the file. It is easy: every function ∇X → ∇Y has the identity as a tracker. But the proofs for essentially small and locally finite both rely on it.

2. disjoint finite coproducts, proof at omega-Set.yaml:130. Severity: minor.
The definition talks about the pullback A ×_{A+B} B. The proof uses only two facts: the forgetful functor preserves finite coproducts, and it reflects initial objects. It also needs the forgetful functor to preserve pullbacks (true, since it is representable by 1). The proof also never checks that the coprojections are monomorphisms (they are injective, so this follows from the characterization of monos).

3. regular subobject classifier, proof at omega-Set.yaml:127. Severity: minor.
The proof shows that χ_{X'} exists, but not that it is unique, which the definition requires. Uniqueness follows because the pullback's underlying set is the pullback in Set, so χ⁻¹(1) = X' is forced. The proof doesn't say this.

4. cartesian closed at omega-Set.yaml:80 and locally cartesian closed at omega-Set.yaml:107. Severity: minor.
Neither proof checks that the new realization relation makes the exponential an ω-set, i.e. that every element has a realizer. Each morphism has a tracker, and the tracker has an index p. In the slice case, z also needs a realizer. This is a one-line check, but it is a required condition on objects.

5. co-Malcev, proof at omega-Set.yaml:201. Severity: minor.
The definition takes a corelation to be a quotient X ⊔ X ↠ R. The proof never checks that [f, g] : ∇1 ⊔ ∇1 → ∇2 is such an epimorphism. It is: the map is surjective, and the constant tracker 0 also shows it is regular. The step from "the represented relation is not transitive" to "the corelation is not cotransitive" goes through Yoneda. That step is valid, but the proof leaves it implicit.

6. extremal generator, Step 3 at omega-Set.yaml:250. Severity: minor.
c(t_n) is well defined only if the enumeration (t_n) is injective, i.e. a bijection ℕ → T. "Enumeration" could also mean a surjection with repeats, and then c could get two different values at the same point. The proof should say "bijective enumeration."

Nothing else came up, including in the adversarial pass:

• Degenerate cases: empty Y in the semi-strongly connected proof, and empty G in the extremal generator proof, are handled.
• Aronszajn tracker: it is well defined.
• Classifications: the regular mono and regular epi characterizations match the iso condition on im(f).
• Disjointness in the extremal generator construction: b_n ∉ T holds.

This is an AI review, not a proof of correctness. The author still has to check every argument thoroughly.

[ScriptRaccoon]

About Claude's review on $\omega$-sets: I think 5. and 6. can be ignored. But 1. - 4. need some small fixes. I kindly ask you to do that.

[ScriptRaccoon]

Claude's review on effective cocongruences in extensive categories

I reviewed content/cocongruences_in_extensive_categories.md, all five ::: Proof blocks (Lemmas 1, 2 and 4, Corollaries 3 and 5).

Overall: All five statements are correct and the overall structure works. I found no demonstrated error. I checked these computations explicitly:

• the generalized-element calculation in Lemma 1;
• the orientation of the dual squares fed into Lemma 2 in Corollary 3;
• the transposed use of Lemma 2 in Lemma 4, and the identification of both legs with (i_1; i_1∘e; i_2∘e; i_2) and (i_1; i_2∘e; i_1∘e; i_2);
• the match with the congruence from content/pushouts-of-monos-via-congruence-quotients.md.

There are three gaps where a step is justified by something that doesn't quite cover it.

Findings

1. Lemma 2, uniqueness, ::: Proof at cocongruences_in_extensive_categories.md:67. Severity: minor (gap in the justification).
The proof says uniqueness follows from the uniqueness in the two given pullbacks plus "the coprojections C_i → C_1 + C_2 are monomorphisms." That isn't enough. Take any w : T → A_1 + A_2 with the right projections. To apply the uniqueness in pullback i, you first need w∘ι_i : T_i → A_1 + A_2 to factor through A_i. This uses a second consequence of extensivity: A_i is the pullback of C_i ↪ C_1 + C_2 along g_1 + g_2. Mono coprojections are then needed to get g_i∘w_i' = v_i. The proof never states the factorization step.

2. Corollary 3, the regular-epi conclusion, ::: Proof at cocongruences_in_extensive_categories.md:85. Severity: minor.

• The proof says E + E → E +_X E is a regular epi, citing the pushouts-of-monos page. That page's lemma assumes quotients of congruences, which Corollary 3 doesn't assume. Corollary 3 only assumes that the pushout exists. The claim is still true for an elementary reason: X + Y → X +_S Y is always the coequalizer of S ⇉ X + Y. But the cited result doesn't support the step under the stated hypotheses.
• Separately, the "In particular" sentence at line 81 says "for any cocongruence," which drops the hypothesis that E +_X E exists. The argument needs that pushout (to have t and to pull back along it). Corollary 5 provides it, so nothing downstream breaks, but as worded the statement is stronger than what is proved.

3. Lemma 4, the second pullback square, ::: Proof at cocongruences_in_extensive_categories.md:117-127. Severity: minor (the citation doesn't cover the step).
The proof needs the equalizer e of the coreflexive pair j_1, j_2 to also be their pullback. The linked implication pullbacks_imply_coreflexive_equalizers proves the converse: assuming a pullback exists, it is an equalizer. That implication also assumes the category has pullbacks, which Lemma 4 doesn't. The needed direction has a one-line proof (j_1∘w_1 = j_2∘w_2 implies w_1 = r∘j_1∘w_1 = r∘j_2∘w_2 = w_2), but the link doesn't supply it.

Nothing else came up. Lemma 1's uniqueness via h = f∘r is fine. Corollary 5 correctly gets its hypotheses: the pushout exists because j_1 and j_2 are split monos, regularity gives pullback-stable regular epis and equalizers, and cocongruences are coreflexive and jointly epic.

This is an AI review, not a proof of correctness. The author still has to check every argument thoroughly.

[ScriptRaccoon]

About Claude's review on effective cocongruences: looks right to me, but easy to fix.

[ScriptRaccoon]

I have rebased again to include the change from #430. Long proofs look much better now, especially for $\omega$-sets. (By the way, #428 also has improved readability a lot.)

[dschepler]

I think I've addressed all the new comments and the Claude reviews. I also added the previously mentioned simplified proof that the category does not have an $\mathbb{N}$-indexed copower of 1.

[ScriptRaccoon]

Alright. I did a few other adjustments, please check them.
You can then rebase again and reduce the whole thing to two commits, if you want to.
I think it makes sense that you are the author and that the description mentions me as co-author.

[dschepler]

Alright, I've gotten the rebase to the state I want it, with author and date fields reset and "Co-authored-by" trailers added in both commits.

[ScriptRaccoon]

Can you do a final rebase? Then I will merge.

[dschepler]

Can you do a final rebase? Then I will merge.

Done.

[ScriptRaccoon]

We didn't notice that the new implication

extensive + regular + quotients of congruences => effective cocongruences

automatically proves that Unif is not regular, and hence does not have pullback-stable regular epis. The non-trivial "ad hoc" proof can be removed. I will make the redundancy check a part of CI now, otherwise we keep forgetting these things.

PS: #437