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.

class CategoryTheory.NatTrans.IsMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F₁ F₂ : Functor C D} (τ : F₁ ⟶ F₂) [F₁.LaxMonoidal] [F₂.LaxMonoidal] : Prop

A natural transformation between (lax) monoidal functors is monoidal if it satisfies ε F ≫ τ.app (𝟙_ C) = ε G and μ F X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ μ G X Y.

• unit : CategoryStruct.comp (Functor.LaxMonoidal.ε F₁) (τ.app (𝟙_ C)) = Functor.LaxMonoidal.ε F₂
• tensor (X Y : C) : CategoryStruct.comp (Functor.LaxMonoidal.μ F₁ X Y) (τ.app (MonoidalCategoryStruct.tensorObj X Y)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (τ.app X) (τ.app Y)) (Functor.LaxMonoidal.μ F₂ X Y)

@[simp]

theorem CategoryTheory.NatTrans.IsMonoidal.tensor_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} {F₁ F₂ : Functor C D} {τ : F₁ ⟶ F₂} {inst✝⁴ : F₁.LaxMonoidal} {inst✝⁵ : F₂.LaxMonoidal} [self : IsMonoidal τ] (X Y : C) {Z : D} (h : F₂.obj (MonoidalCategoryStruct.tensorObj X Y) ⟶ Z) : CategoryStruct.comp (Functor.LaxMonoidal.μ F₁ X Y) (CategoryStruct.comp (τ.app (MonoidalCategoryStruct.tensorObj X Y)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (τ.app X) (τ.app Y)) (CategoryStruct.comp (Functor.LaxMonoidal.μ F₂ X Y) h)

@[simp]

theorem CategoryTheory.NatTrans.IsMonoidal.unit_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} {F₁ F₂ : Functor C D} {τ : F₁ ⟶ F₂} {inst✝⁴ : F₁.LaxMonoidal} {inst✝⁵ : F₂.LaxMonoidal} [self : IsMonoidal τ] {Z : D} (h : F₂.obj (𝟙_ C) ⟶ Z) : CategoryStruct.comp (Functor.LaxMonoidal.ε F₁) (CategoryStruct.comp (τ.app (𝟙_ C)) h) = CategoryStruct.comp (Functor.LaxMonoidal.ε F₂) h

instance CategoryTheory.NatTrans.IsMonoidal.id {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F₁ : Functor C D} [F₁.LaxMonoidal] : IsMonoidal (CategoryStruct.id F₁)

instance CategoryTheory.NatTrans.IsMonoidal.comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F₁ F₂ F₃ : Functor C D} (τ : F₁ ⟶ F₂) [F₁.LaxMonoidal] [F₂.LaxMonoidal] [F₃.LaxMonoidal] (τ' : F₂ ⟶ F₃) [IsMonoidal τ] [IsMonoidal τ'] : IsMonoidal (CategoryStruct.comp τ τ')

instance CategoryTheory.NatTrans.IsMonoidal.hcomp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F₁ F₂ : Functor C D} (τ : F₁ ⟶ F₂) [F₁.LaxMonoidal] [F₂.LaxMonoidal] {G₁ G₂ : Functor D E} [G₁.LaxMonoidal] [G₂.LaxMonoidal] (τ' : G₁ ⟶ G₂) [IsMonoidal τ] [IsMonoidal τ'] : IsMonoidal (τ ◫ τ')

instance CategoryTheory.NatTrans.IsMonoidal.instHomFunctorLeftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] : IsMonoidal F.leftUnitor.hom

instance CategoryTheory.NatTrans.IsMonoidal.instHomFunctorRightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] : IsMonoidal F.rightUnitor.hom

instance CategoryTheory.NatTrans.IsMonoidal.instHomFunctorAssociator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {E' : Type u₄} [Category.{v₄, u₄} E'] [MonoidalCategory E'] (F : Functor C D) (G : Functor D E) (H : Functor E E') [F.LaxMonoidal] [G.LaxMonoidal] [H.LaxMonoidal] : IsMonoidal (F.associator G H).hom

instance CategoryTheory.NatTrans.instIsMonoidalProdProd' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F G : Functor C D} {H K : Functor C E} (α : F ⟶ G) (β : H ⟶ K) [F.LaxMonoidal] [G.LaxMonoidal] [IsMonoidal α] [H.LaxMonoidal] [K.LaxMonoidal] [IsMonoidal β] : IsMonoidal (prod' α β)

instance CategoryTheory.Iso.instIsMonoidalInvFunctor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F₁ F₂ : Functor C D} [F₁.LaxMonoidal] [F₂.LaxMonoidal] (e : F₁ ≅ F₂) [NatTrans.IsMonoidal e.hom] : NatTrans.IsMonoidal e.inv

instance CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [adj.IsMonoidal] : NatTrans.IsMonoidal adj.unit

instance CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalCounit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [adj.IsMonoidal] : NatTrans.IsMonoidal adj.counit

instance CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : NatTrans.IsMonoidal e.unit

instance CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : NatTrans.IsMonoidal e.counit

structure CategoryTheory.LaxMonoidalFunctor.Hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F G : LaxMonoidalFunctor C D) : Type (max u₁ v₂)

The type of monoidal natural transformations between (bundled) lax monoidal functors.

