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.

@[nolint]

def quiver.single_obj (α : Type u_1) :

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

Equations

quiver.single_obj α = unit

Instances for quiver.single_obj

@[protected, instance]

def quiver.single_obj.unique (α : Type u_1) :

unique (quiver.single_obj α)

@[protected, instance]

def quiver.single_obj.quiver (α : Type u_1) :

quiver (quiver.single_obj α)

Equations

quiver.single_obj.quiver α = {hom := λ (_x _x : quiver.single_obj α), α}

def quiver.single_obj.star (α : Type u_1) :

quiver.single_obj α

The single object in single_obj α.

Equations

quiver.single_obj.star α = unit.star()

@[protected, instance]

def quiver.single_obj.inhabited (α : Type u_1) :

inhabited (quiver.single_obj α)

Equations

quiver.single_obj.inhabited α = {default := quiver.single_obj.star α}

@[reducible]

def quiver.single_obj.has_reverse {α : Type u_1} (rev : α → α) :

quiver.has_reverse (quiver.single_obj α)

Equip single_obj α with a reverse operation.

Equations

quiver.single_obj.has_reverse rev = {reverse' := λ (_x _x : quiver.single_obj α), rev}

@[reducible]

def quiver.single_obj.has_involutive_reverse {α : Type u_1} (rev : α → α) (h : function.involutive rev) :

quiver.has_involutive_reverse (quiver.single_obj α)

Equip single_obj α with an involutive reverse operation.

Equations

quiver.single_obj.has_involutive_reverse rev h = {to_has_reverse := quiver.single_obj.has_reverse rev, inv' := _}

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

α ≃ (quiver.single_obj.star α ⟶ quiver.single_obj.star α)

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

Equations

quiver.single_obj.to_hom = equiv.refl α

@[simp]

theorem quiver.single_obj.to_hom_symm_apply {α : Type u_1} (a : α) :

⇑(quiver.single_obj.to_hom.symm) a = a

@[simp]

theorem quiver.single_obj.to_hom_apply {α : Type u_1} (a : α) :

⇑quiver.single_obj.to_hom a = a

@[simp]

theorem quiver.single_obj.to_prefunctor_symm_apply {α : Type u_1} {β : Type u_2} (f : quiver.single_obj α ⥤q quiver.single_obj β) (a : α) :

⇑(quiver.single_obj.to_prefunctor.symm) f a = f.map (⇑quiver.single_obj.to_hom a)

@[simp]

theorem quiver.single_obj.to_prefunctor_apply_obj {α : Type u_1} {β : Type u_2} (f : α → β) (a : quiver.single_obj α) :

(⇑quiver.single_obj.to_prefunctor f).obj a = id a

def quiver.single_obj.to_prefunctor {α : Type u_1} {β : Type u_2} :

(α → β) ≃ quiver.single_obj α ⥤q quiver.single_obj β

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

Equations

quiver.single_obj.to_prefunctor = {to_fun := λ (f : α → β), {obj := id (quiver.single_obj α), map := λ (_x _x : quiver.single_obj α), f}, inv_fun := λ (f : quiver.single_obj α ⥤q quiver.single_obj β) (a : α), f.map (⇑quiver.single_obj.to_hom a), left_inv := _, right_inv := _}

@[simp]

theorem quiver.single_obj.to_prefunctor_apply_map {α : Type u_1} {β : Type u_2} (f : α → β) (_x _x_1 : quiver.single_obj α) (ᾰ : α) :

(⇑quiver.single_obj.to_prefunctor f).map ᾰ = f ᾰ

theorem quiver.single_obj.to_prefunctor_id {α : Type u_1} :

⇑quiver.single_obj.to_prefunctor id = 𝟭q (quiver.single_obj α)

@[simp]

theorem quiver.single_obj.to_prefunctor_symm_id {α : Type u_1} :

⇑(quiver.single_obj.to_prefunctor.symm) (𝟭q (quiver.single_obj α)) = id

theorem quiver.single_obj.to_prefunctor_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) :

⇑quiver.single_obj.to_prefunctor (g ∘ f) = ⇑quiver.single_obj.to_prefunctor f ⋙q ⇑quiver.single_obj.to_prefunctor g

@[simp]

theorem quiver.single_obj.to_prefunctor_symm_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : quiver.single_obj α ⥤q quiver.single_obj β) (g : quiver.single_obj β ⥤q quiver.single_obj γ) :

⇑(quiver.single_obj.to_prefunctor.symm) (f ⋙q g) = ⇑(quiver.single_obj.to_prefunctor.symm) g ∘ ⇑(quiver.single_obj.to_prefunctor.symm) f

@[simp]

def quiver.single_obj.path_to_list {α : Type u_1} {x : quiver.single_obj α} :

quiver.path (quiver.single_obj.star α) x → list α

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]

def quiver.single_obj.list_to_path {α : Type u_1} :

list α → quiver.path (quiver.single_obj.star α) (quiver.single_obj.star α)

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 : quiver.path (quiver.single_obj.star α) x) :

quiver.single_obj.list_to_path (quiver.single_obj.path_to_list p) = quiver.path.cast rfl unit.ext p

theorem quiver.single_obj.list_to_path_to_list {α : Type u_1} (l : list α) :

quiver.single_obj.path_to_list (quiver.single_obj.list_to_path l) = l

def quiver.single_obj.path_equiv_list {α : Type u_1} :

quiver.path (quiver.single_obj.star α) (quiver.single_obj.star α) ≃ list α

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

Equations

quiver.single_obj.path_equiv_list = {to_fun := quiver.single_obj.path_to_list (quiver.single_obj.star α), inv_fun := quiver.single_obj.list_to_path α, left_inv := _, right_inv := _}

@[simp]

theorem quiver.single_obj.path_equiv_list_nil {α : Type u_1} :

⇑quiver.single_obj.path_equiv_list quiver.path.nil = list.nil

@[simp]

theorem quiver.single_obj.path_equiv_list_cons {α : Type u_1} (p : quiver.path (quiver.single_obj.star α) (quiver.single_obj.star α)) (a : quiver.single_obj.star α ⟶ quiver.single_obj.star α) :

⇑quiver.single_obj.path_equiv_list (p.cons a) = a :: quiver.single_obj.path_to_list p

@[simp]

theorem quiver.single_obj.path_equiv_list_symm_nil {α : Type u_1} :

⇑(quiver.single_obj.path_equiv_list.symm) list.nil = quiver.path.nil

@[simp]

theorem quiver.single_obj.path_equiv_list_symm_cons {α : Type u_1} (l : list α) (a : α) :

⇑(quiver.single_obj.path_equiv_list.symm) (a :: l) = (⇑(quiver.single_obj.path_equiv_list.symm) l).cons a