mathlib documentation

category_theory.closed.functor

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.

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
@[protected, instance]

If F is full and faithful and has a left adjoint L which preserves binary products, then the Frobenius morphism is an isomorphism.

@[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