English
Given isomorphisms X ≅ Y and W ≅ Z in a k-linear category, there is a natural k-linear isomorphism between Hom(X,W) and Hom(Y,Z) given by pre- and post-composition with the iso.
Русский
Даны изоморфизмы X ≅ Y и W ≅ Z в k-линейной категории; существует естественная k-линейная изоморфия между Hom(X,W) и Hom(Y,Z), заданная предварительной и последующей композицией с изоморфизмами.
LaTeX
$$$\\mathrm{Hom}_{C}(X,W) \\cong_{k} \\mathrm{Hom}_{C}(Y,Z) \\quad\\text{via pre- and post-composition with } f_1,f_2.$$$
Lean4
/-- Given isomorphic objects `X ≅ Y, W ≅ Z` in a `k`-linear category, we have a `k`-linear
isomorphism between `Hom(X, W)` and `Hom(Y, Z).` -/
def homCongr (k : Type*) {C : Type*} [Category C] [Semiring k] [Preadditive C] [Linear k C] {X Y W Z : C} (f₁ : X ≅ Y)
(f₂ : W ≅ Z) : (X ⟶ W) ≃ₗ[k] Y ⟶ Z :=
{
(rightComp k Y f₂.hom).comp
(leftComp k W
f₁.symm.hom) with
invFun := (leftComp k W f₁.hom).comp (rightComp k Y f₂.symm.hom)
left_inv := fun x => by
simp only [Iso.symm_hom, LinearMap.toFun_eq_coe, LinearMap.coe_comp, Function.comp_apply, leftComp_apply,
rightComp_apply, Category.assoc, Iso.hom_inv_id, Category.comp_id, Iso.hom_inv_id_assoc]
right_inv := fun x => by
simp only [Iso.symm_hom, LinearMap.coe_comp, Function.comp_apply, rightComp_apply, leftComp_apply,
LinearMap.toFun_eq_coe, Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id] }
