Documentation

Mathlib.CategoryTheory.Monoidal.CommMon_

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

source
structure CategoryTheory.CommMon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [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 CategoryTheory.CommMon (since := "2025-09-15")]
    def CategoryTheory.CommMon_ (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
    Type (max u₁ v₁)

    Alias of CategoryTheory.CommMon.

    A commutative monoid object internal to a monoidal category.

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

      A commutative monoid object is a monoid object.

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

        Alias of CategoryTheory.CommMon.toMon.

        A commutative monoid object is a monoid object.

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

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

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

            The forgetful functor from commutative monoid objects to monoid objects.

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

              Alias of CategoryTheory.CommMon.forget₂Mon.

              The forgetful functor from commutative monoid objects to monoid objects.

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

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

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

                  Alias of CategoryTheory.CommMon.fullyFaithfulForget₂Mon.

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

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

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

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.CommMon.forget_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : CommMon C) :
                      (forget C).obj X = X.X
                      source
                      @[simp]
                      theorem CategoryTheory.CommMon.forget_map (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : CommMon C} (f : X✝ ⟶ Y✝) :
                      (forget C).map f = f.hom
                      source
                      instance CategoryTheory.CommMon.instFaithfulForget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                      (forget C).Faithful
                      source
                      @[simp]
                      theorem CategoryTheory.CommMon.forget₂Mon_comp_forget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                      (forget₂Mon C).comp (Mon.forget C) = forget C
                      source
                      instance CategoryTheory.CommMon.instIsIsoHom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : CommMon C} {f : M ⟶ N} [IsIso f] :
                      IsIso f.hom
                      source
                      def CategoryTheory.CommMon.mkIso' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [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 CategoryTheory.CommMon.mkIso'_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [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 CategoryTheory.CommMon.mkIso'_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [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 CategoryTheory.CommMon.mkIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : CommMon C} (e : M.X ≅ N.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (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 CategoryTheory.CommMon.mkIso_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : CommMon C} (e : M.X ≅ N.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                          (mkIso e one_f mul_f).hom.hom = e.hom
                          source
                          @[simp]
                          theorem CategoryTheory.CommMon.mkIso_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : CommMon C} (e : M.X ≅ N.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                          (mkIso e one_f mul_f).inv.hom = e.inv
                          source
                          instance CategoryTheory.CommMon.uniqueHomFromTrivial {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                          Unique (trivial C ⟶ A)
                          Equations
                          source
                          instance CategoryTheory.CommMon.instHasInitial {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                          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_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_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_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_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
                              • One or more equations did not get rendered due to their size.
                              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 CommMonCat(F) : CommMonCat C ⥤ CommMonCat 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_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
                                          @[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
                                          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_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_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
                                            @[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_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
                                            def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                            Functor (LaxBraidedFunctor (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 CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (F : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C) :
                                              (laxBraidedToCommMon C).obj F = F.mapCommMon.obj (trivial (Discrete PUnit.{u + 1}))
                                              source
                                              @[simp]
                                              theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_map (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C} (α : X✝ ⟶ Y✝) :
                                              (laxBraidedToCommMon C).map α = ((Functor.mapCommMonFunctor (Discrete PUnit.{u + 1}) C).map α).app (trivial (Discrete PUnit.{u + 1}))
                                              source
                                              def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                              Functor (Discrete PUnit.{u + 1}) C

                                              Implementation of CommMon.equivLaxBraidedFunctorPUnit.

                                              Equations
                                              Instances For
                                                source
                                                @[simp]
                                                theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_map {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) {X✝ Y✝ : Discrete PUnit.{u + 1}} (x✝ : X✝ ⟶ Y✝) :
                                                (commMonToLaxBraidedObj A).map x✝ = CategoryStruct.id A.X
                                                source
                                                @[simp]
                                                theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_obj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) (x✝ : Discrete PUnit.{u + 1}) :
                                                (commMonToLaxBraidedObj A).obj x✝ = A.X
                                                source
                                                instance CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.instLaxMonoidalDiscretePUnitCommMonToLaxBraidedObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                                (commMonToLaxBraidedObj A).LaxMonoidal
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                source
                                                @[simp]
                                                theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                                Functor.LaxMonoidal.ε (commMonToLaxBraidedObj A) = MonObj.one
                                                source
                                                @[simp]
                                                theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) (X Y : Discrete PUnit.{u_1 + 1}) :
                                                Functor.LaxMonoidal.μ (commMonToLaxBraidedObj A) X Y = MonObj.mul
                                                source
                                                instance CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.instLaxBraidedDiscretePUnitCommMonToLaxBraidedObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                                (commMonToLaxBraidedObj A).LaxBraided
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                source
                                                def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                Functor (CommMon C) (LaxBraidedFunctor (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 CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : CommMon C} (f : X✝ ⟶ Y✝) (x✝ : Discrete PUnit.{u + 1}) :
                                                  ((commMonToLaxBraided C).map f).hom.app x✝ = f.hom
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                                  (commMonToLaxBraided C).obj A = LaxBraidedFunctor.of (commMonToLaxBraidedObj A)
                                                  source
                                                  def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                  Functor.id (LaxBraidedFunctor (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 CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C) (X✝ : Discrete PUnit.{u + 1}) :
                                                    ((unitIso C).inv.app X).hom.app X✝ = CategoryStruct.id (X.obj (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{u + 1})))
                                                    source
                                                    @[simp]
                                                    theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C) (X✝ : Discrete PUnit.{u + 1}) :
                                                    ((unitIso C).hom.app X).hom.app X✝ = CategoryStruct.id (X.obj X✝)
                                                    source
                                                    @[simp]
                                                    theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_one (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                                    MonObj.one = CategoryStruct.comp MonObj.one (CategoryStruct.id A.X)
                                                    source
                                                    @[simp]
                                                    theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_mul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                                    MonObj.mul = CategoryStruct.comp MonObj.mul (CategoryStruct.id A.X)
                                                    source
                                                    def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                    (commMonToLaxBraided C).comp (laxBraidedToCommMon C) ≅ 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 CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : CommMon C) :
                                                      ((counitIso C).inv.app X).hom = CategoryStruct.id X.X
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : CommMon C) :
                                                      ((counitIso C).hom.app X).hom = CategoryStruct.id X.X
                                                      source
                                                      def CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                      LaxBraidedFunctor (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 CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                        equivLaxBraidedFunctorPUnit.unitIso = EquivLaxBraidedFunctorPUnit.unitIso C
                                                        source
                                                        @[simp]
                                                        theorem CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                        equivLaxBraidedFunctorPUnit.functor = EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C
                                                        source
                                                        @[simp]
                                                        theorem CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                        equivLaxBraidedFunctorPUnit.inverse = EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C
                                                        source
                                                        @[simp]
                                                        theorem CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                        equivLaxBraidedFunctorPUnit.counitIso = EquivLaxBraidedFunctorPUnit.counitIso C