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 α is the type α. An element x : α can be reinterpreted as an element of 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 (SingleObj α)

Equations

• Quiver.instUniqueSingleObj = { default := PUnit.unit, uniq := ⋯ }

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

Equations

• Quiver.SingleObj.inst α = { Hom := fun (x x : Quiver.SingleObj α) => α }

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

The single object in SingleObj α.

Equations

• Quiver.SingleObj.star α = ()

instance Quiver.SingleObj.instInhabited (α : Type u_1) : Inhabited (SingleObj α)

Equations

• Quiver.SingleObj.instInhabited α = { default := Quiver.SingleObj.star α }

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

@[reducible, inline]

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

Equip SingleObj α with a reverse operation.

Equations

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

@[reducible, inline]

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

Equip SingleObj α with an involutive reverse operation.

Equations

• Quiver.SingleObj.hasInvolutiveReverse rev h = { toHasReverse := Quiver.SingleObj.hasReverse rev, inv' := ⋯ }

def Quiver.SingleObj.toHom {α : Type u_1} : α ≃ (star α ⟶ 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.toHom_apply {α : Type u_1} (a : α) : toHom a = a

@[simp]

theorem Quiver.SingleObj.toHom_symm_apply {α : Type u_1} (a : α) : toHom.symm a = a

def Quiver.SingleObj.toPrefunctor {α : Type u_1} {β : Type u_2} : (α → β) ≃ SingleObj α ⥤q 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.

@[simp]

theorem Quiver.SingleObj.toPrefunctor_apply_obj {α : Type u_1} {β : Type u_2} (f : α → β) (a : SingleObj α) : (toPrefunctor f).obj a = id a

@[simp]

theorem Quiver.SingleObj.toPrefunctor_symm_apply {α : Type u_1} {β : Type u_2} (f : SingleObj α ⥤q SingleObj β) (a : α) : toPrefunctor.symm f a = f.map (toHom a)

@[simp]

theorem Quiver.SingleObj.toPrefunctor_apply_map {α : Type u_1} {β : Type u_2} (f : α → β) {X✝ Y✝ : SingleObj α} (a✝ : α) : (toPrefunctor f).map a✝ = f a✝

theorem Quiver.SingleObj.toPrefunctor_id {α : Type u_1} : toPrefunctor id = 𝟭q (SingleObj α)

@[simp]

theorem Quiver.SingleObj.toPrefunctor_symm_id {α : Type u_1} : toPrefunctor.symm (𝟭q (SingleObj α)) = id

theorem Quiver.SingleObj.toPrefunctor_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) : toPrefunctor (g ∘ f) = toPrefunctor f ⋙q toPrefunctor g

@[simp]

theorem Quiver.SingleObj.toPrefunctor_symm_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : SingleObj α ⥤q SingleObj β) (g : SingleObj β ⥤q SingleObj γ) : toPrefunctor.symm (f ⋙q g) = toPrefunctor.symm g ∘ toPrefunctor.symm f

def Quiver.SingleObj.pathToList {α : Type u_1} {x : SingleObj α} : Path (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 α → Path (star α) (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.SingleObj.listToPath l).cons a

theorem Quiver.SingleObj.listToPath_pathToList {α : Type u_1} {x : SingleObj α} (p : Path (star α) x) : listToPath (pathToList p) = Path.cast ⋯ ⋯ p

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

def Quiver.SingleObj.pathEquivList {α : Type u_1} : Path (star α) (star α) ≃ List α

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

Equations

• Quiver.SingleObj.pathEquivList = { toFun := Quiver.SingleObj.pathToList, invFun := Quiver.SingleObj.listToPath, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Quiver.SingleObj.pathEquivList_nil {α : Type u_1} : pathEquivList Path.nil = []

@[simp]

theorem Quiver.SingleObj.pathEquivList_cons {α : Type u_1} (p : Path (star α) (star α)) (a : star α ⟶ star α) : pathEquivList (p.cons a) = a :: pathToList p

@[simp]

theorem Quiver.SingleObj.pathEquivList_symm_nil {α : Type u_1} : pathEquivList.symm [] = Path.nil

@[simp]

theorem Quiver.SingleObj.pathEquivList_symm_cons {α : Type u_1} (l : List α) (a : α) : pathEquivList.symm (a :: l) = (pathEquivList.symm l).cons a