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.

References #

See https://stacks.math.columbia.edu/tag/0FFL.

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_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✝) (X : C) (Y : C) :
    (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality) X Y = μ X Y
    @[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✝) :
    (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 oplax monoidal functor is a functor F : C ⥤ D between monoidal categories, equipped with morphisms η : F.obj (𝟙_ C) ⟶ 𝟙 _D and δ X Y : F.obj (X ⊗ Y) ⟶ F.obj X ⊗ F.obj Y, satisfying the appropriate coherences.

      Instances For

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

        See https://stacks.math.columbia.edu/tag/0FFL.

        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 underlying oplax monoidal functor of a (strong) monoidal functor.

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

                Construct a (strong) monoidal functor out of an oplax monoidal functor whose tensorators and unitors are isomorphisms

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

                  The identity lax monoidal functor.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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 composition of two oplax monoidal functors is again oplax monoidal.

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

                                    The composition of two oplax monoidal functors is again oplax 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 = { toLaxMonoidalFunctor := F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor, ε_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 = { toLaxMonoidalFunctor := F.prod G.toLaxMonoidalFunctor, ε_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