Internal Hom comparison for monoidal functors #
A lax monoidal functor F : C ⥤ D has a canonical comparison morphism whenever
A and F.obj A are closed:
F.obj (A ⟶[C] B) ⟶ (F.obj A ⟶[D] F.obj B).
It is the mate, under the two tensor--Hom adjunctions, of the tensorator
F.obj A ⊗ F.obj B ⟶ F.obj (A ⊗ B). This file packages the comparison as a natural
transformation in B, characterizes it by evaluation and coevaluation, and proves its
contravariant naturality in A. These formulas allow closed-structure comparisons to be used
without unfolding the mates construction.
The construction generalizes Mathlib's Cartesian-closed CategoryTheory.expComparison; its
definition and characteristic formulas follow the mate-based development in
Mathlib.CategoryTheory.Monoidal.Closed.Functor.
Main declarations #
CategoryTheory.Functor.ihomComparison: the internal Hom comparison of a lax monoidal functor;CategoryTheory.Functor.ihomComparison_ev: its characteristic equation against evaluation;CategoryTheory.Functor.ihomComparison_app_eq_curry: its componentwise curry formula;CategoryTheory.Functor.ihomComparison_isIso_of_tensor_comparison: an explicit compatibility criterion which turns that formula into an isomorphism;CategoryTheory.Functor.ihomComparison_unit_isIso: invertibility at the tensor unit for a strong monoidal functor;CategoryTheory.Functor.ihomComparison_isIso_of_iso: transport of an invertible comparison along an isomorphism in its source object;CategoryTheory.Functor.coev_ihomComparison: its characteristic equation against coevaluation;CategoryTheory.Functor.ihomComparison_whiskerLeft: its naturality in the source of the internal Hom;CategoryTheory.Functor.ihomComparison_comp: the comparison of a composite of lax monoidal functors;CategoryTheory.Monoidal.Reflective.ihomComparisonUnitIso: the comparison with the internal Hom transported to a reflective subcategory;CategoryTheory.Monoidal.Reflective.ihomComparison_app_eq_ihomComparisonUnitIso_inv: identifies that comparison with the internal-Hom comparison of the reflective right adjoint, which is therefore invertible (CategoryTheory.Monoidal.Reflective.isIso_ihomComparison).
The canonical comparison from the image of an internal Hom to the internal Hom of the images under a lax monoidal functor. It is natural in the target of the internal Hom.
Equations
- F.ihomComparison A = (CategoryTheory.mateEquiv (CategoryTheory.ihom.adjunction A) (CategoryTheory.ihom.adjunction (F.obj A))) (F.laxCommTensorLeft A)
Instances For
Evaluation after the internal Hom comparison is the image of evaluation, preceded by the
tensorator. This equation characterizes ihomComparison.
Evaluation after the internal Hom comparison is the image of evaluation, preceded by the
tensorator. This equation characterizes ihomComparison.
The image of coevaluation followed by the internal Hom comparison is coevaluation followed by the internal Hom of the tensorator.
The image of coevaluation followed by the internal Hom comparison is coevaluation followed by the internal Hom of the tensorator.
Uncurrying the internal Hom comparison gives the tensorator followed by the image of evaluation.
Each component of the internal Hom comparison is the curry of the tensorator followed by the image of evaluation.
The internal Hom comparison of a composite of lax monoidal functors is the image of the comparison of the first functor followed by the comparison of the second.
The internal Hom comparison is contravariantly natural in the source of the internal Hom.
If target comparisons to a common object T are compatible with the image of the
source tensor comparison, then the internal Hom comparison is an isomorphism.
The hypothesis is the evaluation equation for the transported target comparison. It is
the precise compatibility needed when a functor transports a chosen duality structure; it
is not supplied by arbitrary closed objects alone. The common target T is arbitrary; the
tensor object F.obj A ⊗ F.obj B is the natural choice when the target comparisons are
described through the tensorator.
A strong monoidal functor preserves the internal-Hom comparison at the tensor unit.
Transport invertibility of an internal-Hom comparison along an isomorphism in its source object.
The unit isomorphism comparing the internal Hom transported to a reflective subcategory with the ambient internal Hom.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For the closed structure supplied by Day reflection, the internal-Hom comparison of the reflective right adjoint is the inverse of the adjunction unit.
For the closed structure supplied by Day reflection, the internal-Hom comparison of the reflective right adjoint is an isomorphism: the internal Hom of the reflective subcategory is computed in the ambient category.