mathlib3 documentation


Cartesian closed functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Instances for category_theory.frobenius_morphism

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

Instances for category_theory.cartesian_closed_functor
  • category_theory.cartesian_closed_functor.has_sizeof_inst