homEquivOfIso — Mathlib

English

An isomorphism of quivers yields an equivalence on hom-types between the two quivers.

Русский

Изоморфизм киверов порождает эквивалентность типов гом между ними.

LaTeX

$$$(X \to Y) \simeq (e.hom.obj X \to e.hom.obj Y)$$$

Lean4

/-- An isomorphism of quivers defines an equivalence on hom types. -/
@[simps]
def homEquivOfIso {V W : Quiv} (e : V ≅ W) {X Y : V} : (X ⟶ Y) ≃ (e.hom.obj X ⟶ e.hom.obj Y)
    where
  toFun f := e.hom.map f
  invFun g := Quiver.homOfEq (e.inv.map g) (by simp) (by simp)
  left_inv f := by simp [inv_map_hom_map_of_iso]
  right_inv g := by simp [hom_map_inv_map_of_iso]

Похожие утверждения