Theorems · Theorem · combinatorics

Quiver.Symmetrify.lift_unique

∀ {V : Type u_2} [inst : Quiver V] {V' : Type u_4} [inst_1 : Quiver V'] [inst_2 : Quiver.HasReverse V'] (φ : V ⥤q V')
  (Φ : Quiver.Symmetrify V ⥤q V'),
  Quiver.Symmetrify.of ⋙q Φ = φ →
    (∀ {X Y : Quiver.Symmetrify V} (f : X ⟶ Y), Φ.map (Quiver.reverse f) = Quiver.reverse (Φ.map f)) →
      Φ = Quiver.Symmetrify.lift φ

lift φ is the only prefunctor extending φ and preserving reverses.

Defined in

Mathlib.Combinatorics.Quiver.Symmetric

Cited by

1 results in Mathlib

Foundations

Depth 7 from the axioms · uses Quot.sound

Assumes

QuiverQuiverQuiver.HasReverse