# 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_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} (a : 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] (a : 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]
def category_theory.category_theory.lax_monoidal {C : Type u₁} {D : Type u₂}  :

Equations
@[instance]

Equations