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...

[dschepler]

Another idea I had for Ring which ended up not panning out: defining the congruence relation as having $y-x$ which is divisible. But then I found that divisibility structure isn't necessarily unique, for example when applied on

[ Z Q/Z ]
[ 0 Z   ]

so that's likely to have issues with not respecting equalizers, or with not giving an epimorphism to the representing object if adjoining a concrete divisibility structure such as an abelian group homomorphism $\mathbb{Q} \to (R, +)$ with $1 \mapsto y-x$.

[dschepler]

I wonder if there might be group theorists at MO who might have ideas. Especially if we give the concrete versions in terms of systems of equations in $2 \times \kappa$ variables which induce a partial equivalence relation on $G^\kappa$ for each $G$ (including $F(\kappa)$ so that can also be expressed as the existence of formal implications of symmetry and transitivity in the system). And the question becomes: is that always equivalent to a system of the form $f_i(\vec x) = e, f_i(\vec y) = e, g_j(\vec x) = g_j(\vec y)$.

[ScriptRaccoon]

Funny coincidence, since I also wanted to ask on MO right now, but I wanted to coordinate this with you first. Personally, I would like to ask the question about Z first, with the reformulation I gave above. But you can go ahead...

Just to reiterate: I would like to avoid working with words in free groups at all costs, and rather try to use the functorial POV.

PS: I also made several attempts to get an answer from Google Gemini, but they failed.

[dschepler]

Sure, I would be fine with starting with asking about the simple case first. (Feel free to add some of my non-counterexamples if you'd like to use them to illustrate some of the complexities of the question, e.g. $a b^{-1} = a^{-1} b$ as a disguised version of the $n=2$ case, or $(a b^{-1})^2 = e$ as a case where reflexivity and symmetry hold but not transitivity. Another example with reflexivity and symmetry hold but transitivity fails comes from $S_3$ as a corelation on $C_2$, with the maps to (1 2) and (2 3). That has presentation $\langle x, y \mid x^2=1, y^2=1, xyx=yxy \rangle$. But that fails transitivity for example in $S_4$ with elements (1 2), (2 3), (3 4). EDIT: Though that's not an example of the simplified case of course.)

[dschepler]

It's funny enough you mentioned Google Gemini - I had my first session with it on a mathematical question yesterday, regarding my question about whether a divisibility structure on an element of the additive group of a ring is necessarily unique. It had several false starts, where I had to point out a flaw in the reasoning - including some first answers where it thought the result was true - until eventually it reminded me of the construction of adjoining a unit to the rng on Q/Z with zero multiplication.

[ScriptRaccoon]

I made another attempt with Google Gemini (Pro). This time, the proof looks good. I will spend more time, but for now I cannot find a mistake. (Click for a larger version.)

About that "subgroup theorem for amalgamated free products": probably the name is a hallucination, but the statement appears to be true based on the usual element structure.

Relevant: https://www.researchgate.net/publication/266843789_Subgroups_of_amalgamated_free_products

[dschepler]

I wonder if that proof simplifies in any significant way for the special case $G = \mathbb{Z}$, to give some insight into what the proof is doing in that situation. I guess at least $D,X,Y$ become cyclic subgroups.

[dschepler]

Also, unless I'm missing it somewhere, it doesn't use cosymmetry. So, that would imply for example that any representable functor giving a preorder on each group in fact gives an equivalence relation on each group - which I guess isn't that surprising.

[ScriptRaccoon]

Here is my "human" proof that cocongruences in Grp are effective, which is just a slight variation of Gemini's proof. The vague citation of the "subgroup theorem for amalagamted free products" is replaced by a direct argument using the well-known description of the elements of a pushout.

cocongruences_grp.pdf

If you have verified it, I can add a commit which adds it (pdf + tex + Grp.sql).

Ah and yes, cosymmetry is not needed.

EDIT: I am currently also rewriting the proof and making it more general