mathlib documentation

category_theory.closed.functor_category

Functors from a groupoid into a monoidal closed category form a monoidal closed category. #

(Using the pointwise monoidal structure on the functor category.)

Auxiliary definition for category_theory.monoidal_closed.functor_closed. The internal hom functor F ⟶[C] -

Equations

Auxiliary definition for category_theory.monoidal_closed.functor_closed. The unit for the adjunction (tensor_left F) ⊣ (ihom F).

Equations

Auxiliary definition for category_theory.monoidal_closed.functor_closed. The counit for the adjunction (tensor_left F) ⊣ (ihom F).

Equations
@[protected, instance]

If C is a monoidal closed category and D is groupoid, then every functor F : D ⥤ C is closed in the functor category F : D ⥤ C with the pointwise monoidal structure.

Equations
@[protected, instance]

If C is a monoidal closed category and D is groupoid, then the functor category D ⥤ C, with the pointwise monoidal structure, is monoidal closed.

Equations