Documentation

Mathlib.CategoryTheory.Category.RelCat

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 u, which carries the category instance for which morphisms are binary relations.

Equations
Instances For

    The morphisms in the relation category are relations.

    • ofRel :: (
      • rel : Rel X Y

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

    • )
    Instances For

      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 : 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_comp {X Y Z : RelCat} (f : X Y) (g : Y Z) :
      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

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

        The argument-swap isomorphism from RelCat 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

            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.
            Instances For