homToEquiv — Mathlib

English

An isomorphism α: X ≅ Y induces a bijection between morphisms from Z to X and from Z to Y, given by post-composing with α.hom and its inverse by post-composing with α.inv.

Русский

Изоморфизм α: X ≅ Y индуцирует биекции между морфизмами Z → X и Z → Y, задаваясь постсочетанием с α.hom и обратным постсочетанием с α.inv.

LaTeX

$$$(Z \to X) \cong (Z \to Y)$ via $f \mapsto f \circ α.hom$ with inverse $g \mapsto g \circ α.inv$$$

Lean4

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

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