# Basics on the category of relations #

We define the category of types CategoryTheory.RelCat with binary relations as morphisms. Associating each function with the relation defined by its graph yields a faithful and essentially surjective functor graphFunctor that also characterizes all isomorphisms (see rel_iso_iff).

By flipping the arguments to a relation, we construct an equivalence opEquivalence between RelCat and its opposite.

A type synonym for Type, which carries the category instance for which morphisms are binary relations.

Equations
Instances For

The category of types with binary relations as morphisms.

Equations
theorem CategoryTheory.RelCat.hom_ext (f : X Y) (g : X Y) (h : ∀ (a : X) (b : Y), f a b g a b) :
f = g
theorem CategoryTheory.RelCat.Hom.rel_id :
= fun (x x_1 : X) => x = x_1
theorem CategoryTheory.RelCat.Hom.rel_comp (f : X Y) (g : Y Z) :
theorem CategoryTheory.RelCat.Hom.rel_comp_apply₂ (f : X Y) (g : Y Z) (x : X) (z : Z) :
∃ (y : Y), f x y g y z

The essentially surjective faithful embedding from the category of types and functions into the category of types and relations.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.RelCat.graphFunctor_map {X : Type u} {Y : Type u} (f : X Y) (x : X) (y : Y) :
f x = y
Equations
theorem CategoryTheory.RelCat.rel_iso_iff (r : X Y) :
∃ (f : X Y), f.hom = r

A relation is an isomorphism in RelCat iff it is the image of an isomorphism in Type.

The argument-swap isomorphism from rel to its opposite.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The other direction of opFunctor.

Equations
• One or more equations did not get rendered due to their size.
Instances For

rel is self-dual: The map that swaps the argument order of a relation induces an equivalence between rel and its opposite.

Equations
• One or more equations did not get rendered due to their size.
Instances For