mathlib3 documentation

category_theory.closed.functor

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.

TODO #

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

References #

https://ncatlab.org/nlab/show/cartesian+closed+functor https://ncatlab.org/nlab/show/Frobenius+reciprocity

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.

Equations
Instances for category_theory.frobenius_morphism
@[class]

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