HepLean 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
    @[simp]
    theorem CategoryTheory.LaxMonoidal.μ_natural_left {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D} {F : C → D} {inst_4 : CategoryTheory.Functorial F} [self : CategoryTheory.LaxMonoidal F] {X Y : C} (f : X ⟶ Y) (X' : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.map F f) (F X')) (CategoryTheory.LaxMonoidal.μ Y X') = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidal.μ X X') (CategoryTheory.map F (CategoryTheory.MonoidalCategory.whiskerRight f X'))
    source
    @[simp]
    theorem CategoryTheory.LaxMonoidal.μ_natural_right {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D} {F : C → D} {inst_4 : CategoryTheory.Functorial F} [self : CategoryTheory.LaxMonoidal F] {X Y : C} (X' : C) (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F X') (CategoryTheory.map F f)) (CategoryTheory.LaxMonoidal.μ X' Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidal.μ X' X) (CategoryTheory.map F (CategoryTheory.MonoidalCategory.whiskerLeft X' f))
    source
    @[simp]
    theorem CategoryTheory.LaxMonoidal.associativity {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D} {F : C → D} {inst_4 : CategoryTheory.Functorial F} [self : CategoryTheory.LaxMonoidal F] (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.LaxMonoidal.μ X Y) (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.whiskerLeft (F X) (CategoryTheory.LaxMonoidal.μ Y Z)) (CategoryTheory.LaxMonoidal.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))

    associativity of the tensorator

    source
    theorem CategoryTheory.LaxMonoidal.left_unitality {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D} {F : C → D} {inst_4 : CategoryTheory.Functorial F} [self : CategoryTheory.LaxMonoidal F] (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight CategoryTheory.LaxMonoidal.ε (F X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidal.μ (𝟙_ C) X) (CategoryTheory.map F (CategoryTheory.MonoidalCategory.leftUnitor X).hom))

    left unitality

    source
    theorem CategoryTheory.LaxMonoidal.right_unitality {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D} {F : C → D} {inst_4 : CategoryTheory.Functorial F} [self : CategoryTheory.LaxMonoidal F] (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F X) CategoryTheory.LaxMonoidal.ε) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidal.μ X (𝟙_ C)) (CategoryTheory.map F (CategoryTheory.MonoidalCategory.rightUnitor X).hom))

    right unitality

    source
    @[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 : 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
    • One or more equations did not get rendered due to their size.
    Instances For
      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 : C} {Y : C} :
      ∀ (a : X ⟶ Y), (CategoryTheory.LaxMonoidalFunctor.of F).map a = CategoryTheory.Functorial.map' a
      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).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
      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.instLaxMonoidalObj {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
        • CategoryTheory.instLaxMonoidalObj F = { ε := F.ε, μ := F.μ, μ_natural_left := ⋯, μ_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯, right_unitality := ⋯ }
        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.