# mathlibdocumentation

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.

## Tags #

Frobenius reciprocity, cartesian closed functor

noncomputable def category_theory.frobenius_morphism {C : Type u} {D : Type u'} (F : C D) {L : D C} (h : L F) (A : C) :

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]
def category_theory.frobenius_morphism_iso_of_preserves_binary_products {C : Type u} {D : Type u'} (F : C D) {L : D C} (h : L F) (A : C)  :

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

noncomputable def category_theory.exp_comparison {C : Type u} {D : Type u'} (F : C D) (A : C) :

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

Equations
Instances for category_theory.exp_comparison
theorem category_theory.exp_comparison_ev {C : Type u} {D : Type u'} (F : C D) (A B : C) :
theorem category_theory.coev_exp_comparison {C : Type u} {D : Type u'} (F : C D) (A B : C) :
theorem category_theory.exp_comparison_whisker_left {C : Type u} {D : Type u'} (F : C D) {A A' : C} (f : A' A) :

The exponential comparison map is natural in A.

@[class]
• comparison_iso : ∀ (A : C),

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
theorem category_theory.frobenius_morphism_mate {C : Type u} {D : Type u'} (F : C D) {L : D C} (h : L F) (A : C) :
theorem category_theory.frobenius_morphism_iso_of_exp_comparison_iso {C : Type u} {D : Type u'} (F : C D) {L : D C} (h : L F) (A : C)  :

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

theorem category_theory.exp_comparison_iso_of_frobenius_morphism_iso {C : Type u} {D : Type u'} (F : C D) {L : D C} (h : L F) (A : C)  :

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.

Equations