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.

source
def CategoryTheory.RelCat :
Type (u + 1)

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

Equations
Instances For
    source
    instance CategoryTheory.RelCat.inhabited :
    Inhabited CategoryTheory.RelCat
    Equations
    source
    instance CategoryTheory.rel :
    CategoryTheory.LargeCategory CategoryTheory.RelCat

    The category of types with binary relations as morphisms.

    Equations
    source
    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
    source
    theorem CategoryTheory.RelCat.Hom.rel_id (X : CategoryTheory.RelCat) :
    CategoryTheory.CategoryStruct.id X = fun (x1 x2 : X) => x1 = x2
    source
    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
    source
    theorem CategoryTheory.RelCat.Hom.rel_id_apply₂ (X : CategoryTheory.RelCat) (x y : X) :
    CategoryTheory.CategoryStruct.id X x y ↔ x = y
    source
    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
    source
    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.
    Instances For
      source
      @[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
      source
      instance CategoryTheory.RelCat.graphFunctor_faithful :
      CategoryTheory.RelCat.graphFunctor.Faithful
      Equations
      source
      instance CategoryTheory.RelCat.graphFunctor_essSurj :
      CategoryTheory.RelCat.graphFunctor.EssSurj
      Equations
      source
      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.

      source
      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.
      Instances For
        source
        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.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.RelCat.opFunctor_comp_unopFunctor_eq :
          CategoryTheory.RelCat.opFunctor.comp CategoryTheory.RelCat.unopFunctor = CategoryTheory.Functor.id CategoryTheory.RelCat
          source
          @[simp]
          theorem CategoryTheory.RelCat.unopFunctor_comp_opFunctor_eq :
          CategoryTheory.RelCat.unopFunctor.comp CategoryTheory.RelCat.opFunctor = CategoryTheory.Functor.id CategoryTheory.RelCatᵒᵖ
          source
          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.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.RelCat.opEquivalence_unitIso :
            CategoryTheory.RelCat.opEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id CategoryTheory.RelCat)
            source
            @[simp]
            theorem CategoryTheory.RelCat.opEquivalence_counitIso :
            CategoryTheory.RelCat.opEquivalence.counitIso = CategoryTheory.Iso.refl (CategoryTheory.RelCat.unopFunctor.comp CategoryTheory.RelCat.opFunctor)
            source
            @[simp]
            theorem CategoryTheory.RelCat.opEquivalence_functor :
            CategoryTheory.RelCat.opEquivalence.functor = CategoryTheory.RelCat.opFunctor
            source
            @[simp]
            theorem CategoryTheory.RelCat.opEquivalence_inverse :
            CategoryTheory.RelCat.opEquivalence.inverse = CategoryTheory.RelCat.unopFunctor
            source
            instance CategoryTheory.RelCat.instIsEquivalenceOppositeOpFunctor :
            CategoryTheory.RelCat.opFunctor.IsEquivalence
            Equations
            source
            instance CategoryTheory.RelCat.instIsEquivalenceOppositeUnopFunctor :
            CategoryTheory.RelCat.unopFunctor.IsEquivalence
            Equations