# 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

def CategoryTheory.frobeniusMorphism {C : Type u} {D : Type u'} [] (F : ) {L : } (h : L F) (A : C) :
(CategoryTheory.Limits.prod.functor.obj (F.obj A)).comp L L.comp (CategoryTheory.Limits.prod.functor.obj A)

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
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.frobeniusMorphism_iso_of_preserves_binary_products {C : Type u} {D : Type u'} [] (F : ) {L : } (h : L F) (A : C) [F.Full] [F.Faithful] :

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

Equations
• =
def CategoryTheory.expComparison {C : Type u} {D : Type u'} [] (F : ) (A : C) :
.comp F F.comp (CategoryTheory.exp (F.obj A))

The exponential comparison map. F is a cartesian closed functor if this is an iso for all A.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.coev_expComparison {C : Type u} {D : Type u'} [] (F : ) (A : C) (B : C) :
CategoryTheory.CategoryStruct.comp (F.map (.app B)) (.app (A B)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev (F.obj A)).app (F.obj B)) ((CategoryTheory.exp (F.obj A)).map )
theorem CategoryTheory.uncurry_expComparison {C : Type u} {D : Type u'} [] (F : ) (A : C) (B : C) :
theorem CategoryTheory.expComparison_whiskerLeft {C : Type u} {D : Type u'} [] (F : ) {A : C} {A' : C} (f : A' A) :

The exponential comparison map is natural in A.

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

• comparison_iso : ∀ (A : C),
Instances
theorem CategoryTheory.frobeniusMorphism_mate {C : Type u} {D : Type u'} [] (F : ) {L : } (h : L F) (A : C) :

If the exponential comparison transformation (at A) is an isomorphism, then the Frobenius morphism at A is an isomorphism.

If the Frobenius morphism at A is an isomorphism, then the exponential comparison transformation (at A) is an isomorphism.

If F is full and faithful, and has a left adjoint which preserves binary products, then it is cartesian closed.

TODO: Show the converse, that if F is cartesian closed and its left adjoint preserves binary products, then it is full and faithful.