Documentation

Mathlib.CategoryTheory.Category.ReflQuiv

The category of refl quivers #

The category ReflQuiv of (bundled) reflexive quivers, and the free/forgetful adjunction between Cat and ReflQuiv.

def CategoryTheory.ReflQuiv :
Type (max (u + 1) u (v + 1))

Category of refl quivers.

Equations
Instances For

    The underlying quiver of a reflexive quiver.

    Equations
    Instances For

      Construct a bundled ReflQuiv from the underlying type and the typeclass.

      Equations
      Instances For

        The forgetful functor from categories to quivers.

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

          The forgetful functor from categories to quivers.

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

            A refl prefunctor can be promoted to a functor if it respects composition.

            Equations
            Instances For

              The hom relation that identifies the specified reflexivity arrows with the nil paths.

              Instances For

                A reflexive quiver generates a free category, defined as as quotient of the free category on its underlying quiver (called the "path category") by the hom relation that uses the specified reflexivity arrows as the identity arrows.

                Equations
                Instances For

                  The quotient functor associated to a quotient category defines a natural map from the free category on the underlying quiver of a refl quiver to the free category on the reflexive quiver.

                  Equations
                  Instances For

                    This is a specialization of Quotient.lift_unique' rather than Quotient.lift_unique, hence the prime in the name.

                    @[simp]
                    theorem CategoryTheory.Cat.freeRefl_map_map :
                    ∀ {X Y : CategoryTheory.ReflQuiv} (f : X Y) (a b : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel) (hf : a b), (CategoryTheory.Cat.freeRefl.map f).map hf = Quot.liftOn hf (fun (f_1 : a.as b.as) => (CategoryTheory.Cat.FreeRefl.quotientFunctor Y).map (f.mapPath f_1))
                    @[simp]
                    theorem CategoryTheory.Cat.freeRefl_obj_str_comp (V : CategoryTheory.ReflQuiv) ⦃a : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel ⦃b : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel ⦃c : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel :
                    ∀ (a_1 : CategoryTheory.Quotient.Hom CategoryTheory.Cat.FreeReflRel a b) (a_2 : CategoryTheory.Quotient.Hom CategoryTheory.Cat.FreeReflRel b c), CategoryTheory.CategoryStruct.comp a_1 a_2 = CategoryTheory.Quotient.comp CategoryTheory.Cat.FreeReflRel a_1 a_2
                    @[simp]
                    theorem CategoryTheory.Cat.freeRefl_map_obj_as :
                    ∀ {X Y : CategoryTheory.ReflQuiv} (f : X Y) (a : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel), ((CategoryTheory.Cat.freeRefl.map f).obj a).as = f.obj a.as

                    The functor sending a reflexive quiver to the free category it generates, a quotient of its path category.

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

                      We will make use of the natural quotient map from the free category on the underlying quiver of a refl quiver to the free category on the reflexive quiver.

                      Equations
                      Instances For

                        The unit components are defined as the composite of the corresponding unit component for the adjunction between categories and quivers with the map underlying the quotient functor.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem CategoryTheory.ReflQuiv.adj.counit.app_map (C : CategoryTheory.Cat) (a : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel) (b : CategoryTheory.Quotient CategoryTheory.Cat.FreeReflRel) (hf : a b) :
                          (CategoryTheory.ReflQuiv.adj.counit.app C).map hf = Quot.liftOn hf (fun (f : a.as b.as) => (CategoryTheory.Quiv.adj.counit.app C).map f)

                          The counit components are defined using the universal property of the quotient from the corresponding counit component for the adjunction between categories and quivers.

                          Equations
                          Instances For
                            @[simp]

                            The counit of ReflQuiv.adj is closely related to the counit of Quiv.adj. For ease of use, we introduce primed version for unbundled categories.

                            The adjunction between forming the free category on a reflexive quiver, and forgetting a category to a reflexive quiver.

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