mathlib3 documentation

category_theory.closed.functor

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

noncomputable def category_theory.frobenius_morphism {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_finite_products C] [category_theory.limits.has_finite_products D] (F : C ⥤ D) {L : D ⥤ C} (h : L ⊣ F) (A : C) :

category_theory.limits.prod.functor.obj (F.obj A) ⋙ L ⟶ L ⋙ category_theory.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

category_theory.frobenius_morphism F h A = category_theory.limits.prod_comparison_nat_trans L (F.obj A) ≫ category_theory.whisker_left L (category_theory.limits.prod.functor.map (h.counit.app A))

Instances for category_theory.frobenius_morphism

category_theory.frobenius_morphism_iso_of_preserves_binary_products

@[protected, instance]

def category_theory.frobenius_morphism_iso_of_preserves_binary_products {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_finite_products C] [category_theory.limits.has_finite_products D] (F : C ⥤ D) {L : D ⥤ C} (h : L ⊣ F) (A : C) [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) L] [category_theory.full F] [category_theory.faithful F] :

category_theory.is_iso (category_theory.frobenius_morphism 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.

noncomputable def category_theory.exp_comparison {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_finite_products C] [category_theory.limits.has_finite_products D] (F : C ⥤ D) [category_theory.cartesian_closed C] [category_theory.cartesian_closed D] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] (A : C) :

category_theory.exp A ⋙ F ⟶ F ⋙ category_theory.exp (F.obj A)

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

Equations

category_theory.exp_comparison F A = ⇑(category_theory.transfer_nat_trans (category_theory.exp.adjunction A) (category_theory.exp.adjunction (F.obj A))) (category_theory.limits.prod_comparison_nat_iso F A).inv

Instances for category_theory.exp_comparison

category_theory.cartesian_closed_functor.comparison_iso

theorem category_theory.exp_comparison_ev {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_finite_products C] [category_theory.limits.has_finite_products D] (F : C ⥤ D) [category_theory.cartesian_closed C] [category_theory.cartesian_closed D] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] (A B : C) :

category_theory.limits.prod.map (𝟙 (F.obj A)) ((category_theory.exp_comparison F A).app B) ≫ (category_theory.exp.ev (F.obj A)).app (F.obj B) = category_theory.inv (category_theory.limits.prod_comparison F A ((category_theory.exp A).obj B)) ≫ F.map ((category_theory.exp.ev A).app B)

theorem category_theory.coev_exp_comparison {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_finite_products C] [category_theory.limits.has_finite_products D] (F : C ⥤ D) [category_theory.cartesian_closed C] [category_theory.cartesian_closed D] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] (A B : C) :

F.map ((category_theory.exp.coev A).app B) ≫ (category_theory.exp_comparison F A).app (A ⨯ B) = (category_theory.exp.coev (F.obj A)).app (F.obj B) ≫ (category_theory.exp (F.obj A)).map (category_theory.inv (category_theory.limits.prod_comparison F A B))

theorem category_theory.uncurry_exp_comparison {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_finite_products C] [category_theory.limits.has_finite_products D] (F : C ⥤ D) [category_theory.cartesian_closed C] [category_theory.cartesian_closed D] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] (A B : C) :

category_theory.cartesian_closed.uncurry ((category_theory.exp_comparison F A).app B) = category_theory.inv (category_theory.limits.prod_comparison F A ((category_theory.exp A).obj B)) ≫ F.map ((category_theory.exp.ev A).app B)

theorem category_theory.exp_comparison_whisker_left {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_finite_products C] [category_theory.limits.has_finite_products D] (F : C ⥤ D) [category_theory.cartesian_closed C] [category_theory.cartesian_closed D] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] {A A' : C} (f : A' ⟶ A) :

category_theory.exp_comparison F A ≫ category_theory.whisker_left F (category_theory.pre (F.map f)) = category_theory.whisker_right (category_theory.pre f) F ≫ category_theory.exp_comparison F A'

The exponential comparison map is natural in A.

@[class]

structure category_theory.cartesian_closed_functor {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_finite_products C] [category_theory.limits.has_finite_products D] (F : C ⥤ D) [category_theory.cartesian_closed C] [category_theory.cartesian_closed D] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] :

comparison_iso : ∀ (A : C), category_theory.is_iso (category_theory.exp_comparison F A)

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} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_finite_products C] [category_theory.limits.has_finite_products D] (F : C ⥤ D) {L : D ⥤ C} [category_theory.cartesian_closed C] [category_theory.cartesian_closed D] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] (h : L ⊣ F) (A : C) :

⇑(category_theory.transfer_nat_trans_self (h.comp (category_theory.exp.adjunction A)) ((category_theory.exp.adjunction (F.obj A)).comp h)) (category_theory.frobenius_morphism F h A) = category_theory.exp_comparison F A

theorem category_theory.frobenius_morphism_iso_of_exp_comparison_iso {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_finite_products C] [category_theory.limits.has_finite_products D] (F : C ⥤ D) {L : D ⥤ C} [category_theory.cartesian_closed C] [category_theory.cartesian_closed D] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] (h : L ⊣ F) (A : C) [i : category_theory.is_iso (category_theory.exp_comparison F A)] :

category_theory.is_iso (category_theory.frobenius_morphism F h A)

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} [category_theory.category C] {D : Type u'} [category_theory.category D] [category_theory.limits.has_finite_products C] [category_theory.limits.has_finite_products D] (F : C ⥤ D) {L : D ⥤ C} [category_theory.cartesian_closed C] [category_theory.cartesian_closed D] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] (h : L ⊣ F) (A : C) [i : category_theory.is_iso (category_theory.frobenius_morphism F h A)] :

category_theory.is_iso (category_theory.exp_comparison F A)

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

category_theory.cartesian_closed_functor_of_left_adjoint_preserves_binary_products F h = {comparison_iso := _}