hom_map_inv_map_of_iso — Mathlib

English

The map of morphisms under an isomorphism followed by its inverse equals the original morphism (compatibility of hom maps with isomorphisms).

Русский

Отображение морфизмов через изоморфизм и обратное изоморфизма возвращает исходный морфизм.

LaTeX

$$$e.hom.map (e.inv.map f) = \mathrm{homOfEq}(f, \dots)$$$

Lean4

theorem hom_map_inv_map_of_iso {V W : Quiv} (e : V ≅ W) {X Y : W} (f : X ⟶ Y) :
    e.hom.map (e.inv.map f) = Quiver.homOfEq f (by simp) (by simp) :=
  by
  rw [← Prefunctor.comp_map]
  exact (Prefunctor.congr_hom e.inv_hom_id.symm f).symm

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