Theorems · Definition · category theory
CategoryTheory.Quiv.isoOfEquiv
{V W : Type u} →
[inst : Quiver V] →
[inst_1 : Quiver W] →
(e : V ≃ W) → ((X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)) → (CategoryTheory.Quiv.of V ≅ CategoryTheory.Quiv.of W)Compatible equivalences of types and hom-types induce an isomorphism of quivers.
- Defined in
- Mathlib.CategoryTheory.Category.Quiv
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- Equivstatement and proof · cited by 8,337
- CategoryTheory.Isostatement · cited by 3,963
- Equiv.symmproof · cited by 3,681
- CategoryTheory.Bundled.αproof · cited by 736
- Quiverstatement and proof · cited by 405
- CategoryTheory.Quivstatement · cited by 21
- Quiver.homOfEqproof · cited by 21
- CategoryTheory.Quiv.ofstatement and proof · cited by 8
Cited by1
Results whose statement or proof uses this declaration.
- CategoryTheory.ReflQuiv.isoOfEquivproof · cited by 0