isoOfEquiv — Mathlib

English

A compatible equivalence of types and hom-types induces an isomorphism of quivers.

Русский

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

LaTeX

$$$\text{isoOfEquiv}: Quiv.of V \cong Quiv.of W$$$

Lean4

/-- Compatible equivalences of types and hom-types induce an isomorphism of quivers. -/
def isoOfEquiv : Quiv.of V ≅ Quiv.of W where
  hom := Prefunctor.mk e (he _ _)
  inv :=
    { obj := e.symm
      map {X Y} f := (he _ _).symm (Quiver.homOfEq f (by simp) (by simp)) }
  hom_inv_id :=
    Prefunctor.ext' e.left_inv
      (fun X Y f ↦ by
        dsimp [Quiv.id_eq_id, Quiv.comp_eq_comp]
        apply (he _ _).injective
        apply Quiver.homOfEq_injective (X' := e X) (Y' := e Y) (by simp) (by simp)
        simp)
  inv_hom_id := Prefunctor.ext' e.right_inv (by simp [Quiv.id_eq_id, Quiv.comp_eq_comp])

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