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
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]
[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}
[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.exp A).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
Instances For
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.obj A))
((CategoryTheory.expComparison F A).app B))
((CategoryTheory.exp.ev (F.obj A)).app (F.obj B)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A (A ⟹ B)))
(F.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.map ((CategoryTheory.exp.coev A).app B))
((CategoryTheory.expComparison F A).app (A ⨯ B)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev (F.obj A)).app (F.obj B))
((CategoryTheory.exp (F.obj A)).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.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)
:
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]
:
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)
Instances
theorem
CategoryTheory.CartesianClosedFunctor.comparison_iso
{C : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} C} {D : Type u'} {inst_1 : CategoryTheory.Category.{v, u'} D}
{inst_2 : CategoryTheory.Limits.HasFiniteProducts C} {inst_3 : CategoryTheory.Limits.HasFiniteProducts D}
{F : CategoryTheory.Functor C D} {inst_4 : CategoryTheory.CartesianClosed C}
{inst_5 : CategoryTheory.CartesianClosed D}
{inst_6 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F}
[self : CategoryTheory.CartesianClosedFunctor F] (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.conjugateEquiv (h.comp (CategoryTheory.exp.adjunction A))
((CategoryTheory.exp.adjunction (F.obj A)).comp 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)]
:
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)]
:
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)
[F.Full]
[F.Faithful]
[CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) L]
:
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.