Categorization of equivalence relations

Stream: maths

[Robert Maxton]

Suppose I have an equivalence relation eqv : α → α → Prop. Does there necessarily exist an equivalent EquivLike, that is a way of representing that eqv as two antiparallel arrows that are inverses of each other?

(I believe this is equivalent to asking: is there always a way to turn a type α and an equivalence relation on α into a category, such that two objects of the category are isomorphic iff they are equivalent under eqv. But I'm not sure.)

[Joël Riou]

In mathlib, any preorder is equipped with a category structure: there is a (unique) map from x to y iff x is less than or equal y.

[Robert Maxton]

Sure, but that preorder structure works up to equality -- the antisymmetry property specifically asks you to prove that x ≥ y and y ≥ x implies x = y. I'm asking if anything breaks if I weaken that requirement to some specific definition of isomorphism.

[Robert Maxton]

I can see that if I have a reflexive, transitive relation that is antisymmetric up to isomorphism, then I can certainly make a poset out of that. And I can define my arrows according to r. But that assumes some specific r, and the same equality can be implied by the antisymmetry of multiple relations.

[Robert Maxton]

For example, given α := β × β and eqv a b := (a.1 = b.1) ∨ (a.2 = b2), both le on .fst and le on .snd are antisymmetric up to eqv, but they certainly aren't the same relation.

[Robert Maxton]

Well, that being said, that just means that there might different 'completions', different ways of defining the non-iso morphisms of the category, that have the same property that its isomorphisms are some specified equivalence....

[Robert Maxton]

... I guess what I want is a categorical limit on such categorical representations, or something. A limit in Cat, presumably?

[Mitchell Lee]

You can take the preorder to be the equivalence relation itself

[Robert Maxton]

Wouldn't that be minimal? ... I guess that would be the limit, but I guess I probably meant colimit then.

[Edward van de Meent]

I might not be getting the point, but i think your example is not an equivalence relation? It's not transitive.

[Edward van de Meent]

(assuming that beta is not a subsingleton)

[Robert Maxton]

Oops, yeah, I'm too used to tacking on EqvGen onto everything.

[Robert Maxton]

hmmm, better example...

[Robert Maxton]

Mm, there's a lot of psuedo-examples where the two "different" rs are obviously dual in some way -- ≤ and ≥ for =, ∃ f, Injective f and ∃ f, Surjective f for ≃ -- but I'm not sure that really "counts"...

[Robert Maxton]

... Hm. Actually, this feels like a theorem that might exist. Something like, if two relations are antisymmetric up to the same equivalence, then they define isomorphic lattices?

[Robert Maxton]

hmmm
actually, I can probably bypass much of this by just operating on Quot eqv instead

[Robert Maxton]

and then the relevant relations are antisymm up to actual equality on the quotient type, so I can use the existing preorder/poset API

[Robert Maxton]

-- Okay, better counterexample that's basically the same as my old one but actually valid this time. α := Vector β n for some fixed n, β itself has a total order, and equivalence is defined by permutation. Then any relation of the form "sort the list, then sort by each element in turn" will be antisymmetric up to permutation, but there are $n!$ such relations depending on the "priority" of each index, and they generate completely different orders on Vector β n.