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.

Equations

• CategoryTheory.RelCat = Type ?u.2

instance CategoryTheory.RelCat.inhabited : Inhabited RelCat

Equations

• CategoryTheory.RelCat.inhabited = id inferInstance

instance CategoryTheory.rel : LargeCategory RelCat

The category of types with binary relations as morphisms.

Equations

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

theorem CategoryTheory.RelCat.hom_ext {X Y : RelCat} (f g : X ⟶ Y) (h : ∀ (a : X) (b : Y), f a b ↔ g a b) : f = g

theorem CategoryTheory.RelCat.hom_ext_iff {X Y : RelCat} {f g : X ⟶ Y} : f = g ↔ ∀ (a : X) (b : Y), f a b ↔ g a b

theorem CategoryTheory.RelCat.Hom.rel_id (X : RelCat) : CategoryStruct.id X = fun (x1 x2 : X) => x1 = x2

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

theorem CategoryTheory.RelCat.Hom.rel_id_apply₂ (X : RelCat) (x y : X) : CategoryStruct.id X x y ↔ x = y

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

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.

Equations

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

@[simp]

theorem CategoryTheory.RelCat.graphFunctor_map {X Y : Type u} (f : X ⟶ Y) (x : X) (y : Y) : graphFunctor.map f x y ↔ 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.

Equations

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

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

The other direction of opFunctor.

Equations

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

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

Equations

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

@[simp]

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

@[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_unitIso : opEquivalence.unitIso = Iso.refl (Functor.id RelCat)

instance CategoryTheory.RelCat.instIsEquivalenceOppositeOpFunctor : opFunctor.IsEquivalence

instance CategoryTheory.RelCat.instIsEquivalenceOppositeUnopFunctor : unopFunctor.IsEquivalence