homFromEquiv — Mathlib

English

Given X ≅ Y, there is a natural bijection between morphisms X → Z and Y → Z, implemented by precomposing with α⁻¹ and postcomposing with α.

Русский

Если X изоморфен Y, существует естественная биекция между мороморфизмами X → Z и Y → Z, задаваемая через композицию с α⁻¹ слева и α справа.

LaTeX

$$(X ⟶ Z) ≃ (Y ⟶ Z) \u2203 f \mapsto α^{-1} ∘ f, g \mapsto α ∘ g$$

Lean4

/-- The bijection `(X ⟶ Z) ≃ (Y ⟶ Z)` induced by `α : X ≅ Y`. -/
@[simps]
def homFromEquiv (α : X ≅ Y) {Z : C} : (X ⟶ Z) ≃ (Y ⟶ Z)
    where
  toFun f := α.inv ≫ f
  invFun g := α.hom ≫ g
  left_inv := by cat_disch
  right_inv := by cat_disch

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