mathlib3 documentation

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.

@[protected, instance]
@[protected, instance]
Equations

The single object in single_obj α.

Equations
@[reducible]

Equip single_obj α with a reverse operation.

Equations
@[reducible]

Equip single_obj α with an involutive reverse operation.

Equations

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

Equations
@[simp]
@[simp]
@[simp]

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 α) (ᾰ : α) :
@[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