Congruence quotients

[dschepler]

Add property of having quotients of congruence relations, and its dual.

Currently undecided categories for having quotients of congruences:
none

Currently undecided categories for having coquotients of cocongruences:
none

[dschepler]

For category of metric spaces with continuous maps: I could probably make an argument it would imply having all sequential colimits, and reach a contradiction based on the previously existing database entry. I would do this by forming the set-level equivalence relation involved in the sequential colimit, showing that this set with the subspace metric forms a congruence, and then showing that congruence's quotient would have to be a sequential colimit.

[dschepler]

For the category of schemes, I wonder if I could adapt the example of pushout failure by using the relation $k(x,y) \sqcup Z(x-y)$ in $\mathbb{A}^1 \times \mathbb{A}^1 \simeq Spec ~ k[x,y]$.

[ScriptRaccoon]

Most of this is formal. Please add an implication which handles this. I guess we need an infinitary distributive category (maybe more).

[ScriptRaccoon]

Indeed the category of schemes does not have all quotients of congruences. The counterexample for missing pushouts from MO/9961 can be adjusted. But I think there is a general lemma behind this. Let me sketch it for now, maybe we can fill in the details.

Lemma: Assume that $C$ is category which is (finitary) distributive and has disjoint finite coproducts. Assume further that it has quotients of congruences. Then any pair of monomorphisms $f : S \to X$, $g : S \to Y$ has a pushout.

(Unfortunately, I don't know if all pushouts need to exist.)

Proof: Let $W = X + Y$, so that $W \times W = (X \times X) + (Y \times Y) + (X \times Y) + (Y \times X)$. Let $E := X + Y + S + S$ and define $E \hookrightarrow W \times W$ by $\Delta_X$ on $X$, likewise on $Y$, by $(f,g) :S \to X \times Y$ on the first copy of $S$, and by $(g,f) : S \to Y \times X$ on the second copy of $S$. This is a congruence. Intuitively, it is the smallest congruence satisfying $f(s) \equiv g(s)$. So any quotient is a pushout of $f$ and $g$.

[ykawase5048]

Congruences (internal equivalence relations) can be naturally defined in arbitrary categories without finite limits:
A congruence on an object $X$ is a parallel pair $R\rightrightarrows X$ such that the induced morphism $yR \to yX\times yX$ in the presheaf category is monic and is an equivalence relation (pointwise).

[ScriptRaccoon]

Congruences (internal equivalence relations) can be naturally defined in arbitrary categories without finite limits: A congruence on an object X is a parallel pair R ⇉ X such that the induced morphism y R → y X × y X in the presheaf category is monic and is an equivalence relation (pointwise).

I have thought about this as well while reviewing the PR but came to the conclusion that we should keep the assumption here.

[dschepler]

With the removal of the incorrect links to reflexive coequalizers, now the case of free abelian groups is undecided.

Of course, if this were the category of torsion-free abelian groups, then we could just take the torsion-free part of the abelian group quotient. But in this case, maybe there's some theorem about extending a basis of a "saturated" subgroup to a basis of the full group -- "saturated" meaning $nx \in H \rightarrow x \in H$? In which case the quotient group by the saturation of the subgroup corresponding to the congruence would have basis given by the images of the extension vectors, and it would form a quotient in FreeAb.

On the other hand, we again have an existing database entry about not having sequential colimits...

[dschepler]

Maybe a common lemma, to be used for both Met_c and FreeAb, could be something like: Suppose you have a faithful (and exact?) functor U : C -> Set, and suppose furthermore that for each object X of C and subset S of U(X), there exists a subobject S' of X such that (fill in what's needed here). Then if C has quotients of congruences, then C has sequential colimits. (In the case of Met_c, that subobject would be the subspace metric construction; in the case of FreeAb, that subobject would be the generated subgroup, which is free again by the theorem about subgroups of free groups.)

[dschepler]

On the other hand, maybe I could put in the simple implication preadditive + has quotients of congruences -> has cokernels which would also resolve FreeAb.

[ykawase5048]

Congruences (internal equivalence relations) can be naturally defined in arbitrary categories without finite limits: A congruence on an object X is a parallel pair R ⇉ X such that the induced morphism y R → y X × y X in the presheaf category is monic and is an equivalence relation (pointwise).

I have thought about this as well while reviewing the PR but came to the conclusion that we should keep the assumption here.

In multi-algebraic categories, every congruence admits a coequalizer, in which finite limits don't exist in general. We may find other examples where congruences without finite limits play an important role. I strongly recommend adopting the general definition.

[dschepler]

