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.

structure CategoryTheory.MonoidalNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) (G : CategoryTheory.LaxMonoidalFunctor C D) extends CategoryTheory.NatTrans : 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

• app : (X : C) → F.obj X ⟶ G.obj X
• naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (self.app Y) = CategoryTheory.CategoryStruct.comp (self.app X) (G.map f)
• unit : CategoryTheory.CategoryStruct.comp F.ε (self.app (𝟙_ C)) = G.ε

  The unit condition for a monoidal natural transformation.

• tensor : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (F.μ X Y) (self.app (CategoryTheory.MonoidalCategory.tensorObj X Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.app X) (self.app Y)) (G.μ X Y)

  The tensor condition for a monoidal natural transformation.

theorem CategoryTheory.MonoidalNatTrans.ext {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D} {F G : CategoryTheory.LaxMonoidalFunctor C D} {x y : CategoryTheory.MonoidalNatTrans F G}, x.app = y.app → x = y

@[simp]

theorem CategoryTheory.MonoidalNatTrans.unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (self : CategoryTheory.MonoidalNatTrans F G) : CategoryTheory.CategoryStruct.comp F.ε (self.app (𝟙_ C)) = G.ε

The unit condition for a monoidal natural transformation.

@[simp]

theorem CategoryTheory.MonoidalNatTrans.tensor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (self : CategoryTheory.MonoidalNatTrans F G) (X : C) (Y : C) : CategoryTheory.CategoryStruct.comp (F.μ X Y) (self.app (CategoryTheory.MonoidalCategory.tensorObj X Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.app X) (self.app Y)) (G.μ X Y)

The tensor condition for a monoidal natural transformation.

@[simp]

theorem CategoryTheory.MonoidalNatTrans.tensor_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (self : CategoryTheory.MonoidalNatTrans F G) (X : C) (Y : C) {Z : D} (h : G.obj (CategoryTheory.MonoidalCategory.tensorObj X Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.μ X Y) (CategoryTheory.CategoryStruct.comp (self.app (CategoryTheory.MonoidalCategory.tensorObj X Y)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.app X) (self.app Y)) (CategoryTheory.CategoryStruct.comp (G.μ X Y) h)

@[simp]

theorem CategoryTheory.MonoidalNatTrans.unit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (self : CategoryTheory.MonoidalNatTrans F G) {Z : D} (h : G.obj (𝟙_ C) ⟶ Z) : CategoryTheory.CategoryStruct.comp F.ε (CategoryTheory.CategoryStruct.comp (self.app (𝟙_ C)) h) = CategoryTheory.CategoryStruct.comp G.ε h

def CategoryTheory.MonoidalNatTrans.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) : CategoryTheory.MonoidalNatTrans F F

The identity monoidal natural transformation.

Equations

• CategoryTheory.MonoidalNatTrans.id F = { toNatTrans := CategoryTheory.CategoryStruct.id F.toFunctor, unit := ⋯, tensor := ⋯ }

@[simp]

theorem CategoryTheory.MonoidalNatTrans.id_toNatTrans_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) (X : C) : (CategoryTheory.MonoidalNatTrans.id F).app X = CategoryTheory.CategoryStruct.id (F.obj X)

instance CategoryTheory.MonoidalNatTrans.instInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) : Inhabited (CategoryTheory.MonoidalNatTrans F F)

Equations

• CategoryTheory.MonoidalNatTrans.instInhabited F = { default := CategoryTheory.MonoidalNatTrans.id F }

def CategoryTheory.MonoidalNatTrans.vcomp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} {H : CategoryTheory.LaxMonoidalFunctor C D} (α : CategoryTheory.MonoidalNatTrans F G) (β : CategoryTheory.MonoidalNatTrans G H) : CategoryTheory.MonoidalNatTrans F H

Vertical composition of monoidal natural transformations.

Equations

• α.vcomp β = { toNatTrans := α.vcomp β.toNatTrans, unit := ⋯, tensor := ⋯ }

@[simp]

theorem CategoryTheory.MonoidalNatTrans.vcomp_toNatTrans_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} {H : CategoryTheory.LaxMonoidalFunctor C D} (α : CategoryTheory.MonoidalNatTrans F G) (β : CategoryTheory.MonoidalNatTrans G H) (X : C) : (α.vcomp β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)

instance CategoryTheory.MonoidalNatTrans.categoryLaxMonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] : CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (CategoryTheory.LaxMonoidalFunctor C D)

Equations

• CategoryTheory.MonoidalNatTrans.categoryLaxMonoidalFunctor = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.MonoidalNatTrans.comp_toNatTrans_lax {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} {H : CategoryTheory.LaxMonoidalFunctor C D} {α : F ⟶ G} {β : G ⟶ H} : (CategoryTheory.CategoryStruct.comp α β).toNatTrans = CategoryTheory.CategoryStruct.comp α.toNatTrans β.toNatTrans

instance CategoryTheory.MonoidalNatTrans.categoryMonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] : CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (CategoryTheory.MonoidalFunctor C D)

Equations

• CategoryTheory.MonoidalNatTrans.categoryMonoidalFunctor = CategoryTheory.InducedCategory.category CategoryTheory.MonoidalFunctor.toLaxMonoidalFunctor

