mathlib documentation


Cartesian closed functors #

Define the exponential comparison morphisms for a functor which preserves binary products, and use them to define a cartesian closed functor: one which (naturally) preserves exponentials.

Define the Frobenius morphism, and show it is an isomorphism iff the exponential comparison is an isomorphism.


Some of the results here are true more generally for closed objects and for closed monoidal categories, and these could be generalised.

References #

Tags #

Frobenius reciprocity, cartesian closed functor

The Frobenius morphism for an adjunction L ⊣ F at A is given by the morphism

L(FA  B)  LFA  LB  A  LB

natural in B, where the first morphism is the product comparison and the latter uses the counit of the adjunction.

We will show that if C and D are cartesian closed, then this morphism is an isomorphism for all A iff F is a cartesian closed functor, i.e. it preserves exponentials.


The functor F is cartesian closed (ie preserves exponentials) if each natural transformation exp_comparison F A is an isomorphism