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.

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

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 For
    def CategoryTheory.Functor.LaxMonoidal.ofTensorHom {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (ε' : Quiver.Hom MonoidalCategoryStruct.tensorUnit (F.obj MonoidalCategoryStruct.tensorUnit)) (μ' : (X Y : C) → Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj (MonoidalCategoryStruct.tensorObj X Y))) (μ'_natural : ∀ {X Y X' Y' : C} (f : Quiver.Hom X Y) (g : Quiver.Hom X' Y'), Eq (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), Eq (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), Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε' (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ' MonoidalCategoryStruct.tensorUnit X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom))) := by aesop_cat) (right_unitality' : ∀ (X : C), Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε') (CategoryStruct.comp (μ' X MonoidalCategoryStruct.tensorUnit) (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 C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (ε' : Quiver.Hom MonoidalCategoryStruct.tensorUnit (F.obj MonoidalCategoryStruct.tensorUnit)) (μ' : (X Y : C) → Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj (MonoidalCategoryStruct.tensorObj X Y))) (μ'_natural : ∀ {X Y X' Y' : C} (f : Quiver.Hom X Y) (g : Quiver.Hom X' Y'), Eq (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), Eq (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), Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε' (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ' MonoidalCategoryStruct.tensorUnit X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom))) := by aesop_cat) (right_unitality' : ∀ (X : C), Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε') (CategoryStruct.comp (μ' X MonoidalCategoryStruct.tensorUnit) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))) := by aesop_cat) :
      Eq (ε F) ε'
      theorem CategoryTheory.Functor.LaxMonoidal.ofTensorHom_μ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} (ε' : Quiver.Hom MonoidalCategoryStruct.tensorUnit (F.obj MonoidalCategoryStruct.tensorUnit)) (μ' : (X Y : C) → Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj (MonoidalCategoryStruct.tensorObj X Y))) (μ'_natural : ∀ {X Y X' Y' : C} (f : Quiver.Hom X Y) (g : Quiver.Hom X' Y'), Eq (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), Eq (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), Eq (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε' (CategoryStruct.id (F.obj X))) (CategoryStruct.comp (μ' MonoidalCategoryStruct.tensorUnit X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom))) := by aesop_cat) (right_unitality' : ∀ (X : C), Eq (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε') (CategoryStruct.comp (μ' X MonoidalCategoryStruct.tensorUnit) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))) := by aesop_cat) :
      Eq (μ F) μ'
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem CategoryTheory.Functor.LaxMonoidal.comp_ε {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.LaxMonoidal] [G.LaxMonoidal] :
          Eq (ε (F.comp G)) (CategoryStruct.comp (ε G) (G.map (ε F)))
          theorem CategoryTheory.Functor.LaxMonoidal.comp_μ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.LaxMonoidal] [G.LaxMonoidal] (X Y : C) :
          Eq (μ (F.comp G) X Y) (CategoryStruct.comp (μ G (F.obj X) (F.obj Y)) (G.map (μ F X Y)))
          structure CategoryTheory.Functor.OplaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) :
          Type (max u₁ v₂)

          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 For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem CategoryTheory.Functor.OplaxMonoidal.comp_δ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : C) :
                Eq (δ (F.comp G) X Y) (CategoryStruct.comp (G.map (δ F X Y)) (δ G (F.obj X) (F.obj Y)))
                structure CategoryTheory.Functor.Monoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) extends F.LaxMonoidal, F.OplaxMonoidal :
                Type (max u₁ v₂)

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

                Instances For
                  theorem CategoryTheory.Functor.Monoidal.ε_η_assoc {C : Type u₁} {inst✝ : Category C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category D} {inst✝³ : MonoidalCategory D} {F : Functor C D} [self : F.Monoidal] {Z : D} (h : Quiver.Hom MonoidalCategoryStruct.tensorUnit Z) :
                  theorem CategoryTheory.Functor.Monoidal.μ_δ_assoc {C : Type u₁} {inst✝ : Category C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category D} {inst✝³ : MonoidalCategory D} {F : Functor C D} [self : F.Monoidal] (X Y : C) {Z : D} (h : Quiver.Hom (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) Z) :
                  theorem CategoryTheory.Functor.Monoidal.η_ε_assoc {C : Type u₁} {inst✝ : Category C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category D} {inst✝³ : MonoidalCategory D} {F : Functor C D} [self : F.Monoidal] {Z : D} (h : Quiver.Hom (F.obj MonoidalCategoryStruct.tensorUnit) Z) :
                  theorem CategoryTheory.Functor.Monoidal.δ_μ_assoc {C : Type u₁} {inst✝ : Category C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category D} {inst✝³ : MonoidalCategory D} {F : Functor C D} [self : F.Monoidal] (X Y : C) {Z : D} (h : Quiver.Hom (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
                      theorem CategoryTheory.Functor.Monoidal.μIso_inv {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) :
                      Eq (μIso F X Y).inv (OplaxMonoidal.δ F X Y)
                      theorem CategoryTheory.Functor.Monoidal.μIso_hom {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) :
                      Eq (μIso F X Y).hom (LaxMonoidal.μ F X Y)
                      theorem CategoryTheory.Functor.Monoidal.map_μ_δ {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {C' : Type u₁'} [Category C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') (X Y : C) :
                      theorem CategoryTheory.Functor.Monoidal.map_μ_δ_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {C' : Type u₁'} [Category C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') (X Y : C) {Z : C'} (h : Quiver.Hom (G.obj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))) Z) :
                      theorem CategoryTheory.Functor.Monoidal.map_δ_μ_assoc {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {C' : Type u₁'} [Category C'] (F : Functor C D) [F.Monoidal] (G : Functor D C') (X Y : C) {Z : C'} (h : Quiver.Hom (G.obj (F.obj (MonoidalCategoryStruct.tensorObj X Y))) Z) :

                      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
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def CategoryTheory.Functor.Monoidal.instComp {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.Monoidal] [G.Monoidal] :
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                structure CategoryTheory.Functor.CoreMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) :
                                Type (max u₁ v₂)

                                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
                                  • Eq 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
                                        noncomputable def CategoryTheory.Functor.CoreMonoidal.ofLaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] [IsIso (LaxMonoidal.ε F)] [∀ (X Y : C), IsIso (LaxMonoidal.μ F X Y)] :

                                        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
                                            noncomputable def CategoryTheory.Functor.Monoidal.ofLaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] [IsIso (LaxMonoidal.ε F)] [∀ (X Y : C), IsIso (LaxMonoidal.μ F X Y)] :

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

                                            Equations
                                            Instances For
                                              noncomputable def CategoryTheory.Functor.Monoidal.ofOplaxMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] [IsIso (OplaxMonoidal.η F)] [∀ (X Y : C), IsIso (OplaxMonoidal.δ F X Y)] :

                                              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.
                                                Instances For
                                                  theorem CategoryTheory.Functor.prod_ε_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] :
                                                  theorem CategoryTheory.Functor.prod_ε_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] :
                                                  theorem CategoryTheory.Functor.prod_μ_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] (X Y : Prod C E) :
                                                  theorem CategoryTheory.Functor.prod_μ_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.LaxMonoidal] [G.LaxMonoidal] (X Y : Prod C E) :
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    theorem CategoryTheory.Functor.prod_δ_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : Prod C E) :
                                                    theorem CategoryTheory.Functor.prod_δ_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : Prod C E) :
                                                    def CategoryTheory.Functor.instMonoidalProdProd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {C' : Type u₁'} [Category C'] (F : Functor C D) (G : Functor E C') [MonoidalCategory C'] [F.Monoidal] [G.Monoidal] :
                                                    Equations
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

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

                                                        Equations
                                                        Instances For
                                                          theorem CategoryTheory.Functor.prod'_μ_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.LaxMonoidal] [G.LaxMonoidal] (X Y : C) :
                                                          theorem CategoryTheory.Functor.prod'_μ_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.LaxMonoidal] [G.LaxMonoidal] (X Y : C) :

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

                                                          Equations
                                                          Instances For
                                                            theorem CategoryTheory.Functor.prod'_δ_fst {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : C) :
                                                            theorem CategoryTheory.Functor.prod'_δ_snd {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.OplaxMonoidal] [G.OplaxMonoidal] (X Y : C) :
                                                            theorem CategoryTheory.Functor.prod_comp_fst {C : Type u_1} {D : Type u_2} [Category C] [Category D] {X Y Z : Prod C D} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) :
                                                            theorem CategoryTheory.Functor.prod_comp_fst_assoc {C : Type u_1} {D : Type u_2} [Category C] [Category D] {X Y Z : Prod C D} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) {Z✝ : C} (h : Quiver.Hom Z.fst Z✝) :
                                                            theorem CategoryTheory.Functor.prod_comp_snd {C : Type u_1} {D : Type u_2} [Category C] [Category D] {X Y Z : Prod C D} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) :
                                                            theorem CategoryTheory.Functor.prod_comp_snd_assoc {C : Type u_1} {D : Type u_2} [Category C] [Category D] {X Y Z : Prod C D} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) {Z✝ : D} (h : Quiver.Hom Z.snd Z✝) :
                                                            def CategoryTheory.Functor.Monoidal.prod' {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] (F : Functor C D) (G : Functor C E) [F.Monoidal] [G.Monoidal] :

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

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

                                                              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
                                                                structure CategoryTheory.Adjunction.IsMonoidal {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] [G.LaxMonoidal] :

                                                                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 For
                                                                  theorem CategoryTheory.Adjunction.isMonoidal_comp {C : Type u₁} [Category C] [MonoidalCategory C] {D : Type u₂} [Category D] [MonoidalCategory D] {E : Type u₃} [Category E] [MonoidalCategory E] {F : Functor C D} {G : Functor D C} (adj : Adjunction F G) [F.OplaxMonoidal] [G.LaxMonoidal] [adj.IsMonoidal] {F' : Functor D E} {G' : Functor E D} (adj' : Adjunction 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 C] [MonoidalCategory C] (D : Type u₂) [Category 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