# Monoidal natural transformations #

Natural transformations between (lax) monoidal functors must satisfy an additional compatibility relation with the tensorators: F.μ X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ X Y.

(Lax) monoidal functors between a fixed pair of monoidal categories themselves form a category.

theorem CategoryTheory.MonoidalNatTrans.ext {C : Type u₁} :
∀ {inst : } {inst_1 : } {D : Type u₂} {inst_2 : } {inst_3 : } {F G : } (x y : ), x.app = y.appx = y
theorem CategoryTheory.MonoidalNatTrans.ext_iff {C : Type u₁} :
∀ {inst : } {inst_1 : } {D : Type u₂} {inst_2 : } {inst_3 : } {F G : } (x y : ), x = y x.app = y.app
structure CategoryTheory.MonoidalNatTrans {C : Type u₁} [] {D : Type u₂} [] (F : ) (G : ) extends :
Type (max u₁ v₂)

A monoidal natural transformation is a natural transformation between (lax) monoidal functors additionally satisfying: F.μ X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ X Y

Instances For
@[simp]
theorem CategoryTheory.MonoidalNatTrans.unit {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (self : ) :
CategoryTheory.CategoryStruct.comp F (self.app (𝟙_ C)) = G

The unit condition for a monoidal natural transformation.

@[simp]
theorem CategoryTheory.MonoidalNatTrans.tensor {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (self : ) (X : C) (Y : C) :

The tensor condition for a monoidal natural transformation.

@[simp]
theorem CategoryTheory.MonoidalNatTrans.tensor_assoc {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (self : ) (X : C) (Y : C) {Z : D} (h : G.obj Z) :
@[simp]
theorem CategoryTheory.MonoidalNatTrans.unit_assoc {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (self : ) {Z : D} (h : G.obj (𝟙_ C) Z) :
@[simp]
theorem CategoryTheory.MonoidalNatTrans.id_toNatTrans_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
def CategoryTheory.MonoidalNatTrans.id {C : Type u₁} [] {D : Type u₂} [] (F : ) :

The identity monoidal natural transformation.

Equations
Instances For
instance CategoryTheory.MonoidalNatTrans.instInhabited {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Equations
@[simp]
theorem CategoryTheory.MonoidalNatTrans.vcomp_toNatTrans_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } (α : ) (β : ) (X : C) :
(α.vcomp β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
def CategoryTheory.MonoidalNatTrans.vcomp {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } (α : ) (β : ) :

Vertical composition of monoidal natural transformations.

Equations
• α.vcomp β = let __src := α.vcomp β.toNatTrans; { toNatTrans := __src, unit := , tensor := }
Instances For
Equations
• CategoryTheory.MonoidalNatTrans.categoryLaxMonoidalFunctor =
@[simp]
theorem CategoryTheory.MonoidalNatTrans.comp_toNatTrans_lax {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } {α : F G} {β : G H} :
.toNatTrans = CategoryTheory.CategoryStruct.comp α.toNatTrans β.toNatTrans
Equations
theorem CategoryTheory.MonoidalNatTrans.ext' {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {α : F G} {β : F G} (w : ∀ (X : C), α.app X = β.app X) :
α = β
@[simp]
theorem CategoryTheory.MonoidalNatTrans.comp_toNatTrans {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } {α : F G} {β : G H} :
.toNatTrans = CategoryTheory.CategoryStruct.comp α.toNatTrans β.toNatTrans
@[simp]
theorem CategoryTheory.MonoidalNatTrans.hcomp_toNatTrans {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } {K : } (α : ) (β : ) :
(α.hcomp β).toNatTrans = α.toNatTrans β.toNatTrans
def CategoryTheory.MonoidalNatTrans.hcomp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } {K : } (α : ) (β : ) :
CategoryTheory.MonoidalNatTrans (F.comp H) (G.comp K)

Horizontal composition of monoidal natural transformations.

Equations
• α.hcomp β = let __src := α.toNatTrans β.toNatTrans; { toNatTrans := __src, unit := , tensor := }
Instances For
@[simp]
theorem CategoryTheory.MonoidalNatTrans.prod_toNatTrans_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } {K : } (α : ) (β : ) (X : C) :
(α.prod β).app X = (α.app X, β.app X)
def CategoryTheory.MonoidalNatTrans.prod {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } {K : } (α : ) (β : ) :
CategoryTheory.MonoidalNatTrans (F.prod' H) (G.prod' K)

The cartesian product of two monoidal natural transformations is monoidal.

Equations
• α.prod β = { app := fun (X : C) => (α.app X, β.app X), naturality := , unit := , tensor := }
Instances For
def CategoryTheory.MonoidalNatIso.ofComponents {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (app : (X : C) → F.obj X G.obj X) (naturality' : ∀ {X Y : C} (f : X Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f)) (unit' : CategoryTheory.CategoryStruct.comp F (app (𝟙_ C)).hom = G) (tensor' : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (F X Y) ().hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (app X).hom (app Y).hom) (G X Y)) :
F G

Construct a monoidal natural isomorphism from object level isomorphisms, and the monoidal naturality in the forward direction.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.MonoidalNatIso.ofComponents.hom_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (app : (X : C) → F.obj X G.obj X) (naturality : ∀ {X Y : C} (f : X Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f)) (unit : CategoryTheory.CategoryStruct.comp F (app (𝟙_ C)).hom = G) (tensor : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (F X Y) ().hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (app X).hom (app Y).hom) (G X Y)) (X : C) :
(CategoryTheory.MonoidalNatIso.ofComponents app naturality unit tensor).hom.app X = (app X).hom
@[simp]
theorem CategoryTheory.MonoidalNatIso.ofComponents.inv_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (app : (X : C) → F.obj X G.obj X) (naturality : ∀ {X Y : C} (f : X Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f)) (unit : CategoryTheory.CategoryStruct.comp F (app (𝟙_ C)).hom = G) (tensor : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (F X Y) ().hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (app X).hom (app Y).hom) (G X Y)) (X : C) :
(CategoryTheory.MonoidalNatIso.ofComponents app naturality unit tensor).inv.app X = (app X).inv
instance CategoryTheory.MonoidalNatIso.isIso_of_isIso_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) [∀ (X : C), CategoryTheory.IsIso (α.app X)] :
Equations
• =
def CategoryTheory.monoidalUnit {C : Type u₁} [] {D : Type u₂} [] (F : ) {G : } (h : F.toFunctor G) :

The unit of a adjunction can be upgraded to a monoidal natural transformation.

Equations
• = { toNatTrans := h.unit, unit := , tensor := }
Instances For
@[simp]
theorem CategoryTheory.monoidalCounit_toNatTrans {C : Type u₁} [] {D : Type u₂} [] (F : ) {G : } (h : F.toFunctor G) :
.toNatTrans = h.counit
def CategoryTheory.monoidalCounit {C : Type u₁} [] {D : Type u₂} [] (F : ) {G : } (h : F.toFunctor G) :
.comp F.toLaxMonoidalFunctor

The unit of a adjunction can be upgraded to a monoidal natural transformation.

Equations
• = { toNatTrans := h.counit, unit := , tensor := }
Instances For
instance CategoryTheory.instIsIsoLaxMonoidalFunctorMonoidalUnitOfIsEquivalence {C : Type u₁} [] {D : Type u₂} [] (F : ) {G : } (h : F.toFunctor G) [F.IsEquivalence] :
Equations
• =
instance CategoryTheory.instIsIsoLaxMonoidalFunctorMonoidalCounitOfIsEquivalence {C : Type u₁} [] {D : Type u₂} [] (F : ) {G : } (h : F.toFunctor G) [F.IsEquivalence] :
Equations
• =