# 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 α⟶ star α is the type α. An element x : α can be reinterpreted as an element of star α ⟶ 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
instance Quiver.instUniqueSingleObj {α : Type u_1} :
Equations
• Quiver.instUniqueSingleObj = { toInhabited := { default := PUnit.unit }, uniq := (_ : ∀ (x : ), x = x) }
Equations
• = { Hom := fun x x => α }
def Quiver.SingleObj.star (α : Type u_1) :

The single object in SingleObj α.

Equations
Equations
• = { default := }
theorem Quiver.SingleObj.ext {α : Type u_1} {x : } {y : } :
x = y
def Quiver.SingleObj.hasReverse {α : Type u_1} (rev : αα) :

Equip SingleObj α with a reverse operation.

Equations
• = { reverse' := fun {a b} => rev }
def Quiver.SingleObj.hasInvolutiveReverse {α : Type u_1} (rev : αα) (h : ) :

Equip SingleObj α with an involutive reverse operation.

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

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

Equations
• Quiver.SingleObj.toHom =
@[simp]
theorem Quiver.SingleObj.toPrefunctor_symm_apply {α : Type u_1} {β : Type u_2} (f : ) (a : α) :
↑(Equiv.symm Quiver.SingleObj.toPrefunctor) f a = Prefunctor.map f (Quiver.SingleObj.toHom a)
@[simp]
theorem Quiver.SingleObj.toPrefunctor_apply_obj {α : Type u_1} {β : Type u_2} (f : αβ) (a : ) :
Prefunctor.obj (Quiver.SingleObj.toPrefunctor f) a = id a
@[simp]
theorem Quiver.SingleObj.toPrefunctor_apply_map {α : Type u_1} {β : Type u_2} (f : αβ) :
∀ {X Y : } (a : α), Prefunctor.map (Quiver.SingleObj.toPrefunctor f) 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.
theorem Quiver.SingleObj.toPrefunctor_id {α : Type u_1} :
Quiver.SingleObj.toPrefunctor id =
@[simp]
theorem Quiver.SingleObj.toPrefunctor_symm_id {α : Type u_1} :
↑(Equiv.symm Quiver.SingleObj.toPrefunctor) () = id
theorem Quiver.SingleObj.toPrefunctor_comp {α : Type u_1} {β : Type u_3} {γ : Type u_2} (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 : ) (g : ) :
↑(Equiv.symm Quiver.SingleObj.toPrefunctor) (f ⋙q g) = ↑(Equiv.symm Quiver.SingleObj.toPrefunctor) g ↑(Equiv.symm Quiver.SingleObj.toPrefunctor) f
def Quiver.SingleObj.pathToList {α : Type u_1} {x : } :
List α

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

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

Equations
• = Quiver.Path.nil
theorem Quiver.SingleObj.listToPath_pathToList {α : Type u_1} {x : } (p : ) :

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Quiver.SingleObj.pathEquivList_nil {α : Type u_1} :
Quiver.SingleObj.pathEquivList Quiver.Path.nil = []
@[simp]
theorem Quiver.SingleObj.pathEquivList_cons {α : Type u_1} (p : ) (a : ) :
Quiver.SingleObj.pathEquivList () =
@[simp]
theorem Quiver.SingleObj.pathEquivList_symm_nil {α : Type u_1} :
↑(Equiv.symm Quiver.SingleObj.pathEquivList) [] = Quiver.Path.nil
@[simp]
theorem Quiver.SingleObj.pathEquivList_symm_cons {α : Type u_1} (l : List α) (a : α) :
↑(Equiv.symm Quiver.SingleObj.pathEquivList) (a :: l) = Quiver.Path.cons (↑(Equiv.symm Quiver.SingleObj.pathEquivList) l) a