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
Some of the results here are true more generally for closed objects and for closed monoidal
categories, and these could be generalised.
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
B, where the first morphism is the product comparison and the latter uses the counit
of the adjunction.
We will show that if
D are cartesian closed, then this morphism is an isomorphism for all
F is a cartesian closed functor, i.e. it preserves exponentials.
F is full and faithful and has a left adjoint
L which preserves binary products, then the
Frobenius morphism is an isomorphism.
The exponential comparison map.
F is a cartesian closed functor if this is an iso for all
The exponential comparison map is natural in
F is cartesian closed (ie preserves exponentials) if each natural transformation
exp_comparison F A is an isomorphism
If the exponential comparison transformation (at
A) is an isomorphism, then the Frobenius morphism
A is an isomorphism.
If the Frobenius morphism at
A is an isomorphism, then the exponential comparison transformation
A) is an isomorphism.
F is full and faithful, and has a left adjoint which preserves binary products, then it is
TODO: Show the converse, that if
F is cartesian closed and its left adjoint preserves binary
products, then it is full and faithful.