isoOfQuivIso — Mathlib

Lean4
/-- An isomorphism of quivers lifts to an isomorphism of reflexive quivers given a suitable
compatibility with the identities. -/
def isoOfQuivIso {V W : Type u} [ReflQuiver V] [ReflQuiver W] (e : Quiv.of V ≅ Quiv.of W)
    (h_id : ∀ (X : V), e.hom.map (𝟙rq X) = ReflQuiver.id (obj := W) (e.hom.obj X)) : ReflQuiv.of V ≅ ReflQuiv.of W
    where
  hom := ReflPrefunctor.mk e.hom h_id
  inv :=
    ReflPrefunctor.mk e.inv (fun Y => (Quiv.homEquivOfIso e).injective (by simp [Quiv.hom_map_inv_map_of_iso, h_id]))
  hom_inv_id := by
    apply forgetToQuiv.map_injective
    exact e.hom_inv_id
  inv_hom_id := by
    apply forgetToQuiv.map_injective
    exact e.inv_hom_id
Похожие утверждения