Embeddings of quivers

A TauCeti.QuiverEmbedding models a subquiver, which need not be full, by a prefunctor injective on vertices and on each set of arrows. Its vertex fibers have at most one point; this lets constructions such as extension by zero index their values over a vertex without choosing a preimage.

structure TauCeti.QuiverEmbedding (Q' : Type v') [Quiver Q'] (Q : Type v) [Quiver Q] extends Q' ⥤q Q : Type (max (max (max v v') w) w')

A prefunctor injective on vertices and on arrows between each pair of vertices. Its image is a subquiver that need not be full.

• obj : Q' → Q
• map {X Y : Q'} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
• obj_injective : Function.Injective self.obj

  The embedding is injective on vertices.

• map_injective {a b : Q'} : Function.Injective self.map

  The embedding is injective on the arrows between each pair of vertices.

theorem TauCeti.QuiverEmbedding.ext {Q' : Type v'} [Quiver Q'] {Q : Type v} [Quiver Q] (φ : QuiverEmbedding Q' Q) {ψ : QuiverEmbedding Q' Q} (h_obj : ∀ (u : Q'), φ.obj u = ψ.obj u) (h_map : ∀ (u u' : Q') (a : u ⟶ u'), φ.map a = Eq.recOn ⋯ (Eq.recOn ⋯ (ψ.map a))) : φ = ψ

Two quiver embeddings are equal when their vertex and arrow maps agree.

@[reducible, inline]

abbrev TauCeti.QuiverEmbedding.Fiber {Q' : Type v'} [Quiver Q'] {Q : Type v} [Quiver Q] (φ : QuiverEmbedding Q' Q) (v : Q) : Type v'

The vertices of Q' over a vertex v of Q. There is at most one, since φ is injective on vertices.

Equations

• φ.Fiber v = { u : Q' // φ.obj u = v }

instance TauCeti.QuiverEmbedding.instSubsingletonFiber {Q' : Type v'} [Quiver Q'] {Q : Type v} [Quiver Q] (φ : QuiverEmbedding Q' Q) (v : Q) : Subsingleton (φ.Fiber v)

Each vertex fiber of an embedding contains at most one point.