Theorems · Definition · category theory

CategoryTheory.ReflQuiv.isoOfQuivIso

{V W : Type u} →
  [inst : CategoryTheory.ReflQuiver V] →
    [inst_1 : CategoryTheory.ReflQuiver W] →
      (e : CategoryTheory.Quiv.of V ≅ CategoryTheory.Quiv.of W) →
        (∀ (X : V), e.hom.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (e.hom.obj X)) →
          (CategoryTheory.ReflQuiv.of V ≅ CategoryTheory.ReflQuiv.of W)

An isomorphism of quivers lifts to an isomorphism of reflexive quivers given a suitable compatibility with the identities.

Defined in

Mathlib.CategoryTheory.Category.ReflQuiv

Cited by

0 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.ReflQuiverCategoryTheory.ReflQuiver