Documentation

Mathlib.Combinatorics.Quiver.SingleObj

Single-object quiver #

Single object quiver with a given arrows type.

Main definitions #

Given a type α, SingleObj α is the Unit type, whose single object is called star α, with Quiver structure such that star α ⟶ star α is the type α. An element x : α can be reinterpreted as an element of star α ⟶ star α using toHom. More generally, a list of elements of a can be reinterpreted as a path from star α to itself using pathEquivList.

Type tag on Unit used to define single-object quivers.

Equations
Instances For
    Equations
    • Quiver.instUniqueSingleObj = { default := PUnit.unit, uniq := }
    Equations

    The single object in SingleObj α.

    Equations
    Instances For
      theorem Quiver.SingleObj.ext {α : Type u_1} {x : Quiver.SingleObj α} {y : Quiver.SingleObj α} :
      x = y
      @[reducible, inline]
      abbrev Quiver.SingleObj.hasReverse {α : Type u_1} (rev : αα) :

      Equip SingleObj α with a reverse operation.

      Equations
      Instances For
        @[reducible, inline]

        Equip SingleObj α with an involutive reverse operation.

        Equations
        Instances For
          @[simp]
          theorem Quiver.SingleObj.toHom_symm_apply {α : Type u_1} (a : α) :
          Quiver.SingleObj.toHom.symm a = a
          @[simp]
          theorem Quiver.SingleObj.toHom_apply {α : Type u_1} (a : α) :
          Quiver.SingleObj.toHom a = a

          The type of arrows from star α to itself is equivalent to the original type α.

          Equations
          Instances For
            @[simp]
            theorem Quiver.SingleObj.toPrefunctor_symm_apply {α : Type u_1} {β : Type u_2} (f : Quiver.SingleObj α ⥤q Quiver.SingleObj β) (a : α) :
            Quiver.SingleObj.toPrefunctor.symm f a = f.map (Quiver.SingleObj.toHom a)
            @[simp]
            theorem Quiver.SingleObj.toPrefunctor_apply_obj {α : Type u_1} {β : Type u_2} (f : αβ) (a : Quiver.SingleObj α) :
            (Quiver.SingleObj.toPrefunctor f).obj a = id a
            @[simp]
            theorem Quiver.SingleObj.toPrefunctor_apply_map {α : Type u_1} {β : Type u_2} (f : αβ) :
            ∀ {X Y : Quiver.SingleObj α} (a : α), (Quiver.SingleObj.toPrefunctor f).map a = f a
            def Quiver.SingleObj.toPrefunctor {α : Type u_1} {β : Type u_2} :

            Prefunctors between two SingleObj quivers correspond to functions between the corresponding arrows types.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem Quiver.SingleObj.toPrefunctor_id {α : Type u_1} :
              Quiver.SingleObj.toPrefunctor id = 𝟭q (Quiver.SingleObj α)
              @[simp]
              theorem Quiver.SingleObj.toPrefunctor_symm_id {α : Type u_1} :
              Quiver.SingleObj.toPrefunctor.symm (𝟭q (Quiver.SingleObj α)) = id
              theorem Quiver.SingleObj.toPrefunctor_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : βγ) :
              Quiver.SingleObj.toPrefunctor (g f) = Quiver.SingleObj.toPrefunctor f ⋙q Quiver.SingleObj.toPrefunctor g
              @[simp]
              theorem Quiver.SingleObj.toPrefunctor_symm_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Quiver.SingleObj α ⥤q Quiver.SingleObj β) (g : Quiver.SingleObj β ⥤q Quiver.SingleObj γ) :
              Quiver.SingleObj.toPrefunctor.symm (f ⋙q g) = Quiver.SingleObj.toPrefunctor.symm g Quiver.SingleObj.toPrefunctor.symm f

              Auxiliary definition for quiver.SingleObj.pathEquivList. Converts a path in the quiver single_obj α into a list of elements of type a.

              Instances For

                Auxiliary definition for quiver.SingleObj.pathEquivList. Converts a list of elements of type α into a path in the quiver SingleObj α.

                Equations
                Instances For

                  Paths in SingleObj α quiver correspond to lists of elements of type α.

                  Equations
                  • Quiver.SingleObj.pathEquivList = { toFun := Quiver.SingleObj.pathToList, invFun := Quiver.SingleObj.listToPath, left_inv := , right_inv := }
                  Instances For
                    @[simp]
                    theorem Quiver.SingleObj.pathEquivList_nil {α : Type u_1} :
                    Quiver.SingleObj.pathEquivList Quiver.Path.nil = []
                    @[simp]
                    theorem Quiver.SingleObj.pathEquivList_symm_nil {α : Type u_1} :
                    Quiver.SingleObj.pathEquivList.symm [] = Quiver.Path.nil
                    @[simp]
                    theorem Quiver.SingleObj.pathEquivList_symm_cons {α : Type u_1} (l : List α) (a : α) :
                    Quiver.SingleObj.pathEquivList.symm (a :: l) = (Quiver.SingleObj.pathEquivList.symm l).cons a