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 (outdated, see next comment)

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

Ah and yes, cosymmetry is not needed.

[ScriptRaccoon]

I have improved the proof in many ways and also generalized it. You can have a look at the commit I just added.

I find this result quite beautiful!

So only Ring is missing to make (current) unit test work (we can always change that test if the challenge is too big!). But tbh I also would like to know the answer for Mon.

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

[ScriptRaccoon]

Maybe #149 has some (minor) interesting consequences for this PR.

... and merge conflicts, sorry!

[dschepler]

The nature of this counterexample, along with my failure to find counterexamples on small finite $X$, leads me to the conjecture that the category of complete metric spaces with non-expansive maps does have effective cocongruences.

[dschepler]

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

I think it is done and ready for review. (Unless you want me to rebase instead of leaving the merges as is, in which case I would probably have to come back to that tomorrow.)

[ScriptRaccoon]

Great!

I will do a detailed review now. I will also make some commits with minor edits if required.

Regarding rebase, I will write a separate comment. That will only be relevant before we merge, so not now.

[ScriptRaccoon]

I added a commit with various minor adjustments. Most of them improve the readability of the formulas. Please check these files because I made a bit more there:

• 005_additional-structure-implications.sql (used a calculation with generalized elements)
• 001_lemmas.sql (changed the lemma title)
• FinGrp.sql (simplification of the proof)

In the proof of regular_epi-regular_extensive_consequences I would like to see more details in the paragraph "Since the $X$ pieces are already equalized by the kernel pair ...". Maybe using a bit more formulas would make it more clear what is happening here.

Apart from that, everything looks very good now. Thanks a lot for this massive work! This PR has added a lot of new material, both general results and interesting proofs for specific categories.

As for the merge, I would like to request two things:

• no merge commits
• only a few commits (max. 10)

How I would do it: Make sure that the main branch is uptodate. Then, in the feature branch, execute git rebase -i main. Change the order of the commits and squash them into each other when they are related.

For a more brutal approach, and I think this is necessary here: Execute git reset --soft main. Now, all commits are gone, but the changes are in the staging area. Unstage all files. Now, make a few commits based on topic, and commit all the changes per file. For this PR, the 3 commits could be:

• add properties: effective congruences / effective cocongruences

This commit contains the changes in the files 001_limits-colimits-existence.sql and 100_related-category-properties.sql.

• add results on congruences

This commit contains the changes in the files001_lemmas.sql and all the files in the folder /004_category-implications/.

• decide effective (co)congruences for most categories

This contains all other changes. (It can also be split into several commits, but not too many.)

When no file is left, force push viagit push -f.

I do not recommend merge commits. For future PRs, I suggest to use git rebase main instead.

This will yield a clean commit history in the main branch. Of course we lose some of the history during the development of this PR, but I don't think that any of this is relevant in the future. The results matter, and these are kept, of course.

These remarks apply to all PRs. I wanted to write already the same in #115 (which had 40 commits, which could be grouped to 3 commits as well), but didn't want to overwhelm you with "rules" (as if there weren't already enough).

So this is what I recommend, but if you have strong objections, or need help, please let me know.

[ScriptRaccoon]

Things like \mathbb{R} can be abbreviated to \IR after merging #152 . I wonder which PR we should merge first? How to minimize the work?

I think it makes sense to merge #152 first. I can also make the required adjustments here. There will be a merge conflict in TorsFreeAb.sql which is easy to handle.

[dschepler]

Things like \mathbb{R} can be abbreviated to \IR after merging #152 . I wonder which PR we should merge first? How to minimize the work?

I think it makes sense to merge #152 first. I can also make the required adjustments here. There will be a merge conflict in TorsFreeAb.sql which is easy to handle.

I see you just merged #152 a few minutes ago. I'm done with the other content revision you requested - so you can make the required adjustments if you want without worrying about stepping on my toes. Or, if you prefer, I can merge it and do the adjustments, and then do the requested history squash.

[ScriptRaccoon]

Ok I will do the adjustments now. This will hopefully make the rebase also easier. Remark: this means the formulas will not render properly for the time being ...

[ScriptRaccoon]

No wait, this does not make any sense. The process will be much smoother if we first incorporate the main branch with 152 in particular. This is because the macros are optional to use. But for using the macros, their definition is not optional ...

Can you first do* git reset --soft main and "collapse" the commits as explained in the other comment? (I don't want to do it since then all the commits will belong to me, but it's your work.)

Then I can go ahead and change the formulas.

*I just noticed that this produces quite a lot of files that have not been changed in your PR. This is the problem of merge commits, the history diverges too much ... I hope we don't need to repeat #97

[ScriptRaccoon]

It seems you managed to do it? :)

Ah regarding

