inv_map_hom_map_of_iso — Mathlib

English

Dual statement: mapping through the inverse then the forward equals the original morphism.

Русский

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

LaTeX

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

Lean4

theorem inv_map_hom_map_of_iso {V W : Quiv} (e : V ≅ W) {X Y : V} (f : X ⟶ Y) :
    e.inv.map (e.hom.map f) = Quiver.homOfEq f (by simp) (by simp) :=
  hom_map_inv_map_of_iso e.symm f

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