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
    theorem CategoryTheory.RelCat.hom_ext_iff {X : CategoryTheory.RelCat} {Y : CategoryTheory.RelCat} {f : X Y} {g : X Y} :
    f = g ∀ (a : X) (b : Y), f a b g a b
    theorem CategoryTheory.RelCat.hom_ext {X : CategoryTheory.RelCat} {Y : CategoryTheory.RelCat} (f : X Y) (g : X Y) (h : ∀ (a : X) (b : Y), f a b g a b) :
    f = g

    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) :

      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