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' : LaxMonoidalFunctor C D, and assert F'.toFunctor ≅ F.
2. Introduce unbundled functors and unbundled lax monoidal functors, and construct LaxMonoidal F.obj, then construct F' := LaxMonoidalFunctor.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 CategoryTheory.LaxMonoidal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : C → D) [CategoryTheory.Functorial F] : Type (max u₁ v₂)

• ε : CategoryTheory.MonoidalCategory.tensorUnit D ⟶ F (CategoryTheory.MonoidalCategory.tensorUnit C)

  unit morphism

• μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F X) (F Y) ⟶ F (CategoryTheory.MonoidalCategory.tensorObj X Y)

  tensorator

• μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.map F f) (CategoryTheory.map F g)) (CategoryTheory.LaxMonoidal.μ Y Y') = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidal.μ X X') (CategoryTheory.map F (CategoryTheory.MonoidalCategory.tensorHom f g))

  naturality

• associativity : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.LaxMonoidal.μ X Y) (CategoryTheory.CategoryStruct.id (F Z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidal.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.map F (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F X) (F Y) (F Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F X)) (CategoryTheory.LaxMonoidal.μ Y Z)) (CategoryTheory.LaxMonoidal.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))

  associativity of the tensorator

• left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom CategoryTheory.LaxMonoidal.ε (CategoryTheory.CategoryStruct.id (F X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidal.μ (CategoryTheory.MonoidalCategory.tensorUnit C) X) (CategoryTheory.map F (CategoryTheory.MonoidalCategory.leftUnitor X).hom))

  left unitality

• right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F X)) CategoryTheory.LaxMonoidal.ε) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidal.μ X (CategoryTheory.MonoidalCategory.tensorUnit C)) (CategoryTheory.map F (CategoryTheory.MonoidalCategory.rightUnitor X).hom))

  right unitality

An unbundled description of lax monoidal functors.

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.of_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : C → D) [I₁ : CategoryTheory.Functorial F] [I₂ : CategoryTheory.LaxMonoidal F] : (CategoryTheory.LaxMonoidalFunctor.of F).ε = CategoryTheory.LaxMonoidal.ε

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.of_toFunctor_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : C → D) [I₁ : CategoryTheory.Functorial F] [I₂ : CategoryTheory.LaxMonoidal F] : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.LaxMonoidalFunctor.of F).toFunctor.map f = CategoryTheory.Functorial.map' f

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.of_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : C → D) [I₁ : CategoryTheory.Functorial F] [I₂ : CategoryTheory.LaxMonoidal F] (X : C) (Y : C) : CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.LaxMonoidalFunctor.of F) X Y = CategoryTheory.LaxMonoidal.μ X Y

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.of_toFunctor_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : C → D) [I₁ : CategoryTheory.Functorial F] [I₂ : CategoryTheory.LaxMonoidal F] : ∀ (a : C), (CategoryTheory.LaxMonoidalFunctor.of F).toFunctor.obj a = F a

def CategoryTheory.LaxMonoidalFunctor.of {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : C → D) [I₁ : CategoryTheory.Functorial F] [I₂ : CategoryTheory.LaxMonoidal F] : CategoryTheory.LaxMonoidalFunctor C D

Construct a bundled LaxMonoidalFunctor from the object level function and Functorial and LaxMonoidal typeclasses.

instance CategoryTheory.instLaxMonoidalObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorToFunctorInstFunctorialObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) : CategoryTheory.LaxMonoidal F.obj

instance CategoryTheory.laxMonoidalId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.LaxMonoidal id