• hom : F.toFunctor ⟶ G.toFunctor

  the natural transformation between the underlying functors

• isMonoidal : NatTrans.IsMonoidal self.hom

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

Equations

• CategoryTheory.LaxMonoidalFunctor.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.id_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : LaxMonoidalFunctor C D) : (CategoryStruct.id F).hom = CategoryStruct.id F.toFunctor

@[simp]

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

theorem CategoryTheory.LaxMonoidalFunctor.comp_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G H : LaxMonoidalFunctor C D} (α : F ⟶ G) (β : G ⟶ H) {Z : Functor C D} (h : H.toFunctor ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp α β).hom h = CategoryStruct.comp α.hom (CategoryStruct.comp β.hom h)

theorem CategoryTheory.LaxMonoidalFunctor.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G : LaxMonoidalFunctor C D} {α β : F ⟶ G} (h : α.hom = β.hom) : α = β

def CategoryTheory.LaxMonoidalFunctor.homMk {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G : LaxMonoidalFunctor C D} (f : F.toFunctor ⟶ G.toFunctor) [NatTrans.IsMonoidal f] : F ⟶ G

Constructor for morphisms in the category LaxMonoidalFunctor C D.

Equations

• CategoryTheory.LaxMonoidalFunctor.homMk f = { hom := f, isMonoidal := ⋯ }

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.homMk_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G : LaxMonoidalFunctor C D} (f : F.toFunctor ⟶ G.toFunctor) [NatTrans.IsMonoidal f] : (homMk f).hom = f

def CategoryTheory.LaxMonoidalFunctor.isoMk {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G : LaxMonoidalFunctor C D} (e : F.toFunctor ≅ G.toFunctor) [NatTrans.IsMonoidal e.hom] : F ≅ G

Constructor for isomorphisms in the category LaxMonoidalFunctor C D.

Equations

• CategoryTheory.LaxMonoidalFunctor.isoMk e = { hom := CategoryTheory.LaxMonoidalFunctor.homMk e.hom, inv := CategoryTheory.LaxMonoidalFunctor.homMk e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.isoMk_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G : LaxMonoidalFunctor C D} (e : F.toFunctor ≅ G.toFunctor) [NatTrans.IsMonoidal e.hom] : (isoMk e).hom = homMk e.hom

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.isoMk_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G : LaxMonoidalFunctor C D} (e : F.toFunctor ≅ G.toFunctor) [NatTrans.IsMonoidal e.hom] : (isoMk e).inv = homMk e.inv

def CategoryTheory.LaxMonoidalFunctor.isoOfComponents {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G : LaxMonoidalFunctor C D} (e : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryStruct.comp (F.map f) (e Y).hom = CategoryStruct.comp (e X).hom (G.map f) := by aesop_cat) (unit : CategoryStruct.comp (Functor.LaxMonoidal.ε F.toFunctor) (e (𝟙_ C)).hom = Functor.LaxMonoidal.ε G.toFunctor := by aesop_cat) (tensor : ∀ (X Y : C), CategoryStruct.comp (Functor.LaxMonoidal.μ F.toFunctor X Y) (e (MonoidalCategoryStruct.tensorObj X Y)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom) (Functor.LaxMonoidal.μ G.toFunctor X Y) := by aesop_cat) : F ≅ G

Constructor for isomorphisms between lax monoidal functors.

Equations

• CategoryTheory.LaxMonoidalFunctor.isoOfComponents e naturality unit tensor = CategoryTheory.LaxMonoidalFunctor.isoMk (CategoryTheory.NatIso.ofComponents e ⋯)

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.isoOfComponents_inv_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G : LaxMonoidalFunctor C D} (e : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryStruct.comp (F.map f) (e Y).hom = CategoryStruct.comp (e X).hom (G.map f) := by aesop_cat) (unit : CategoryStruct.comp (Functor.LaxMonoidal.ε F.toFunctor) (e (𝟙_ C)).hom = Functor.LaxMonoidal.ε G.toFunctor := by aesop_cat) (tensor : ∀ (X Y : C), CategoryStruct.comp (Functor.LaxMonoidal.μ F.toFunctor X Y) (e (MonoidalCategoryStruct.tensorObj X Y)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom) (Functor.LaxMonoidal.μ G.toFunctor X Y) := by aesop_cat) (X : C) : (isoOfComponents e naturality unit tensor).inv.hom.app X = (e X).inv

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.isoOfComponents_hom_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G : LaxMonoidalFunctor C D} (e : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryStruct.comp (F.map f) (e Y).hom = CategoryStruct.comp (e X).hom (G.map f) := by aesop_cat) (unit : CategoryStruct.comp (Functor.LaxMonoidal.ε F.toFunctor) (e (𝟙_ C)).hom = Functor.LaxMonoidal.ε G.toFunctor := by aesop_cat) (tensor : ∀ (X Y : C), CategoryStruct.comp (Functor.LaxMonoidal.μ F.toFunctor X Y) (e (MonoidalCategoryStruct.tensorObj X Y)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom) (Functor.LaxMonoidal.μ G.toFunctor X Y) := by aesop_cat) (X : C) : (isoOfComponents e naturality unit tensor).hom.hom.app X = (e X).hom