Documentation

Mathlib.CategoryTheory.Monoidal.Functor

(Lax) monoidal functors #

A lax monoidal functor F between monoidal categories C and D is a functor between the underlying categories equipped with morphisms

A monoidal functor is a lax monoidal functor for which ε and μ are isomorphisms.

We show that the composition of (lax) monoidal functors gives a (lax) monoidal functor.

See also CategoryTheory.Monoidal.Functorial for a typeclass decorating an object-level function with the additional data of a monoidal functor. This is useful when stating that a pre-existing functor is monoidal.

See CategoryTheory.Monoidal.NaturalTransformation for monoidal natural transformations.

We show in CategoryTheory.Monoidal.Mon_ that lax monoidal functors take monoid objects to monoid objects.

Future work #

References #

See .

A lax monoidal functor is a functor F : C ⥤ D between monoidal categories, equipped with morphisms ε : 𝟙 _D ⟶ F.obj (𝟙_ C) and μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y), satisfying the appropriate coherences.

Instances For
    @[simp]
    theorem CategoryTheory.LaxMonoidalFunctor.ofTensorHom_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 : CategoryTheory.Functor C D) (ε : 𝟙_ D F.obj (𝟙_ C)) (μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)) (μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X Y) (g : X' Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (μ Y Y') = CategoryTheory.CategoryStruct.comp (μ X X') (F.map (CategoryTheory.MonoidalCategory.tensorHom f g))) _auto✝) (associativity : autoParam (∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (CategoryTheory.CategoryStruct.id (F.obj Z))) (CategoryTheory.CategoryStruct.comp (μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.obj X)) (μ Y Z)) (μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))) _auto✝) (left_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ε (CategoryTheory.CategoryStruct.id (F.obj X))) (CategoryTheory.CategoryStruct.comp (μ (𝟙_ C) X) (F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))) _auto✝) (right_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.obj X)) ε) (CategoryTheory.CategoryStruct.comp (μ X (𝟙_ C)) (F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))) _auto✝) :
    ∀ {X Y : C} (a : X Y), (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality).map a = F.map a
    @[simp]
    theorem CategoryTheory.LaxMonoidalFunctor.ofTensorHom_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) (ε : 𝟙_ D F.obj (𝟙_ C)) (μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)) (μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X Y) (g : X' Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (μ Y Y') = CategoryTheory.CategoryStruct.comp (μ X X') (F.map (CategoryTheory.MonoidalCategory.tensorHom f g))) _auto✝) (associativity : autoParam (∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (CategoryTheory.CategoryStruct.id (F.obj Z))) (CategoryTheory.CategoryStruct.comp (μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.obj X)) (μ Y Z)) (μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))) _auto✝) (left_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ε (CategoryTheory.CategoryStruct.id (F.obj X))) (CategoryTheory.CategoryStruct.comp (μ (𝟙_ C) X) (F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))) _auto✝) (right_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.obj X)) ε) (CategoryTheory.CategoryStruct.comp (μ X (𝟙_ C)) (F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))) _auto✝) (X : C) (Y : C) :
    (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality) X Y = μ X Y
    @[simp]
    theorem CategoryTheory.LaxMonoidalFunctor.ofTensorHom_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 : CategoryTheory.Functor C D) (ε : 𝟙_ D F.obj (𝟙_ C)) (μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)) (μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X Y) (g : X' Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (μ Y Y') = CategoryTheory.CategoryStruct.comp (μ X X') (F.map (CategoryTheory.MonoidalCategory.tensorHom f g))) _auto✝) (associativity : autoParam (∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (CategoryTheory.CategoryStruct.id (F.obj Z))) (CategoryTheory.CategoryStruct.comp (μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.obj X)) (μ Y Z)) (μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))) _auto✝) (left_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ε (CategoryTheory.CategoryStruct.id (F.obj X))) (CategoryTheory.CategoryStruct.comp (μ (𝟙_ C) X) (F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))) _auto✝) (right_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.obj X)) ε) (CategoryTheory.CategoryStruct.comp (μ X (𝟙_ C)) (F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))) _auto✝) :
    ∀ (a : C), (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality).obj a = F.obj a
    @[simp]
    theorem CategoryTheory.LaxMonoidalFunctor.ofTensorHom_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) (ε : 𝟙_ D F.obj (𝟙_ C)) (μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)) (μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X Y) (g : X' Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (μ Y Y') = CategoryTheory.CategoryStruct.comp (μ X X') (F.map (CategoryTheory.MonoidalCategory.tensorHom f g))) _auto✝) (associativity : autoParam (∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (CategoryTheory.CategoryStruct.id (F.obj Z))) (CategoryTheory.CategoryStruct.comp (μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.obj X)) (μ Y Z)) (μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))) _auto✝) (left_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ε (CategoryTheory.CategoryStruct.id (F.obj X))) (CategoryTheory.CategoryStruct.comp (μ (𝟙_ C) X) (F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))) _auto✝) (right_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.obj X)) ε) (CategoryTheory.CategoryStruct.comp (μ X (𝟙_ C)) (F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))) _auto✝) :
    (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality) = ε
    def CategoryTheory.LaxMonoidalFunctor.ofTensorHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) (ε : 𝟙_ D F.obj (𝟙_ C)) (μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)) (μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X Y) (g : X' Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (μ Y Y') = CategoryTheory.CategoryStruct.comp (μ X X') (F.map (CategoryTheory.MonoidalCategory.tensorHom f g))) _auto✝) (associativity : autoParam (∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (μ X Y) (CategoryTheory.CategoryStruct.id (F.obj Z))) (CategoryTheory.CategoryStruct.comp (μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.obj X)) (μ Y Z)) (μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))) _auto✝) (left_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ε (CategoryTheory.CategoryStruct.id (F.obj X))) (CategoryTheory.CategoryStruct.comp (μ (𝟙_ C) X) (F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))) _auto✝) (right_unitality : autoParam (∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (F.obj X)) ε) (CategoryTheory.CategoryStruct.comp (μ X (𝟙_ C)) (F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))) _auto✝) :

    A constructor for lax monoidal functors whose axioms are described by tensorHom instead of whiskerLeft and whiskerRight.

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

      A monoidal functor is a lax monoidal functor for which the tensorator and unitor as isomorphisms.

      See .

      Instances For

        The unit morphism of a (strong) monoidal functor as an isomorphism.

        Equations
        Instances For

          The tensorator of a (strong) monoidal functor as an isomorphism.

          Equations
          Instances For

            The identity lax monoidal functor.

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

              The tensorator as a natural isomorphism.

              Equations
              Instances For

                Monoidal functors commute with left tensoring up to isomorphism

                Equations
                Instances For

                  Monoidal functors commute with right tensoring up to isomorphism

                  Equations
                  Instances For

                    The identity monoidal functor.

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

                      The composition of two lax monoidal functors is again lax monoidal.

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

                        The composition of two lax monoidal functors is again lax monoidal.

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

                          The diagonal functor as a monoidal functor.

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

                            The cartesian product of two lax monoidal functors starting from the same monoidal category C is lax monoidal.

                            Equations
                            Instances For

                              The composition of two monoidal functors is again monoidal.

                              Equations
                              • F ⊗⋙ G = let __src := F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor; { toLaxMonoidalFunctor := __src, ε_isIso := , μ_isIso := }
                              Instances For

                                The composition of two monoidal functors is again monoidal.

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

                                  The cartesian product of two monoidal functors is monoidal.

                                  Equations
                                  • F.prod G = let __src := F.prod G.toLaxMonoidalFunctor; { toLaxMonoidalFunctor := __src, ε_isIso := , μ_isIso := }
                                  Instances For

                                    If we have a right adjoint functor G to a monoidal functor F, then G has a lax monoidal structure as well.

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

                                      If a monoidal functor F is an equivalence of categories then its inverse is also monoidal.

                                      Equations
                                      Instances For