mathlib documentation

category_theory.monoidal.functor

(Lax) monoidal functors #

A lax monoidal functor F between monoidal categories C and D is a functor between the underlying categories equipped with morphisms

ε : 𝟙_ D ⟶ F.obj (𝟙_ C) (called the unit morphism)
μ X Y : (F.obj X) ⊗ (F.obj Y) ⟶ F.obj (X ⊗ Y) (called the tensorator, or strength). satisfying various axioms.

A monoidal functor is a lax monoidal functor for which ε and μ are isomorphisms.

We show that the composition of (lax) monoidal functors gives a (lax) monoidal functor.

See also category_theory.monoidal.functorial for a typeclass decorating an object-level function with the additional data of a monoidal functor. This is useful when stating that a pre-existing functor is monoidal.

See category_theory.monoidal.natural_transformation for monoidal natural transformations.

We show in category_theory.monoidal.Mon_ that lax monoidal functors take monoid objects to monoid objects.

Future work #

Oplax monoidal functors.

References #

See https://stacks.math.columbia.edu/tag/0FFL.

structure category_theory.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] :

Type (max u₁ u₂ v₁ v₂)

to_functor : C ⥤ D
ε : 𝟙_ D ⟶ self.to_functor.obj (𝟙_ C)
μ : Π (X Y : C), self.to_functor.obj X ⊗ self.to_functor.obj Y ⟶ self.to_functor.obj (X ⊗ Y)
μ_natural' : (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (self.to_functor.map f ⊗ self.to_functor.map g) ≫ self.μ Y Y' = self.μ X X' ≫ self.to_functor.map (f ⊗ g)) . "obviously"
associativity' : (∀ (X Y Z : C), (self.μ X Y ⊗ 𝟙 (self.to_functor.obj Z)) ≫ self.μ (X ⊗ Y) Z ≫ self.to_functor.map (α_ X Y Z).hom = (α_ (self.to_functor.obj X) (self.to_functor.obj Y) (self.to_functor.obj Z)).hom ≫ (𝟙 (self.to_functor.obj X) ⊗ self.μ Y Z) ≫ self.μ X (Y ⊗ Z)) . "obviously"
left_unitality' : (∀ (X : C), (λ_ (self.to_functor.obj X)).hom = (self.ε ⊗ 𝟙 (self.to_functor.obj X)) ≫ self.μ (𝟙_ C) X ≫ self.to_functor.map (λ_ X).hom) . "obviously"
right_unitality' : (∀ (X : C), (ρ_ (self.to_functor.obj X)).hom = (𝟙 (self.to_functor.obj X) ⊗ self.ε) ≫ self.μ X (𝟙_ C) ≫ self.to_functor.map (ρ_ X).hom) . "obviously"

A lax monoidal functor is a functor F : C ⥤ D between monoidal categories, equipped with morphisms ε : 𝟙 _D ⟶ F.obj (𝟙_ C) and μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y), satisfying the appropriate coherences.

Instances for category_theory.lax_monoidal_functor

category_theory.lax_monoidal_functor.has_sizeof_inst
category_theory.lax_monoidal_functor.inhabited
category_theory.monoidal_nat_trans.category_lax_monoidal_functor

@[simp]