theorem CategoryTheory.MonoidalNatTrans.ext' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} {α : F ⟶ G} {β : F ⟶ G} (w : ∀ (X : C), α.app X = β.app X) : α = β

@[simp]

theorem CategoryTheory.MonoidalNatTrans.comp_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.MonoidalFunctor C D} {G : CategoryTheory.MonoidalFunctor C D} {H : CategoryTheory.MonoidalFunctor C D} {α : F ⟶ G} {β : G ⟶ H} : (CategoryTheory.CategoryStruct.comp α β).toNatTrans = CategoryTheory.CategoryStruct.comp α.toNatTrans β.toNatTrans

def CategoryTheory.MonoidalNatTrans.hcomp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} {H : CategoryTheory.LaxMonoidalFunctor D E} {K : CategoryTheory.LaxMonoidalFunctor D E} (α : CategoryTheory.MonoidalNatTrans F G) (β : CategoryTheory.MonoidalNatTrans H K) : CategoryTheory.MonoidalNatTrans (F ⊗⋙ H) (G ⊗⋙ K)

Horizontal composition of monoidal natural transformations.

Equations

• α.hcomp β = { toNatTrans := α.toNatTrans ◫ β.toNatTrans, unit := ⋯, tensor := ⋯ }

@[simp]

theorem CategoryTheory.MonoidalNatTrans.hcomp_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} {H : CategoryTheory.LaxMonoidalFunctor D E} {K : CategoryTheory.LaxMonoidalFunctor D E} (α : CategoryTheory.MonoidalNatTrans F G) (β : CategoryTheory.MonoidalNatTrans H K) : (α.hcomp β).toNatTrans = α.toNatTrans ◫ β.toNatTrans

def CategoryTheory.MonoidalNatTrans.prod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} {H : CategoryTheory.LaxMonoidalFunctor C E} {K : CategoryTheory.LaxMonoidalFunctor C E} (α : CategoryTheory.MonoidalNatTrans F G) (β : CategoryTheory.MonoidalNatTrans 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 := ⋯ }

@[simp]

theorem CategoryTheory.MonoidalNatTrans.prod_toNatTrans_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} {H : CategoryTheory.LaxMonoidalFunctor C E} {K : CategoryTheory.LaxMonoidalFunctor C E} (α : CategoryTheory.MonoidalNatTrans F G) (β : CategoryTheory.MonoidalNatTrans H K) (X : C) : (α.prod β).app X = (α.app X, β.app X)

def CategoryTheory.MonoidalNatIso.ofComponents {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality' : autoParam (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f)) _auto✝) (unit' : autoParam (CategoryTheory.CategoryStruct.comp F.ε (app (𝟙_ C)).hom = G.ε) _auto✝) (tensor' : autoParam (∀ (X Y : C), CategoryTheory.CategoryStruct.comp (F.μ X Y) (app (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (app X).hom (app Y).hom) (G.μ X Y)) _auto✝) : 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.

@[simp]

theorem CategoryTheory.MonoidalNatIso.ofComponents.hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (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) (app (CategoryTheory.MonoidalCategory.tensorObj 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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (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) (app (CategoryTheory.MonoidalCategory.tensorObj 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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (α : F ⟶ G) [∀ (X : C), CategoryTheory.IsIso (α.app X)] : CategoryTheory.IsIso α

Equations

• ⋯ = ⋯

def CategoryTheory.monoidalUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {G : CategoryTheory.Functor D C} (h : F.toFunctor ⊣ G) : CategoryTheory.LaxMonoidalFunctor.id C ⟶ F.toLaxMonoidalFunctor ⊗⋙ CategoryTheory.monoidalAdjoint F h

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

Equations

• CategoryTheory.monoidalUnit F h = { toNatTrans := h.unit, unit := ⋯, tensor := ⋯ }

def CategoryTheory.monoidalCounit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {G : CategoryTheory.Functor D C} (h : F.toFunctor ⊣ G) : CategoryTheory.monoidalAdjoint F h ⊗⋙ F.toLaxMonoidalFunctor ⟶ CategoryTheory.LaxMonoidalFunctor.id D

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

Equations

• CategoryTheory.monoidalCounit F h = { toNatTrans := h.counit, unit := ⋯, tensor := ⋯ }

@[simp]

theorem CategoryTheory.monoidalCounit_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {G : CategoryTheory.Functor D C} (h : F.toFunctor ⊣ G) : (CategoryTheory.monoidalCounit F h).toNatTrans = h.counit

instance CategoryTheory.instIsIsoLaxMonoidalFunctorMonoidalUnitOfIsEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {G : CategoryTheory.Functor D C} (h : F.toFunctor ⊣ G) [F.IsEquivalence] : CategoryTheory.IsIso (CategoryTheory.monoidalUnit F h)

Equations

• ⋯ = ⋯

instance CategoryTheory.instIsIsoLaxMonoidalFunctorMonoidalCounitOfIsEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {G : CategoryTheory.Functor D C} (h : F.toFunctor ⊣ G) [F.IsEquivalence] : CategoryTheory.IsIso (CategoryTheory.monoidalCounit F h)

Equations

• ⋯ = ⋯