Note that ScriptRaccoon scriptraccoon@gmail.com contributed many enhancements to
the proofs and presentation, and in particular contributed the proof that Grp has
effective cocongruences.

Maybe it is better to remove the additions for Grp then. I can commit this again. I have the TeX file here.

I totally forgot about that proof, isn't this months ago? :D

[dschepler]

Yes, the squash into 3 commits worked pretty smoothly as described. The only addition I needed to make was: after the git reset --soft main it still had all the branch changes staged, so I also needed to git reset and then do the selective adds and commits.

[ScriptRaccoon]

Alright. In case you didn't see my edit:

Maybe it is better to remove the additions for Grp then. I can commit this again. I have the TeX file here.

[dschepler]

In the proof of regular_epi-regular_extensive_consequences I would like to see more details in the paragraph "Since the X pieces are already equalized by the kernel pair ...". Maybe using a bit more formulas would make it more clear what is happening here.

I've just pushed a change to clarify things in terms of generalized elements.

I wonder if it would also make sense to remove the topos_is_co-Malcev implication which should be redundant now. Maybe it could make sense to move the citation from there to the comment you added at the end of regular_epi-regular_extensive_consequences.

[ScriptRaccoon]

Sorry for producing millions of merge conflicts ...

I wonder if it would also make sense to remove the topos_is_co-Malcev implication which should be redundant now.

Yes, let's remove it.

Maybe it could make sense to move the citation from there to the comment you added at the end of regular_epi-regular_extensive_consequences.

Yes. Please phrase it as optional information, since the reader already has the proof above.

I've just pushed a change to clarify things in terms of generalized elements.

Thanks! I will have a look.

EDIT. The proof is much better now. 👍🏼

[dschepler]

I've just done another rebase with the Grp contributions sorted into a separate commit (for which I used --author to credit you).

I also found online the git workflow where you establish a few topics up front, and then for subsequent commits to add to a topic you set a commit message of the form:
fixup! general results
More explanation for reviewers in the meantime before the next rebase

So that you prepare for using "git rebase -i --autosquash main" later.

I think I'll be using that workflow on future PRs. (And if you want, you can establish a topic or two for commits that you contribute and do the same.)

[ScriptRaccoon]

Yes I am familiar with that workflow. I have used it for a while, tbh I didn't really like it. With interactive rebase I can do the same much more easily, but that's just personal preference. Also, these things don't necessarily need to be done during the PR, only in the end! Please don't spend too much time rewriting the history during development, only here it was necessary, I guess (since there were no rebases to the main branch).

Thank you for adjusting the commit for Grp. I have now also added the (final?) commit where the LaTeX macros are added in. I didn't check every formula, but like 20 examples, and they looked fine.

So when you are ready, I will smash that merge button!

[dschepler]

So when you are ready, I will smash that merge button!

Sounds good to me!

[ScriptRaccoon]

✅

[ScriptRaccoon]

The proof that FreeAb does not have effective cocongruences seems to be generalizable, it looks very formal. Maybe a connection with balanced, here applied to $2 : Z \to Z$. We already have "effective congruences + extensive => mono-regular".

---

We will let $E$ be the abelian group with presentation $\langle a, b, c \mid a - b = 2c \rangle$, with two morphisms $Z \rightrightarrows E$ given by $1\mapsto a$, $1\mapsto b$. Note that $E$ is free with basis ${ b, c }$. Then $Hom(E, G) \cong \{ (x, y, z) \in G^3 \mid x - y = 2z \}$. Observe that since $G$ is torsion-free, the projection onto the first two coordinates is injective; and $(x, y)$ is in the image precisely when $x \equiv y \pmod{2G}$, which gives an equivalence relation. Therefore, $E$ gives a cocongruence on $Z$.
On the other hand, if $E$ were the cokernel pair of $h : H \to Z$, that would mean that for $x, y : Z \to G$, $x \equiv y \pmod{2G}$ if and only if $x \circ h = y \circ h$. In particular, from the case $G := Z$, $x := 2 id$, $y := 0$, we would have $2h = 0$. That implies $h = 0$, but then that would give $id_{Z} \equiv 0 \pmod{2}$, resulting in a contradiction.

[dschepler]

The proof that FreeAb does not have effective cocongruences seems to be generalizable, it looks very formal. Maybe a connection with balanced, here applied to 2 : Z → Z . We already have "effective congruences + extensive => mono-regular".

Maybe on the dual side, this generalizes to a proof of: additive + effective congruences => normal, forming a revision of the current additive_effective_congruences_imply_normal. The revised proof: given $i : X \hookrightarrow Y$, form the congruence of $\equiv \pmod{i(X)}$ as $E := X \times Y$, with one map being $(x, y) \mapsto y+i(x)$ and the other map being $(x,y) \mapsto y$.

I can do a quick PR for that this evening.