Add the category of Jónsson-Tarski algebras

[ScriptRaccoon]

This PR resolves #89. It adds the category of Jónsson-Tarski algebras, aka Cantor algebras. This is finitary algebraic and a Grothendieck topos.

All properties have been decided. For two of these (Malcev, cofiltered-limit-stable epis), two results about topoi have been added. This made it possible to remove several manual assignments from other categories.

[ScriptRaccoon]

@dschepler Do you see why epis are surjective here?

[dschepler]

@dschepler Do you see why epis are surjective here?

Maybe make use of the description as a Grothendieck topos, where the site is the delooping space of the free monoid on ${ \ell, r }$ and the topology is generated by the sieve ${ \ell, r }$. More concretely, the covering sieves are the ones that induce covers of the Cantor space ${ 0, 1 }^\omega$. That means a morphism $X \to Y$ is epi if and only if for each $y \in Y(\bullet)$ there is a cover ${ m_i : F({ \ell, r }) }$ such that for each $m_i$, there exists $x_i \in X$ such that $m_i^* x_i \mapsto m_i^* y$. Using compactness of ${ 0, 1 }^\omega$, you can find a finite subcover, and then use the "mixing" operator $m$ appropriately to reconstruct an $x \in X(\bullet)$ such that $x \mapsto y$. Or equivalently, we may assume without loss of generality that the covering sieve is disjoint, and then use the sheaf property on $X$. (More formally, it might work to do a proof by "structural induction" on the covering sieve.)

[dschepler]

On the Malcev property: it seems like any elementary topos which is Malcev would have to be trivial, since then the $\rightarrow$ relation on $\Omega$ would have to be symmetric so $\top \le \bot$.

[dschepler]

@dschepler Do you see why epis are surjective here?

For a much simpler proof: being a Grothendieck topos, the category is epi-regular. And then viewing it as a finitary algebraic category, we know the regular epimorphisms are just the surjective homomorphisms.

[ScriptRaccoon]

For a much simpler proof: being a Grothendieck topos, the category is epi-regular. And then viewing it as a finitary algebraic category, we know the regular epimorphisms are just the surjective homomorphisms.

Ah, of course. Thanks!

On the Malcev property: it seems like any elementary topos which is Malcev would have to be trivial, since then the → relation on Ω would have to be symmetric so ⊤ ≤ ⊥ .

Yes, this works. That's very nice. With this implication I could remove 7 manual assignments! (see recent commit)

It seems we don't need ccc for this. Maybe something like subobject classifier, finite limits, and distributive (?) will be sufficient (to conclude that Malcev => trivial). But I haven't thought about the details.

[ScriptRaccoon]

Regarding cofiltered-limit-stable epis, I expect that we can also formulate a general result. Idea:

elementary topos + countable coproducts + cofiltered-limit-stable epis ===> trivial

Sketch: Let $N = \coprod_{n} 1$, this is a NNO (nno_criterion). The maps $N_{\geq n} \to 1$ are (split) epis, so their limit $0 = \bigcap_{n} N_{\geq n} \to 1$ is an epi. It must be a regular epi, but $0$ is a strict initial object, so $0 \to 1$ is an isomorphism, and then $X \cong X \times 1 \cong X \times 0 \cong 0$.

At least, this is the proof in Set. The question is if this really works in an elementary topos.

EDIT: yes I think this works, but maybe we can make the assumptions a bit weaker

[dschepler]

It seems we don't need ccc for this. Maybe something like subobject classifier, finite limits, and distributive (?) will be sufficient (to conclude that Malcev => trivial). But I haven't thought about the details.

Yes, just from a subobject classifier and finite completeness, the subobject classifier is canonically a pre-Heyting algebra object. The $\land$ operation, of course, corresponds to intersections (aka pullbacks of monomorphisms). The $\rightarrow$ operation is then defined on subobject posets by: $A \rightarrow B$ is the equalizer of the characteristic morphisms of $A\cap B$ and $A$. The proof this respects pullbacks, and therefore induces a morphism $\Omega \times \Omega \to \Omega$, is again entirely formal.

And then, even if you don't assume the existence of $\bot$, by replacing it with any characteristic morphism, you conclude that every monomorphism is an isomorphism. Applying that to equalizers, you get that the category is thin. That being the case, every morphism is a monomorphism, so you get a groupoid. And of course, having a terminal object implies the category is also connected.

[ScriptRaccoon]

Thanks! What is a pre-Heyting algebra? ("pre")

So you are saying the result is

subobject classifier [which included finite limits by convention] + Malcev ===> thin

?

[dschepler]

Thanks! What is a pre-Heyting algebra? ("pre")

It's the fragment of the Heyting algebra theory involving just $\top$, $\wedge$ and $\rightarrow$, without necessarily requiring the $\lor$ or $\bot$ operations. In other words, it's a $\wedge$-semilattice with a top element, and a binary $\rightarrow$ operation satisfying $a \le (b \rightarrow c)$ if and only if $(a \wedge b) \le c$. So, a pre-Heyting algebra is equivalent to a small thin category with finite products which is cartesian closed (whereas the thin category corresponding to a Heyting algebra also has finite coproducts).

So you are saying the result is

subobject classifier [which included finite limits by convention] + Malcev ===> thin

?

The conclusion is: subobject classifier + Malcev [which both include finite limits by convention] ===> trivial. The first steps show any category with equalizers in which all monomorphisms are isomorphisms is essentially discrete.

[ScriptRaccoon]

I see. But the end of the proof, showing thin ===> trivial in that setting, can be done automatically with existing implications (in fact, thin + mono-regular + terminal object ===> trivial). Hence, when I only add
subobject classifier + Malcev ===> thin
to the database, it can automatically deduce
subobject classifier + Malcev ===> trivial.

The question is which version I should add?

Adding subobject classifier + Malcev ===> thin has the advantage that it is minimal and does not repeat arguments. In the proof, I can also add a remark like (And from here, we can infer that it is trivial.) in the end. I have done this before with the implication nno_terminal which says NNO + strict-terminal object ===> one-way (which actually yields ===> thin).

Adding subobject classifier + Malcev ===> trivial has the advantage that it is stronger and clearer. But it repeats arguments.

WDYT? @dschepler

---

For now I went with "thin". I will merge this PR now since the number of open PRs troubles me, but I can change this later directly on main.