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.

def CategoryTheory.RelCat : Type (u + 1)

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

instance CategoryTheory.RelCat.inhabited : Inhabited RelCat

structure CategoryTheory.RelCat.Hom (X Y : RelCat) : Type u

The morphisms in the relation category are relations.

• ofRel :: (
• rel : SetRel X Y

  The underlying relation between X and Y of a morphism X ⟶ Y for X Y : RelCat.

• )

instance CategoryTheory.RelCat.instLargeCategory : LargeCategory RelCat

The category of types with binary relations as morphisms.

theorem CategoryTheory.RelCat.Hom.ext {X Y : RelCat} (f g : X ⟶ Y) (h : f.rel = g.rel) : f = g

theorem CategoryTheory.RelCat.Hom.ext_iff {X Y : RelCat} {f g : X ⟶ Y} : f = g ↔ f.rel = g.rel

@[simp]

theorem CategoryTheory.RelCat.Hom.rel_id (X : RelCat) : (CategoryStruct.id X).rel = SetRel.id

@[simp]

theorem CategoryTheory.RelCat.Hom.rel_comp {X Y Z : RelCat} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).rel = f.rel.comp g.rel

theorem CategoryTheory.RelCat.Hom.rel_id_apply₂ {X : RelCat} (x y : X) : (x, y) ∈ (CategoryStruct.id X).rel ↔ x = y

theorem CategoryTheory.RelCat.Hom.rel_comp_apply₂ {X Y Z : RelCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) (z : Z) : (x, z) ∈ (CategoryStruct.comp f g).rel ↔ ∃ (y : Y), (x, y) ∈ f.rel ∧ (y, z) ∈ g.rel

def CategoryTheory.RelCat.graphFunctor : Functor (Type u) RelCat

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

@[simp]

theorem CategoryTheory.RelCat.graphFunctor_obj (X : Type u) : graphFunctor.obj X = X

@[simp]

theorem CategoryTheory.RelCat.rel_graphFunctor_map {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : (graphFunctor.map f).rel = Function.graph f

@[deprecated CategoryTheory.RelCat.rel_graphFunctor_map (since := "2025-06-08")]

theorem CategoryTheory.RelCat.graphFunctor_map {X Y : Type u} (f : X ⟶ Y) (x : X) (y : Y) : (x, y) ∈ (graphFunctor.map f).rel ↔ f x = y

instance CategoryTheory.RelCat.graphFunctor_faithful : graphFunctor.Faithful

instance CategoryTheory.RelCat.graphFunctor_essSurj : graphFunctor.EssSurj

theorem CategoryTheory.RelCat.rel_iso_iff {X Y : RelCat} (r : X ⟶ Y) : IsIso r ↔ ∃ (f : X ≅ Y), graphFunctor.map f.hom = r

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

def CategoryTheory.RelCat.opFunctor : Functor RelCat RelCatᵒᵖ

The argument-swap isomorphism from RelCat to its opposite.

def CategoryTheory.RelCat.unopFunctor : Functor RelCatᵒᵖ RelCat

The other direction of opFunctor.

@[simp]

theorem CategoryTheory.RelCat.opFunctor_comp_unopFunctor_eq : opFunctor.comp unopFunctor = Functor.id RelCat

@[simp]

theorem CategoryTheory.RelCat.unopFunctor_comp_opFunctor_eq : unopFunctor.comp opFunctor = Functor.id RelCatᵒᵖ

def CategoryTheory.RelCat.opEquivalence : RelCat ≌ RelCatᵒᵖ

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

@[simp]

theorem CategoryTheory.RelCat.opEquivalence_counitIso : opEquivalence.counitIso = Iso.refl (unopFunctor.comp opFunctor)

@[simp]

theorem CategoryTheory.RelCat.opEquivalence_inverse : opEquivalence.inverse = unopFunctor

@[simp]

theorem CategoryTheory.RelCat.opEquivalence_functor : opEquivalence.functor = opFunctor

@[simp]

theorem CategoryTheory.RelCat.opEquivalence_unitIso : opEquivalence.unitIso = Iso.refl (Functor.id RelCat)

instance CategoryTheory.RelCat.instIsEquivalenceOppositeOpFunctor : opFunctor.IsEquivalence

instance CategoryTheory.RelCat.instIsEquivalenceOppositeUnopFunctor : unopFunctor.IsEquivalence