Theorems · Definition · combinatorics

Quiver.Symmetrify.lift

{V : Type u_2} →
  [inst : Quiver V] →
    {V' : Type u_4} → [inst_1 : Quiver V'] → [Quiver.HasReverse V'] → V ⥤q V' → Quiver.Symmetrify V ⥤q V'

Given a quiver V' with reversible arrows, a prefunctor to V' can be lifted to one from Symmetrify V to V'

Defined in

Mathlib.Combinatorics.Quiver.Symmetric

Cited by

5 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

QuiverQuiverQuiver.HasReverse