English
Let X, X′, Y, Y′ be objects in a quiver, with arrows f: X → Y and g: X′ → Y′, and with identifications hX: X = X′ and hY: Y = Y′. Then the arrow obtained from f by transporting along hX and hY equals g if and only if f equals the arrow obtained by transporting g along hX⁻¹ and hY⁻¹.
Русский
Пусть X, X′, Y, Y′ — объекты квира, стрелы f: X → Y и g: X′ → Y′, а также тождества hX: X = X′ и hY: Y = Y′. Тогда стрелка, полученная из f после переноса вдоль hX и hY, равна g тогда и только если f равен стрелке, полученной переносом g вдоль hX⁻¹ и hY⁻¹.
LaTeX
$$$ \\forall X,X',Y,Y'\\, (f\\in\\operatorname{Hom}(X,Y)) (g\\in\\operatorname{Hom}(X',Y')) (hX:X=X') (hY:Y=Y'):\\; \\operatorname{homOfEq}(f,hX,hY) = g \\iff \\operatorname{homOfEq}(f,hX^{-1},hY^{-1}) = g.$$$
Lean4
theorem homOfEq_eq_iff {X X' Y Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X = X') (hY : Y = Y') :
Quiver.homOfEq f hX hY = g ↔ f = Quiver.homOfEq g hX.symm hY.symm := by subst hX hY; simp
