Theorems · Definition · category theory

CategoryTheory.Functor.homObjEquiv

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G A : CategoryTheory.Functor C (Type w)) →
      F.HomObj G A ≃ (CategoryTheory.MonoidalCategoryStruct.tensorObj F A ⟶ G)

When F, G, and A are all functors C ⥤ Type w, then HomObj F G A is in bijection with F ⊗ A ⟶ G.

Defined in

Mathlib.CategoryTheory.Functor.FunctorHom

Cited by

3 results in Mathlib

Foundations

Depth 44 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category