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.

def Quiver.SingleObj :

Type u_1 → Type

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

Equations

Quiver.SingleObj x = Unit

instance Quiver.instUniqueSingleObj {α : Type u_1} :

Unique (Quiver.SingleObj α)

Equations

Quiver.instUniqueSingleObj = { toInhabited := { default := PUnit.unit }, uniq := (_ : ∀ (x : Quiver.SingleObj α), x = x) }

instance Quiver.SingleObj.instQuiverSingleObj (α : Type u_1) :

Quiver (Quiver.SingleObj α)

Equations

Quiver.SingleObj.instQuiverSingleObj α = { Hom := fun x x => α }

def Quiver.SingleObj.star (α : Type u_1) :

Quiver.SingleObj α

The single object in SingleObj α.

Equations

Quiver.SingleObj.star α = ()

instance Quiver.SingleObj.instInhabitedSingleObj (α : Type u_1) :

Inhabited (Quiver.SingleObj α)

Equations

Quiver.SingleObj.instInhabitedSingleObj α = { default := Quiver.SingleObj.star α }

theorem Quiver.SingleObj.ext {α : Type u_1} {x : Quiver.SingleObj α} {y : Quiver.SingleObj α} :

x = y

def Quiver.SingleObj.hasReverse {α : Type u_1} (rev : α → α) :

Quiver.HasReverse (Quiver.SingleObj α)

Equip SingleObj α with a reverse operation.

Equations

Quiver.SingleObj.hasReverse rev = { reverse' := fun {a b} => rev }

def Quiver.SingleObj.hasInvolutiveReverse {α : Type u_1} (rev : α → α) (h : Function.Involutive rev) :

Quiver.HasInvolutiveReverse (Quiver.SingleObj α)

Equip SingleObj α with an involutive reverse operation.

Equations

Quiver.SingleObj.hasInvolutiveReverse rev h = Quiver.HasInvolutiveReverse.mk (_ : ∀ {a b : Quiver.SingleObj α}, Function.Involutive rev)

@[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} :

α ≃ (Quiver.SingleObj.star α ⟶ Quiver.SingleObj.star α)

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

Equations

Quiver.SingleObj.toHom = Equiv.refl α

@[simp]

theorem Quiver.SingleObj.toPrefunctor_symm_apply {α : Type u_1} {β : Type u_2} (f : Quiver.SingleObj α ⥤q Quiver.SingleObj β) (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 : Quiver.SingleObj α) :

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 : Quiver.SingleObj α} (a : α), Prefunctor.map (↑Quiver.SingleObj.toPrefunctor f) a = f a

def Quiver.SingleObj.toPrefunctor {α : Type u_1} {β : Type u_2} :

(α → β) ≃ Quiver.SingleObj α ⥤q Quiver.SingleObj β

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 = 𝟭q (Quiver.SingleObj α)

@[simp]

theorem Quiver.SingleObj.toPrefunctor_symm_id {α : Type u_1} :

↑(Equiv.symm Quiver.SingleObj.toPrefunctor) (𝟭q (Quiver.SingleObj α)) = 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 : Quiver.SingleObj α ⥤q Quiver.SingleObj β) (g : Quiver.SingleObj β ⥤q Quiver.SingleObj γ) :

↑(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 : Quiver.SingleObj α} :

Quiver.Path (Quiver.SingleObj.star α) x → List α

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

def Quiver.SingleObj.listToPath {α : Type u_1} :

List α → Quiver.Path (Quiver.SingleObj.star α) (Quiver.SingleObj.star α)

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

Equations

Quiver.SingleObj.listToPath [] = Quiver.Path.nil
Quiver.SingleObj.listToPath (a :: l) = Quiver.Path.cons (Quiver.SingleObj.listToPath l) a

theorem Quiver.SingleObj.listToPath_pathToList {α : Type u_1} {x : Quiver.SingleObj α} (p : Quiver.Path (Quiver.SingleObj.star α) x) :

Quiver.SingleObj.listToPath (Quiver.SingleObj.pathToList p) = Quiver.Path.cast (_ : Quiver.SingleObj.star α = Quiver.SingleObj.star α) (_ : x = Quiver.SingleObj.star α) p

theorem Quiver.SingleObj.pathToList_listToPath {α : Type u_1} (l : List α) :

Quiver.SingleObj.pathToList (Quiver.SingleObj.listToPath l) = l

def Quiver.SingleObj.pathEquivList {α : Type u_1} :

Quiver.Path (Quiver.SingleObj.star α) (Quiver.SingleObj.star α) ≃ List α

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 : Quiver.Path (Quiver.SingleObj.star α) (Quiver.SingleObj.star α)) (a : Quiver.SingleObj.star α ⟶ Quiver.SingleObj.star α) :

↑Quiver.SingleObj.pathEquivList (Quiver.Path.cons p a) = a :: Quiver.SingleObj.pathToList p

@[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