Documentation

Mathlib.Combinatorics.Quiver.ReflQuiver

Reflexive Quivers #

This module defines reflexive quivers. A reflexive quiver, or "refl quiver" for short, extends a quiver with a specified endoarrow on each term in its type of objects.

We also introduce morphisms between reflexive quivers, called reflexive prefunctors or "refl prefunctors" for short.

Note: Currently Category does not extend ReflQuiver, although it could. (TODO: do this)

class CategoryTheory.ReflQuiver (obj : Type u) extends Quiver :
Type (max u v)

A reflexive quiver extends a quiver with a specified arrow id X : X ⟶ X for each X in its type of objects. We denote these arrows by id since categories can be understood as an extension of refl quivers.

  • Hom : objobjSort v
  • id : (X : obj) → X X

    The identity morphism on an object.

Instances

    Notation for the identity morphism in a category.

    Equations
    Instances For
      Equations
      structure CategoryTheory.ReflPrefunctor (V : Type u₁) [CategoryTheory.ReflQuiver V] (W : Type u₂) [CategoryTheory.ReflQuiver W] extends Prefunctor :
      Sort (max (max (max (u₁ + 1) (u₂ + 1)) v₁) v₂)

      A morphism of reflexive quivers called a ReflPrefunctor.

      Instances For

        A functor preserves identity morphisms.

        theorem CategoryTheory.ReflPrefunctor.mk_obj {V : Type u_1} {W : Type u_2} [CategoryTheory.ReflQuiver V] [CategoryTheory.ReflQuiver W] {obj : VW} {map : {X Y : V} → (X Y)(obj X obj Y)} {X : V} :
        { obj := obj, map := map }.obj X = obj X
        theorem CategoryTheory.ReflPrefunctor.mk_map {V : Type u_1} {W : Type u_2} [CategoryTheory.ReflQuiver V] [CategoryTheory.ReflQuiver W] {obj : VW} {map : {X Y : V} → (X Y)(obj X obj Y)} {X : V} {Y : V} {f : X Y} :
        { obj := obj, map := map }.map f = map f
        theorem CategoryTheory.ReflPrefunctor.ext {V : Type u} [CategoryTheory.ReflQuiver V] {W : Type u₂} [CategoryTheory.ReflQuiver W] {F : V ⥤rq W} {G : V ⥤rq W} (h_obj : ∀ (X : V), F.obj X = G.obj X) (h_map : ∀ (X Y : V) (f : X Y), F.map f = Eq.recOn (Eq.recOn (G.map f))) :
        F = G

        Proving equality between reflexive prefunctors. This isn't an extensionality lemma, because usually you don't really want to do this.

        @[simp]
        @[simp]
        theorem CategoryTheory.ReflPrefunctor.id_map (V : Type u_1) [CategoryTheory.ReflQuiver V] :
        ∀ {X Y : V} (f : X Y), (𝟭rq V).map f = f

        The identity morphism between reflexive quivers.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.ReflPrefunctor.comp_obj {U : Type u_1} [CategoryTheory.ReflQuiver U] {V : Type u_2} [CategoryTheory.ReflQuiver V] {W : Type u_3} [CategoryTheory.ReflQuiver W] (F : U ⥤rq V) (G : V ⥤rq W) (X : U) :
          (F ⋙rq G).obj X = G.obj (F.obj X)
          @[simp]
          theorem CategoryTheory.ReflPrefunctor.comp_map {U : Type u_1} [CategoryTheory.ReflQuiver U] {V : Type u_2} [CategoryTheory.ReflQuiver V] {W : Type u_3} [CategoryTheory.ReflQuiver W] (F : U ⥤rq V) (G : V ⥤rq W) :
          ∀ {X Y : U} (f : X Y), (F ⋙rq G).map f = G.map (F.map f)

          Composition of morphisms between reflexive quivers.

          Equations
          • F ⋙rq G = { toPrefunctor := F.toPrefunctor ⋙q G.toPrefunctor, map_id := }
          Instances For
            @[simp]

            Notation for a prefunctor between reflexive quivers.

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

              Notation for composition of reflexive prefunctors.

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

                Notation for the identity prefunctor on a reflexive quiver.

                Equations
                Instances For
                  theorem CategoryTheory.ReflPrefunctor.congr_map {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (F : U ⥤q V) {X : U} {Y : U} {f : X Y} {g : X Y} (h : f = g) :
                  F.map f = F.map g

                  A functor has an underlying refl prefunctor.

                  Equations
                  • F.toReflPrefunctor = { toPrefunctor := F.toPrefunctor, map_id := }
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Functor.toReflPrefunctor_toPrefunctor {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} (F : CategoryTheory.Functor C D) :
                    F.toReflPrefunctor.toPrefunctor = F.toPrefunctor

                    Vᵒᵖ reverses the direction of all arrows of V.

                    Equations