mathlib3documentation

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.

theorem category_theory.monoidal_nat_trans.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.monoidal_category C} {D : Type u₂} {_inst_3 : category_theory.category D} {_inst_4 : category_theory.monoidal_category D} {F G : D} (x y : G) :
x = y
theorem category_theory.monoidal_nat_trans.ext {C : Type u₁} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.monoidal_category C} {D : Type u₂} {_inst_3 : category_theory.category D} {_inst_4 : category_theory.monoidal_category D} {F G : D} (x y : G) (h : x.to_nat_trans = y.to_nat_trans) :
x = y
@[ext]
structure category_theory.monoidal_nat_trans {C : Type u₁} {D : Type u₂} (F G : D) :
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 category_theory.monoidal_nat_trans
@[simp]
theorem category_theory.monoidal_nat_trans.tensor {C : Type u₁} {D : Type u₂} {F G : D} (self : G) (X Y : C) :
F.μ X Y self.to_nat_trans.app (X Y) = (self.to_nat_trans.app X self.to_nat_trans.app Y) G.μ X Y
@[simp]
theorem category_theory.monoidal_nat_trans.tensor_assoc {C : Type u₁} {D : Type u₂} {F G : D} (self : G) (X Y : C) {X' : D} (f' : G.to_functor.obj (X Y) X') :
F.μ X Y self.to_nat_trans.app (X Y) f' = (self.to_nat_trans.app X self.to_nat_trans.app Y) G.μ X Y f'
@[simp]
theorem category_theory.monoidal_nat_trans.unit {C : Type u₁} {D : Type u₂} {F G : D} (self : G) :
F.ε self.to_nat_trans.app (𝟙_ C) = G.ε
@[simp]
theorem category_theory.monoidal_nat_trans.unit_assoc {C : Type u₁} {D : Type u₂} {F G : D} (self : G) {X' : D} (f' : G.to_functor.obj (𝟙_ C) X') :
F.ε self.to_nat_trans.app (𝟙_ C) f' = G.ε f'
@[simp]

The identity monoidal natural transformation.

Equations
@[protected, instance]
Equations
@[simp]
theorem category_theory.monoidal_nat_trans.vcomp_to_nat_trans {C : Type u₁} {D : Type u₂} {F G H : D}  :
def category_theory.monoidal_nat_trans.vcomp {C : Type u₁} {D : Type u₂} {F G H : D}  :

Vertical composition of monoidal natural transformations.

Equations
@[protected, instance]
Equations
@[simp]
theorem category_theory.monoidal_nat_trans.comp_to_nat_trans_lax {C : Type u₁} {D : Type u₂} {F G H : D} {α : F G} {β : G H} :
β).to_nat_trans =
@[protected, instance]
Equations
@[simp]
theorem category_theory.monoidal_nat_trans.comp_to_nat_trans {C : Type u₁} {D : Type u₂} {F G H : D} {α : F G} {β : G H} :
β).to_nat_trans =
@[simp]
theorem category_theory.monoidal_nat_trans.hcomp_to_nat_trans {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : D} {H K : E}  :
def category_theory.monoidal_nat_trans.hcomp {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : D} {H K : E}  :
(G ⊗⋙ K)

Horizontal composition of monoidal natural transformations.

Equations
def category_theory.monoidal_nat_trans.prod {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : D} {H K : E}  :
(G.prod' K)

The cartesian product of two monoidal natural transformations is monoidal.

Equations
@[simp]
theorem category_theory.monoidal_nat_trans.prod_to_nat_trans_app {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : D} {H K : E} (X : C) :
def category_theory.monoidal_nat_iso.of_components {C : Type u₁} {D : Type u₂} {F G : 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₁} {D : Type u₂} {F G : 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) :
naturality unit tensor).hom.to_nat_trans.app X = (app X).hom
@[simp]
theorem category_theory.monoidal_nat_iso.of_components.inv_app {C : Type u₁} {D : Type u₂} {F G : 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) :
naturality unit tensor).inv.to_nat_trans.app X = (app X).inv
@[protected, instance]
def category_theory.monoidal_nat_iso.is_iso_of_is_iso_app {C : Type u₁} {D : Type u₂} {F G : D} (α : F G) [ (X : C), ] :

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

Equations
Instances for category_theory.monoidal_unit
@[simp]
@[protected, instance]

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

Equations
Instances for category_theory.monoidal_counit
@[simp]
@[protected, instance]