Congruences (internal equivalence relations) can be naturally defined in arbitrary categories without finite limits: A congruence on an object X is a parallel pair R ⇉ X such that the induced morphism y R → y X × y X in the presheaf category is monic and is an equivalence relation (pointwise).

I have thought about this as well while reviewing the PR but came to the conclusion that we should keep the assumption here.

In multi-algebraic categories, every congruence admits a coequalizer, in which finite limits don't exist in general. We may find other examples where congruences without finite limits play an important role. I strongly recommend adopting the general definition.

Maybe we could make that into another property for those situations - something like "has representable quotients of Yoneda embeddings". (And off the top of my head, I wouldn't expect that to be equivalent to the current property even in finitely complete categories, since the corresponding subfunctors of Hom(-,X) x Hom(-,X) wouldn't necessarily be representable.)

[ykawase5048]

(And off the top of my head, I wouldn't expect that to be equivalent to the current property even in finitely complete categories, since the corresponding subfunctors of Hom(-,X) x Hom(-,X) wouldn't necessarily be representable.)

We define a (general) congruence as a special parallel pair of morphisms, so the corresponding subfunctor is trivially representable.

[dschepler]

We define a (general) congruence as a special parallel pair of morphisms, so the corresponding subfunctor is trivially representable.

Oh, right. So, that could be "has quotients of congruence pairs". Or, if @ScriptRaccoon changes their mind, I'd be happy to use the more general definition (and see what new unresolved categories get exposed - in that case, I could need some help with the implications you've mentioned related to multi-algebraic categories).

[dschepler]

Indeed the category of schemes does not have all quotients of congruences. The counterexample for missing pushouts from MO/9961 can be adjusted. But I think there is a general lemma behind this. Let me sketch it for now, maybe we can fill in the details.

Lemma: Assume that C is category which is (finitary) distributive and has disjoint finite coproducts. Assume further that it has quotients of congruences. Then any pair of monomorphisms f : S → X , g : S → Y has a pushout.

