Documentation

Mathlib.CategoryTheory.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' : 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.

An unbundled description of lax monoidal functors.

Instances
    @[reducible, inline]
    abbrev CategoryTheory.LaxMonoidal.ofTensorHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CD) [CategoryTheory.Functorial F] (ε : 𝟙_ D F (𝟙_ C)) (μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F X) (F Y) F (CategoryTheory.MonoidalCategory.tensorObj X Y)) (μ_natural : autoParam (∀ {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)) (μ Y Y') = CategoryTheory.CategoryStruct.comp (μ X X') (CategoryTheory.map F (CategoryTheory.MonoidalCategory.tensorHom f g))) _auto✝) (associativity : autoParam (∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (CategoryTheory.CategoryStruct.id (F Z))) (CategoryTheory.CategoryStruct.comp (μ (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)) (μ Y Z)) (μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))) _auto✝) (left_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ε (CategoryTheory.CategoryStruct.id (F X))) (CategoryTheory.CategoryStruct.comp (μ (𝟙_ C) X) (CategoryTheory.map F (CategoryTheory.MonoidalCategory.leftUnitor X).hom))) _auto✝) (right_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F X)) ε) (CategoryTheory.CategoryStruct.comp (μ X (𝟙_ C)) (CategoryTheory.map F (CategoryTheory.MonoidalCategory.rightUnitor X).hom))) _auto✝) :

    An unbundled description of lax monoidal functors.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • CategoryTheory.instLaxMonoidalObj F = { ε := F, μ := F, μ_natural_left := , μ_natural_right := , associativity := , left_unitality := , right_unitality := }
        Equations
        • One or more equations did not get rendered due to their size.