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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasFiniteProducts D] (F : CategoryTheory.Functor C D) {L : CategoryTheory.Functor D C} (h : L ⊣ F) (A : C) : CategoryTheory.Functor.comp (CategoryTheory.Limits.prod.functor.toPrefunctor.obj (F.toPrefunctor.obj A)) L ⟶ CategoryTheory.Functor.comp L (CategoryTheory.Limits.prod.functor.toPrefunctor.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.

instance CategoryTheory.frobeniusMorphism_iso_of_preserves_binary_products {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasFiniteProducts D] (F : CategoryTheory.Functor C D) {L : CategoryTheory.Functor D C} (h : L ⊣ F) (A : C) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) L] [CategoryTheory.Full F] [CategoryTheory.Faithful F] : CategoryTheory.IsIso (CategoryTheory.frobeniusMorphism F h A)

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

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.frobeniusMorphism F h A)) = (_ : CategoryTheory.IsIso (CategoryTheory.frobeniusMorphism F h A))

def CategoryTheory.expComparison {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasFiniteProducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.CartesianClosed C] [CategoryTheory.CartesianClosed D] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] (A : C) : CategoryTheory.Functor.comp (CategoryTheory.exp A) F ⟶ CategoryTheory.Functor.comp F (CategoryTheory.exp (F.toPrefunctor.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.

theorem CategoryTheory.expComparison_ev {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasFiniteProducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.CartesianClosed C] [CategoryTheory.CartesianClosed D] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] (A : C) (B : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj A)) ((CategoryTheory.expComparison F A).app B)) ((CategoryTheory.exp.ev (F.toPrefunctor.obj A)).app (F.toPrefunctor.obj B)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A (A ⟹ B))) (F.toPrefunctor.map ((CategoryTheory.exp.ev A).app B))

theorem CategoryTheory.coev_expComparison {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasFiniteProducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.CartesianClosed C] [CategoryTheory.CartesianClosed D] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] (A : C) (B : C) : CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map ((CategoryTheory.exp.coev A).app B)) ((CategoryTheory.expComparison F A).app (A ⨯ B)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev (F.toPrefunctor.obj A)).app (F.toPrefunctor.obj B)) ((CategoryTheory.exp (F.toPrefunctor.obj A)).toPrefunctor.map (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B)))

theorem CategoryTheory.uncurry_expComparison {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasFiniteProducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.CartesianClosed C] [CategoryTheory.CartesianClosed D] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] (A : C) (B : C) : CategoryTheory.CartesianClosed.uncurry ((CategoryTheory.expComparison F A).app B) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A (A ⟹ B))) (F.toPrefunctor.map ((CategoryTheory.exp.ev A).app B))

theorem CategoryTheory.expComparison_whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasFiniteProducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.CartesianClosed C] [CategoryTheory.CartesianClosed D] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] {A : C} {A' : C} (f : A' ⟶ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.expComparison F A) (CategoryTheory.whiskerLeft F (CategoryTheory.pre (F.toPrefunctor.map f))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.pre f) F) (CategoryTheory.expComparison F A')

The exponential comparison map is natural in A.

class CategoryTheory.CartesianClosedFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasFiniteProducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.CartesianClosed C] [CategoryTheory.CartesianClosed D] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] : Prop

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

• comparison_iso : ∀ (A : C), CategoryTheory.IsIso (CategoryTheory.expComparison F A)

theorem CategoryTheory.frobeniusMorphism_mate {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasFiniteProducts D] (F : CategoryTheory.Functor C D) {L : CategoryTheory.Functor D C} [CategoryTheory.CartesianClosed C] [CategoryTheory.CartesianClosed D] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] (h : L ⊣ F) (A : C) : (CategoryTheory.transferNatTransSelf (CategoryTheory.Adjunction.comp h (CategoryTheory.exp.adjunction A)) (CategoryTheory.Adjunction.comp (CategoryTheory.exp.adjunction (F.toPrefunctor.obj A)) h)) (CategoryTheory.frobeniusMorphism F h A) = CategoryTheory.expComparison F A

theorem CategoryTheory.frobeniusMorphism_iso_of_expComparison_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasFiniteProducts D] (F : CategoryTheory.Functor C D) {L : CategoryTheory.Functor D C} [CategoryTheory.CartesianClosed C] [CategoryTheory.CartesianClosed D] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] (h : L ⊣ F) (A : C) [i : CategoryTheory.IsIso (CategoryTheory.expComparison F A)] : CategoryTheory.IsIso (CategoryTheory.frobeniusMorphism F h A)

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

theorem CategoryTheory.expComparison_iso_of_frobeniusMorphism_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasFiniteProducts D] (F : CategoryTheory.Functor C D) {L : CategoryTheory.Functor D C} [CategoryTheory.CartesianClosed C] [CategoryTheory.CartesianClosed D] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] (h : L ⊣ F) (A : C) [i : CategoryTheory.IsIso (CategoryTheory.frobeniusMorphism F h A)] : CategoryTheory.IsIso (CategoryTheory.expComparison F A)

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

theorem CategoryTheory.cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasFiniteProducts D] (F : CategoryTheory.Functor C D) {L : CategoryTheory.Functor D C} [CategoryTheory.CartesianClosed C] [CategoryTheory.CartesianClosed D] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] (h : L ⊣ F) [CategoryTheory.Full F] [CategoryTheory.Faithful F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) L] : CategoryTheory.CartesianClosedFunctor F

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.