Has effective (co)congruences properties

[dschepler]

I just started a trial run of the property of having effective congruences; and so far, it's not going well. I only found a couple basic properties to put in, along with a preliminary version of the theorem that a pretopos is balanced; but there are still 34 unresolved cases for congruences and 50 unresolved cases for cocongruences. I don't even know whether Group has effective cocongruences. And certainly, there are a lot of cases I could fill in by hand, but that would be a lot of individual entries to maintain.

Any ideas would be welcome on how to proceed.

(I know this is still draft and has several places that need details or citations filled in; at this point I'm just posting to give an idea of the current status.)

[dschepler]

Current status: For "has effective congruences" there are two unresolved cases left:
category of Banach spaces with linear contractions
category of pseudo-metric spaces with non-expansive maps

(For the second, I think I might be able to adapt the proof of extensive + has effective congruences -> balanced, by considering $(0, 1) \hookrightarrow [0, 1]$ to bound distances within components, then placing copies "far enough" from each other for the construction to still work even if it's not making a coproduct. I'd still have to think about the details and whether they work out. For the first, obviously that trick won't work.)

For "has effective cocongruences" there are still 21 unresolved cases. Among them are Group and Ring which are blockers.

[ScriptRaccoon]

I am not surprised that deciding effective cocongruences for concrete categories is so hard. This amounts to a classification of all cocongruences, and this is hard, as we already saw in Rel for example, but also Set is a good starting point, where it is not trivial. Often we do not even understand all epimorphisms.

I suggest that in this PR we only try to fill the remaining cases where it is required by the unit tests (Grp and Ring).

EDIT. I am pretty confident that for Grp the answer is yes, cocongruences are effective.

[dschepler]

Heh, ended up coming back to #114 and also using it to prove elementary topoi have effective cocongruences.

[ykawase5048]

Suggestion. The implication "lsfp → effective congruences" can be refined by "multi-algebraic → effective congruences". Note that the database already includes the implication "lsfp → multi-algebraic". The reference is Thm. 4.0 in Diers's paper (fr) or it's English translation.

[dschepler]

I am pretty confident that for Grp the answer is yes, cocongruences are effective.

Do you have any ideas on how we might prove that? So far, I haven't made much progress even on the simplest case I can think of, proving that a cocongruence on $\mathbb{Z}$, $F_2 \twoheadrightarrow E$, necessarily has kernel normally generated by $a^n b^{-n}$ for some $n$.

[dschepler]

On Ring I was wondering if the counterexample in CommRing could be adapted there. If I trace through the proofs, I guess the counterexample in CommRing is something like $\mathbb{Z} \times \mathbb{Q} \times \mathbb{Q} \times \mathbb{Z}$ as a cocongruence on $\mathbb{Z} \times \mathbb{Z}$. But then again, if you have two maps $\mathbb{Z} \times \mathbb{Q} \times \mathbb{Q} \times \mathbb{Z} \to R$ then the corresponding idempotents of $R$ don't necessarily have an idempotent as product, so that might not extend to a cocongruence on Ring.

Any other ideas on Ring?

[ScriptRaccoon]

Do you have any ideas on how we might prove that? So far, I haven't made much progress even on the simplest case I can think of, proving that a cocongruence on Z , F 2 ↠ E , necessarily has kernel normally generated by a n b − n for some n .

I don't have a proof for Grp, I just voiced my strong suspicion that it is true. Let me explain this a bit.

Here is a formulation that I find quite instructive: a cocongruence on a group $U$ is a way of putting equivalence relations on the hom-sets $hom(U,G)$ for all groups $G$, such that

• homomorphisms $h : G \to G'$ preserve it
• they are compatible with limits $G = \lim_i G_i$

So we have an equivalence relation $f \sim g$ for homomorphisms $f,g : U \to G$, such that $f \sim g \implies hf \sim hg$ for $h : G \to G'$, and when $G = \lim_i G_i$, then $f \sim g$ iff $p_i f \sim p_i g$ for all $i$.

We also need that the equivalence relation on $hom(U,-)$ is representable, but in many cases this follows because of the limit compatibility. (The only thing left is accessibility, right?)

It is effective when there is a subgroup $V \subseteq U$ such that the equivalence relation is given by $f \sim g \iff f|_V = g|_V$.

(All that holds similarly for general categories, but I find it instructive to write it down in this special case.)

The special case $U = \mathbb{Z}$ means: on the underlying set of any group $G$ we have a natural equivalence relation (we could call it "universal") which is limit-compatible, and we need to find $n \in \mathbb{Z}$ such that it is given by $a \sim b \iff a^n = b^n$. This is an interesting classification result (if true).

And here is why I think it is true: I would literally fall off my chair if somebody writes down an equivalence relation (with the mentioned properties) that does not have this form (for general groups). Yes, this is no proof.

What I find remarkable is that this does not seem to be trivial at all for Ab, but your (almost formal) implication preadditive_kernels_normal_imply_effective_congruences handles this case automatically. Maybe here my POV of ignoring the representable object is not ideal. But still, I think we can use $\mathbb{Q} / \mathbb{Z}$ to find the number $n$, alongside with the lemma that (in the abelian case!) the equivalence relation is actually a subgroup.

From this we get some global $n$ such that $a \sim b \iff a^n = b^n$ when $a$ and $b$ commute. But for non-abelian groups, I have no clue (yet). Since Grp is mono-regular, one can show that the relation descends to subgroups. In particular, it suffices to look at 2-generated groups, at least in theory. Free groups are of no use since here powers cancel.

Random remark: We are proving here that Grp does not satisfy the second half of the definition of being Barr-coexact. But we already know that it is not coregular anyway (the first half of the definition).

Question: I just saw that you have proven that CRing does not have effective cocongruences (using pretopos_balanced), which I find quite surprising. How does the counterexample look like in the description above?

[dschepler]

Yes, that's precisely the line of thought I was going along. One thought which occurs is that the equivalence relation of conjugacy is preserved by homomorphisms. However, it's not representable (at least I think it isn't, else you'd essentially get a counterexample to Grp being epi-regular). Another thought: Any proof is going to have to take into account the cotransitivity map in some way. For example, the relation $(a b^{-1})^2 = 1$ is certainly reflexive and symmetric; but it's not transitive, as you can see for example in a dihedral group with $b$ being a reflection and $a,c$ being arbitrary rotations.

As for the example in CRing, I think the counterexample is a corelation on $\mathbb{Z} \times \mathbb{Z}$. I could simplify it a bit by using $\mathbb{Z}[1/2]$ instead of $\mathbb{Q}$. Here $\mathbb{Z} \times \mathbb{Z}$ represents the functor taking a ring to its idempotents; and the equivalence relation represented by $\mathbb{Z} \times \mathbb{Z}[1/2] \times \mathbb{Z}[1/2] \times \mathbb{Z}$ is that two idempotents $e_1, e_2$ are equivalent if and only if 2 is invertible in the rings $e_1 (1-e_2) R$ and $(1-e_1) e_2 R$. I guess the picture under Spec makes it clearer why this is an equivalence relation, involving the cross terms both missing the point $\langle 2\rangle$. Maybe a similar example using $\mathbb{C}[t]$ and $\mathbb{C}[t,1/t]$ would make an example that's easier to think about geometrically, now with two maps to $\mathbb{A}^1+\mathbb{A}^1$ being equivalent if the projections to $\mathbb{A}^1$ are equal and if the cross terms both miss 0. Except algebraically that complicates the picture because now you also have to keep track of elements of the ring along with idempotents, and maybe now you want $a=b$, and for $e_1 (1-e_2) a$ and $(1-e_1) e_2 a$ to be units in their respective rings.

Anyway, as far as I can tell, all that breaks down completely in noncommutative rings since you no longer have $eR$ forming a sub-rng.

[ScriptRaccoon]

Ok. I haven't thought about this long, but why cannot we take $eRe$?

Also, images of two commuting idempotents are still commuting. So their product is still idempotent.

For groups, the conjugation relation is not limit-preserving. I think we can say straight away that the equivalence relation must be some algebraic equation.

[dschepler]

Hmm... OK, I guess maybe an idempotent would split a ring into $\begin{bmatrix} eRe & (1-e)Re \ eR(1-e) & (1-e)R(1-e) \end{bmatrix}$ or something along those lines.

For the comments on groups: yes, certainly in the general case if you take a presentation $(A, R)$ of $X$, then from generators of the kernel of $FA+FA \to E$ you get some algebraic equations in terms of some number of paired variables, which form an equivalence on tuples satisfying the relations $R$. EDIT: For a slightly different point of view but equivalently, the equations define a partial equivalence relation whose natural domain is the tuples satisfying the relations from $R$. (Of course that description only works for algebraic categories which are epi-regular.) The thing is that those equations could nomimally involve cross terms and the proof would have to find some way to detangle the cross terms, either implicitly or explicitly. The example I have in mind is that $E := \langle a, b \mid b^{-1} a = b a^{-1} \rangle$ as a corelation on $\mathbb{Z}$ is a disguised version of the relation $a^2 = b^2$. (I guess maybe that's another reason why the proof is so easy in R-Mod: you can just move cross terms to the other side. :) )

[dschepler]

For another example I have in mind, in the full subcategory of integral (or cancellative) commutative monoids, the equivalence $(a, b) \sim (c, d)$ if and only if $a+d = b+c$ is representable, but not effective. Of course, there's no reason to believe that category is particularly well-behaved...

[ScriptRaccoon]

Here is how I would write down the proof. I like to work with generalized elements, since for me it makes the proof more easy to understand and also the motivation (=translating the proof from sets) more clear. Furthermore, I don't need to introduce notation for morphisms.

---

Notice that ' needs to be written as '' in SQlite, hence all these '' below. They get rendered as '.

Let $\alpha : A \to B$ be a monomorphism (and also an epimorphism, which we only need later). Let $B''$ be a copy of $B$, and likewise $A''$ be a copy of $A$. Consider the congruence on $B + B''$ generated by $\alpha(a) \sim \alpha(a)''$ for $a \in A$. Formally, we define $E := B + B'' + A + A''$ and define the two morphisms $f,g : E \rightrightarrows B + B''$ by extending the identity on $B + B''$ and
$$f(a) = \alpha(a),\quad f(a'') = \alpha(a)'',$$
$$g(a) = \alpha(a)'',\quad g(a'') = \alpha(a),$$
on generalized elements. Extensitivity can be used to show that $f,g$ are jointly monomorphic. Clearly, the pair $f,g$ is reflexive and symmetric. For transitivity, one uses again extensivity. By assumption, there is a morphism $h : B + B'' \to C$ such that $f,g$ is the kernel pair of $h$, that is, two generalized elements $x,y \in B + B''$ satisfy $h(x)=h(y)$ satisfy iff $x=f(e)$, $y=g(e)$ for some $e \in E$. In particular, we have $h(\alpha(a)) = h(\alpha(a)'')$ for all $a \in A$. Now assume that $\alpha$ is also an epimorphism. Then we get $h(b) = h(b'')$ for all $b \in B$. Then for all $b \in B$ there is some $e \in E$ with $b = f(e)$ and $b'' = g(e)$. Hence, there is some $a \in A$ with $b = \alpha(a)$ and $b'' = \alpha(a)''$. This shows that $\alpha$ is surjective on generalized elements, i.e. that $\alpha$ is a split epimorphism. Since $\alpha$ is also a monomorphism, we win.

[dschepler]

I'll take a closer look at the comments this evening. For now, I think among the (easy to trivial) lemmas I'll use to plug the gaps in proofs for subcategories will be: If $f, g : E \rightrightarrows X$ is a congruence which has a quotient $p : X \to X/E$ and which is effective, then in fact we get a cartesian square with $f, g, p, p$. And: If $U : \mathcal{C} \to \mathcal{D}$ is fully faithful, and $U$ applied to a square (not necessarily even a commutative square in the assumptions) gives a cartesian square, then the original square was cartesian as well.

So, for example, the proof that FinGrp has effective congruences would be: take the coequalizer in the category of groups, which is finite; then we get a cartesian square in Grp involving the quotient; so we also get the required cartesian square in FinGrp.

[dschepler]

I'm out of time for this evening. I think I addressed most of the comments, though at the moment I'm not happy with the expanded wording on the $\mathbf{Top}_*$ example. I think maybe the more general lemma there is: if a base category is extensive, and a coslice category has effective congruences, then the base category also has effective congruences.

[dschepler]

Regarding generalized elements, I wonder which of the following notations (treating a general category as "being like" a category of sheaves to some extent or another) you accept:
$X(U)$ as a notation for $\mathrm{Hom}(U, X)$
$f(x) \in Y(U)$ for $f : X \to Y$, $x \in X(U)$ as a notation for $f \circ x$ (I see you used this one in the restatement of the proof)
$\alpha^* x \in X(V)$ for $\alpha : V \to U$, $x \in X(U)$ as a notation for $x \circ \alpha$.

[ScriptRaccoon]

Regarding generalized elements, I wonder which of the following notations [...] you accept:

all of them! :)

[dschepler]

It almost looks like this could be generalized to a statement about adjoint pairs (in this case the left adjoint being $X \mapsto A+X$ from $\mathcal{C}$ to $A \backslash \mathcal{C}$ and the right adjoint being the forgetful functor from $A \backslash \mathcal{C}$ to $\mathcal{C}$) -- except that we're also making essential use of the specific form of the left adjoint as a disjoint coproduct.

[ScriptRaccoon]

Great to see all the progress here!

Please keep me updated and tell me when you think it is done. Then I will do another review.

I have just merged #142. Can you please rebase and make the adjustment in TorsFreeAb.sql where I already wrote a comment? That is, replace the property in the last assignment with effective congruences and adjust the text accordingly.

I haven't thought about if TorsFreeAb has effective cocongruences. Maybe it is already deduced automatically. But if not, maybe you can find a proof.