functorHomEquiv — Mathlib

English

For functors G,H: C ⥤ Type, the natural equivalence between morphisms G ⟶ F.functorHom H and morphisms F ⊗ G ⟶ H is established; this is a canonical transport through two standard equivalences.

Русский

Для функторов G,H: C ⥤ Type существует естественное эквивалентство между морфизмами G ⟶ F.functorHom H и F ⊗ G ⟶ H, получаемое через две стандартные эквивалентности.

LaTeX

$$$ (G \\rightarrow F.functorHom H) \\simeq (F \\otimes G \\rightarrow H) $$$

Lean4

/-- When `F G H : C ⥤ Type max w v u`, we have `(G ⟶ F.functorHom H) ≃ (F ⊗ G ⟶ H)`. -/
@[simps!]
def functorHomEquiv (G H : C ⥤ Type max w v u) : (G ⟶ F.functorHom H) ≃ (F ⊗ G ⟶ H) :=
  (Functor.functorHomEquiv F H G).trans (homObjEquiv F H G)

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