Documentation

Mathlib.CategoryTheory.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

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.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