Monoidal functors: tensor comparisons, transport, and conjugates #
The tensorator of a lax monoidal functor is natural in its right argument, giving a square between left tensoring and the functor.
For an oplax monoidal functor with invertible unit comparison, its tensor comparisons at the unit are invertible. Invertibility in either argument propagates across any colimit preserved by the two functors in the corresponding tensor comparison. This reduces tensor compatibility for objects built from coproducts and cokernels to the unit case.
A lax monoidal structure transports along a natural isomorphism of functors
(CategoryTheory.Functor.LaxMonoidal.transport), in the same way as Mathlib's
CategoryTheory.Functor.Monoidal.transport transports a monoidal structure. This is how a
functor isomorphic to a composite of lax monoidal functors inherits a lax monoidal structure.
For two monoidal adjunctions F₁ ⊣ G₁ and F₂ ⊣ G₂, where the right adjoints are lax monoidal
and the left adjoints carry the induced oplax monoidal structures, a natural transformation
σ : F₂ ⟶ F₁ whose conjugate G₁ ⟶ G₂ is a monoidal natural transformation is compatible with
the oplax structures (CategoryTheory.Adjunction.app_tensorUnit_comp_η_of_conjugateEquiv and
CategoryTheory.Adjunction.app_tensor_comp_δ_of_conjugateEquiv). This is how the comparison
isomorphisms between left adjoints, such as the composition isomorphism of pullback functors, are
shown to respect their oplax monoidal structures from the corresponding facts about the right
adjoints.
Doctrinal adjunction for tensorators: if F ⊣ G is an adjunction between lax monoidal
functors whose unit and counit are compatible with the tensorators, then the tensorator of the
left adjoint F is invertible (CategoryTheory.Adjunction.isIso_μ_of_unit_of_counit), and its
inverse is the mate of the tensorator of G (CategoryTheory.Adjunction.inv_μ_eq_homEquiv_symm),
the tensor comparison of CategoryTheory.Adjunction.leftAdjointOplaxMonoidal. This is how a
left adjoint that is lax monoidal for an independent reason, such as restriction of sheaves to an
open subset, is shown to have invertible oplax tensor comparisons.
References #
- G. M. Kelly, Doctrinal adjunction, Lecture Notes in Mathematics 420 (1974).
The natural tensorator square for left tensoring by A under a lax monoidal functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The component of the tensorator square is the tensorator.
The natural oplax tensor comparison for right tensoring by B.
Equations
- F.oplaxCommTensorRight B = { app := fun (A : C) => CategoryTheory.Functor.OplaxMonoidal.δ F A B, naturality := ⋯ }
Instances For
The component of the oplax tensor comparison is the oplax tensorator.
The natural oplax tensor comparison for left tensoring by A.
Equations
- F.oplaxCommTensorLeft A = { app := fun (B : C) => CategoryTheory.Functor.OplaxMonoidal.δ F A B, naturality := ⋯ }
Instances For
The component of the oplax tensor comparison is the oplax tensorator.
An invertible unit comparison makes the tensor comparison at the left unit invertible.
Invertibility of an oplax tensor comparison extends across a colimit when the functor and right tensoring preserve that colimit.
An invertible unit comparison makes the tensor comparison at the right unit invertible.
Invertibility of an oplax tensor comparison extends across a colimit when the functor and left tensoring preserve that colimit.
Transport a lax monoidal structure along a natural isomorphism of functors. This is the lax
analogue of Mathlib's CategoryTheory.Functor.Monoidal.transport.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unit of the transported lax monoidal structure.
The unit of the transported lax monoidal structure.
The tensorator of the transported lax monoidal structure.
The tensorator of the transported lax monoidal structure.
A natural transformation between left adjoints whose conjugate is a monoidal natural transformation of the lax monoidal right adjoints is compatible with the units of the oplax monoidal structures.
A natural transformation between left adjoints whose conjugate is a monoidal natural transformation of the lax monoidal right adjoints is compatible with the tensor comparison maps of the oplax monoidal structures.
A natural transformation between left adjoints whose conjugate is a monoidal natural transformation of the lax monoidal right adjoints is compatible with the tensor comparison maps of the oplax monoidal structures.
If the counit of an adjunction between lax monoidal functors is compatible with the tensorators, then the tensorator of the left adjoint is a split monomorphism, split by the mate of the tensorator of the right adjoint.
If the unit of an adjunction between lax monoidal functors is compatible with the tensorators, then the mate of the tensorator of the right adjoint is a section of the tensorator of the left adjoint.
Doctrinal adjunction for tensorators: if the unit and the counit of an adjunction
between lax monoidal functors are compatible with the tensorators, then the tensorator of the
left adjoint is invertible. Its inverse is computed by inv_μ_eq_homEquiv_symm.
If the counit of an adjunction between lax monoidal functors is compatible with the
tensorators, then an inverse of the tensorator of the left adjoint is the mate of the tensorator
of the right adjoint, that is, the tensor comparison of the oplax monoidal structure
CategoryTheory.Adjunction.leftAdjointOplaxMonoidal.