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.
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 : category_theory.lax_monoidal_functor C D}
(x y : category_theory.monoidal_nat_trans F G) :
x = y ↔ x.to_nat_trans = y.to_nat_trans
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 : category_theory.lax_monoidal_functor C D}
(x y : category_theory.monoidal_nat_trans F G)
(h : x.to_nat_trans = y.to_nat_trans) :
x = y
@[ext]
structure
category_theory.monoidal_nat_trans
{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) :
Type (max u₁ v₂)
- to_nat_trans : category_theory.nat_trans F.to_functor G.to_functor
- unit' : F.ε ≫ c.to_nat_trans.app (𝟙_ C) = G.ε . "obviously"
- tensor' : (∀ (X Y : C), F.μ X Y ≫ c.to_nat_trans.app (X ⊗ Y) = (c.to_nat_trans.app X ⊗ c.to_nat_trans.app Y) ≫ G.μ X Y) . "obviously"
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
@[simp]
theorem
category_theory.monoidal_nat_trans.id_to_nat_trans
{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 : category_theory.lax_monoidal_functor C D) :
def
category_theory.monoidal_nat_trans.id
{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 : category_theory.lax_monoidal_functor C D) :
The identity monoidal natural transformation.
Equations
- category_theory.monoidal_nat_trans.id F = {to_nat_trans := {app := (𝟙 F.to_functor).app, naturality' := _}, unit' := _, tensor' := _}
@[instance]
def
category_theory.monoidal_nat_trans.inhabited
{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 : category_theory.lax_monoidal_functor C D) :
@[simp]
theorem
category_theory.monoidal_nat_trans.vcomp_to_nat_trans
{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 H : category_theory.lax_monoidal_functor C D}
(α : category_theory.monoidal_nat_trans F G)
(β : category_theory.monoidal_nat_trans G H) :
(α.vcomp β).to_nat_trans = α.to_nat_trans.vcomp β.to_nat_trans
def
category_theory.monoidal_nat_trans.vcomp
{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 H : category_theory.lax_monoidal_functor C D}
(α : category_theory.monoidal_nat_trans F G)
(β : category_theory.monoidal_nat_trans G H) :
Vertical composition of monoidal natural transformations.
Equations
- α.vcomp β = {to_nat_trans := {app := (α.to_nat_trans.vcomp β.to_nat_trans).app, naturality' := _}, unit' := _, tensor' := _}
@[instance]
def
category_theory.monoidal_nat_trans.category_lax_monoidal_functor
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D] :
Equations
- category_theory.monoidal_nat_trans.category_lax_monoidal_functor = {to_category_struct := {to_has_hom := {hom := category_theory.monoidal_nat_trans _inst_4}, id := category_theory.monoidal_nat_trans.id _inst_4, comp := λ (F G H : category_theory.lax_monoidal_functor C D) (α : F ⟶ G) (β : G ⟶ H), category_theory.monoidal_nat_trans.vcomp α β}, id_comp' := _, comp_id' := _, assoc' := _}
@[simp]
theorem
category_theory.monoidal_nat_trans.comp_to_nat_trans'
{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 H : category_theory.lax_monoidal_functor C D}
{α : F ⟶ G}
{β : G ⟶ H} :
(α ≫ β).to_nat_trans = α.to_nat_trans ≫ β.to_nat_trans
@[instance]
def
category_theory.monoidal_nat_trans.category_monoidal_functor
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D] :
@[simp]
theorem
category_theory.monoidal_nat_trans.comp_to_nat_trans''
{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 H : category_theory.monoidal_functor C D}
{α : F ⟶ G}
{β : G ⟶ H} :
(α ≫ β).to_nat_trans = α.to_nat_trans ≫ β.to_nat_trans
@[simp]
theorem
category_theory.monoidal_nat_trans.hcomp_to_nat_trans
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
{E : Type u₃}
[category_theory.category E]
[category_theory.monoidal_category E]
{F G : category_theory.lax_monoidal_functor C D}
{H K : category_theory.lax_monoidal_functor D E}
(α : category_theory.monoidal_nat_trans F G)
(β : category_theory.monoidal_nat_trans H K) :
(α.hcomp β).to_nat_trans = α.to_nat_trans ◫ β.to_nat_trans
def
category_theory.monoidal_nat_trans.hcomp
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
{E : Type u₃}
[category_theory.category E]
[category_theory.monoidal_category E]
{F G : category_theory.lax_monoidal_functor C D}
{H K : category_theory.lax_monoidal_functor D E}
(α : category_theory.monoidal_nat_trans F G)
(β : category_theory.monoidal_nat_trans H K) :
category_theory.monoidal_nat_trans (F ⊗⋙ H) (G ⊗⋙ K)
Horizontal composition of monoidal natural transformations.
Equations
- α.hcomp β = {to_nat_trans := {app := (α.to_nat_trans ◫ β.to_nat_trans).app, naturality' := _}, unit' := _, tensor' := _}
@[instance]
def
category_theory.monoidal_nat_iso.is_iso_of_is_iso_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}
(α : F ⟶ G)
[Π (X : C), category_theory.is_iso (α.to_nat_trans.app X)] :
Equations
- category_theory.monoidal_nat_iso.is_iso_of_is_iso_app α = {inv := {to_nat_trans := {app := λ (X : C), category_theory.is_iso.inv (α.to_nat_trans.app X), naturality' := _}, unit' := _, tensor' := _}, hom_inv_id' := _, inv_hom_id' := _}
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
- category_theory.monoidal_nat_iso.of_components app naturality unit tensor = category_theory.as_iso {to_nat_trans := {app := λ (X : C), (app X).hom, naturality' := naturality}, unit' := unit, tensor' := tensor}
@[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) :
(category_theory.monoidal_nat_iso.of_components app 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₁}
[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) :
(category_theory.monoidal_nat_iso.of_components app naturality unit tensor).inv.to_nat_trans.app X = (app X).inv