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.3

instance CategoryTheory.RelCat.inhabited : Inhabited CategoryTheory.RelCat

Equations

• CategoryTheory.RelCat.inhabited = id inferInstance

instance CategoryTheory.rel : CategoryTheory.LargeCategory CategoryTheory.RelCat

The category of types with binary relations as morphisms.

Equations

• CategoryTheory.rel = CategoryTheory.Category.mk @CategoryTheory.rel.proof_1 @CategoryTheory.rel.proof_2 @CategoryTheory.rel.proof_3

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

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

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

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

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

def CategoryTheory.RelCat.graphFunctor : CategoryTheory.Functor (Type u) CategoryTheory.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) : CategoryTheory.RelCat.graphFunctor.map f x y ↔ f x = y

instance CategoryTheory.RelCat.graphFunctor_faithful : CategoryTheory.RelCat.graphFunctor.Faithful

instance CategoryTheory.RelCat.graphFunctor_essSurj : CategoryTheory.RelCat.graphFunctor.EssSurj

theorem CategoryTheory.RelCat.rel_iso_iff {X Y : CategoryTheory.RelCat} (r : X ⟶ Y) : CategoryTheory.IsIso r ↔ ∃ (f : X ≅ Y), CategoryTheory.RelCat.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 : CategoryTheory.Functor CategoryTheory.RelCat CategoryTheory.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 : CategoryTheory.Functor CategoryTheory.RelCatᵒᵖ CategoryTheory.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 : CategoryTheory.RelCat.opFunctor.comp CategoryTheory.RelCat.unopFunctor = CategoryTheory.Functor.id CategoryTheory.RelCat

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

instance CategoryTheory.RelCat.instIsEquivalenceOppositeOpFunctor : CategoryTheory.RelCat.opFunctor.IsEquivalence

instance CategoryTheory.RelCat.instIsEquivalenceOppositeUnopFunctor : CategoryTheory.RelCat.unopFunctor.IsEquivalence