# mathlibdocumentation

category_theory.monoidal.functorial

# Unbundled lax monoidal functors #

## Design considerations #

The essential problem I've encountered that requires unbundled functors is having an existing (non-monoidal) functor F : C ⥤ D between monoidal categories, and wanting to assert that it has an extension to a lax monoidal functor.

The two options seem to be

1. Construct a separate F' : lax_monoidal_functor C D, and assert F'.to_functor ≅ F.
2. Introduce unbundled functors and unbundled lax monoidal functors, and construct lax_monoidal F.obj, then construct F' := lax_monoidal_functor.of F.obj.

Both have costs, but as for option 2. the cost is in library design, while in option 1. the cost is users having to carry around additional isomorphisms forever, I wanted to introduce unbundled functors.

TODO: later, we may want to do this for strong monoidal functors as well, but the immediate application, for enriched categories, only requires this notion.

@[class]
structure category_theory.lax_monoidal {C : Type u₁} {D : Type u₂} (F : C → D)  :
Type (max u₁ v₂)

An unbundled description of lax monoidal functors.

Instances
@[simp]
theorem category_theory.lax_monoidal.μ_natural {C : Type u₁} {D : Type u₂} {F : C → D} {X Y X' Y' : C} (f : X Y) (g : X' Y') :
= (f g)
theorem category_theory.lax_monoidal.left_unitality {C : Type u₁} {D : Type u₂} {F : C → D} (X : C) :
(λ_ (F X)).hom = 𝟙 (F X)) X (λ_ X).hom
theorem category_theory.lax_monoidal.right_unitality {C : Type u₁} {D : Type u₂} {F : C → D} (X : C) :
(ρ_ (F X)).hom = (𝟙 (F X) (𝟙_ C) (ρ_ X).hom
@[simp]
theorem category_theory.lax_monoidal.associativity {C : Type u₁} {D : Type u₂} {F : C → D} (X Y Z : C) :
𝟙 (F Z)) (X Y) Z (α_ X Y Z).hom = (α_ (F X) (F Y) (F Z)).hom (𝟙 (F X) (Y Z)
@[simp]
theorem category_theory.lax_monoidal_functor.of_μ {C : Type u₁} {D : Type u₂} (F : C → D) [I₁ : category_theory.functorial F] [I₂ : category_theory.lax_monoidal F] (X Y : C) :
def category_theory.lax_monoidal_functor.of {C : Type u₁} {D : Type u₂} (F : C → D) [I₁ : category_theory.functorial F] [I₂ : category_theory.lax_monoidal F] :

Construct a bundled lax_monoidal_functor from the object level function and functorial and lax_monoidal typeclasses.

Equations
@[simp]
theorem category_theory.lax_monoidal_functor.of_to_functor_map {C : Type u₁} {D : Type u₂} (F : C → D) [I₁ : category_theory.functorial F] [I₂ : category_theory.lax_monoidal F] {X Y : C} (ᾰ : X Y) :
@[simp]
theorem category_theory.lax_monoidal_functor.of_to_functor_obj {C : Type u₁} {D : Type u₂} (F : C → D) [I₁ : category_theory.functorial F] [I₂ : category_theory.lax_monoidal F] (ᾰ : C) :
@[simp]
theorem category_theory.lax_monoidal_functor.of_ε {C : Type u₁} {D : Type u₂} (F : C → D) [I₁ : category_theory.functorial F] [I₂ : category_theory.lax_monoidal F] :
@[instance]
Equations
@[instance]
Equations