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 ⟶ c.to_functor.obj (𝟙_ C)
μ : Π (X Y : C), c.to_functor.obj X ⊗ c.to_functor.obj Y ⟶ c.to_functor.obj (X ⊗ Y)
μ_natural' : (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (c.to_functor.map f ⊗ c.to_functor.map g) ≫ c.μ Y Y' = c.μ X X' ≫ c.to_functor.map (f ⊗ g)) . "obviously"
associativity' : (∀ (X Y Z : C), (c.μ X Y ⊗ 𝟙 (c.to_functor.obj Z)) ≫ c.μ (X ⊗ Y) Z ≫ c.to_functor.map (α_ X Y Z).hom = (α_ (c.to_functor.obj X) (c.to_functor.obj Y) (c.to_functor.obj Z)).hom ≫ (𝟙 (c.to_functor.obj X) ⊗ c.μ Y Z) ≫ c.μ X (Y ⊗ Z)) . "obviously"
left_unitality' : (∀ (X : C), (λ_ (c.to_functor.obj X)).hom = (c.ε ⊗ 𝟙 (c.to_functor.obj X)) ≫ c.μ (𝟙_ C) X ≫ c.to_functor.map (λ_ X).hom) . "obviously"
right_unitality' : (∀ (X : C), (ρ_ (c.to_functor.obj X)).hom = (𝟙 (c.to_functor.obj X) ⊗ c.ε) ≫ c.μ X (𝟙_ C) ≫ c.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 the appropriate coherences.

@[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] (c : category_theory.lax_monoidal_functor C D) {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :

(c.to_functor.map f ⊗ c.to_functor.map g) ≫ c.μ Y Y' = c.μ X X' ≫ c.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] (c : category_theory.lax_monoidal_functor C D) {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {X'_1 : D} (f' : c.to_functor.obj (Y ⊗ Y') ⟶ X'_1) :

(c.to_functor.map f ⊗ c.to_functor.map g) ≫ c.μ Y Y' ≫ f' = c.μ X X' ≫ c.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] (c : category_theory.lax_monoidal_functor C D) (X : C) :

(λ_ (c.to_functor.obj X)).hom = (c.ε ⊗ 𝟙 (c.to_functor.obj X)) ≫ c.μ (𝟙_ C) X ≫ c.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] (c : category_theory.lax_monoidal_functor C D) (X : C) :

(ρ_ (c.to_functor.obj X)).hom = (𝟙 (c.to_functor.obj X) ⊗ c.ε) ≫ c.μ X (𝟙_ C) ≫ c.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] (c : category_theory.lax_monoidal_functor C D) (X Y Z : C) :

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

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 c.to_lax_monoidal_functor.ε . "apply_instance"
μ_is_iso : (Π (X Y : C), category_theory.is_iso (c.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.

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.ε

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

@[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.is_iso.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) :

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) :

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) _

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 := category_theory.is_iso.id (𝟙_ C), μ_is_iso := λ (X Y : C), category_theory.is_iso.id ({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_ε (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

@[simp]

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

(category_theory.monoidal_functor.id C).μ_is_iso X Y = category_theory.is_iso.id ({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_ε_is_iso (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.monoidal_functor.id C).ε_is_iso = category_theory.is_iso.id (𝟙_ C)

@[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.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 := id category_theory.is_iso.comp_is_iso, μ_is_iso := id (λ (X Y : C), category_theory.is_iso.comp_is_iso)}

@[simp]

theorem category_theory.monoidal_functor.comp_ε_is_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] {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).ε_is_iso = id category_theory.is_iso.comp_is_iso

@[simp]

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

(F ⊗⋙ G).μ_is_iso X Y = id (λ (X Y : C), category_theory.is_iso.comp_is_iso) X Y