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.

source
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₂)

An unbundled description of lax monoidal functors.

Instances
    source
    @[inline, reducible]
    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 : C → D) [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✝) :
    CategoryTheory.LaxMonoidal F

    An unbundled description of lax monoidal functors.

    Equations
    Instances For
      source
      @[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.toPrefunctor.obj a = F a
      source
      @[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.ε
      source
      @[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.of F).μ X Y = CategoryTheory.LaxMonoidal.μ X Y
      source
      @[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.toPrefunctor.map f = CategoryTheory.Functorial.map' f
      source
      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        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
        Equations
        • One or more equations did not get rendered due to their size.
        source
        instance CategoryTheory.laxMonoidalId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
        CategoryTheory.LaxMonoidal id
        Equations
        • One or more equations did not get rendered due to their size.