(Unfortunately, I don't know if all pushouts need to exist.)

Proof: Let W = X + Y , so that W × W = ( X × X ) + ( Y × Y ) + ( X × Y ) + ( Y × X ) . Let E := X + Y + S + S and define E ↪ W × W by Δ X on X , likewise on Y , by ( f , g ) : S → X × Y on the first copy of S , and by ( g , f ) : S → Y × X on the second copy of S . This is a congruence. Intuitively, it is the smallest congruence satisfying f ( s ) ≡ g ( s ) . So any quotient is a pushout of f and g .

I think we might need to add extensivity to prove transitivity, since for that one pullbacks are involved.

So yes, eventually I think we could put an implication "extensive + quotients of congruences -> pushouts of monomorphisms" - though I certainly wouldn't want to introduce a new property to this PR and risk it growing out of scope like the previous one.

[ScriptRaccoon]

In multi-algebraic categories, every congruence admits a coequalizer, in which finite limits don't exist in general. We may find other examples where congruences without finite limits play an important role. I strongly recommend adopting the general definition.

My idea was that assuming finite limits is in alignment with many other properties where other properties are assumed beforehand even though they are not strictly necessary - it just makes things more convenient. Typical example: "exact filtered colimits". Here I assume that both finite limits and filtered colimits exist. (For a good reason, otherwise the 3 equivalent characterizations would not be equivalent anymore!)

But I trust your expertise here when you say it is better to omit finite limits here. And you can also change the definition now @dschepler and see how the PR evolves. This is the nice thing about git, we can always go back (unless one force pushes all the time like myself ...).

So, that could be "has quotients of congruence pairs".

For now, let's not have two properties in the database which sound very similar.

So yes, eventually I think we could put an implication "extensive + quotients of congruences -> pushouts of monomorphisms" - though I certainly wouldn't want to introduce a new property to this PR and risk it growing out of scope like the previous one.

For this, we have lemmas, see #41. Here is a recent example.

[dschepler]

I just tried a quick experiment removing the implication "quotients of congruences -> finitely complete" and removing the hypothesis of finitely complete where appropriate (for example, I couldn't remove it from the implication of congruence quotients -> cokernels because it depends on constructing a kernel of a map from $X^2$). Once I added back in the implication "reflexive coequalizers -> quotients of congruences" which I guess I was too hasty to remove, that leaves as undecided cases:
For quotients of congruences: category of sets and relations, category of smooth manifolds.
For coquotients of cocongruences: category of non-empty sets, category of sets and relations, category of smooth manifolds, simplex category.

(For smooth manifolds, it's of course tempting to try the congruence identifying two points of a line. But as usual, just because the topological space quotient isn't a manifold doesn't mean there isn't a quotient in the subcategory. For example, it could be that $S^1$ works as a quotient.)

[ScriptRaccoon]

Cool! Thanks for adding this. I was hoping that you could fill in the details for my proof sketch. Your proof is even shorter than my sketch :D

[ScriptRaccoon]

Looks very good already! Maybe we can settle the remaining cases as well.

If time permits, please have a look at the open comments.

[dschepler]

I just realized that the "Malcev" property also involves congruences and in that case the decision was to assume the category was finitely complete.

[ScriptRaccoon]

I just realized that the "Malcev" property also involves congruences and in that case the decision was to assume the category was finitely complete.

Yes. This is part of Definition 2.2.3 in Borceux-Bourn.

[dschepler]

Well, I ended up showing RelSet has quotients of congruences, but the proof was fairly long. It's the sort of proof where you gather bits of information little by little, until eventually you can put together enough to classify the congruences (and there aren't that many of them). Given how long it turned out, I'm wondering if it might make sense to move it to "lemmas" even though it's probably not of use for anything else.

[dschepler]

At this point, the only unresolved case is: does Man have coquotients of cocongruences. Given the picture of a cocongruence on X in a concrete category looking like a branching of X into one or two parts at various points, I'd strongly suspect that means the number of branches is locally constant, so the equalizer where you have one part is an open subset of X. From the Hausdorff property of E it's easy to see where you have two parts is open but that doesn't help.

[dschepler]

That would also leave the proof for Met_c which I've been thinking about but haven't yet found a good way to generalize the argument.

[ScriptRaccoon]

@dschepler @ykawase5048 Remark: after I merge #119 and you pull the change, you need to update your local .env file (see the updated .env.example as a guideline), since location of the local databases will be different. I will inform you when I merge.

[dschepler]

In multi-algebraic categories, every congruence admits a coequalizer...

Does that mean it would be appropriate to add an implication "multi-algebraic -> has quotients of congruences"? And if so, is there a citation you can provide for the proof entry? (Though it doesn't look like it would add any resolved entries in the current state of the database, it could be useful in the background for future categories.)

[dschepler]

I've now filled in an entry for Man on coquotients of cocongruences. With that, all current categories are settled for the new properties.

[dschepler]

In multi-algebraic categories, every congruence admits a coequalizer...

Does that mean it would be appropriate to add an implication "multi-algebraic -> has quotients of congruences"? And if so, is there a citation you can provide for the proof entry? (Though it doesn't look like it would add any resolved entries in the current state of the database, it could be useful in the background for future categories.)

Actually, I guess we already have the chain of implications multi-algebraic -> generalized variety -> sifted colimits -> reflexive coequalizers -> quotients of congruences so we don't need to add an explicit implication there.

[dschepler]

Now I'm worried... The proof I found for Man would seem to apply for any coreflexive equalizer, but the implications say Man doesn't have general coreflexive equalizers. So, I may have to trace through the implications from a failure to have pullbacks, in order to see whether my proof is flawed, or if I'm OK and I just missed something I used that's not true in the general coreflexive equalizer case. It might be a while before I can get enough time to devote to the detailed analysis, though.

[dschepler]

OK, in the general case of a coreflexive equalizer $X \rightrightarrows Y$ you don't necessarily require $X + X \to Y$ to be an epimorphism, so in the case of Man, Y could certainly have higher dimension than X. On the other hand, I forgot that the epimorphism only has to have a dense image at the level of sets, so I'm not sure whether the part about fibers of one or two points would necessarily hold. Given the setup it seems unlikely to be able to have something like a "spirograph curve" as the epimorphism, but I'd have to think about that some more.

[ScriptRaccoon]

Since #119 is now merged, a big rebase is required. (I can also do it if you prefer.)

Also, because of the new location of the local database files, .env needs to be adjusted (this is not part of the repo, hence this message).

[ScriptRaccoon]

I must say that I don't understand this proof.
e.g. why must f(i), g(i) be adjacent?

[ScriptRaccoon]

Well, I ended up showing RelSet has quotients of congruences, but the proof was fairly long. It's the sort of proof where you gather bits of information little by little, until eventually you can put together enough to classify the congruences (and there aren't that many of them). Given how long it turned out, I'm wondering if it might make sense to move it to "lemmas" even though it's probably not of use for anything else.

I will have a look at this proof. For now, let me just remark that there is also an option to just put a pdf into the /static/pdf folder and link to it. This can be used for longer proofs, or proofs which require complicated diagrams. This has been done once before: #43

(I am not happy that we have basically four ways to add proofs: property assignment reasons, implication reasons, lemmas, pdfs. And for the foundations I also built a markdown renderer. There should be just one way ... But for now it is what it is.)