Braiding and monoidal adjunctions

In a monoidal adjunction, a lax braided right adjoint makes the left adjoint's oplax tensor map compatible with braiding. If the left adjoint is strong monoidal, it is therefore braided. Conversely, a braided strong monoidal left adjoint gives its right adjoint a lax braided structure.

These facts apply to sheafification and to the pullback--pushforward adjunction of modules.

theorem CategoryTheory.Adjunction.map_braiding_hom_comp_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] [G.LaxBraided] [adj.IsMonoidal] (X Y : C) : CategoryStruct.comp (F.map (β_ X Y).hom) (Functor.OplaxMonoidal.δ F Y X) = CategoryStruct.comp (Functor.OplaxMonoidal.δ F X Y) (β_ (F.obj X) (F.obj Y)).hom

The oplax tensor map of a left adjoint respects braiding when the lax tensor map of its right adjoint does. No invertibility of the left adjoint's tensor map is required.

theorem CategoryTheory.Adjunction.map_braiding_hom_comp_δ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.OplaxMonoidal] [G.LaxBraided] [adj.IsMonoidal] (X Y : C) {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj X) ⟶ Z) : CategoryStruct.comp (F.map (β_ X Y).hom) (CategoryStruct.comp (Functor.OplaxMonoidal.δ F Y X) h) = CategoryStruct.comp (Functor.OplaxMonoidal.δ F X Y) (CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom h)

The oplax tensor map of a left adjoint respects braiding when the lax tensor map of its right adjoint does. No invertibility of the left adjoint's tensor map is required.

@[instance_reducible]

def CategoryTheory.Adjunction.leftAdjointBraided {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Monoidal] [G.LaxBraided] [adj.IsMonoidal] : F.Braided

A strong monoidal left adjoint of a lax braided right adjoint is braided, for compatible monoidal structures. Its monoidal structure is the given structure on F.

Equations

• adj.leftAdjointBraided = { toMonoidal := inferInstance, braided := ⋯ }

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointBraided_toMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [hF : F.Monoidal] [G.LaxBraided] [adj.IsMonoidal] : adj.leftAdjointBraided.toMonoidal = hF

The braided left adjoint retains its supplied monoidal structure.

@[instance_reducible]

def CategoryTheory.Adjunction.rightAdjointLaxBraided {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Braided] [G.LaxMonoidal] [adj.IsMonoidal] : G.LaxBraided

A braided strong monoidal left adjoint gives a compatible lax monoidal right adjoint a lax braided structure, with the given lax monoidal structure on G.

Equations

• adj.rightAdjointLaxBraided = { toLaxMonoidal := inferInstance, braided := ⋯ }

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointLaxBraided_toLaxMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Braided] [hG : G.LaxMonoidal] [adj.IsMonoidal] : adj.rightAdjointLaxBraided.toLaxMonoidal = hG

The lax braided right adjoint retains its supplied lax monoidal structure.