mathlib documentation

category_theory.monoidal.natural_transformation

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.

@[ext]

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

def category_theory.monoidal_nat_iso.of_components {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G : category_theory.lax_monoidal_functor C D} (app : Π (X : C), F.to_functor.obj X G.to_functor.obj X) :
(∀ {X Y : C} (f : X Y), F.to_functor.map f (app Y).hom = (app X).hom G.to_functor.map f)F.ε (app (𝟙_ C)).hom = G.ε(∀ (X Y : C), F.μ X Y (app (X Y)).hom = ((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
@[simp]
theorem category_theory.monoidal_nat_iso.of_components.hom_app {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G : category_theory.lax_monoidal_functor C D} (app : Π (X : C), F.to_functor.obj X G.to_functor.obj X) (naturality : ∀ {X Y : C} (f : X Y), F.to_functor.map f (app Y).hom = (app X).hom G.to_functor.map f) (unit : F.ε (app (𝟙_ C)).hom = G.ε) (tensor : ∀ (X Y : C), F.μ X Y (app (X Y)).hom = ((app X).hom (app Y).hom) G.μ X Y) (X : C) :

@[simp]
theorem category_theory.monoidal_nat_iso.of_components.inv_app {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G : category_theory.lax_monoidal_functor C D} (app : Π (X : C), F.to_functor.obj X G.to_functor.obj X) (naturality : ∀ {X Y : C} (f : X Y), F.to_functor.map f (app Y).hom = (app X).hom G.to_functor.map f) (unit : F.ε (app (𝟙_ C)).hom = G.ε) (tensor : ∀ (X Y : C), F.μ X Y (app (X Y)).hom = ((app X).hom (app Y).hom) G.μ X Y) (X : C) :