# Documentation

Mathlib.CategoryTheory.Monoidal.NaturalTransformation

# 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.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 : 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.

Instances For
@[simp]
theorem CategoryTheory.MonoidalNatTrans.vcomp_toNatTrans_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } (α : ) (β : ) (X : C) :
().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.

Instances For
@[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
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_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } {K : } (α : ) (β : ) (X : C) :
().app X = (α.toNatTrans β.toNatTrans).app X
def CategoryTheory.MonoidalNatTrans.hcomp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } {K : } (α : ) (β : ) :

Horizontal composition of monoidal natural transformations.

Instances For
@[simp]
theorem CategoryTheory.MonoidalNatTrans.prod_toNatTrans_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } {K : } (α : ) (β : ) (X : C) :
().app X = (α.app X, β.app X)
def CategoryTheory.MonoidalNatTrans.prod {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } {K : } (α : ) (β : ) :

The cartesian product of two monoidal natural transformations is monoidal.

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' : = G) (tensor' : ∀ (X Y : C), = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (app X).hom (app Y).hom) ()) :
F G

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

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 : = G) (tensor : ∀ (X Y : C), = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (app X).hom (app Y).hom) ()) (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 : = G) (tensor : ∀ (X Y : C), = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (app X).hom (app Y).hom) ()) (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)] :
@[simp]
theorem CategoryTheory.monoidalUnit_toNatTrans {C : Type u₁} [] {D : Type u₂} [] (F : ) [CategoryTheory.IsEquivalence F.toFunctor] :
().toNatTrans = (CategoryTheory.Functor.asEquivalence F.toFunctor).unit
def CategoryTheory.monoidalUnit {C : Type u₁} [] {D : Type u₂} [] (F : ) [CategoryTheory.IsEquivalence F.toFunctor] :
F.toLaxMonoidalFunctor ⊗⋙ ().toLaxMonoidalFunctor

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

Instances For
@[simp]
theorem CategoryTheory.monoidalCounit_toNatTrans {C : Type u₁} [] {D : Type u₂} [] (F : ) [CategoryTheory.IsEquivalence F.toFunctor] :
().toNatTrans = (CategoryTheory.Functor.asEquivalence F.toFunctor).counit
def CategoryTheory.monoidalCounit {C : Type u₁} [] {D : Type u₂} [] (F : ) [CategoryTheory.IsEquivalence F.toFunctor] :
().toLaxMonoidalFunctor ⊗⋙ F.toLaxMonoidalFunctor

The counit of a monoidal equivalence can be upgraded to a monoidal natural transformation.

Instances For