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

Similarly, we define the typeclass F.OplaxMonoidal. For these oplax monoidal functors, we have similar data η and δ, but with morphisms in the opposite direction.

A monoidal functor (F.Monoidal) is defined here as the combination of F.LaxMonoidal and F.OplaxMonoidal, with the additional conditions that ε/η and μ/δ are inverse isomorphisms.

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

See Mathlib.CategoryTheory.Monoidal.NaturalTransformation for monoidal natural transformations.

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

References #

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

A functor F : C ⥤ D between monoidal categories is lax monoidal if it is 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
    def CategoryTheory.Functor.LaxMonoidal.ofTensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (ε' : 𝟙_ D F.obj (𝟙_ C)) (μ' : (X Y : C) → MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) F.obj (MonoidalCategoryStruct.tensorObj X Y)) (μ'_natural : ∀ {X Y X' Y' : C} (f : X Y) (g : X' Y'), CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μ' Y Y') = CategoryStruct.comp (μ' X X') (F.map (MonoidalCategoryStruct.tensorHom f g)) := by aesop_cat) (associativity' : ∀ (X Y Z : C), CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (μ' X Y) (CategoryStruct.id (F.obj Z))) (CategoryStruct.comp (μ' (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) (μ' Y Z)) (μ' X (MonoidalCategoryStruct.tensorObj Y Z))) := by aesop_cat) (left_unitality' : ∀ (X : C), (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε' (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ' (𝟙_ C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom)) := by aesop_cat) (right_unitality' : ∀ (X : C), (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε') (CategoryStruct.comp (μ' X (𝟙_ C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom)) := by aesop_cat) :

    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
      theorem CategoryTheory.Functor.LaxMonoidal.ofTensorHom_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (ε' : 𝟙_ D F.obj (𝟙_ C)) (μ' : (X Y : C) → MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) F.obj (MonoidalCategoryStruct.tensorObj X Y)) (μ'_natural : ∀ {X Y X' Y' : C} (f : X Y) (g : X' Y'), CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μ' Y Y') = CategoryStruct.comp (μ' X X') (F.map (MonoidalCategoryStruct.tensorHom f g)) := by aesop_cat) (associativity' : ∀ (X Y Z : C), CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (μ' X Y) (CategoryStruct.id (F.obj Z))) (CategoryStruct.comp (μ' (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) (μ' Y Z)) (μ' X (MonoidalCategoryStruct.tensorObj Y Z))) := by aesop_cat) (left_unitality' : ∀ (X : C), (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε' (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ' (𝟙_ C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom)) := by aesop_cat) (right_unitality' : ∀ (X : C), (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε') (CategoryStruct.comp (μ' X (𝟙_ C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom)) := by aesop_cat) :
      ε F = ε'
      theorem CategoryTheory.Functor.LaxMonoidal.ofTensorHom_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} (ε' : 𝟙_ D F.obj (𝟙_ C)) (μ' : (X Y : C) → MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) F.obj (MonoidalCategoryStruct.tensorObj X Y)) (μ'_natural : ∀ {X Y X' Y' : C} (f : X Y) (g : X' Y'), CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μ' Y Y') = CategoryStruct.comp (μ' X X') (F.map (MonoidalCategoryStruct.tensorHom f g)) := by aesop_cat) (associativity' : ∀ (X Y Z : C), CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (μ' X Y) (CategoryStruct.id (F.obj Z))) (CategoryStruct.comp (μ' (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) (μ' Y Z)) (μ' X (MonoidalCategoryStruct.tensorObj Y Z))) := by aesop_cat) (left_unitality' : ∀ (X : C), (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε' (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ' (𝟙_ C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom)) := by aesop_cat) (right_unitality' : ∀ (X : C), (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε') (CategoryStruct.comp (μ' X (𝟙_ C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom)) := by aesop_cat) :
      μ F = μ'
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem CategoryTheory.Functor.LaxMonoidal.comp_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.LaxMonoidal] [G.LaxMonoidal] (X Y : C) :
      μ (F.comp G) X Y = CategoryStruct.comp (μ G (F.obj X) (F.obj Y)) (G.map (μ F X Y))

      A functor F : C ⥤ D between monoidal categories is oplax monoidal if it is 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
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem CategoryTheory.Functor.OplaxMonoidal.comp_δ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : C) :
        δ (F.comp G) X Y = CategoryStruct.comp (G.map (δ F X Y)) (δ G (F.obj X) (F.obj Y))

        A functor between monoidal categories is monoidal if it is lax and oplax monoidals, and both data give inverse isomorphisms.

        Instances
          @[simp]
          theorem CategoryTheory.Functor.Monoidal.ε_η_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} {F : Functor C D} [self : F.Monoidal] {Z : D} (h : 𝟙_ D Z) :
          @[simp]
          theorem CategoryTheory.Functor.Monoidal.μ_δ_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} {F : Functor C D} [self : F.Monoidal] (X Y : C) {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) Z) :
          @[simp]
          theorem CategoryTheory.Functor.Monoidal.η_ε_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} {F : Functor C D} [self : F.Monoidal] {Z : D} (h : F.obj (𝟙_ C) Z) :
          @[simp]
          theorem CategoryTheory.Functor.Monoidal.δ_μ_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory D} {F : Functor C D} [self : F.Monoidal] (X Y : C) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj X Y) Z) :

          The isomorphism 𝟙_ D ≅ F.obj (𝟙_ C) when F is a monoidal functor.

          Equations
          Instances For

            The isomorphism F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y) when F is a monoidal functor.

            Equations
            Instances For

              Monoidal functors commute with left tensoring up to isomorphism

              Equations
              Instances For

                Structure which is a helper in order to show that a functor is monoidal. It consists of isomorphisms εIso and μIso such that the morphisms .hom induced by these isomorphisms satisfy the axioms of lax monoidal functors.

                Instances For

                  The lax monoidal functor structure induced by a Functor.CoreMonoidal structure.

                  Equations
                  • h.toLaxMonoidal = { ε' := h.εIso.hom, μ' := fun (X Y : C) => (h.μIso X Y).hom, μ'_natural_left := , μ'_natural_right := , associativity' := , left_unitality' := , right_unitality' := }
                  Instances For

                    The oplax monoidal functor structure induced by a Functor.CoreMonoidal structure.

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

                      The monoidal functor structure induced by a Functor.CoreMonoidal structure.

                      Equations
                      Instances For

                        The Functor.CoreMonoidal structure given by a lax monoidal functor such that ε and μ are isomorphisms.

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

                          The Functor.CoreMonoidal structure given by an oplax monoidal functor such that η and δ are isomorphisms.

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

                            The Functor.Monoidal structure given by a lax monoidal functor such that ε and μ are isomorphisms.

                            Equations
                            Instances For

                              The Functor.Monoidal structure given by an oplax monoidal functor such that η and δ are isomorphisms.

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

                                The functor C ⥤ D × E obtained from two lax monoidal functors is lax monoidal.

                                Equations

                                The functor C ⥤ D × E obtained from two oplax monoidal functors is oplax monoidal.

                                Equations
                                @[simp]
                                @[simp]

                                The functor C ⥤ D × E obtained from two monoidal functors is monoidal.

                                Equations

                                The right adjoint of an oplax monoidal functor is lax monoidal.

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

                                  When adj : F ⊣ G is an adjunction, with F oplax monoidal and G monoidal, this typeclass expresses compatibilities between the adjunction and the (op)lax monoidal structures.

                                  Instances
                                    instance CategoryTheory.Adjunction.isMonoidal_comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D C} (adj : F G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] {F' : Functor D E} {G' : Functor E D} (adj' : F' G') [F'.OplaxMonoidal] [G'.LaxMonoidal] [adj'.IsMonoidal] :
                                    (adj.comp adj').IsMonoidal

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

                                    Equations
                                    Instances For
                                      @[reducible, inline]

                                      An equivalence of categories involving monoidal functors is monoidal if the underlying adjunction satisfies certain compatibilities with respect to the monoidal functor data.

                                      Equations
                                      Instances For

                                        The obvious auto-equivalence of a monoidal category is monoidal.

                                        The inverse of a monoidal category equivalence is also a monoidal category equivalence.

                                        The composition of two monoidal category equivalences is monoidal.

                                        structure CategoryTheory.LaxMonoidalFunctor (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] extends CategoryTheory.Functor C D :
                                        Type (max (max (max u₁ u₂) v₁) v₂)

                                        Bundled version of lax monoidal functors. This type is equipped with a category structure in CategoryTheory.Monoidal.NaturalTransformation.

                                        Instances For

                                          Constructor for LaxMonoidalFunctor C D.

                                          Equations
                                          Instances For