theorem category_theory.lax_monoidal_functor.μ_natural {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (self : category_theory.lax_monoidal_functor C D) {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :

(self.to_functor.map f ⊗ self.to_functor.map g) ≫ self.μ Y Y' = self.μ X X' ≫ self.to_functor.map (f ⊗ g)

@[simp]

theorem category_theory.lax_monoidal_functor.μ_natural_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (self : category_theory.lax_monoidal_functor C D) {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {X'_1 : D} (f' : self.to_functor.obj (Y ⊗ Y') ⟶ X'_1) :

(self.to_functor.map f ⊗ self.to_functor.map g) ≫ self.μ Y Y' ≫ f' = self.μ X X' ≫ self.to_functor.map (f ⊗ g) ≫ f'

@[simp]

theorem category_theory.lax_monoidal_functor.left_unitality {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (self : category_theory.lax_monoidal_functor C D) (X : C) :

(λ_ (self.to_functor.obj X)).hom = (self.ε ⊗ 𝟙 (self.to_functor.obj X)) ≫ self.μ (𝟙_ C) X ≫ self.to_functor.map (λ_ X).hom

@[simp]

theorem category_theory.lax_monoidal_functor.right_unitality {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (self : category_theory.lax_monoidal_functor C D) (X : C) :

(ρ_ (self.to_functor.obj X)).hom = (𝟙 (self.to_functor.obj X) ⊗ self.ε) ≫ self.μ X (𝟙_ C) ≫ self.to_functor.map (ρ_ X).hom

@[simp]

theorem category_theory.lax_monoidal_functor.associativity {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (self : category_theory.lax_monoidal_functor C D) (X Y Z : C) :

(self.μ X Y ⊗ 𝟙 (self.to_functor.obj Z)) ≫ self.μ (X ⊗ Y) Z ≫ self.to_functor.map (α_ X Y Z).hom = (α_ (self.to_functor.obj X) (self.to_functor.obj Y) (self.to_functor.obj Z)).hom ≫ (𝟙 (self.to_functor.obj X) ⊗ self.μ Y Z) ≫ self.μ X (Y ⊗ Z)

@[simp]

theorem category_theory.lax_monoidal_functor.associativity_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (self : category_theory.lax_monoidal_functor C D) (X Y Z : C) {X' : D} (f' : self.to_functor.obj (X ⊗ Y ⊗ Z) ⟶ X') :

(self.μ X Y ⊗ 𝟙 (self.to_functor.obj Z)) ≫ self.μ (X ⊗ Y) Z ≫ self.to_functor.map (α_ X Y Z).hom ≫ f' = (α_ (self.to_functor.obj X) (self.to_functor.obj Y) (self.to_functor.obj Z)).hom ≫ (𝟙 (self.to_functor.obj X) ⊗ self.μ Y Z) ≫ self.μ X (Y ⊗ Z) ≫ f'

@[simp]

theorem category_theory.lax_monoidal_functor.left_unitality_inv_assoc {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) (X : C) {X' : D} (f' : F.to_functor.obj (𝟙_ C ⊗ X) ⟶ X') :

(λ_ (F.to_functor.obj X)).inv ≫ (F.ε ⊗ 𝟙 (F.to_functor.obj X)) ≫ F.μ (𝟙_ C) X ≫ f' = F.to_functor.map (λ_ X).inv ≫ f'

@[simp]

theorem category_theory.lax_monoidal_functor.left_unitality_inv {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) (X : C) :

(λ_ (F.to_functor.obj X)).inv ≫ (F.ε ⊗ 𝟙 (F.to_functor.obj X)) ≫ F.μ (𝟙_ C) X = F.to_functor.map (λ_ X).inv

@[simp]

theorem category_theory.lax_monoidal_functor.right_unitality_inv_assoc {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) (X : C) {X' : D} (f' : F.to_functor.obj (X ⊗ 𝟙_ C) ⟶ X') :

(ρ_ (F.to_functor.obj X)).inv ≫ (𝟙 (F.to_functor.obj X) ⊗ F.ε) ≫ F.μ X (𝟙_ C) ≫ f' = F.to_functor.map (ρ_ X).inv ≫ f'

@[simp]

theorem category_theory.lax_monoidal_functor.right_unitality_inv {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) (X : C) :

(ρ_ (F.to_functor.obj X)).inv ≫ (𝟙 (F.to_functor.obj X) ⊗ F.ε) ≫ F.μ X (𝟙_ C) = F.to_functor.map (ρ_ X).inv

@[simp]

theorem category_theory.lax_monoidal_functor.associativity_inv {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) (X Y Z : C) :

(𝟙 (F.to_functor.obj X) ⊗ F.μ Y Z) ≫ F.μ X (Y ⊗ Z) ≫ F.to_functor.map (α_ X Y Z).inv = (α_ (F.to_functor.obj X) (F.to_functor.obj Y) (F.to_functor.obj Z)).inv ≫ (F.μ X Y ⊗ 𝟙 (F.to_functor.obj Z)) ≫ F.μ (X ⊗ Y) Z

@[simp]

theorem category_theory.lax_monoidal_functor.associativity_inv_assoc {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) (X Y Z : C) {X' : D} (f' : F.to_functor.obj ((X ⊗ Y) ⊗ Z) ⟶ X') :

(𝟙 (F.to_functor.obj X) ⊗ F.μ Y Z) ≫ F.μ X (Y ⊗ Z) ≫ F.to_functor.map (α_ X Y Z).inv ≫ f' = (α_ (F.to_functor.obj X) (F.to_functor.obj Y) (F.to_functor.obj Z)).inv ≫ (F.μ X Y ⊗ 𝟙 (F.to_functor.obj Z)) ≫ F.μ (X ⊗ Y) Z ≫ f'

structure category_theory.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] :

Type (max u₁ u₂ v₁ v₂)

to_lax_monoidal_functor : category_theory.lax_monoidal_functor C D
ε_is_iso : category_theory.is_iso self.to_lax_monoidal_functor.ε . "apply_instance"
μ_is_iso : (∀ (X Y : C), category_theory.is_iso (self.to_lax_monoidal_functor.μ X Y)) . "apply_instance"

A monoidal functor is a lax monoidal functor for which the tensorator and unitor as isomorphisms.

See https://stacks.math.columbia.edu/tag/0FFL.

Instances for category_theory.monoidal_functor

category_theory.monoidal_functor.has_sizeof_inst
category_theory.monoidal_functor.inhabited
category_theory.monoidal_nat_trans.category_monoidal_functor

noncomputable def category_theory.monoidal_functor.ε_iso {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.monoidal_functor C D) :

𝟙_ D ≅ F.to_lax_monoidal_functor.to_functor.obj (𝟙_ C)

The unit morphism of a (strong) monoidal functor as an isomorphism.

Equations

F.ε_iso = category_theory.as_iso F.to_lax_monoidal_functor.ε

noncomputable def category_theory.monoidal_functor.μ_iso {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.monoidal_functor C D) (X Y : C) :

F.to_lax_monoidal_functor.to_functor.obj X ⊗ F.to_lax_monoidal_functor.to_functor.obj Y ≅ F.to_lax_monoidal_functor.to_functor.obj (X ⊗ Y)

The tensorator of a (strong) monoidal functor as an isomorphism.

Equations

F.μ_iso X Y = category_theory.as_iso (F.to_lax_monoidal_functor.μ X Y)

@[simp]

theorem category_theory.lax_monoidal_functor.id_μ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

(category_theory.lax_monoidal_functor.id C).μ X Y = 𝟙 ({obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj Y)

def category_theory.lax_monoidal_functor.id (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.lax_monoidal_functor C C

The identity lax monoidal functor.

Equations

category_theory.lax_monoidal_functor.id C = {to_functor := {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}, ε := 𝟙 (𝟙_ C), μ := λ (X Y : C), 𝟙 ({obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}

@[simp]

theorem category_theory.lax_monoidal_functor.id_ε (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.lax_monoidal_functor.id C).ε = 𝟙 (𝟙_ C)

@[simp]

theorem category_theory.lax_monoidal_functor.id_to_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.lax_monoidal_functor.id C).to_functor = 𝟭 C

@[protected, instance]

def category_theory.lax_monoidal_functor.inhabited (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

inhabited (category_theory.lax_monoidal_functor C C)

Equations

category_theory.lax_monoidal_functor.inhabited C = {default := category_theory.lax_monoidal_functor.id C _inst_2}

theorem category_theory.monoidal_functor.map_tensor {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.monoidal_functor C D) {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :

F.to_lax_monoidal_functor.to_functor.map (f ⊗ g) = category_theory.inv (F.to_lax_monoidal_functor.μ X X') ≫ (F.to_lax_monoidal_functor.to_functor.map f ⊗ F.to_lax_monoidal_functor.to_functor.map g) ≫ F.to_lax_monoidal_functor.μ Y Y'

theorem category_theory.monoidal_functor.map_left_unitor {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.monoidal_functor C D) (X : C) :

F.to_lax_monoidal_functor.to_functor.map (λ_ X).hom = category_theory.inv (F.to_lax_monoidal_functor.μ (𝟙_ C) X) ≫ (category_theory.inv F.to_lax_monoidal_functor.ε ⊗ 𝟙 (F.to_lax_monoidal_functor.to_functor.obj X)) ≫ (λ_ (F.to_lax_monoidal_functor.to_functor.obj X)).hom

theorem category_theory.monoidal_functor.map_right_unitor {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.monoidal_functor C D) (X : C) :

F.to_lax_monoidal_functor.to_functor.map (ρ_ X).hom = category_theory.inv (F.to_lax_monoidal_functor.μ X (𝟙_ C)) ≫ (𝟙 (F.to_lax_monoidal_functor.to_functor.obj X) ⊗ category_theory.inv F.to_lax_monoidal_functor.ε) ≫ (ρ_ (F.to_lax_monoidal_functor.to_functor.obj X)).hom

noncomputable def category_theory.monoidal_functor.μ_nat_iso {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.monoidal_functor C D) :

F.to_lax_monoidal_functor.to_functor.prod F.to_lax_monoidal_functor.to_functor ⋙ category_theory.monoidal_category.tensor D ≅ category_theory.monoidal_category.tensor C ⋙ F.to_lax_monoidal_functor.to_functor

The tensorator as a natural isomorphism.

Equations

F.μ_nat_iso = category_theory.nat_iso.of_components (λ (X : C × C), F.μ_iso X.fst X.snd) _

@[simp]

theorem category_theory.monoidal_functor.μ_iso_hom {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.monoidal_functor C D) (X Y : C) :

(F.μ_iso X Y).hom = F.to_lax_monoidal_functor.μ X Y

@[simp]

theorem category_theory.monoidal_functor.μ_inv_hom_id_assoc {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.monoidal_functor C D) (X Y : C) {X' : D} (f' : F.to_lax_monoidal_functor.to_functor.obj (X ⊗ Y) ⟶ X') :

(F.μ_iso X Y).inv ≫ F.to_lax_monoidal_functor.μ X Y ≫ f' = f'

@[simp]

theorem category_theory.monoidal_functor.μ_inv_hom_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.monoidal_functor C D) (X Y : C) :

(F.μ_iso X Y).inv ≫ F.to_lax_monoidal_functor.μ X Y = 𝟙 (F.to_lax_monoidal_functor.to_functor.obj (X ⊗ Y))

@[simp]

theorem category_theory.monoidal_functor.μ_hom_inv_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.monoidal_functor C D) (X Y : C) :

F.to_lax_monoidal_functor.μ X Y ≫ (F.μ_iso X Y).inv = 𝟙 (F.to_lax_monoidal_functor.to_functor.obj X ⊗ F.to_lax_monoidal_functor.to_functor.obj Y)

@[simp]

theorem category_theory.monoidal_functor.ε_iso_hom {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.monoidal_functor C D) :

F.ε_iso.hom = F.to_lax_monoidal_functor.ε

@[simp]

theorem category_theory.monoidal_functor.ε_inv_hom_id_assoc {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.monoidal_functor C D) {X' : D} (f' : F.to_lax_monoidal_functor.to_functor.obj (𝟙_ C) ⟶ X') :

F.ε_iso.inv ≫ F.to_lax_monoidal_functor.ε ≫ f' = f'

@[simp]

theorem category_theory.monoidal_functor.ε_inv_hom_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.monoidal_functor C D) :

F.ε_iso.inv ≫ F.to_lax_monoidal_functor.ε = 𝟙 (F.to_lax_monoidal_functor.to_functor.obj (𝟙_ C))

@[simp]

theorem category_theory.monoidal_functor.ε_hom_inv_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.monoidal_functor C D) :

F.to_lax_monoidal_functor.ε ≫ F.ε_iso.inv = 𝟙 (𝟙_ D)

@[simp]

theorem category_theory.monoidal_functor.comm_tensor_left_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 : category_theory.monoidal_functor C D) (X X_1 : C) :

(F.comm_tensor_left X).hom.app X_1 = F.to_lax_monoidal_functor.μ X X_1

noncomputable def category_theory.monoidal_functor.comm_tensor_left {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.monoidal_functor C D) (X : C) :

F.to_lax_monoidal_functor.to_functor ⋙ category_theory.monoidal_category.tensor_left (F.to_lax_monoidal_functor.to_functor.obj X) ≅ category_theory.monoidal_category.tensor_left X ⋙ F.to_lax_monoidal_functor.to_functor

Monoidal functors commute with left tensoring up to isomorphism

Equations

F.comm_tensor_left X = category_theory.nat_iso.of_components (λ (Y : C), F.μ_iso X Y) _

@[simp]

theorem category_theory.monoidal_functor.comm_tensor_left_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 : category_theory.monoidal_functor C D) (X X_1 : C) :

(F.comm_tensor_left X).inv.app X_1 = (F.μ_iso X X_1).inv

@[simp]

theorem category_theory.monoidal_functor.comm_tensor_right_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 : category_theory.monoidal_functor C D) (X X_1 : C) :

(F.comm_tensor_right X).hom.app X_1 = F.to_lax_monoidal_functor.μ X_1 X

noncomputable def category_theory.monoidal_functor.comm_tensor_right {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.monoidal_functor C D) (X : C) :

F.to_lax_monoidal_functor.to_functor ⋙ category_theory.monoidal_category.tensor_right (F.to_lax_monoidal_functor.to_functor.obj X) ≅ category_theory.monoidal_category.tensor_right X ⋙ F.to_lax_monoidal_functor.to_functor

Monoidal functors commute with right tensoring up to isomorphism

Equations

F.comm_tensor_right X = category_theory.nat_iso.of_components (λ (Y : C), F.μ_iso Y X) _

@[simp]

theorem category_theory.monoidal_functor.comm_tensor_right_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 : category_theory.monoidal_functor C D) (X X_1 : C) :

(F.comm_tensor_right X).inv.app X_1 = (F.μ_iso X_1 X).inv

def category_theory.monoidal_functor.id (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.monoidal_functor C C

The identity monoidal functor.

Equations

category_theory.monoidal_functor.id C = {to_lax_monoidal_functor := {to_functor := {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}, ε := 𝟙 (𝟙_ C), μ := λ (X Y : C), 𝟙 ({obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}

@[simp]

theorem category_theory.monoidal_functor.id_to_lax_monoidal_functor_ε (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.monoidal_functor.id C).to_lax_monoidal_functor.ε = 𝟙 (𝟙_ C)

@[simp]

theorem category_theory.monoidal_functor.id_to_lax_monoidal_functor_μ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

(category_theory.monoidal_functor.id C).to_lax_monoidal_functor.μ X Y = 𝟙 ({obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj Y)

@[simp]

theorem category_theory.monoidal_functor.id_to_lax_monoidal_functor_to_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.monoidal_functor.id C).to_lax_monoidal_functor.to_functor = 𝟭 C

@[protected, instance]

def category_theory.monoidal_functor.inhabited (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

inhabited (category_theory.monoidal_functor C C)

Equations

category_theory.monoidal_functor.inhabited C = {default := category_theory.monoidal_functor.id C _inst_2}

@[simp]

theorem category_theory.lax_monoidal_functor.comp_ε {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 : category_theory.lax_monoidal_functor C D) (G : category_theory.lax_monoidal_functor D E) :

(F ⊗⋙ G).ε = G.ε ≫ G.to_functor.map F.ε

@[simp]

theorem category_theory.lax_monoidal_functor.comp_to_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] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] (F : category_theory.lax_monoidal_functor C D) (G : category_theory.lax_monoidal_functor D E) :

(F ⊗⋙ G).to_functor = F.to_functor ⋙ G.to_functor

def category_theory.lax_monoidal_functor.comp {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 : category_theory.lax_monoidal_functor C D) (G : category_theory.lax_monoidal_functor D E) :

category_theory.lax_monoidal_functor C E

The composition of two lax monoidal functors is again lax monoidal.

Equations

F ⊗⋙ G = {to_functor := {obj := (F.to_functor ⋙ G.to_functor).obj, map := (F.to_functor ⋙ G.to_functor).map, map_id' := _, map_comp' := _}, ε := G.ε ≫ G.to_functor.map F.ε, μ := λ (X Y : C), G.μ (F.to_functor.obj X) (F.to_functor.obj Y) ≫ G.to_functor.map (F.μ X Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}

@[simp]

theorem category_theory.lax_monoidal_functor.comp_μ {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 : category_theory.lax_monoidal_functor C D) (G : category_theory.lax_monoidal_functor D E) (X Y : C) :

(F ⊗⋙ G).μ X Y = G.μ (F.to_functor.obj X) (F.to_functor.obj Y) ≫ G.to_functor.map (F.μ X Y)

@[simp]

theorem category_theory.lax_monoidal_functor.prod_ε {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] {B : Type u₀} [category_theory.category B] [category_theory.monoidal_category B] (F : category_theory.lax_monoidal_functor B C) (G : category_theory.lax_monoidal_functor D E) :

(F.prod G).ε = (F.ε, G.ε)

@[simp]

theorem category_theory.lax_monoidal_functor.prod_μ {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] {B : Type u₀} [category_theory.category B] [category_theory.monoidal_category B] (F : category_theory.lax_monoidal_functor B C) (G : category_theory.lax_monoidal_functor D E) (X Y : B × D) :

(F.prod G).μ X Y = (F.μ X.fst Y.fst, G.μ X.snd Y.snd)

def category_theory.lax_monoidal_functor.prod {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] {B : Type u₀} [category_theory.category B] [category_theory.monoidal_category B] (F : category_theory.lax_monoidal_functor B C) (G : category_theory.lax_monoidal_functor D E) :

category_theory.lax_monoidal_functor (B × D) (C × E)

The cartesian product of two lax monoidal functors is lax monoidal.

Equations

F.prod G = {to_functor := {obj := (F.to_functor.prod G.to_functor).obj, map := (F.to_functor.prod G.to_functor).map, map_id' := _, map_comp' := _}, ε := (F.ε, G.ε), μ := λ (X Y : B × D), (F.μ X.fst Y.fst, G.μ X.snd Y.snd), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}

@[simp]

theorem category_theory.lax_monoidal_functor.prod_to_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] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] {B : Type u₀} [category_theory.category B] [category_theory.monoidal_category B] (F : category_theory.lax_monoidal_functor B C) (G : category_theory.lax_monoidal_functor D E) :

(F.prod G).to_functor = F.to_functor.prod G.to_functor

def category_theory.monoidal_functor.diag (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.monoidal_functor C (C × C)

The diagonal functor as a monoidal functor.

Equations

category_theory.monoidal_functor.diag C = {to_lax_monoidal_functor := {to_functor := {obj := (category_theory.functor.diag C).obj, map := (category_theory.functor.diag C).map, map_id' := _, map_comp' := _}, ε := 𝟙 (𝟙_ (C × C)), μ := λ (X Y : C), 𝟙 ({obj := (category_theory.functor.diag C).obj, map := (category_theory.functor.diag C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (category_theory.functor.diag C).obj, map := (category_theory.functor.diag C).map, map_id' := _, map_comp' := _}.obj Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}

@[simp]

theorem category_theory.monoidal_functor.diag_to_lax_monoidal_functor_μ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

(category_theory.monoidal_functor.diag C).to_lax_monoidal_functor.μ X Y = 𝟙 ({obj := (category_theory.functor.diag C).obj, map := (category_theory.functor.diag C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (category_theory.functor.diag C).obj, map := (category_theory.functor.diag C).map, map_id' := _, map_comp' := _}.obj Y)

@[simp]

theorem category_theory.monoidal_functor.diag_to_lax_monoidal_functor_ε (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.monoidal_functor.diag C).to_lax_monoidal_functor.ε = 𝟙 (𝟙_ (C × C))

@[simp]

theorem category_theory.monoidal_functor.diag_to_lax_monoidal_functor_to_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.monoidal_functor.diag C).to_lax_monoidal_functor.to_functor = category_theory.functor.diag C

def category_theory.lax_monoidal_functor.prod' {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 : category_theory.lax_monoidal_functor C D) (G : category_theory.lax_monoidal_functor C E) :

category_theory.lax_monoidal_functor C (D × E)

The cartesian product of two lax monoidal functors starting from the same monoidal category C is lax monoidal.

Equations

F.prod' G = (category_theory.monoidal_functor.diag C).to_lax_monoidal_functor ⊗⋙ F.prod G

@[simp]

theorem category_theory.lax_monoidal_functor.prod'_to_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] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] (F : category_theory.lax_monoidal_functor C D) (G : category_theory.lax_monoidal_functor C E) :

(F.prod' G).to_functor = F.to_functor.prod' G.to_functor

@[simp]

theorem category_theory.lax_monoidal_functor.prod'_ε {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 : category_theory.lax_monoidal_functor C D) (G : category_theory.lax_monoidal_functor C E) :

(F.prod' G).ε = (F.ε, G.ε)

@[simp]

theorem category_theory.lax_monoidal_functor.prod'_μ {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 : category_theory.lax_monoidal_functor C D) (G : category_theory.lax_monoidal_functor C E) (X Y : C) :

(F.prod' G).μ X Y = (F.μ X Y, G.μ X Y)

@[simp]

theorem category_theory.monoidal_functor.comp_to_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] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] (F : category_theory.monoidal_functor C D) (G : category_theory.monoidal_functor D E) :

(F ⊗⋙ G).to_lax_monoidal_functor = F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor

def category_theory.monoidal_functor.comp {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 : category_theory.monoidal_functor C D) (G : category_theory.monoidal_functor D E) :

category_theory.monoidal_functor C E

The composition of two monoidal functors is again monoidal.

Equations

F ⊗⋙ G = {to_lax_monoidal_functor := {to_functor := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).to_functor, ε := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).ε, μ := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).μ, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}

def category_theory.monoidal_functor.prod {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] {B : Type u₀} [category_theory.category B] [category_theory.monoidal_category B] (F : category_theory.monoidal_functor B C) (G : category_theory.monoidal_functor D E) :

category_theory.monoidal_functor (B × D) (C × E)

The cartesian product of two monoidal functors is monoidal.

Equations

F.prod G = {to_lax_monoidal_functor := {to_functor := (F.to_lax_monoidal_functor.prod G.to_lax_monoidal_functor).to_functor, ε := (F.to_lax_monoidal_functor.prod G.to_lax_monoidal_functor).ε, μ := (F.to_lax_monoidal_functor.prod G.to_lax_monoidal_functor).μ, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}

@[simp]

theorem category_theory.monoidal_functor.prod_to_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] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] {B : Type u₀} [category_theory.category B] [category_theory.monoidal_category B] (F : category_theory.monoidal_functor B C) (G : category_theory.monoidal_functor D E) :

(F.prod G).to_lax_monoidal_functor = F.to_lax_monoidal_functor.prod G.to_lax_monoidal_functor

def category_theory.monoidal_functor.prod' {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 : category_theory.monoidal_functor C D) (G : category_theory.monoidal_functor C E) :

category_theory.monoidal_functor C (D × E)

The cartesian product of two monoidal functors starting from the same monoidal category C is monoidal.

Equations

F.prod' G = category_theory.monoidal_functor.diag C ⊗⋙ F.prod G

@[simp]

theorem category_theory.monoidal_functor.prod'_to_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] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] (F : category_theory.monoidal_functor C D) (G : category_theory.monoidal_functor C E) :

(F.prod' G).to_lax_monoidal_functor = F.to_lax_monoidal_functor.prod' G.to_lax_monoidal_functor

@[simp]

theorem category_theory.monoidal_adjoint_to_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] (F : category_theory.monoidal_functor C D) {G : D ⥤ C} (h : F.to_lax_monoidal_functor.to_functor ⊣ G) :

(category_theory.monoidal_adjoint F h).to_functor = G

@[simp]

theorem category_theory.monoidal_adjoint_μ {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.monoidal_functor C D) {G : D ⥤ C} (h : F.to_lax_monoidal_functor.to_functor ⊣ G) (X Y : D) :

(category_theory.monoidal_adjoint F h).μ X Y = ⇑(h.hom_equiv (G.obj X ⊗ G.obj Y) (X ⊗ Y)) (category_theory.inv (F.to_lax_monoidal_functor.μ (G.obj X) (G.obj Y)) ≫ (h.counit.app X ⊗ h.counit.app Y))

@[simp]

theorem category_theory.monoidal_adjoint_ε {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.monoidal_functor C D) {G : D ⥤ C} (h : F.to_lax_monoidal_functor.to_functor ⊣ G) :

(category_theory.monoidal_adjoint F h).ε = ⇑(h.hom_equiv (𝟙_ C) (𝟙_ D)) (category_theory.inv F.to_lax_monoidal_functor.ε)

noncomputable def category_theory.monoidal_adjoint {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.monoidal_functor C D) {G : D ⥤ C} (h : F.to_lax_monoidal_functor.to_functor ⊣ G) :

category_theory.lax_monoidal_functor D C

If we have a right adjoint functor G to a monoidal functor F, then G has a lax monoidal structure as well.

Equations

category_theory.monoidal_adjoint F h = {to_functor := G, ε := ⇑(h.hom_equiv (𝟙_ C) (𝟙_ D)) (category_theory.inv F.to_lax_monoidal_functor.ε), μ := λ (X Y : D), ⇑(h.hom_equiv (G.obj X ⊗ G.obj Y) (X ⊗ Y)) (category_theory.inv (F.to_lax_monoidal_functor.μ (G.obj X) (G.obj Y)) ≫ (h.counit.app X ⊗ h.counit.app Y)), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}

noncomputable def category_theory.monoidal_inverse {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.monoidal_functor C D) [category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor] :

category_theory.monoidal_functor D C

If a monoidal functor F is an equivalence of categories then its inverse is also monoidal.

Equations

category_theory.monoidal_inverse F = {to_lax_monoidal_functor := category_theory.monoidal_adjoint F F.to_lax_monoidal_functor.to_functor.as_equivalence.to_adjunction, ε_is_iso := _, μ_is_iso := _}

@[simp]

theorem category_theory.monoidal_inverse_to_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] (F : category_theory.monoidal_functor C D) [category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor] :

(category_theory.monoidal_inverse F).to_lax_monoidal_functor = category_theory.monoidal_adjoint F F.to_lax_monoidal_functor.to_functor.as_equivalence.to_adjunction