CategoryTheory.expComparison_whiskerLeft
theorem CategoryTheory.expComparison_whiskerLeft :
∀ {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]
{A A' : C} (f : A' ⟶ A),
CategoryTheory.CategoryStruct.comp (CategoryTheory.expComparison F A)
(CategoryTheory.whiskerLeft F (CategoryTheory.pre (F.map f))) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.pre f) F)
(CategoryTheory.expComparison F A')
The theorem `CategoryTheory.expComparison_whiskerLeft` states that for any categories `C` and `D` that have finite products and are cartesian closed, and a given functor `F` from `C` to `D` that preserves the limits of shape `WalkingPair`, the exponential comparison map is natural in `A`. Specifically, if we have a morphism `f` from `A'` to `A` in `C`, the composition of `expComparison F A` and the left whisker of `CategoryTheory.pre (F.map f)` is equal to the composition of the right whisker of `CategoryTheory.pre f` and `expComparison F A'`.
In other words, it demonstrates a specific commutative diagram concerning the exponential comparison map in cartesian closed categories with finite products, highlighting its naturality with respect to a morphism in the category.
More concisely: In cartesian closed categories with finite products, for any functor preserving `WalkingPair` limits and any morphism, the exponential comparison map commutes with left and right whiskering, i.e., `expComparison F A . (CategoryTheory.pre (F.map f)) = CategoryTheory.pre f . expComparison F A'`.
|
CategoryTheory.frobeniusMorphism_iso_of_expComparison_iso
theorem CategoryTheory.frobeniusMorphism_iso_of_expComparison_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) {L : CategoryTheory.Functor D C} [inst_4 : CategoryTheory.CartesianClosed C]
[inst_5 : CategoryTheory.CartesianClosed D]
[inst_6 :
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)
This theorem states that in the context of two categories `C` and `D` that both have finite products and are cartesian closed, given a functor `F` from `C` to `D` and a functor `L` from `D` to `C` such that `L` is left adjoint to `F`, if the exponential comparison transformation at an object `A` in the category `C` is an isomorphism, then the Frobenius morphism at `A` is also an isomorphism. The Frobenius morphism and the exponential comparison transformation are both concepts related to adjunctions in category theory, and this theorem essentially connects the isomorphism properties of these two transformations in a specific setting.
More concisely: If functors `F: C -> D` and `L: D -> C` form an adjunction with `L` left adjoint to `F`, and the exponential comparison transformation at an object `A` in `C` is an isomorphism, then the Frobenius morphism at `A` is also an isomorphism.
|
CategoryTheory.cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts
theorem CategoryTheory.cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts :
∀ {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) {L : CategoryTheory.Functor D C} [inst_4 : CategoryTheory.CartesianClosed C]
[inst_5 : CategoryTheory.CartesianClosed D]
[inst_6 :
CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F],
(L ⊣ F) →
∀ [inst_7 : F.Full] [inst_8 : F.Faithful]
[inst_9 :
CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) L],
CategoryTheory.CartesianClosedFunctor F
This theorem states that for any categories `C` and `D`, if `C` and `D` both have finite products and are cartesian closed, and a functor `F` from `C` to `D` is both full and faithful, and there is a left adjoint functor `L` to `F` from `D` to `C` preserving binary products, then the functor `F` is cartesian closed. In other words, if you have a functor that fully and faithfully captures the structure of its domain category, and it has a left adjoint that preserves the specific structure of binary products, then this functor also preserves the cartesian closed structure. The converse of this statement, that a cartesian closed functor whose left adjoint preserves binary products is full and faithful, remains to be proven.
More concisely: If functors F : C -> D between cartesian closed categories C and D with finite products are full, faithful, and have a left adjoint L preserving binary products, then F is cartesian closed.
|
CategoryTheory.expComparison_iso_of_frobeniusMorphism_iso
theorem CategoryTheory.expComparison_iso_of_frobeniusMorphism_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) {L : CategoryTheory.Functor D C} [inst_4 : CategoryTheory.CartesianClosed C]
[inst_5 : CategoryTheory.CartesianClosed D]
[inst_6 :
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)
This theorem states that if the Frobenius morphism at a given object `A` in category `C` is an isomorphism, then the exponential comparison transformation (at `A`) is also an isomorphism. Specifically, it is applicable for categories `C` and `D` that have finite products and are cartesian closed, and for a functor `F` from `C` to `D` that preserves product limits. The functor `F` is assumed to have a right adjoint `L`, and the Frobenius morphism is defined in terms of `F` and `L`. The theorem ensures the isomorphism of the exponential comparison, which is a concept associated with the adjunction between `F` and `L` in cartesian closed categories.
More concisely: If the Frobenius morphism of a functor with a right adjoint between two cartesian closed categories preserving finite products and product limits is an isomorphism, then the exponential comparison transformation is also an isomorphism.
|