mathlib3 documentation

category_theory.monoidal.natural_transformation

Monoidal natural transformations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Instances for category_theory.monoidal_nat_trans
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) (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) :
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) :