Documentation

Mathlib.CategoryTheory.Monoidal.CommMon_

The category of commutative monoids in a braided monoidal category. #

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

A commutative monoid object internal to a monoidal category.

  • X : C

    The underlying object in the ambient monoidal category

  • mon : MonObj self.X
  • comm : IsCommMonObj self.X
Instances For
    source
    @[deprecated CommMon (since := "2025-09-15")]
    def CommMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
    Type (max u₁ v₁)

    Alias of CommMon.

    A commutative monoid object internal to a monoidal category.

    Equations
    Instances For
      source
      def CommMon.toMon {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
      Mon C

      A commutative monoid object is a monoid object.

      Equations
      Instances For
        source
        @[simp]
        theorem CommMon.toMon_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
        A.toMon.X = A.X
        source
        @[deprecated CommMon.toMon (since := "2025-09-15")]
        def CommMon.toMon_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
        Mon C

        Alias of CommMon.toMon.

        A commutative monoid object is a monoid object.

        Equations
        Instances For
          source
          def CommMon.trivial (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
          CommMon C

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

          Equations
          Instances For
            source
            @[simp]
            theorem CommMon.trivial_mon_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
            MonObj.mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
            source
            @[simp]
            theorem CommMon.trivial_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
            (trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
            source
            @[simp]
            theorem CommMon.trivial_mon_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
            MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
            source
            instance CommMon.instInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
            Inhabited (CommMon C)
            Equations
            source
            instance CommMon.instCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
            CategoryTheory.Category.{v₁, max u₁ v₁} (CommMon C)
            Equations
            source
            @[simp]
            theorem CommMon.id_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
            (CategoryTheory.CategoryStruct.id A).hom = CategoryTheory.CategoryStruct.id A.X
            source
            @[simp]
            theorem CommMon.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {R S T : CommMon C} (f : R ⟶ S) (g : S ⟶ T) :
            (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
            source
            theorem CommMon.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommMon C} (f g : A ⟶ B) (h : f.hom = g.hom) :
            f = g
            source
            theorem CommMon.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommMon C} {f g : A ⟶ B} :
            f = g ↔ f.hom = g.hom
            source
            @[simp]
            theorem CommMon.id' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
            CategoryTheory.CategoryStruct.id A = CategoryTheory.CategoryStruct.id A.toMon
            source
            @[simp]
            theorem CommMon.comp' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A₁ A₂ A₃ : CommMon C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) :
            CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f g
            source
            def CommMon.forget₂Mon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
            CategoryTheory.Functor (CommMon C) (Mon C)

            The forgetful functor from commutative monoid objects to monoid objects.

            Equations
            Instances For
              source
              @[simp]
              theorem CommMon.forget₂Mon_obj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
              ((forget₂Mon C).obj A).X = A.X
              source
              @[deprecated CommMon.forget₂Mon (since := "2025-09-15")]
              def CommMon.forget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
              CategoryTheory.Functor (CommMon C) (Mon C)

              Alias of CommMon.forget₂Mon.

              The forgetful functor from commutative monoid objects to monoid objects.

              Equations
              Instances For
                source
                def CommMon.fullyFaithfulForget₂Mon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                (forget₂Mon C).FullyFaithful

                The forgetful functor from commutative monoid objects to monoid objects is fully faithful.

                Equations
                Instances For
                  source
                  @[deprecated CommMon.fullyFaithfulForget₂Mon (since := "2025-09-15")]
                  def CommMon.fullyFaithfulForget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                  (forget₂Mon C).FullyFaithful

                  Alias of CommMon.fullyFaithfulForget₂Mon.

                  The forgetful functor from commutative monoid objects to monoid objects is fully faithful.

                  Equations
                  Instances For
                    source
                    instance CommMon.instFullMonForget₂Mon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                    (forget₂Mon C).Full
                    source
                    instance CommMon.instFaithfulMonForget₂Mon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                    (forget₂Mon C).Faithful
                    source
                    @[simp]
                    theorem CommMon.forget₂Mon_obj_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
                    MonObj.one = MonObj.one
                    source
                    @[simp]
                    theorem CommMon.forget₂Mon_obj_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
                    MonObj.mul = MonObj.mul
                    source
                    @[simp]
                    theorem CommMon.forget₂Mon_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommMon C} (f : A ⟶ B) :
                    ((forget₂Mon C).map f).hom = f.hom
                    source
                    def CommMon.forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                    CategoryTheory.Functor (CommMon C) C

                    The forgetful functor from commutative monoid objects to the ambient category.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem CommMon.forget_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CommMon C) :
                      (forget C).obj X = X.X
                      source
                      @[simp]
                      theorem CommMon.forget_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : CommMon C} (f : X✝ ⟶ Y✝) :
                      (forget C).map f = f.hom
                      source
                      instance CommMon.instFaithfulForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                      (forget C).Faithful
                      source
                      @[simp]
                      theorem CommMon.forget₂Mon_comp_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                      (forget₂Mon C).comp (Mon.forget C) = forget C
                      source
                      instance CommMon.instIsIsoHom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon C} {f : M ⟶ N} [CategoryTheory.IsIso f] :
                      CategoryTheory.IsIso f.hom
                      source
                      def CommMon.mkIso' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} (e : M ≅ N) [MonObj M] [IsCommMonObj M] [MonObj N] [IsCommMonObj N] [IsMonHom e.hom] :
                      { X := M, mon := inst✝, comm := inst✝¹ } ≅ { X := N, mon := inst✝², comm := inst✝³ }

                      Construct an isomorphism of commutative monoid objects by giving a monoid isomorphism between the underlying objects.

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem CommMon.mkIso'_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} (e : M ≅ N) [MonObj M] [IsCommMonObj M] [MonObj N] [IsCommMonObj N] [IsMonHom e.hom] :
                        (mkIso' e).hom.hom = e.hom
                        source
                        @[simp]
                        theorem CommMon.mkIso'_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} (e : M ≅ N) [MonObj M] [IsCommMonObj M] [MonObj N] [IsCommMonObj N] [IsMonHom e.hom] :
                        (mkIso' e).inv.hom = e.inv
                        source
                        @[reducible, inline]
                        abbrev CommMon.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon C} (e : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                        M ≅ N

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

                        Equations
                        Instances For
                          source
                          @[simp]
                          theorem CommMon.mkIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon C} (e : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                          (mkIso e one_f mul_f).inv.hom = e.inv
                          source
                          @[simp]
                          theorem CommMon.mkIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon C} (e : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                          (mkIso e one_f mul_f).hom.hom = e.hom
                          source
                          instance CommMon.uniqueHomFromTrivial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
                          Unique (trivial C ⟶ A)
                          Equations
                          source
                          instance CommMon.instHasInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                          CategoryTheory.Limits.HasInitial (CommMon C)
                          source
                          instance CategoryTheory.Functor.isCommMonObj_obj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.LaxBraided] {M : C} [MonObj M] [IsCommMonObj M] :
                          IsCommMonObj (F.obj M)
                          source
                          def CategoryTheory.Functor.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] :
                          Functor (CommMon C) (CommMon D)

                          A lax braided functor takes commutative monoid objects to commutative monoid objects.

                          That is, a lax braided functor F : C ⥤ D induces a functor CommMon C ⥤ CommMon D.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.mapCommMon_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] (A : CommMon C) :
                            (F.mapCommMon.obj A).X = F.obj A.X
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.mapCommMon_obj_mon_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] (A : CommMon C) :
                            MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map MonObj.mul)
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.mapCommMon_obj_mon_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] (A : CommMon C) :
                            MonObj.one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map MonObj.one)
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.mapCommMon_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] {X✝ Y✝ : CommMon C} (f : X✝ ⟶ Y✝) :
                            (F.mapCommMon.map f).hom = F.map f.hom
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.mapCommMon_id_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                            MonObj.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) MonObj.one
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.mapCommMon_id_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                            MonObj.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj A.X A.X)) MonObj.mul
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.comp_mapCommMon_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} {G : Functor D E} [F.LaxBraided] [G.LaxBraided] (A : CommMon C) :
                            MonObj.one = CategoryStruct.comp (LaxMonoidal.ε (F.comp G)) ((F.comp G).map MonObj.one)
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.comp_mapCommMon_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} {G : Functor D E} [F.LaxBraided] [G.LaxBraided] (A : CommMon C) :
                            MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ (F.comp G) A.X A.X) ((F.comp G).map MonObj.mul)
                            source
                            def CategoryTheory.Functor.mapCommMonIdIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                            (Functor.id C).mapCommMon ≅ Functor.id (CommMon C)

                            The identity functor is also the identity on commutative monoid objects.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.Functor.mapCommMonIdIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : CommMon C) :
                              (mapCommMonIdIso.inv.app X).hom = CategoryStruct.id X.X
                              source
                              @[simp]
                              theorem CategoryTheory.Functor.mapCommMonIdIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : CommMon C) :
                              (mapCommMonIdIso.hom.app X).hom = CategoryStruct.id X.X
                              source
                              def CategoryTheory.Functor.mapCommMonCompIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} {G : Functor D E} [F.LaxBraided] [G.LaxBraided] :
                              (F.comp G).mapCommMon ≅ F.mapCommMon.comp G.mapCommMon

                              The composition functor is also the composition on commutative monoid objects.

                              Equations
                              Instances For
                                source
                                @[simp]
                                theorem CategoryTheory.Functor.mapCommMonCompIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} {G : Functor D E} [F.LaxBraided] [G.LaxBraided] (X : CommMon C) :
                                (mapCommMonCompIso.hom.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))
                                source
                                @[simp]
                                theorem CategoryTheory.Functor.mapCommMonCompIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} {G : Functor D E} [F.LaxBraided] [G.LaxBraided] (X : CommMon C) :
                                (mapCommMonCompIso.inv.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))
                                source
                                def CategoryTheory.Functor.mapCommMonFunctor (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] :
                                Functor (LaxBraidedFunctor C D) (Functor (CommMon C) (CommMon D))

                                mapCommMon is functorial in the lax braided functor.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Functor.mapCommMonFunctor_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : LaxBraidedFunctor C D) :
                                  (mapCommMonFunctor C D).obj F = F.mapCommMon
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Functor.mapCommMonFunctor_map_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {X✝ Y✝ : LaxBraidedFunctor C D} (α : X✝ ⟶ Y✝) (A : CommMon C) :
                                  (((mapCommMonFunctor C D).map α).app A).hom = α.hom.app A.X
                                  source
                                  instance CategoryTheory.Functor.Faithful.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.LaxBraided] [F.Faithful] :
                                  F.mapCommMon.Faithful
                                  source
                                  def CategoryTheory.Functor.mapCommMonNatTrans {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (f : F ⟶ F') [NatTrans.IsMonoidal f] :
                                  F.mapCommMon ⟶ F'.mapCommMon

                                  Natural transformations between functors lift to monoid objects.

                                  Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Functor.mapCommMonNatTrans_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (f : F ⟶ F') [NatTrans.IsMonoidal f] (X : CommMon C) :
                                    ((mapCommMonNatTrans f).app X).hom = f.app X.X
                                    source
                                    def CategoryTheory.Functor.mapCommMonNatIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] :
                                    F.mapCommMon ≅ F'.mapCommMon

                                    Natural isomorphisms between functors lift to monoid objects.

                                    Equations
                                    Instances For
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Functor.mapCommMonNatIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] (X : CommMon C) :
                                      ((mapCommMonNatIso e).hom.app X).hom = e.hom.app X.X
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Functor.mapCommMonNatIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] (X : CommMon C) :
                                      ((mapCommMonNatIso e).inv.app X).hom = e.inv.app X.X
                                      source
                                      instance CategoryTheory.Functor.Full.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] [F.Full] [F.Faithful] :
                                      F.mapCommMon.Full
                                      source
                                      def CategoryTheory.Functor.FullyFaithful.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] (hF : F.FullyFaithful) :
                                      F.mapCommMon.FullyFaithful

                                      If F : C ⥤ D is a fully faithful monoidal functor, then Grp(F) : Grp C ⥤ Grp D is fully faithful too.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        @[simp]
                                        theorem CategoryTheory.Functor.FullyFaithful.mapCommMon_preimage_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] (hF : F.FullyFaithful) {X✝ Y✝ : CommMon C} (f : F.mapCommMon.obj X✝ ⟶ F.mapCommMon.obj Y✝) :
                                        (hF.mapCommMon.preimage f).hom = hF.preimage f.hom
                                        source
                                        def CategoryTheory.Adjunction.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.LaxBraided] [a.IsMonoidal] :
                                        F.mapCommMon ⊣ G.mapCommMon

                                        An adjunction of braided functors lifts to an adjunction of their lifts to commutative monoid objects.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Adjunction.mapCommMon_unit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.LaxBraided] [a.IsMonoidal] :
                                          a.mapCommMon.unit = CategoryStruct.comp Functor.mapCommMonIdIso.inv (CategoryStruct.comp (Functor.mapCommMonNatTrans a.unit) Functor.mapCommMonCompIso.hom)
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Adjunction.mapCommMon_counit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.LaxBraided] [a.IsMonoidal] :
                                          a.mapCommMon.counit = CategoryStruct.comp Functor.mapCommMonCompIso.inv (CategoryStruct.comp (Functor.mapCommMonNatTrans a.counit) Functor.mapCommMonIdIso.hom)
                                          source
                                          def CategoryTheory.Equivalence.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :
                                          CommMon C ≌ CommMon D

                                          An equivalence of categories lifts to an equivalence of their commutative monoid objects.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            @[simp]
                                            theorem CategoryTheory.Equivalence.mapCommMon_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :
                                            e.mapCommMon.inverse = e.inverse.mapCommMon
                                            source
                                            @[simp]
                                            theorem CategoryTheory.Equivalence.mapCommMon_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :
                                            e.mapCommMon.unitIso = Functor.mapCommMonIdIso.symm ≪≫ Functor.mapCommMonNatIso e.unitIso ≪≫ Functor.mapCommMonCompIso
                                            source
                                            @[simp]
                                            theorem CategoryTheory.Equivalence.mapCommMon_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :
                                            e.mapCommMon.counitIso = Functor.mapCommMonCompIso.symm ≪≫ Functor.mapCommMonNatIso e.counitIso ≪≫ Functor.mapCommMonIdIso
                                            source
                                            @[simp]
                                            theorem CategoryTheory.Equivalence.mapCommMon_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :
                                            e.mapCommMon.functor = e.functor.mapCommMon
                                            source
                                            def CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                            CategoryTheory.Functor (CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C) (CommMon C)

                                            Implementation of CommMon.equivLaxBraidedFunctorPUnit.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              source
                                              @[simp]
                                              theorem CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C} (α : X✝ ⟶ Y✝) :
                                              (laxBraidedToCommMon C).map α = ((CategoryTheory.Functor.mapCommMonFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C).map α).app (trivial (CategoryTheory.Discrete PUnit.{u + 1}))
                                              source
                                              @[simp]
                                              theorem CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (F : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C) :
                                              (laxBraidedToCommMon C).obj F = F.mapCommMon.obj (trivial (CategoryTheory.Discrete PUnit.{u + 1}))
                                              source
                                              def CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
                                              CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u + 1}) C

                                              Implementation of CommMon.equivLaxBraidedFunctorPUnit.

                                              Equations
                                              Instances For
                                                source
                                                @[simp]
                                                theorem CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) (x✝ : CategoryTheory.Discrete PUnit.{u + 1}) :
                                                (commMonToLaxBraidedObj A).obj x✝ = A.X
                                                source
                                                @[simp]
                                                theorem CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) {X✝ Y✝ : CategoryTheory.Discrete PUnit.{u + 1}} (x✝ : X✝ ⟶ Y✝) :
                                                (commMonToLaxBraidedObj A).map x✝ = CategoryTheory.CategoryStruct.id A.X
                                                source
                                                instance CommMon.EquivLaxBraidedFunctorPUnit.instLaxMonoidalDiscretePUnitCommMonToLaxBraidedObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
                                                (commMonToLaxBraidedObj A).LaxMonoidal
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                source
                                                @[simp]
                                                theorem CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
                                                CategoryTheory.Functor.LaxMonoidal.ε (commMonToLaxBraidedObj A) = MonObj.one
                                                source
                                                @[simp]
                                                theorem CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) (X Y : CategoryTheory.Discrete PUnit.{u_1 + 1}) :
                                                CategoryTheory.Functor.LaxMonoidal.μ (commMonToLaxBraidedObj A) X Y = MonObj.mul
                                                source
                                                instance CommMon.EquivLaxBraidedFunctorPUnit.instLaxBraidedDiscretePUnitCommMonToLaxBraidedObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
                                                (commMonToLaxBraidedObj A).LaxBraided
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                source
                                                def CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                                CategoryTheory.Functor (CommMon C) (CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C)

                                                Implementation of CommMon.equivLaxBraidedFunctorPUnit.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  @[simp]
                                                  theorem CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
                                                  (commMonToLaxBraided C).obj A = CategoryTheory.LaxBraidedFunctor.of (commMonToLaxBraidedObj A)
                                                  source
                                                  @[simp]
                                                  theorem CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : CommMon C} (f : X✝ ⟶ Y✝) (x✝ : CategoryTheory.Discrete PUnit.{u + 1}) :
                                                  ((commMonToLaxBraided C).map f).hom.app x✝ = f.hom
                                                  source
                                                  def CommMon.EquivLaxBraidedFunctorPUnit.unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                                  CategoryTheory.Functor.id (CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C) ≅ (laxBraidedToCommMon C).comp (commMonToLaxBraided C)

                                                  Implementation of CommMon.equivLaxBraidedFunctorPUnit.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    source
                                                    @[simp]
                                                    theorem CommMon.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C) (X✝ : CategoryTheory.Discrete PUnit.{u + 1}) :
                                                    ((unitIso C).hom.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
                                                    source
                                                    @[simp]
                                                    theorem CommMon.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C) (X✝ : CategoryTheory.Discrete PUnit.{u + 1}) :
                                                    ((unitIso C).inv.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{u + 1})))
                                                    source
                                                    @[simp]
                                                    theorem CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
                                                    MonObj.one = CategoryTheory.CategoryStruct.comp MonObj.one (CategoryTheory.CategoryStruct.id A.X)
                                                    source
                                                    @[simp]
                                                    theorem CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon C) :
                                                    MonObj.mul = CategoryTheory.CategoryStruct.comp MonObj.mul (CategoryTheory.CategoryStruct.id A.X)
                                                    source
                                                    def CommMon.EquivLaxBraidedFunctorPUnit.counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                                    (commMonToLaxBraided C).comp (laxBraidedToCommMon C) ≅ CategoryTheory.Functor.id (CommMon C)

                                                    Implementation of CommMon.equivLaxBraidedFunctorPUnit.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      source
                                                      @[simp]
                                                      theorem CommMon.EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CommMon C) :
                                                      ((counitIso C).hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
                                                      source
                                                      @[simp]
                                                      theorem CommMon.EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CommMon C) :
                                                      ((counitIso C).inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
                                                      source
                                                      def CommMon.equivLaxBraidedFunctorPUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                                      CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C ≌ CommMon C

                                                      Commutative monoid objects in C are "just" braided lax monoidal functors from the trivial braided monoidal category to C.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        source
                                                        @[simp]
                                                        theorem CommMon.equivLaxBraidedFunctorPUnit_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                                        equivLaxBraidedFunctorPUnit.counitIso = EquivLaxBraidedFunctorPUnit.counitIso C
                                                        source
                                                        @[simp]
                                                        theorem CommMon.equivLaxBraidedFunctorPUnit_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                                        equivLaxBraidedFunctorPUnit.inverse = EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C
                                                        source
                                                        @[simp]
                                                        theorem CommMon.equivLaxBraidedFunctorPUnit_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                                        equivLaxBraidedFunctorPUnit.functor = EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C
                                                        source
                                                        @[simp]
                                                        theorem CommMon.equivLaxBraidedFunctorPUnit_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                                        equivLaxBraidedFunctorPUnit.unitIso = EquivLaxBraidedFunctorPUnit.unitIso C