The loop quiver

The loop quiver •↺ has a single vertex and a single arrow from it to itself. It is the smallest quiver that is not acyclic, which makes it the standard boundary case of the theory: its path algebra is the infinite-dimensional k[X] (TauCeti.RepresentationTheory.Quiver.OneLoop.PathAlgebra), and it has infinite representation type over every field (TauCeti.RepresentationTheory.Quiver.OneLoop.FiniteRepType).

This file defines the vertex and arrow data and classifies paths by their length, independently of the algebra and representation theory.

Main definitions

• TauCeti.Quiver.OneLoop: the vertex type, a singleton, with a Quiver instance whose only arrow type is PUnit.
• TauCeti.Quiver.OneLoop.loop: the unique arrow, from the vertex to itself.
• TauCeti.Quiver.OneLoop.totalPathEquivNat: paths are classified by their length.

inductive TauCeti.Quiver.OneLoop : Type

The quiver with one vertex and one loop.

• vertex : OneLoop

@[instance_reducible]

instance TauCeti.Quiver.instDecidableEqOneLoop : DecidableEq OneLoop

Equations

• TauCeti.Quiver.instDecidableEqOneLoop x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TauCeti.Quiver.OneLoop.instFintype : Fintype OneLoop

Equations

• TauCeti.Quiver.OneLoop.instFintype = { elems := {TauCeti.Quiver.OneLoop.vertex}, complete := ⋯ }

@[instance_reducible]

instance TauCeti.Quiver.OneLoop.instUnique : Unique OneLoop

Equations

• TauCeti.Quiver.OneLoop.instUnique = { default := TauCeti.Quiver.OneLoop.vertex, uniq := ⋯ }

@[instance_reducible]

instance TauCeti.Quiver.OneLoop.instQuiver : Quiver OneLoop

Equations

• TauCeti.Quiver.OneLoop.instQuiver = { Hom := fun (x x_1 : TauCeti.Quiver.OneLoop) => PUnit.{?u.1 + 1} }

instance TauCeti.Quiver.OneLoop.instSubsingletonHom (a b : OneLoop) : Subsingleton (a ⟶ b)

def TauCeti.Quiver.OneLoop.loop : vertex ⟶ vertex

The unique loop in the one-loop quiver.

Equations

• TauCeti.Quiver.OneLoop.loop = PUnit.unit

def TauCeti.Quiver.OneLoop.totalPathEquivNat : (a : OneLoop) × (b : OneLoop) × Quiver.Path a b ≃ ℕ

Paths in the one-loop quiver are classified by their length.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Quiver.OneLoop.totalPathEquivNat_apply (x : (a : OneLoop) × (b : OneLoop) × Quiver.Path a b) : totalPathEquivNat x = x.snd.snd.length

The path classification sends each path to its length.

@[simp]

theorem TauCeti.Quiver.OneLoop.length_totalPathEquivNat_symm (n : ℕ) : (totalPathEquivNat.symm n).snd.snd.length = n

The canonical path associated with n has length n.