Theorems · Definition · combinatorics

Prefunctor.costar

{U : Type u_1} →
  [inst : Quiver U] →
    {V : Type u_2} → [inst_1 : Quiver V] → (φ : U ⥤q V) → (u : U) → Quiver.Costar u → Quiver.Costar (φ.obj u)

A prefunctor induces a map of Quiver.Costar at every vertex.

Defined in

Mathlib.Combinatorics.Quiver.Covering

Cited by

14 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

QuiverQuiver