Documentation

Mathlib.CategoryTheory.Monoidal.Mon_

The category of monoids in a monoidal category. #

We define monoids in a monoidal category C and show that the category of monoids is equivalent to the category of lax monoidal functors from the unit monoidal category to C. We also show that if C is braided, then the category of monoids is naturally monoidal.

source
structure Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
Type (max u₁ v₁)

A monoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called an "algebra object".

Instances For
    source
    theorem Mon_.mul_one_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : Mon_ C) {Z : C} (h : self.X ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id self.X) self.one) (CategoryTheory.CategoryStruct.comp self.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor self.X).hom h
    source
    theorem Mon_.one_mul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : Mon_ C) {Z : C} (h : self.X ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom self.one (CategoryTheory.CategoryStruct.id self.X)) (CategoryTheory.CategoryStruct.comp self.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor self.X).hom h
    source
    @[simp]
    theorem Mon_.mul_assoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (self : Mon_ C) {Z : C} (h : self.X ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom self.mul (CategoryTheory.CategoryStruct.id self.X)) (CategoryTheory.CategoryStruct.comp self.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator self.X self.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id self.X) self.mul) (CategoryTheory.CategoryStruct.comp self.mul h))
    source
    @[simp]
    theorem Mon_.trivial_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
    (Mon_.trivial C).X = CategoryTheory.MonoidalCategory.tensorUnit C
    source
    @[simp]
    theorem Mon_.trivial_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
    (Mon_.trivial C).one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)
    source
    @[simp]
    theorem Mon_.trivial_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
    (Mon_.trivial C).mul = (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).hom
    source
    def Mon_.trivial (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
    Mon_ C

    The trivial monoid object. We later show this is initial in Mon_ C.

    Instances For
      source
      instance Mon_.instInhabitedMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
      Inhabited (Mon_ C)
      source
      @[simp]
      theorem Mon_.one_mul_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} {Z : C} (f : Z ⟶ M.X) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom M.one f) M.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor Z).hom f
      source
      @[simp]
      theorem Mon_.mul_one_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} {Z : C} (f : Z ⟶ M.X) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f M.one) M.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor Z).hom f
      source
      theorem Mon_.assoc_flip {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id M.X) M.mul) M.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M.X M.X M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom M.mul (CategoryTheory.CategoryStruct.id M.X)) M.mul)
      source
      theorem Mon_.Hom.ext_iff {C : Type u₁} :
      ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M N : Mon_ C} (x y : Mon_.Hom M N), x = y ↔ x.hom = y.hom
      source
      theorem Mon_.Hom.ext {C : Type u₁} :
      ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M N : Mon_ C} (x y : Mon_.Hom M N), x.hom = y.hom → x = y
      source
      structure Mon_.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ C) (N : Mon_ C) :
      Type v₁

      A morphism of monoid objects.

      Instances For
        source
        @[simp]
        theorem Mon_.Hom.mul_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} {N : Mon_ C} (self : Mon_.Hom M N) {Z : C} (h : N.X ⟶ Z) :
        CategoryTheory.CategoryStruct.comp M.mul (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom self.hom self.hom) (CategoryTheory.CategoryStruct.comp N.mul h)
        source
        @[simp]
        theorem Mon_.Hom.one_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} {N : Mon_ C} (self : Mon_.Hom M N) {Z : C} (h : N.X ⟶ Z) :
        CategoryTheory.CategoryStruct.comp M.one (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp N.one h
        source
        @[simp]
        theorem Mon_.id_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ C) :
        (Mon_.id M).hom = CategoryTheory.CategoryStruct.id M.X
        source
        def Mon_.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ C) :
        Mon_.Hom M M

        The identity morphism on a monoid object.

        Instances For
          source
          instance Mon_.homInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ C) :
          Inhabited (Mon_.Hom M M)
          source
          @[simp]
          theorem Mon_.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} {N : Mon_ C} {O : Mon_ C} (f : Mon_.Hom M N) (g : Mon_.Hom N O) :
          (Mon_.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
          source
          def Mon_.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} {N : Mon_ C} {O : Mon_ C} (f : Mon_.Hom M N) (g : Mon_.Hom N O) :
          Mon_.Hom M O

          Composition of morphisms of monoid objects.

          Instances For
            source
            instance Mon_.instCategoryMon_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
            CategoryTheory.Category.{v₁, max u₁ v₁} (Mon_ C)
            source
            theorem Mon_.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : Mon_ C} {Y : Mon_ C} {f : X ⟶ Y} {g : X ⟶ Y} (w : f.hom = g.hom) :
            f = g
            source
            @[simp]
            theorem Mon_.id_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : Mon_ C) :
            (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X
            source
            @[simp]
            theorem Mon_.comp_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} {N : Mon_ C} {K : Mon_ C} (f : M ⟶ N) (g : N ⟶ K) :
            (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
            source
            @[simp]
            theorem Mon_.forget_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) :
            (Mon_.forget C).obj A = A.X
            source
            @[simp]
            theorem Mon_.forget_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
            ∀ {X Y : Mon_ C} (f : X ⟶ Y), (Mon_.forget C).map f = f.hom
            source
            def Mon_.forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
            CategoryTheory.Functor (Mon_ C) C

            The forgetful functor from monoid objects to the ambient category.

            Instances For
              source
              instance Mon_.forget_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
              CategoryTheory.Faithful (Mon_.forget C)
              source
              instance Mon_.instIsIsoXHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (f : A ⟶ B) [e : CategoryTheory.IsIso ((Mon_.forget C).map f)] :
              CategoryTheory.IsIso f.hom
              source
              instance Mon_.instReflectsIsomorphismsMon_InstCategoryMon_Forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
              CategoryTheory.ReflectsIsomorphisms (Mon_.forget C)

              The forgetful functor from monoid objects to the ambient category reflects isomorphisms.

              source
              def Mon_.isoOfIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} {N : Mon_ C} (f : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one) (mul_f : CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.hom f.hom) N.mul) :
              M ≅ N

              Construct an isomorphism of monoids by giving an isomorphism between the underlying objects and checking compatibility with unit and multiplication only in the forward direction.

              Instances For
                source
                instance Mon_.uniqueHomFromTrivial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) :
                Unique (Mon_.trivial C ⟶ A)
                source
                instance Mon_.instHasInitialMon_InstCategoryMon_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                CategoryTheory.Limits.HasInitial (Mon_ C)
                source
                @[simp]
                theorem CategoryTheory.LaxMonoidalFunctor.mapMon_obj_X {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) (A : Mon_ C) :
                ((CategoryTheory.LaxMonoidalFunctor.mapMon F).obj A).X = F.obj A.X
                source
                @[simp]
                theorem CategoryTheory.LaxMonoidalFunctor.mapMon_obj_mul {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) (A : Mon_ C) :
                ((CategoryTheory.LaxMonoidalFunctor.mapMon F).obj A).mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ F A.X A.X) (F.map A.mul)
                source
                @[simp]
                theorem CategoryTheory.LaxMonoidalFunctor.mapMon_map_hom {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) :
                ∀ {X Y : Mon_ C} (f : X ⟶ Y), ((CategoryTheory.LaxMonoidalFunctor.mapMon F).map f).hom = F.map f.hom
                source
                @[simp]
                theorem CategoryTheory.LaxMonoidalFunctor.mapMon_obj_one {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) (A : Mon_ C) :
                ((CategoryTheory.LaxMonoidalFunctor.mapMon F).obj A).one = CategoryTheory.CategoryStruct.comp F.ε (F.map A.one)
                source
                def CategoryTheory.LaxMonoidalFunctor.mapMon {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.Functor (Mon_ C) (Mon_ D)

                A lax monoidal functor takes monoid objects to monoid objects.

                That is, a lax monoidal functor F : C ⥤ D induces a functor Mon_ C ⥤ Mon_ D.

                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.LaxMonoidalFunctor.mapMonFunctor_map_app_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                  ∀ {X Y : CategoryTheory.LaxMonoidalFunctor C D} (α : X ⟶ Y) (A : Mon_ C), (((CategoryTheory.LaxMonoidalFunctor.mapMonFunctor C D).map α).app A).hom = α.app A.X
                  source
                  @[simp]
                  theorem CategoryTheory.LaxMonoidalFunctor.mapMonFunctor_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.LaxMonoidalFunctor C D) :
                  (CategoryTheory.LaxMonoidalFunctor.mapMonFunctor C D).obj F = CategoryTheory.LaxMonoidalFunctor.mapMon F
                  source
                  def CategoryTheory.LaxMonoidalFunctor.mapMonFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                  CategoryTheory.Functor (CategoryTheory.LaxMonoidalFunctor C D) (CategoryTheory.Functor (Mon_ C) (Mon_ D))

                  mapMon is functorial in the lax monoidal functor.

                  Instances For
                    source
                    @[simp]
                    theorem Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) :
                    (Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).obj F = (CategoryTheory.LaxMonoidalFunctor.mapMon F).obj (Mon_.trivial (CategoryTheory.Discrete PUnit.{u + 1} ))
                    source
                    @[simp]
                    theorem Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                    ∀ {X Y : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C} (α : X ⟶ Y), (Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).map α = ((CategoryTheory.LaxMonoidalFunctor.mapMonFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C).map α).app (Mon_.trivial (CategoryTheory.Discrete PUnit.{u + 1} ))
                    source
                    def Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                    CategoryTheory.Functor (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) (Mon_ C)

                    Implementation of Mon_.equivLaxMonoidalFunctorPUnit.

                    Instances For
                      source
                      @[simp]
                      theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj_toFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) :
                      ∀ (x : CategoryTheory.Discrete PUnit.{u + 1} ), ((Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).obj A).obj x = A.X
                      source
                      @[simp]
                      theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) :
                      ∀ (x x_1 : CategoryTheory.Discrete PUnit.{u + 1} ), CategoryTheory.LaxMonoidalFunctor.μ ((Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).obj A) x x_1 = A.mul
                      source
                      @[simp]
                      theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) :
                      ((Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).obj A).ε = A.one
                      source
                      @[simp]
                      theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj_toFunctor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) :
                      ∀ {X Y : CategoryTheory.Discrete PUnit.{u + 1} } (x : X ⟶ Y), ((Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).obj A).map x = CategoryTheory.CategoryStruct.id ((fun x => A.X) X)
                      source
                      @[simp]
                      theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_toNatTrans_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                      ∀ {X Y : Mon_ C} (f : X ⟶ Y) (x : CategoryTheory.Discrete PUnit.{u + 1} ), ((Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).map f).app x = f.hom
                      source
                      def Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                      CategoryTheory.Functor (Mon_ C) (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C)

                      Implementation of Mon_.equivLaxMonoidalFunctorPUnit.

                      Instances For
                        source
                        @[simp]
                        theorem Mon_.EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_toNatTrans_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) (X : CategoryTheory.Discrete PUnit.{u + 1} ) :
                        ((Mon_.EquivLaxMonoidalFunctorPUnit.unitIso C).hom.app X).app X = CategoryTheory.CategoryStruct.id (X.obj X)
                        source
                        @[simp]
                        theorem Mon_.EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_toNatTrans_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) (X : CategoryTheory.Discrete PUnit.{u + 1} ) :
                        ((Mon_.EquivLaxMonoidalFunctorPUnit.unitIso C).inv.app X).app X = CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete PUnit.{u + 1} )))
                        source
                        def Mon_.EquivLaxMonoidalFunctorPUnit.unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                        CategoryTheory.Functor.id (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C) ≅ CategoryTheory.Functor.comp (Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C) (Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C)

                        Implementation of Mon_.equivLaxMonoidalFunctorPUnit.

                        Instances For
                          source
                          @[simp]
                          theorem Mon_.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Mon_ C) :
                          ((Mon_.EquivLaxMonoidalFunctorPUnit.counitIso C).inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
                          source
                          @[simp]
                          theorem Mon_.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : Mon_ C) :
                          ((Mon_.EquivLaxMonoidalFunctorPUnit.counitIso C).hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
                          source
                          def Mon_.EquivLaxMonoidalFunctorPUnit.counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                          CategoryTheory.Functor.comp (Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C) (Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C) ≅ CategoryTheory.Functor.id (Mon_ C)

                          Implementation of Mon_.equivLaxMonoidalFunctorPUnit.

                          Instances For
                            source
                            @[simp]
                            theorem Mon_.equivLaxMonoidalFunctorPUnit_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                            (Mon_.equivLaxMonoidalFunctorPUnit C).unitIso = Mon_.EquivLaxMonoidalFunctorPUnit.unitIso C
                            source
                            @[simp]
                            theorem Mon_.equivLaxMonoidalFunctorPUnit_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                            (Mon_.equivLaxMonoidalFunctorPUnit C).functor = Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C
                            source
                            @[simp]
                            theorem Mon_.equivLaxMonoidalFunctorPUnit_inverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                            (Mon_.equivLaxMonoidalFunctorPUnit C).inverse = Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C
                            source
                            @[simp]
                            theorem Mon_.equivLaxMonoidalFunctorPUnit_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                            (Mon_.equivLaxMonoidalFunctorPUnit C).counitIso = Mon_.EquivLaxMonoidalFunctorPUnit.counitIso C
                            source
                            def Mon_.equivLaxMonoidalFunctorPUnit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                            CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1} ) C ≌ Mon_ C

                            Monoid objects in C are "just" lax monoidal functors from the trivial monoidal category to C.

                            Instances For

                              In this section, we prove that the category of monoids in a braided monoidal category is monoidal.

                              Given two monoids M and N in a braided monoidal category C, the multiplication on the tensor product M.X ⊗ N.X is defined in the obvious way: it is the tensor product of the multiplications on M and N, except that the tensor factors in the source come in the wrong order, which we fix by pre-composing with a permutation isomorphism constructed from the braiding.

                              (There is a subtlety here: in fact there are two ways to do these, using either the positive or negative crossing.)

                              A more conceptual way of understanding this definition is the following: The braiding on C gives rise to a monoidal structure on the tensor product functor from C × C to C. A pair of monoids in C gives rise to a monoid in C × C, which the tensor product functor by being monoidal takes to a monoid in C. The permutation isomorphism appearing in the definition of the multiplication on the tensor product of two monoids is an instance of a more general family of isomorphisms which together form a strength that equips the tensor product functor with a monoidal structure, and the monoid axioms for the tensor product follow from the monoid axioms for the tensor factors plus the properties of the strength (i.e., monoidal functor axioms). The strength tensor_μ of the tensor product functor has been defined in Mathlib.CategoryTheory.Monoidal.Braided. Its properties, stated as independent lemmas in that module, are used extensively in the proofs below. Notice that we could have followed the above plan not only conceptually but also as a possible implementation and could have constructed the tensor product of monoids via mapMon, but we chose to give a more explicit definition directly in terms of tensor_μ.

                              To complete the definition of the monoidal category structure on the category of monoids, we need to provide definitions of associator and unitors. The obvious candidates are the associator and unitors from C, but we need to prove that they are monoid morphisms, i.e., compatible with unit and multiplication. These properties translate to the monoidality of the associator and unitors (with respect to the monoidal structures on the functors they relate), which have also been proved in Mathlib.CategoryTheory.Monoidal.Braided.

                              source
                              theorem Mon_.one_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} {N : Mon_ C} {P : Mon_ C} :
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).inv (CategoryTheory.MonoidalCategory.tensorHom M.one N.one)) P.one)) (CategoryTheory.MonoidalCategory.associator M.X N.X P.X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).inv (CategoryTheory.MonoidalCategory.tensorHom M.one (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).inv (CategoryTheory.MonoidalCategory.tensorHom N.one P.one)))
                              source
                              theorem Mon_.one_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} :
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)) M.one)) (CategoryTheory.MonoidalCategory.leftUnitor M.X).hom = M.one
                              source
                              theorem Mon_.one_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Mon_ C} :
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).inv (CategoryTheory.MonoidalCategory.tensorHom M.one (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)))) (CategoryTheory.MonoidalCategory.rightUnitor M.X).hom = M.one
                              source
                              theorem Mon_.Mon_tensor_one_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ C) (N : Mon_ C) :
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).inv (CategoryTheory.MonoidalCategory.tensorHom M.one N.one)) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj M.X N.X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X)) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)) = (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj M.X N.X)).hom
                              source
                              theorem Mon_.Mon_tensor_mul_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ C) (N : Mon_ C) :
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj M.X N.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).inv (CategoryTheory.MonoidalCategory.tensorHom M.one N.one))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X)) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)) = (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj M.X N.X)).hom
                              source
                              theorem Mon_.Mon_tensor_mul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ C) (N : Mon_ C) :
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X)) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj M.X N.X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X)) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj M.X N.X) (CategoryTheory.MonoidalCategory.tensorObj M.X N.X) (CategoryTheory.MonoidalCategory.tensorObj M.X N.X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj M.X N.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X)) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X)) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)))
                              source
                              theorem Mon_.mul_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : Mon_ C} {N : Mon_ C} {P : Mon_ C} :
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (CategoryTheory.MonoidalCategory.tensorObj M.X N.X, P.X) (CategoryTheory.MonoidalCategory.tensorObj M.X N.X, P.X)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X)) (CategoryTheory.MonoidalCategory.tensorHom M.mul N.mul)) P.mul)) (CategoryTheory.MonoidalCategory.associator M.X N.X P.X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator M.X N.X P.X).hom (CategoryTheory.MonoidalCategory.associator M.X N.X P.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (M.X, CategoryTheory.MonoidalCategory.tensorObj N.X P.X) (M.X, CategoryTheory.MonoidalCategory.tensorObj N.X P.X)) (CategoryTheory.MonoidalCategory.tensorHom M.mul (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (N.X, P.X) (N.X, P.X)) (CategoryTheory.MonoidalCategory.tensorHom N.mul P.mul))))
                              source
                              theorem Mon_.mul_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : Mon_ C} :
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (CategoryTheory.MonoidalCategory.tensorUnit C, M.X) (CategoryTheory.MonoidalCategory.tensorUnit C, M.X)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).hom M.mul)) (CategoryTheory.MonoidalCategory.leftUnitor M.X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor M.X).hom (CategoryTheory.MonoidalCategory.leftUnitor M.X).hom) M.mul
                              source
                              theorem Mon_.mul_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : Mon_ C} :
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (M.X, CategoryTheory.MonoidalCategory.tensorUnit C) (M.X, CategoryTheory.MonoidalCategory.tensorUnit C)) (CategoryTheory.MonoidalCategory.tensorHom M.mul (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).hom)) (CategoryTheory.MonoidalCategory.rightUnitor M.X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor M.X).hom (CategoryTheory.MonoidalCategory.rightUnitor M.X).hom) M.mul
                              source
                              instance Mon_.monMonoidal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                              CategoryTheory.MonoidalCategory (Mon_ C)

                              Projects: