# mathlib3documentation

combinatorics.quiver.single_obj

# Single-object quiver #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Single object quiver with a given arrows type.

## Main definitions #

Given a type α, single_obj α 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 to_hom. More generally, a list of elements of a can be reinterpreted as a path from star α to itself using path_equiv_list.

@[nolint]
def quiver.single_obj (α : Type u_1) :

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

Equations
Instances for quiver.single_obj
@[protected, instance]
def quiver.single_obj.unique (α : Type u_1) :
@[protected, instance]
def quiver.single_obj.quiver (α : Type u_1) :
Equations
• = {hom := λ (_x _x : , α}
def quiver.single_obj.star (α : Type u_1) :

The single object in single_obj α.

Equations
@[protected, instance]
def quiver.single_obj.inhabited (α : Type u_1) :
Equations
@[reducible]
def quiver.single_obj.has_reverse {α : Type u_1} (rev : α α) :

Equip single_obj α with a reverse operation.

Equations
@[reducible]
def quiver.single_obj.has_involutive_reverse {α : Type u_1} (rev : α α) (h : function.involutive rev) :

Equip single_obj α with an involutive reverse operation.

Equations
def quiver.single_obj.to_hom {α : Type u_1} :

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

Equations
@[simp]
theorem quiver.single_obj.to_hom_symm_apply {α : Type u_1} (a : α) :
@[simp]
theorem quiver.single_obj.to_hom_apply {α : Type u_1} (a : α) :
@[simp]
theorem quiver.single_obj.to_prefunctor_symm_apply {α : Type u_1} {β : Type u_2} (f : ⥤q ) (a : α) :
@[simp]
theorem quiver.single_obj.to_prefunctor_apply_obj {α : Type u_1} {β : Type u_2} (f : α β) (a : quiver.single_obj α) :
def quiver.single_obj.to_prefunctor {α : Type u_1} {β : Type u_2} :
β)

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

Equations
@[simp]
theorem quiver.single_obj.to_prefunctor_apply_map {α : Type u_1} {β : Type u_2} (f : α β) (_x _x_1 : quiver.single_obj α) (ᾰ : α) :
= f ᾰ
@[simp]
theorem quiver.single_obj.to_prefunctor_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) (g : β γ) :
@[simp]
theorem quiver.single_obj.to_prefunctor_symm_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : ⥤q ) (g : ⥤q ) :
@[simp]

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

Equations
@[simp]

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

Equations
theorem quiver.single_obj.path_to_list_to_path {α : Type u_1} {x : quiver.single_obj α} (p : x) :
theorem quiver.single_obj.list_to_path_to_list {α : Type u_1} (l : list α) :

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

Equations
@[simp]
@[simp]
theorem quiver.single_obj.path_equiv_list_cons {α : Type u_1} (p : )  :
@[simp]
@[simp]
theorem quiver.single_obj.path_equiv_list_symm_cons {α : Type u_1} (l : list α) (a : α) :